GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-12-24 08:24:19 +03:00
Code Issues Projects Releases Wiki Activity
1,781 Commits 67 Branches 28 Tags 96 MiB
5def499908
Commit Graph

1781 Commits

This Branch
This Branch
All Branches
Author SHA1 Message Date
Brian Huffman
5def499908 Capitalize sentences in output of :check and :exhaust. 2018-07-20 10:55:24 -07:00
Brian Huffman
409e544772 Restrict polynomial literals to bitvector types. Fixes #530. 2018-07-20 10:06:16 -07:00
Aaron Tomb
031b236e66 Update CI scripts 2018-07-20 10:05:44 -07:00
Aaron Tomb
0b46db36ce Fix capitalization of MiniLock in test 2018-07-20 10:04:11 -07:00
Brian Huffman
73a8c19b58 Update cryptol primitives appendix in the book. 2018-07-20 09:48:31 -07:00
Brian Huffman
eef8924dfe Update operator names in Cryptol book index. 2018-07-20 09:00:29 -07:00
Brian Huffman
6201415c66 Remove index entries and text about non-existent :i, :p commands. 2018-07-20 08:28:35 -07:00
Brian Huffman
dd2c4b6507 Introduce command for more uniform exercise references in the book. 2018-07-19 18:25:55 -07:00
Brian Huffman
abbce5405c Tweak fix for #494: it should never say an equation is unsolvable. 2018-07-19 18:01:12 -07:00
Brian Huffman
af6b830162 Use autoref command and lowercase section refs consistently in the book. 2018-07-19 18:00:17 -07:00
Brian Huffman
10f43b4279 Switch Cryptol book exercises to use split instead of groupBy. 2018-07-19 16:46:48 -07:00
Brian Huffman
5451683f4a Add regression test for #494. 2018-07-19 15:08:24 -07:00
Brian Huffman
b19cac5fab Add simplification rule: t1 == min (K + t1) t2 ~> t1 == t2, if K >= 1. 
Fixes #494.
 2018-07-19 15:07:21 -07:00
Brian Huffman
d58aebcee8 Fix shadowing warnings in example cryptol code. 
Shadowing a name from the Cryptol prelude produces an unpredictable
warning message with a temporary file name, which is not good for our
regression test suite.
 2018-07-19 14:48:12 -07:00
Brian Huffman
d803192b2b Add regression test that loads all modules from examples directory. 
This file should be updated every time a new module is added to
`examples`.

Fixes #529.
 2018-07-19 09:57:18 -07:00
Brian Huffman
48e0e1989b Fix examples/param_modules/Common/AES_GCM_SIV.cry. 
Some types had been renamed in a module that it imports.
 2018-07-19 09:55:18 -07:00
Brian Huffman
b812241481 Fix type error in examples/Karatsuba.cry. 
The error was caused by the recent change of the type of `demote`
when class `Literal` was introduced.
 2018-07-19 09:37:51 -07:00
Brian Huffman
ca1dd23173 Fix error in examples/AE.cry. 
The error was: "built-in type 'Integer' shadowed in type synonym"
 2018-07-19 09:31:46 -07:00
Brian Huffman
a66338293a Memoize result of binary logic operators on LargeBitsVal arguments. 
Fixes #446.

This fix is very similar to the one for #514, which added memoization
for symbolic if-then-else on sequences. This is another instance where
a SeqMap is created where each lookup triggers two further lookups,
causing exponential runtime behavior in the worst case.
 2018-07-18 23:02:27 -07:00
Brian Huffman
ec7c44d36e Fix typo in comment. 2018-07-18 22:57:12 -07:00
Brian Huffman
95cedc3135 Send symbolic typechecking goals involving != to the SMT solver. 
Fixes #528.
 2018-07-18 18:35:50 -07:00
Brian Huffman
f98903e739 Fix typo in comment. 2018-07-18 18:34:56 -07:00
Brian Huffman
f4ce1a46f0 Fix typo in comment. 2018-07-18 17:53:47 -07:00
Brian Huffman
e4f6f65502 Fix type error in examples/SHA256.cry. 
This seems to have been broken when the desugaring of [_ ..] was
changed.
 2018-07-18 17:29:13 -07:00
Brian Huffman
7259507d04 Unifier now returns a substitution even on unification failure. 
For example, when type checking `[1..10]:[6][8]`, `mgu` would be called
on [10]?a and [6][8], and `mgu` would return the substitution `?a = [8]`
and the mismatch error `10 != 6`.

