GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-11-24 15:08:58 +03:00
Code Issues Projects Releases Wiki Activity
1,764 Commits 68 Branches 28 Tags 95 MiB
ca1dd23173
Commit Graph

1764 Commits

This Branch
This Branch
All Branches
Author SHA1 Message Date
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
Brian Huffman
186e2a0a82 Reference evaluator tracks lengths of list values. 2018-07-10 09:35:06 -07:00
Brian Huffman
ca62acc727 Remove non-primitives @@ and !! from reference evaluator prims. 2018-07-10 09:30:49 -07:00
Brian Huffman
ee2d2ec9c4 Fix typo in comment. 2018-07-10 08:47:53 -07:00
Brian Huffman
f3a9a7ceb7 Fix typo in typechecker error message. 2018-07-09 18:30:38 -07:00
Aaron Tomb
89cce64253
Merge pull request #520 from lemmarathon/feature/docker 
Add Dockerfile
 2018-07-06 09:56:04 -07:00
Aaron Tomb
8496ddfe13 Remove obsolete reference to cryptol-server 2018-07-05 10:05:27 -07:00
lemmarathon
7c282538ea Add Dockerfile. 2018-07-02 12:29:45 -04:00
Brian Huffman
fe4b2d9f70 Update tab-completion for :help to also complete type names. 2018-06-29 16:28:52 -07:00
Brian Huffman
99773d71b7 Memoize result of symbolic if-then-else on sequence types. 
It is important that we memoize `mergeSeqMap`: Because one
lookup into the merged sequence leads to two other sequence
lookups, the lack of memoization could led to exponential runtime
behavior in the worst case.

Fixes #514.
 2018-06-29 14:16:35 -07:00
Brian Huffman
debe4df76d Fix broken compilation on ghc 8.2. 2018-06-28 19:34:10 -07:00
Iavor Diatchki
4c6a69c0cf Improvements to naming of variables. 
This does a bunch of small changes, that should improve the usability
of Cryptol.  Namely:
  * When we are forced to make up a name, pick something derived from
    the source of the variable, annotated with the unique.
  * When pretty printing a schema, use "n,m,i,j,k" for numeric variables
    and "a,b,c,d,e" for value type vairable.
  * When generalizing, put numeric vairables first.
 2018-06-28 15:58:11 -07:00
Iavor Diatchki
1d5d5cdf2f Merge branch 'master' of github.com:GaloisInc/cryptol 2018-06-28 14:23:24 -07:00
Iavor Diatchki
cf6e7161f5 Bugfix: Remember the results of defaulting. 2018-06-28 14:23:13 -07:00
Brian Huffman
836771aded Tweak names and order of type variables on Cryptol prelude functions. 
Also update test output for new type variable names.

See #517.
 2018-06-28 14:14:44 -07:00
Iavor Diatchki
75b56e251e Complain when we spot invalid literals. Fixes #519 2018-06-28 14:13:07 -07:00
Iavor Diatchki
3560161490 Use the existing test for numeric predicates. Fixes #518 2018-06-28 13:56:01 -07:00
Brian Huffman
a4a3207f9f Swap type argument order for zext and sext. 
The new argument order works better for partial type application,
so e.g. zext`{32} extends its argument to 32 bits.
 2018-06-28 10:40:37 -07:00