GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-12-29 10:53:31 +03:00
Code Issues Projects Releases Wiki Activity
3,001 Commits 67 Branches 28 Tags 96 MiB
2c00714a2b
Commit Graph

3001 Commits

This Branch
This Branch
All Branches
Author SHA1 Message Date
Ryan Scott
2c00714a2b Use correct link for GitHub Actions README badge 2021-04-22 16:39:37 -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
Iavor Diatchki
a25fde4473 Correct how to specify constraint 2021-04-22 10:40:33 -07: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
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
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
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
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
Rob Dockins
69ad34b231 Add test case for issue640 
I think we've finally cracked the nut on this strictness bug.
Fixes #640
 2021-04-13 10:27:17 -07:00
Rob Dockins
31ab387c19 Update the test for issue 211 to restore the old test behavior. 
Also, test for looping computations in addition to `error` computations.
This doesn't let us cheat by eta-expanding the error, as we were
doing before.
 2021-04-13 10:27:17 -07:00
Rob Dockins
838a252770 Make the "large bit size" a bit more reasonable. 2021-04-13 10:27:17 -07:00
Rob Dockins
d4c3402496 Make joinWords lazier in its arguments 2021-04-13 10:27:17 -07:00
Rob Dockins
5d96829dcd Increase the strictness in the SuiteB SHA padding function. 
With the lazier join operator, this squashes a space leak in examples that
do a lot of hashing.
 2021-04-13 10:27:17 -07:00
Rob Dockins
77f6718766 Make joinWordVal lazier in its arguments. 2021-04-13 10:27:17 -07:00
Rob Dockins
f7d66df8e2 Keep a thunk for packed words alongside bitmap representations. 
This lets us share work, and lets us optimistically treat the word
as packed if we know it has already been forced.  It also lets
us delay unpacking decisions.
 2021-04-13 10:27:17 -07:00
Rob Dockins
6853ba0330 Don't reexport the SeqMap API 2021-04-13 10:27:17 -07:00
Rob Dockins
5f4b979d0b Tweak the way delayWordValue works. 
This should eliminte the possiblity of building up chains
of thunked word values.
 2021-04-13 10:27:17 -07:00
Rob Dockins
149428c0d8 Remove the splitWordVal operation. 
Replace it with `takeWordVal` and `dropWordVal` instead.
 2021-04-13 10:27:17 -07:00
Rob Dockins
cc8822f736 Update reference implementation and documentation 2021-04-13 10:27:17 -07:00
Rob Dockins
b812cd5036 Temporary fix to the test for issue211. 
We should either decide that the semantics of `#` requires it to be
strict in its arguments, or we should fix the definition.
 2021-04-13 10:27:17 -07:00
Rob Dockins
e65bf8cd0c Change largeBitsVal into bitmapWordVal. 
Update it's type to prepare for upcoming changes
 2021-04-13 10:27:17 -07:00
Rob Dockins
55a48ba34e Stop eta-expanding the error combinator. 
This breaks the test for issue211, but we were cheating
on it anyway.
 2021-04-13 10:27:17 -07:00
Rob Dockins
6d53e912e0 Fix another width accounting bug 2021-04-13 10:27:17 -07:00
Rob Dockins
62bcabac12 Fix a bug with width accounting 2021-04-13 10:27:17 -07:00
Rob Dockins
9823884083 typo 2021-04-13 10:27:17 -07:00
Rob Dockins
afd4cd6234 Try harder to see if thunks have already been forced. 2021-04-13 10:27:17 -07:00
Rob Dockins
f88b67d838 Make word updates more uniform between SBV and What4. 
Push word updating logic into the WordValue module, which
finally allows us to delete the abstraction leaking `viewWordOrBits`
family of helpers.
 2021-04-13 10:27:17 -07:00
Rob Dockins
7c3f1ac67b Implement signed right shift uniformly 2021-04-13 10:27:17 -07:00
Rob Dockins
9d4183975e Push word shifts into the Backend class and define shifts uniformly. 2021-04-13 10:27:17 -07:00
Rob Dockins
e7df405732 Fix import in cryptol-remote-api 2021-04-13 10:27:17 -07:00
Rob Dockins
07f4ba9d67 Make indexPrim lazier in its sequence argument. 2021-04-13 10:27:17 -07:00
Rob Dockins
d291318bdf Rework shifting in the concrete simulator to use the same code paths 
as the symbolic simulators.
 2021-04-13 10:27:17 -07:00
Rob Dockins
8ca536d387 Reduce the amount of sequence memoization that occurs in shifts. 
Memoization now only occurs in the barrel shifter when a symbolic
bit is encountered, instead of at every shift.
 2021-04-13 10:27:17 -07:00
Rob Dockins
ebc83275ad Consolidate some code related to indexing and shifting. 
Introduce the concept of "index segments", which allows us to
delay deciding if index values should be treated as packed
or unpacked until they are consumed in an indexing operation.
 2021-04-13 10:27:17 -07:00