GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-09-11 14:06:13 +03:00
Code Issues Projects Releases Wiki Activity
3,027 Commits 68 Branches 27 Tags 82 MiB
WIP/rpc/feat/newtype
Commit Graph

3027 Commits

This Branch
This Branch
All Branches
Author SHA1 Message Date
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
Rob Dockins
a2aa432420 Continue consolidating WordValue code into the related module 2021-04-13 10:27:17 -07:00
Rob Dockins
6bf4d2e44e Remove uses of panic in SeqMap 2021-04-13 10:27:17 -07:00
Rob Dockins
69a589d151 Update the reference interpreter 2021-04-13 10:27:17 -07:00
Rob Dockins
50117717a5 Tweak split, join, reverse and transpose. 
Make sure they are sufficently lazy in their arguments.
Join is still to eager in some cases, but that will require
a larger refactoring.
 2021-04-13 10:27:17 -07:00
Rob Dockins
b5454bce29 Fix test suite 2021-04-13 10:27:17 -07:00
Rob Dockins
d3accfb042 Make take and drop primitive instead of splitAt. 
This allows us to generalize the type of `take` and simplifies
the implementations.
 2021-04-13 10:27:17 -07:00
Rob Dockins
a112ed8cf7 Update cryptol-remote-api 2021-04-13 10:27:17 -07:00
Rob Dockins
87d8912fa3 Complete the job of making SeqMap abstract. 2021-04-13 10:27:17 -07:00
Rob Dockins
3f185449ee Move WordValue into a separate module. 2021-04-13 10:27:17 -07:00
Rob Dockins
7fc748d9f9 Complete the process of making WordVal abstract. 2021-04-13 10:27:17 -07:00
Rob Dockins
b9635b26dc Relocate most of the logic that works directly on WordValue values 
into the `Value` module.  Remove most uses of the `WordValue` constructors
in other modules, but don't quite make the type abstract yet.
 2021-04-13 10:27:17 -07:00
Rob Dockins
3f710468e8 Break SeqMap out into a separate module 2021-04-13 10:27:17 -07:00
Rob Dockins
5a84ea5b58 Squash warnings 2021-04-13 10:27:17 -07:00
Rob Dockins
b24e2f5130 Remove the eta delay mechanisim from the evaluator. 
This brings the evaluator more in line with the reference semantics,
although there may still be some differences.
 2021-04-13 10:27:17 -07:00
Rob Dockins
3942a3decf Rework the # operator. 
It is now lazier in its arguments when required.
 2021-04-13 10:27:17 -07:00
Rob Dockins
d4e5fc2895 Remove obsolete functions 2021-04-13 10:27:17 -07:00
Rob Dockins
1377fc9675 Refactor the VWord constructor and WordValue type. 
Instead of every `WordValue` being wrapped in the `SEval` monad,
create a separate `ThunkWordVal` constructor that captures exactly
when lazy behavior is needed.  This simplifies several things, and
makes it more clear some places where we can actually be stricter
in the spine of word values.
 2021-04-13 10:27:17 -07:00
Andrew Kent
4ab4c687e7 feat(rpc): check, AES example/test 2021-04-08 14:56:52 -07:00
robdockins
0ea0881955
Merge pull request #1156 from GaloisInc/random-tf 
Remove our dependency on the `random` package
 2021-04-08 10:12:50 -07:00
robdockins
7dd050331a
Merge pull request #1158 from GaloisInc/issue1157 
Reset the TC solver on CTRL^C
 2021-04-08 10:11:24 -07:00
Rob Dockins
a45072dcb4 Reset the TC solver on CTRL^C. 
Generally, the CTRL^C will cause the solver to exit, so
this shuts down the current instance forces the REPL to
reopen a fresh instance the next time it is required.

Fixes #1157
 2021-04-07 17:54:09 -07:00
Rob Dockins
234437af06 Remove our dependency on the random package. 
Instead, directly use the generators defined in `tf-random`.
This changes the generation algorithm for some types, so we
need to update the tests that depend on those concrete values.

Fixes #1102
 2021-04-07 12:12:32 -07:00
robdockins
c2ef506902
Merge pull request #1139 from felixonmars/patch-2 
Allow sbv 8.13
 2021-04-06 10:15:20 -07:00
robdockins
b72f80112c
Merge pull request #1152 from GaloisInc/ref-panic 
Include REPL let bindings in the reference interpreter
 2021-04-06 10:14:58 -07:00