Commit Graph

177 Commits

Author SHA1 Message Date
Robert Dockins
e66db956a8 Add a primitive for arrayEq
Currently, this primitive (like the other Array primitives) has
no computational interpretation, and is only used for stating
specifications that are used in SAW. As such, there are no changes to
the interpreter.
2022-07-20 09:43:41 -07:00
Rob Dockins
41613ade02 Tweak the type signature for scanl and scanr.
It is convenient for Coq extraction for the constant 1 factor
to be on the left of the addition symbol.
2021-12-07 11:56:46 -08:00
Rob Dockins
253a7f26ab Add reference implementations for foldl and scanl and iterate 2021-12-07 11:56:34 -08:00
Rob Dockins
849a79c9bc Reimplement the updates, updatesEnd and iterate functions
in the prelude to use `foldr` or `scanl`.

This leaves `sortBy` as the only remaining operation in the Cryptol
prelude defined directly by recursion.
2021-12-06 14:33:18 -08:00
Rob Dockins
750ce5f00a Make scanl into a primitive. This puts it on similar footing as foldl. 2021-12-06 14:33:18 -08:00
Sean Weaver
3fabe4a21f selected the first merge option 2021-11-12 22:00:13 -05:00
Sean Weaver
c064d408dc Updating private scoping 2021-11-06 10:11:55 -04:00
Sean Weaver
2375055403 A take at updating Cryptol's sort function from insertion sort to merge sort. This implementation is much more computationally efficient. 2021-11-04 16:25:39 -04:00
Brian Huffman
d1883caa6a Add primitive toSignedInteger. 2021-09-10 17:05:22 -07:00
Andrei Stefanescu
052228e79a
Add arrayCopy, arraySet, arrayRangeEqual array primitives. (#1268)
* Add arrayCopy, arraySet, arrayRangeEqual array primitives. Add arrayRangeLookup and arrayRangeUpdate.

* Address comments.

* Address comments.

* Fix test.
2021-08-25 12:02:55 -07:00
Rob Dockins
d740442035 Update documenetation with new enumeration forms,
and update the reference semantics.
Other minor documentation fixes and updates.
2021-07-20 17:01:50 -07:00
Rob Dockins
362649bb74 Documentation tweaks and spellcheck in the prelude 2021-06-30 16:23:15 -07:00
Rob Dockins
b3c4317784 Update solver definitions related to /^ and %^. 2021-06-30 13:18:12 -07:00
Rob Dockins
94a4c77fdb Relax the finiteness restriction on the first argument of /^ and %^.
We define `inf /^ n = inf` and `inf %^ n` for finite, positive `n`.
2021-06-30 08:32:39 -07:00
Rob Dockins
6fe2970b52 Add new primtives for the explicit stride enumerations.
Hook them up through the typechecker.  However, we still
need implementations.
2021-06-29 16:23:51 -07:00
Brian Huffman
3b62788841 Add sort and sortBy functions to the Cryptol prelude. 2021-05-06 12:01:33 -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
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
8915ee3899 Teach the typechecker a bit more about exponents.
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.
2021-04-06 09:28:31 -07:00
Rob Dockins
8009e8a9c0 Implement syntax for enumerations with exclusive upper bounds.
`[ x   .. < y ]` --> ``fromToLessThan`{first=x, bound=y}``
`[ x:t .. < y ]` --> ``fromToLessThan`{first=x, bound=y, a=t}``
2021-03-02 17:18:36 -08:00
Rob Dockins
ddbb673601 Add LiteralLessThan and fromToLessThan primitives.
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`.
2021-03-02 17:18:36 -08:00
Rob Dockins
0909120a68 Convert to using the SFloat module from What4.
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.
2021-02-08 17:47:49 -08:00
Rob Dockins
aefc93b9b2 Add some special case handling for ec_twin_mult.
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.
2020-11-16 09:15:32 -08:00
Rob Dockins
5bba75fbb6 Move the Cryptol implementations of pmod, pdiv and pmult into
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.
2020-10-27 10:51:10 -07:00
Rob Dockins
44e5f45ae3 Add faster primitive implementations for pmult, pdiv, and pmod. 2020-10-27 10:51:10 -07:00
Brian Huffman
f54f2ffee4 Improve help texts for lg2 type and value operators.
This addresses part of #931.
2020-10-13 10:26:59 -07:00
Rob Dockins
2d88b7b018 Fix typos in PrimeEC.cry 2020-09-29 22:33:06 -07:00
Rob Dockins
6f54f5e1c2 Add tests that validate the NIST prime field curves and exercise some
test vectors for ECDSA public key generation and signature generation.
2020-09-29 22:00:14 -07:00
Rob Dockins
b6d5044279 Add documentation to the PrimeEC module and do some other minor cleanups. 2020-09-29 22:00:14 -07:00
Rob Dockins
dfd7020a68 Add a new built-in module for prime-field eliptic curves,
based on the arithemetic routines from:
https://github.com/GaloisInc/cryptol-specs/blob/master/Primitive/Asymmetric/Signature/ECDSA/doc/10.1.1.204.9073.pdf
2020-09-29 22:00:14 -07:00
Rob Dockins
9822d5fd9a Update documentation and reference interpreter 2020-09-29 14:55:05 -07:00
Rob Dockins
b5bdd0fa80 Add basic support for primality checking in the type system. 2020-09-29 14:55:05 -07:00
Rob Dockins
1262fcf5a1 More precicely express the constraints on AES key expansion. 2020-09-21 14:54:28 -07:00
Rob Dockins
912536662f Whitespace: untabify 2020-09-21 14:54:28 -07:00
Rob Dockins
6ab3262ec0 Add docstrings to the SuiteB module 2020-09-21 14:54:28 -07:00
Rob Dockins
ad9e479018 Cut down the AES implementation to just the primivite bits we need.
Expand the lookup tables manually and remove the basic GF(2^8)
polynomial arithmetic algorithms.

Rename the SHA primitives.
2020-09-21 14:54:28 -07:00
Rob Dockins
e8f7fa9435 Add a basic implementation of AES to the SuiteB module.
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.
2020-09-21 14:54:28 -07:00
Rob Dockins
4494c43a53 Separate the public API for SuiteB from the implementation details. 2020-09-21 14:54:28 -07:00
Rob Dockins
cc63eb568f Remove the restrictions on message length in the SuiteB::sha*
implementations.  Not sure this is actually a good idea, but
propigating the constraints around in larger algorithms is
very inconvenient.
2020-09-21 14:54:28 -07:00
Rob Dockins
65090ac81d Rearrange the new SHA primitives into a separate built-in module
named `SuiteB`, and finish packaging up the primitives.
2020-09-21 14:54:28 -07:00
Rob Dockins
44dae69012 Add a Haskell-native implementation of the SHA256 and SHA512
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.
2020-09-21 14:54:28 -07:00
Rob Dockins
e79786edb0 Remove seq and change foldl' to always perform normal-form evaluation.
The extra flexability aforded by WHNF evaluation is mostly just confusing,
I think.
2020-09-14 12:41:38 -07:00
Rob Dockins
6feeafa74f Add seq and deepseq primitives, and rewrite some prelude
functions to use stricter variants.  Add an `Eq` constraint
to `parmap` to mirror the restriction on `deepseq`.
2020-09-14 10:42:59 -07:00
Rob Dockins
2029605a3c Implement primitive foldl and foldl' operations.
Reimplement `foldr` and add `foldr'` in terms of
the left folds.
2020-09-14 10:42:59 -07:00
Rob Dockins
82187952e7 Generalize the type of generate.
This allows the indexing type to be arbitraty `Integral` types,
provided the type is large enough to index the sequence.

Fixes #848
2020-08-22 15:28:13 -07:00
Brian Huffman
b9eb076441 Add docstring for 'RoundingMode'. Fixes #836. 2020-07-28 14:58:39 -07:00
Iavor Diatchki
1c34b8eb9b Add fpToRational fpFromRational and fpIsFinite.
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.
2020-07-15 17:50:15 -07:00
Iavor Diatchki
eed0bdeafa Adjust comment to match declared type 2020-07-14 15:36:56 -07:00
Rob Dockins
7b0f69de28 Implement an experimental parmap operation.
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.
2020-07-09 10:54:03 -07:00
robdockins
87d5edab00
Documentation updates (#779)
* 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
2020-06-30 10:58:25 -07:00