GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-09-11 22:17:18 +03:00
Code Issues Projects Releases Wiki Activity
3,310 Commits 68 Branches 27 Tags 82 MiB
3892615998
Commit Graph

3310 Commits

This Branch
This Branch
All Branches
Author SHA1 Message Date
Ryan Scott
3892615998 Address review comments 2022-01-25 17:03:03 -05:00
Ryan Scott
3b9eafbc91 CI: Update what4-solvers to use Z3 4.8.14 
The previous `what4-solvers` snapshot used Z3 4.8.10, which is known to cause
severe performance regressions with the `negshift` regression test. See #1107.
This updates to a more recent `what4-solvers` snapshot that uses Z3 4.8.14
instead, which is known to work more reliably with `negshift`.
 2022-01-14 14:48:11 -05:00
Ryan Scott
09aaf1d82c Make issue{066,093} resilient to different solvers' behavior 
This adopts the same approach as in commit
3ea5e9e51c:
use `:set show-examples=false` in the affected examples to avoid showing the
particular data that a solver picks for examples/counterexamples. Also avoid
printing the contents of `it` for similar reasons. I have verified that the
new output works across a wide range of Z3 versions.

Fixes #1280.
 2022-01-14 14:45:10 -05:00
Ryan Scott
3a204fc4aa Make integerRecipMod return a Maybe instead of an unboxed sum 2022-01-13 15:35:41 -05:00
Ryan Scott
cb1cf652ae Use test-lib-0.4 2022-01-13 15:12:57 -05:00
Ryan Scott
7030088e13 Ensure that there is at least one Windows build 2022-01-13 15:09:47 -05:00
Ryan Scott
2255e942f2 Avoid an -Woverlapping-patterns warning on GHC 9.0 
GHC 9.0's pattern-match coverage checker is more clever and flags this guard as
redundant:

```
[ 48 of 111] Compiling Cryptol.TypeCheck.SimpleSolver ( src/Cryptol/TypeCheck/SimpleSolver.hs, /tmp/ghc54946_0/ghc_169.o )

src/Cryptol/TypeCheck/SimpleSolver.hs:37:7: warning: [-Woverlapping-patterns]
    Pattern match is redundant
    In an equation for ‘dbg’: dbg msg x | False = ...
   |
37 |     | False     = ppTrace msg x
   |       ^^^^^
```

While true, we want to keep this code in to keep in from bitrotting. I have
tweaked the code slightly so that it is just clever enough to defeat the
pattern-match coverage checker.
 2022-01-13 13:16:41 -05:00
Ryan Scott
c6cd69d531 Only enable UnliftedNewtypes on GHC 9.0+ 2022-01-13 12:57:23 -05:00
Ryan Scott
31ca666b3a Regenerate cabal.GHC-*.config files 2022-01-13 12:16:10 -05:00
Ryan Scott
1181076f1f Factor out compatibility shims into GHC.Num.Compat 2022-01-13 12:13:40 -05:00
Ryan Scott
7bdb84beca CI: Drop GHC 8.6 2022-01-13 09:47:10 -05:00
Ryan Scott
38935c0c51 CI: Test GHC 9.0.2 2022-01-12 09:41:48 -05:00
Ryan Scott
2e32fcd619 Bump some upper version bounds for GHC 9.0 2022-01-12 09:40:20 -05:00
Ryan Scott
644d33bf1f Merge branch 'master' into ghc9 2022-01-12 09:33:24 -05:00
Matthew Yacavone
34404d7930
Merge pull request #1317 from GaloisInc/rpc/clean-cryptoltypes-2 
[RPC] Finish cleaning cryptoltypes.py
 2021-12-23 15:12:28 -05:00
Matthew Yacavone
6685a6bc46 bump cryptol-client version number for dev 2021-12-22 13:53:19 -08:00
Matthew Yacavone
6f049ce0c3 cryptol-client 2.12.2 release 2021-12-22 13:09:37 -08:00
Matthew Yacavone
9102e23e06 have check_type return schema if relevant, check types in test_types 2021-12-22 13:09:37 -08:00
Matthew Yacavone
82d03c8cc6 make PropCon class, clean up CryptolTypeSchema in cryptoltypes.py 2021-12-22 13:09:36 -08:00
Matthew Yacavone
9a2773df19 make TypeOp class in cryptoltypes.py 2021-12-22 13:09:36 -08:00
Matthew Yacavone
1323366572 add args to CryptolApplication.__init__ error message 2021-12-21 16:48:22 -08:00
Matthew Yacavone
098c046a43 add case for lengthFromThenTo to to_type 2021-12-21 15:44:37 -08:00
Matthew Yacavone
aef1edd7d2 actually finish Cryptol props, add missing case to test_basics.py 2021-12-21 15:40:49 -08:00
Matthew Yacavone
fbb50dbdd5 add section headers 2021-12-21 15:03:52 -08:00
Matthew Yacavone
d726646506 add remaining props, lengthFromThenTo, unit to cryptoltypes.py 2021-12-21 14:57:48 -08:00
Iavor S. Diatchki
08cd609c4c
Merge pull request #1301 from GaloisInc/T1299 
T1299
 2021-12-20 21:56:20 +02:00
