and the What4 symbolic simulator.
We use the EGCD algorithm to compute inverses for concrete values.
For symbolic values, we posit a multiplicitive inverse via a defining
equation. To get this to work, we needed to fix a bug in the
equation definition code for What4; it was asserting definitions
with the wrong polarity for "prove" calls.
This implementation is taken fairly directly from the SBV
tutorial module. It is a Word32-oriented implementation using
TBoxes. We make the implementation avalible via Cryptol primitives
that are similar to the AESNI instructions, with primitives for
the individual rounds and some utility primitives for performing
key expansion.
block functions, ripped out of the SHA package, and expose
it via new Cryptol primitives.
Using these primitives in place of the defined reference implementations
leads to approx 100x speed-up in larger protocols that do a lot of hashing.
I don't know if this is the implementation we'll actually end up using,
but this verifies the overall idea and helps design the API.
Thunk state is now controlled using transational memory variables
instead of IORefs, and the thunk likecycle is made more explicit
in the relevant datatypes. Threads will now properly block and wait
when forcing a thunk that is already under evaluation by a different
thread. Hopefully, using optimistic concurrency (transactional memory)
will help reduce concurrency contention. The reworked lifecycle
datastructures hopefully will release closures related to evaluation
faster, which should reduce memory pressure somewhat.
Fixes#856
* Fix Dockerfile
* Include version number in CHANGES.md
* Update copyright dates
* Don't include cryptol-specs in release archives
* Remove duplicate copy of Programming Cryptol
This turned out to be relatively straightforward. Using
a simliar strategy to SBV, we simply spawn off all the solvers
in separate threads and wait using the `async` package.
Some minor fixes in `What4` allow the threads to respond properly
to being interrupted.
Some care is required to install the necessary solver options
_before_ spawning off the threads to avoid race conditions
in the configuration datastructure itself; such race conditions should
be fixed in What4 at some point.
This type stores records as a finite map from field names to
values, while also remembering the original order of the fields
from when the record was generated (usually, from the program source).
For all "semantic" purposes, the fields are treated as appearing in
a canoical order (in sorted order of the field names). However, for
user display purposes, records are presented in the order in which
the fields were originally stated.
In the course of implementing this, I discovered that we were not
previously checking for repeated fields in the parser or typechecker,
which would result in some rather strange situations and could probably
be used to break the type safety. This is now fixed and repeated fields
will result in either a parse error or a panic (for records generated
internally).
Fixes#706
into a `Generic` module. Refactor the `EvalPrims` class away,
pusing the `iteValue` operation into `BitWord` and demoting
the `evalPrim` operation into an ordinary (non-typeclass)
operation.
For the time being, there is still some information about them that
is duplicated in Cryptol.TypeCheck.TCon, but we at least the parsed syntax
does not depend on the typechecked syntax.
The latest version causes build failures. Ultimately, we should be able
to fix the code to work with newer base-compat versions on various GHC
verions, but this gets builds to work for now.
The main user visible effect of this might be that sometime things on
the Cryptol command line are instantiated in a slightly different way:
we get `inf` sometimes when we got a finite example before.
We could work around this if it is an issue, but I am not sure which
behavior is more reasonable.
Regression test check31 was failing somewhat unpredictably due to the
use of lazy I/O when loading the Z3 prelude for the type checker. Using
the `strict` package seems to fix it.
There are two major changes in this patch. The first is that sequence maps
now have special representations for point updates, of the sort produced by
the 'update' and 'updateEnd' primtives. These updates are stored in a
finite map, rather than as a functional-update thunk using lambdas; this
reduces memory usage and improves time efficecy of sequences defined by
sequences of updates.
The second change is that the caching policy for sequences is changed
to retain all previously-calculated values. This is a change from the
previous LRU policy, which retained only a small finite number of previous
values. Benchmarking showed that unbounded memoization was better for
performance in essentially all cases over both an LRU and an adaptive
caching strategy. The potential downside is that we may retain values
longer than necessary. If this becomes a problem, we may need to revisit
this decision.
This greatly increases mutator productivity, and thus provides
significant speedups on some examples. The tradeoff with
larger nurseries is the potential for long GC pause times.
This is probably acceptable tradeoff for a tool like Cryptol,
despite the potential for unresponsiveness at the REPL.
Fix some minor conflicts in the test suite.
Conflicts:
tests/issues/issue002.icry.fails
tests/issues/issue148.icry.stdout
tests/issues/issue198.icry.stdout
tests/issues/issue214.icry.stdout
tests/issues/issue290v2.icry.stdout
tests/issues/issue312.icry.fails
The major change in this patch is to add a new type of 'WordValue'
which is always used to represent finite sequences of bits. A word
value is either a packed word, or a sequence of lazy bits. The 'VSeq'
constructor, in constrast, is now never used for a finite sequence of
bits.
This avoids certain thorny problems that arise when trying to faithfully
implement the lazy semantics of Cryptol. We now do not have to commit
to a value at type '[n]' being represented as a packed word or as an
unpacked word until relatively late. This allows us to perform type-directed
eta-expansion at every recursive call before we know how words will be represented.
This patch fixes all the outstanding strictness bugs that I know of.
Unfortunately, we seem to lose some ground on performance. The new evaluator
is now about 5% slower than the old one on the AES benchmark, and quite a bit
slower on the SHA1 benchmark. Fortunately, the use if LRU caches for memoization
of sequences seems to keep heap usage to manageable levels; so programs generally
complete, even if they take a long time.
