This fixes issue #734, and partially addresses #930.
The basic issue with 734 was that the solver was chosing
spurious counterexamples for the exponent function; in particular,
models where the output was not at least 1. The fairly restricted
axiom we add here just says that the exponent function is at least
as large as its base for positive inputs.
This allows us to express enumerations with exclusive upper bounds.
In contrast with the `Literal` constraint, `LiteralLessThan n a`
express that `a` contains all the literals strictly less than `n`,
and explicitly allows `n` to be `inf` for unbounded types like
`Integer` and `Rational`.
It is possible to define `Literal n a` as
`(fin n, LiteralLessThan (n+1) a)` instead of leaving it primitve.
However, this makes infered types and error messages worse, IMO.
As it stands, the typechecker has no real knowledge of the connection
between `Literal` and `LiteralLessThan`.
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.
Previously we were computing incorrect answers for `ec_twin_mult j S k T`
in the following 4 special cases: `S == 0`, `T == 0`, `S+T == 0` and
`S-T == 0`. In these cases, we must be more careful about performing
normalization in the twin multiply procedure.
a new `Cryptol::Reference` module. Change the evaluator API slightly
so that primitives can be bound to expressions, in addition to values.
We can use this to inject the reference implementations of the above
operations into the symbolic evaluators.
Because of the exact way evaluation environments are piped around,
the bound expression will be evaluated in the environment that
the primitive symbol is declared. So, we can't just reference
the name of the reference implementation when we inject it.
Instead, we abuse the `EWhere` construct to add local definitions
corresponding to the entire module. This works, but is a bit
unsatisfying, as any top-level CAFs will not be shared across
different invocations. This doesn't matter for these
functions, but might for e.g, AES.
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.
These are useful for switching between rationals and floats.
This also cleans up the implementation a bit, removing some duplicated
code.
NOTE: I am not sure if the translation from `float` to `rational`
is quite right in the what-4 backend, but I can't think of a better
way to do it at the moment.
This is semantically the same as `map` on finite sequences,
but forks a separate Haskell thread for each element of the sequence.
When the GHC runtime is instructed to use multiple OS threads,
data-parallel exeuction can be achieved.
* Add docstrings for all prelude functions and fix minor style issues.
Fixes#771
* Update `CryptolPrims` documentation
* Minor updates to the prelude
* Update CHANGES
* Updates to the cryptol book and CryptolPrims
* Fix several additional docstrings
* Specify and document properties of signed bitvector division.
Fixes#677
* Fixup test
* typos and style
* Regenerate PDFs