Iavor Diatchki
92e3174b2f Fix loop in TC 
The issue is that we use a think to represent dictionaries for selectors,
and we can't extract position information from the thunk, as it will
force it.  Instead, we compute the location from the source expression
instead.
 2021-12-20 20:49:02 +02:00
Iavor Diatchki
d9057100f9 Improve locations of error messages. 
Fixes #1299
 2021-12-20 10:44:33 +02:00
Iavor Diatchki
009f400a44 Use the same location for property as we do for normal declarations. 2021-12-20 10:41:29 +02:00
Matthew Yacavone
234324f381 add more docstrings to cryptoltypes, check types in CryptolApplication 2021-12-10 16:28:43 -08:00
Matthew Yacavone
16e35f689a use @dataclass, add missing __str__ methods in cryptoltypes 2021-12-10 16:02:22 -08:00
Matthew Yacavone
07c689a699
Merge pull request #1312 from GaloisInc/rpc/clean-cryptoltypes-1 
[RPC] Clean up `to_cryptol` interface in cryptoltypes.py
 2021-12-10 19:01:54 -05:00
Matthew Yacavone
6628bcd36d update CHANGELOG 2021-12-10 14:57:06 -08:00
Matthew Yacavone
554f53124d add docstring to to_cryptol, remove eval_numeric 2021-12-10 14:45:36 -08:00
Matthew Yacavone
565a48a2c7 add deprecation errors to CryptolType.from_python and .convert 2021-12-10 14:41:21 -08:00
Andrew Kent
cec87706e5
bump argo submodule (#1300) 2021-12-10 11:26:26 -08:00
Andrew Kent
c332ad987f
chore: bump cryptol client python deps (#1306) 
* chore: bump cryptol client python deps

* bump argo-client (and in turn, urllib3)

Co-authored-by: Matthew Yacavone <matthew@yacavone.net>
 2021-12-10 11:24:12 -08:00
Matthew Yacavone
780c572858 allow bytearrays in BV.from_bytes 2021-12-09 14:29:38 -08:00
Matthew Yacavone
faa4e78504 clean up interface for converting to JSON in cryptoltypes 2021-12-09 14:04:15 -08:00
Andrew Kent
490e046b07
fix what4-abc solver in python client, add more SMT tests (#1311) 
* fix what4-abc solver in python client, add more SMT tests (include more solvers)
 2021-12-09 11:17:19 -08:00
robdockins
435bb81e52
Merge pull request #1303 from GaloisInc/primitive-scanl 
Primitive scanl
 2021-12-07 15:00:24 -08:00
Rob Dockins
7b3121f0b6 Make sure to memoize the sequence map inside the scanl primitive. 
This speeds up concrete computation and preserves sharing for
symbolic computation.
 2021-12-07 13:46:43 -08:00
Rob Dockins
928cc98768 Add a test comparing the reference implemntations of foldl, 
`scanl` and `iterate` to their primitive implementations.
 2021-12-07 11:56:46 -08:00
Rob Dockins
22af290eae Update test output 2021-12-07 11:56:46 -08:00
Rob Dockins
41613ade02 Tweak the type signature for scanl and scanr. 
It is convenient for Coq extraction for the constant 1 factor
to be on the left of the addition symbol.
 2021-12-07 11:56:46 -08:00
Rob Dockins
253a7f26ab Add reference implementations for foldl and scanl and iterate 2021-12-07 11:56:34 -08:00
Rob Dockins
849a79c9bc Reimplement the updates, updatesEnd and iterate functions 
in the prelude to use `foldr` or `scanl`.

This leaves `sortBy` as the only remaining operation in the Cryptol
prelude defined directly by recursion.
 2021-12-06 14:33:18 -08:00
Rob Dockins
750ce5f00a Make scanl into a primitive. This puts it on similar footing as foldl. 2021-12-06 14:33:18 -08:00
Ryan Scott
ebb1dd152f
cryptol-remote-api: Allow building with aeson-2.0.* (#1308) 
This introduces some CPP, unfortunately, but this probably necessary to
continue allowing `cryptol-remote-api` to be buildable with old versions of
`aeson` until the ecosystem catches up with `aeson-2.0.*`.
 2021-11-30 09:05:30 -05:00
Matthew Yacavone
abb41f5b4e
Merge pull request #1307 from GaloisInc/rpc/quoted-cryptol 
[RPC] f-string-like Cryptol quasiquotation
 2021-11-29 17:07:30 -05:00