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