GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-08-16 17:30:27 +03:00
Code Issues Projects Releases Wiki Activity
3,027 Commits 64 Branches 26 Tags 81 MiB
WIP/rpc/feat/newtype
Commit Graph

3027 Commits

This Branch
This Branch
All Branches
Author SHA1 Message Date
Andrew Kent
f9d9f30f59 WIP: RPC support for newtypes and other opaque types 
+ `readBack` now introduces fresh names which can be sent back to
  an RPC client when the structure of the value cannot be uniquely/
  unambiguously syntactically represented.
+ `getCryptolExpr` needs to be modified, likely to return a `Expr Name`
  instead of the current return type `Expr PName`, since the fresh
  names introduced by `readBack` cannot be represented as `PName`s.
+ saw-remote-api compatibility for changes to `getCryptolExpr` should
  be considered (i.e., it also uses that function but in a slightly
  different monad, however that monad _also_ has a ModuleEnv from
  Cryptol so it should be possible to define it in a way it works
  for both servers).
 2021-05-12 14:52:15 -07:00
brianhuffman
282613d320
Merge pull request #1170 from GaloisInc/faster-pmod 
Add a shortcut to speed up concrete evaluation of pmod.
 2021-04-28 16:31:21 -07:00
Iavor S. Diatchki
eec1fb0bfb
Merge pull request #1183 from GaloisInc/T1182 
Don't panic on ambig, so that we have a chance to report the error
 2021-04-27 18:44:26 -07:00
Matthew Yacavone
0edcbfcb4e
Merge pull request #1173 from GaloisInc/rpc/more-examples 
rpc: add more tests
 2021-04-27 18:02:22 -04:00
Iavor Diatchki
df1e574e96 Don't panic on ambig, so that we have a chance to report the error 
Fixes #1182
 2021-04-27 15:00:35 -07:00
Matthew Yacavone
fe62c14735 Merge branch 'master' into rpc/more-examples 2021-04-27 15:55:43 -04:00
Matthew Yacavone
79505847df
Merge pull request #1181 from GaloisInc/rpc/refactor-init-py 
rpc: Move contents of __init__.py to new commands.py, connection.py files
 2021-04-27 15:53:33 -04:00
Matthew Yacavone
e431ce9f14 add all submodules to __all__ 2021-04-23 18:54:22 -04:00
Matthew Yacavone
d5d0c1d2ea restore old __init__.py imports, in case anyone uses them 2021-04-23 15:44:51 -04:00
Matthew Yacavone
e4345a89c4 move contents of __init__.py to commands.py, connection.py 2021-04-23 15:29:32 -04:00
Matthew Yacavone
90baa856f2 whoops, added back result() to test-cryptol-remote-api.py 2021-04-23 14:54:36 -04:00
Matthew Yacavone
9572ddbbf4 update evaluate_expression call in test-cryptol-remote-api.py 2021-04-23 14:02:29 -04:00
Iavor S. Diatchki
74c5f4efdc
Merge pull request #1171 from GaloisInc/T1169 
T1169
 2021-04-22 21:39:11 -07:00