Fixes #525.
 2018-07-18 14:01:30 -07:00
Brian Huffman
7a307a704d Add bounds assumptions for solver queries about type Z n. 
Fixes #526.
 2018-07-17 16:20:26 -07:00
Brian Huffman
c925a82dce Update function toExpr for new type of demote primitive. 
Also avoid using removed primitive `integer`.

Previously this caused a panic when printing counterexamples
of type Integer.
 2018-07-17 16:00:50 -07:00
Brian Huffman
751bb4e7e1 Further avoid printing constructors "Nat" and "Inf" in error messages. 2018-07-17 14:56:04 -07:00
Brian Huffman
8892759a93 More edits to Cryptol book, rewrite type synonym section. 2018-07-17 10:52:21 -07:00
Aaron Tomb
2cae92944b Update PDF of Programming in Cryptol 2018-07-16 15:02:08 -07:00
Brian Huffman
0d074ce231 Many updates to Programming Cryptol book (work in progress). 2018-07-16 09:48:39 -07:00
Brian Huffman
3ed98578de Avoid printing constructor names "Nat" and "Inf" in error messages. 2018-07-13 12:09:24 -07:00
Brian Huffman
531be1145e Merge branch 'master' of github.com:GaloisInc/cryptol 2018-07-13 11:57:37 -07:00
Iavor Diatchki
6f67924894 Add some more simplification on user defined signatures. 
This is not great, but since we do it, we should do it more consistently.
Avoids a panic in the bench mark suite (more generally, when users write
trivial things in their type signatures, eg. see `pad` in SHA512)
 2018-07-13 11:00:21 -07:00
Iavor Diatchki
021e71bd82 Add some missing cases. 2018-07-12 14:28:45 -07:00
Iavor Diatchki
6f3c855ef6 Tuples are now indexed from 0, so selector 3 is really the 4th field of a tuple 2018-07-12 14:28:35 -07:00
Iavor Diatchki
7c74ed2daf Fixes #524 2018-07-12 14:27:54 -07:00
Brian Huffman
5f795d4644 Restrict output number base to 2, 8, 10 and 16. 
The output bases now match the possible input bases for
numeric literals.

Fixes #179.
 2018-07-12 09:57:41 -07:00
Brian Huffman
a1bb918840 Command ":help :set <option-name>" prints help text for settable option. 
This mostly takes care of #154, but we still need tab-completion.
 2018-07-12 09:27:44 -07:00
Brian Huffman
844e80085d Print ambiguous command warning for :help with ambiguous command name. 
For example:

Cryptol> :help :c
:c is ambiguous, it could mean one of:
	:cd, :check

Previously we would print the help text for all matching commands,
which was a bit much.
 2018-07-12 08:07:23 -07:00
Brian Huffman
b302dc044e Make :help print documentation for other REPL commands. 
For example, `:help :sat` prints documentation for the :sat command.
 2018-07-11 17:51:37 -07:00
Iavor Diatchki
0739448933 Do and-goal splitting in more places. 
This alleviates some of the problems in #522
 2018-07-11 15:18:08 -07:00
Brian Huffman
1e5209ade5 Add regression test for #413. 2018-07-11 13:00:53 -07:00
Brian Huffman
56824291b2 Add inequality constraints to types of fromThen and fromThenTo. 
This ensures that all applications of partial type functions are
well-defined.

Fixes #416.
 2018-07-11 12:58:49 -07:00
Brian Huffman
5ba712bde3 Add concrete type-level syntax m != n for inequality constraints. 2018-07-11 12:52:32 -07:00
Brian Huffman
e6c0852339 Add implementation of Threefish tweakable block cipher. 
Threefish is used as part of the Skein hash function.
 2018-07-11 11:40:27 -07:00
Brian Huffman
b8ecb4abbe Fix typo in comment. 2018-07-11 04:52:55 -07:00
Iavor Diatchki
1666ea3bd0 Merge branch 'master' of github.com:GaloisInc/cryptol 2018-07-10 17:05:37 -07:00
Iavor Diatchki
2f00384038 Fixes #521 2018-07-10 17:05:31 -07:00
Brian Huffman
be8c334efe Reference interpreter uses base and infLength printing options. 
Fixes #412.
 2018-07-10 09:58:37 -07:00