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
This fixes a bug where the scoping on the command line was incorrect
for nested modules.
It also changes the semantics of `:browse` (whose implementation is now
in a separate module), to be more reasonable. See #689
* Limitations:
Does not work in combination parameterized modules, as I am
about to redo how that works.
* General refeactorings:
* Namespaces:
- We have an explicit type for namespaces, see `Cryptol.Util.Ident`
- Display environments should now be aware of the namespace of the
name being displayed.
* Renamer:
- Factor out the renamer monad and error type into separate modules
- All name resultion is done through a single function `resolveName`
- The renamer now computes the dependencies between declarations,
orders things in dependency order, and checks for bad recursion.
* Typechecker: Redo checking of declarations (both top-level and local).
Previously we used a sort of CPS to add things in scope. Now we use
a state monad and add things to the state. We assume that the renamer
has been run, which means that declarations are ordered in dependency
order, and things have unique name, so we don't need to worry about
scoping too much.
* Change specific to nested modules:
- We have a new namespace for module names
- The interface file of a module contains the interfaces for nested modules
- Most of the changes related to nested modules in the renamer are
in `ModuleSystem.NamingEnv` and `ModuleSystem.Rename`
- There is some trickiness when resolving module names when importing
submodules (seed `processOpen` and `openLoop`)
- There are some changes to the representation of modules in the typechecked
syntax, in particular:
- During type-checking we "flatten" nested module declarations into
a single big declaration. Hopefully, this means that passes after
the type checker don't need to worry about nested modules
- There is a new field containing the interfaces of the nested modules,
this is needed so that when we import the module we know we have the
nested structure
- Declarations in functor/parameterzied modules do not appear in the
flattened list of declarations. Instead thouse modules are collected
in a separate field, and the plan is that they would be used from
there when we implmenet functor instantiation.
Expose some additional primitives, such as FMA,
abs, sqrt, and more classification predicates.
Refactor the primitives table for floating-point
values into a single generic table that uses
methods from the `Backend` class.
for primitives that is evaluated to values when a primitive is looked up
at evaluation time. Currently, this does not add any additional capabilities,
but gives us the ability to modify the representation of values
without touching all the primitive definitions, and gives us a place to
hook in additional capabilies to the primitives.
As part of this refactoring, the primitives that are defined totally
generically are moved to the `Cryptol.Eval.Generic` module and
used uniformly in all the backends.
* Adds a stub executable to cabal file for checking docs
* [WIP] Adds check-exercises executable
A program that checks that the exercises in Programming Cryptol actual work when
executed against an Cryptol REPL. Instead of using \begin{Verbatim}, we use
\begin{REPL} in both the exercise and the answer, which is rendered the same but
gets checked by this program.
This is a WIP -- we still need to do a number of things, including (but not
limited to):
* Move the "REPL" macro out of CrashCourse.tex and into some including latex
file
* Change many of the "Verbatim"s into "REPL"s to test if this approach works in
general
* Several updates
* Moves REPL command definitions into main latex file
* Generalizes repl commands
* Several improvements:
* documentation of CheckExercises.hs
* factoring out addReplData, addReplin, addReplout, nextLine functions
* took the IO out of P monad (shouldn't have been there)
* worked on annotating repls for many exercises/examples in crash course
* Adds a README for check-exercises
* Uses cryptol's -e option to detect errors
* updates ProgrammingCryptol.pdf
* Fixes main function
After changing to use the -e option to detect errors, I used cabal v2-exec which
apparently does not rebuild anything, but I thought it did. This just fixes the
code so it builds again.
* Update CHANGES for 2.10
* Remove profiling flags from Cabal file
They result in `cabal check` warnings and probably don’t need to be
hard-coded.
* Remove commented-out Cryptol server references
The code no longer exists, so we’ll never uncomment these.
Equivalent functionality is now provided by `cryptol-remote-api`.
* Update references to version numbers in README. Closes#719.
that created the `Backend` module tree.
The main change here is that the `Cryptol.Eval.SBV` module was split
into two, similar to how the concrete and What4 evaluators were already
split. Various other small bits of code are rearranged to detangle
module dependencies.
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