Iavor Diatchki
54780379cf Rename files to have correct OS extension 2021-04-22 16:39:37 -07:00
Andrew Kent
62707426be feat(rpc): safe for python api (#1168) 
* feat(rpc): safe for python api

* refactor: use enum for smt query type

* Update cryptol-remote-api/python/cryptol/__init__.py

Co-authored-by: Ryan Scott <ryan.gl.scott@gmail.com>

* Update cryptol-remote-api/python/cryptol/__init__.py

Co-authored-by: Ryan Scott <ryan.gl.scott@gmail.com>

Co-authored-by: Ryan Scott <ryan.gl.scott@gmail.com>
 2021-04-22 16:39:37 -07:00
Ryan Scott
2c00714a2b Use correct link for GitHub Actions README badge 2021-04-22 16:39:37 -07:00
Andrew Kent
9995513098
chore: ensure run_rpc_tests.sh uses up-to-date server binaries (#1174) 2021-04-22 16:16:28 -07:00
Iavor Diatchki
b2a8a23798 Remove constraints on cabal install, as we made the most progress with that... 2021-04-22 15:13:52 -07:00
Iavor Diatchki
a7daa1e9c0 Overwrite test-runner if it was already there 2021-04-22 14:18:28 -07:00
Iavor Diatchki
c16583230a Print test-runner version, and always build it. 2021-04-22 14:04:15 -07:00
Lisanna Dettwyler
ec614b26cd Fix test-lib step 2021-04-22 12:35:17 -07:00
Matthew Yacavone
8528e1dbf3 Merge branch 'master' into rpc/more-examples 2021-04-22 15:00:49 -04:00
Matthew Yacavone
bc03778420 add test_EvenMansour 2021-04-22 14:55:52 -04:00
Andrew Kent
966b3431c1
feat(rpc): safe for python api (#1168) 
* feat(rpc): safe for python api

* refactor: use enum for smt query type

* Update cryptol-remote-api/python/cryptol/__init__.py

Co-authored-by: Ryan Scott <ryan.gl.scott@gmail.com>

* Update cryptol-remote-api/python/cryptol/__init__.py

Co-authored-by: Ryan Scott <ryan.gl.scott@gmail.com>

Co-authored-by: Ryan Scott <ryan.gl.scott@gmail.com>
 2021-04-22 11:27:31 -07:00
Iavor Diatchki
a25fde4473 Correct how to specify constraint 2021-04-22 10:40:33 -07:00
Matthew Yacavone
57778d18e2 Merge branch 'master' into rpc/more-examples 2021-04-22 13:01:10 -04:00
Iavor Diatchki
b572b086b0 Require version 0.3 of test-lib 2021-04-22 09:08:19 -07:00
Iavor Diatchki
4e0da53ff3 Change freeze files to use test-lib 0.3 2021-04-21 17:20:37 -07:00
Iavor Diatchki
0c65f5e82b Change CI to use test-lib-0.3 and add a windows test for modsys/T18 2021-04-21 15:33:29 -07:00
Iavor Diatchki
aa7cce1668 Require version 0.3 of test-runner and a windows specific result for the test 2021-04-21 14:38:37 -07:00
Lisanna Dettwyler
867096c07f
Merge pull request #1172 from GaloisInc/fix-gha-readme-badge 
Use correct link for GitHub Actions README badge
 2021-04-21 12:08:28 -07:00
Ryan Scott
1681707bd0 Use correct link for GitHub Actions README badge 2021-04-21 11:57:44 -04:00
Iavor Diatchki
1c175f5c85 Fix test (accounts for chanes in the standard library) 2021-04-20 14:53:21 -07:00
Iavor Diatchki
6818969db6 Fixes #1169 2021-04-20 14:47:32 -07:00
Iavor Diatchki
3df9273041 Add a pretty printing instance for naming environments 
This is useful for debugging
 2021-04-20 14:47:32 -07:00
Brian Huffman
44ed895a4c Add a shortcut to speed up concrete evaluation of pmod. 
Used with a modulus of degree `d`, the low `d` bits of
the input can be copied directly to the output unchanged.
This lets us skip the first `d` iterations of the main loop.
 2021-04-20 13:26:10 -07:00
robdockins
cd0748cc74
Merge pull request #1161 from felixonmars/patch-2 
Allow sbv 8.14
 2021-04-20 10:22:19 -07:00
Andrew Kent
dbf9d63750
Merge pull request #1164 from GaloisInc/rpc/chore/remove-dead-code 
chore: remove dead rpc code for change directory
 2021-04-19 14:03:52 -07:00
robdockins
51e5d91bc1
Merge pull request #1165 from GaloisInc/expose-utils 
Expose `modPathSplit` and `defaultSolverConfig` for downstream use
 2021-04-19 10:11:58 -07:00
Rob Dockins
a279e78d53 Expose modPathSplit and defaultSolverConfig for downstream use. 2021-04-16 12:12:38 -07:00
Andrew Kent
47f1428279 chore: remove dead rpc code for change directory 2021-04-15 16:11:04 -07:00
Matthew Yacavone
ff26feb83c add test_DES, fix string literals in test_SHA256 2021-04-15 13:38:13 -04:00
Matthew Yacavone
1a34e05361 Merge branch 'master' into rpc/more-examples 2021-04-15 12:57:43 -04:00
Andrew Kent
34749601e6
Merge pull request #1159 from GaloisInc/rpc/feat/check 
feat(rpc): check, AES example/test
 2021-04-14 14:53:12 -07:00
Matthew Yacavone
ec2a23abf1 add SHA256 test, add from_cryptol_arg to CryptolEvalExpr 2021-04-14 17:33:06 -04:00
robdockins
76d1dc9df7
Merge pull request #1136 from GaloisInc/word-eval-refactor 
Word eval refactor
 2021-04-14 08:39:23 -07:00
Rob Dockins
3f66dbf713 Rework memoMap to squash space leaks. 
The main benefit of this reorganization is that it
notices when a memoized `SeqMap` has been forced
at all of its locations.  This allows us to
discard the underlying computation, which will
never need to be consulted again.  This, in turn,
allows the garbage collector to reclaim the associated
memory and help prevent certain classes of space leaks.
 2021-04-13 16:14:57 -07:00
Rob Dockins
29c5bc9224 Fixes that help a small amount with space leaks 2021-04-13 15:35:57 -07:00
Felix Yan
6d17c2e97b
Allow sbv 8.14 
Tested to build fine here.
 2021-04-14 03:33:21 +08:00
Rob Dockins
aac42f4991 Fix test suite 2021-04-13 10:27:17 -07:00