Brian Huffman
f67480fae2
Reference interpreter: Fix strictness of Arith and polynomial functions
2017-05-05 09:02:29 -07:00
Aaron Tomb
9add6a4b2f
Clarify which prover finished first
...
With `:set prover=any`, and when prover stats are enabled, the prover
that finished first is now prefixed with a "*".
2017-03-31 14:02:41 -07:00
Aaron Tomb
aeff31d0c0
Add rendered semantics document to repository
2017-03-31 08:28:04 -07:00
Trevor Elliott
7fc50a9cbb
Write out the typechecker prelude when necessary
...
Bundle the typechecker prelude (CryptolTC.z3) with the executable, so
that it's able to write it out and re-use it when necessary.
Fixes #404
2017-03-28 16:30:40 -07:00
Brian Huffman
f89c23b594
Edit documentation for reference interpreter.
2017-03-28 14:19:32 -07:00
Brian Huffman
ecfcb6ad25
Add rules for Semantics.pdf to docs/Makefile
2017-03-28 14:19:24 -07:00
Brian Huffman
9228cf0400
Reorder and add documentation to reference evaluator
2017-03-28 14:19:08 -07:00
Brian Huffman
e15e8ee8bb
Makefile looks for .lhs source files
2017-03-28 14:18:52 -07:00
Brian Huffman
1a38f470a1
Convert module Cryptol.Eval.Reference to literate Haskell.
2017-03-28 14:18:35 -07:00
Trevor Elliott
20f4f9a108
Simplify addition of constants in equality and geq constraints
...
Simplifying constraints of the form `k1 + a == k2 + b`. If `k1 > k2`,
then the constraint can be rewritten to `(k1 - k2) + a == b`, or
`a == (k2 - k1) + b` otherwise. This allows the constraint solver to
make progress in cases where `a` or `b` include unification variables.
2017-03-28 13:20:35 -07:00
Trevor Elliott
576df9fa95
More precise rule for k >= width var interval derivation
2017-03-27 16:47:26 -07:00
Trevor Elliott
5a43c1d1fe
More precise definition of chunks
...
Use `padding` directly in the definition of `chunks`, giving an aligned
value to the division.
2017-03-27 16:37:55 -07:00
Trevor Elliott
b93f84cf78
Remove unnecessary constraint that was preventing malicious_SHA1.cry from loading
...
Cryptol could not prove that subtracting `65 + padding` from `512 * chunks`
in the constraint `msgLen == 512 * chunks - (65 + padding)` was well
defined, and rejected the function. This constraint was redundant, so
removing it allowed the function to typecheck.
2017-03-27 16:36:09 -07:00
Trevor Elliott
4dc5eda23a
Expand the width table, and fix a bug in CryptoBox (Thanks @tommd)
...
The width table in CryptolTC.z3 wasn't large enough to solve constraints
about the width of 64-bit words. This change is a bit of a band-aid, as
larger words will expose the same problem. Longer-term, we should try to
solve these constraints after the SMT-based phase, using some other
approach.
The constraints in CryptoBox were too permissive, and when adjusted to
represent the true intent (that values fit within 64-bits), and the
width table was updated, the example will type-check again.
Thanks to @tommd for tracking both of these down.
2017-03-27 13:45:50 -07:00
Trevor Elliott
f018522b31
Fix upper bound on the interval derived from k >= width x
2017-03-25 09:44:32 -07:00
Trevor Elliott
8a4eadfdac
Add a rule for simplifying x +y = inf
2017-03-24 18:02:29 -07:00
Trevor Elliott
90f7d0c330
First attempt at interval computation for k >= width x
2017-03-24 18:02:03 -07:00
Trevor Elliott
1e723d5265
Add a rule for multiplication
...
When the constraint is of the form, `k1 * x = k2 * y`, and `gcd k1 k2 /= 1`,
simplify the constraint to `(k1 / gcd k1 k2) * x = (k2 / gcd k1 k2) * y`.
(NOTE: this doesn't produce a new constraint that uses division, but
evaluates the two two constants.)
2017-03-24 16:41:12 -07:00
Aaron Tomb
d498212684
Update Programming Cryptol PDF
2017-03-21 13:25:00 -07:00
Aaron Tomb
d76f21f89e
Update benchmarks to find Prelude and CryptolTC.z3
...
Since they don’t run in the normal REPL environment, they need to know
about where to find the Prelude and CryptolTC.z3 more directly.
2017-03-21 12:31:04 -07:00
Aaron Tomb
5dea49e6af
Process CRYPTOLPATH before smoke test
2017-03-21 12:29:55 -07:00
Aaron Tomb
6a3043ff21
Improve error message when CryptolTC.z3 not found
2017-03-21 12:29:14 -07:00
Aaron Tomb
254283f7cb
Document configuration of support files
...
Now README.md describes how to tell Cryptol where to find the Prelude
and Z3 configuration files that it needs.
2017-03-21 09:14:09 -07:00
Aaron Tomb
77db35ffda
Document success and error exit codes.
2017-03-21 09:08:48 -07:00
Aaron Tomb
c025f874db
Document the prover-stats option.
2017-03-21 09:06:18 -07:00
Aaron Tomb
aa900df04c
Set user option if exact match, even if prefix
...
The `:set` command wasn't allowing `prover` as a key, since
`prover-stats` also exists. Now it allows an exact match even if it's a
prefix of some other option. To set `prover-stats` or a similar option,
spell it out more completely.
2017-03-21 09:04:17 -07:00
Trevor Elliott
d174ac38ba
Remove transformers-compat and crackNum in the GHC710 config
2017-03-13 16:04:36 -07:00
Trevor Elliott
28d24c151b
Remove QuickCheck from the GHC710 stackage snapshot
2017-03-13 15:54:14 -07:00
Trevor Elliott
5fc47c8dab
Remove monadLib and simple-smt from stackage snapshots
2017-03-13 15:51:28 -07:00
Trevor Elliott
7e1ad7d970
Remove cryptol from the stackage snapshots
2017-03-13 15:50:00 -07:00
Trevor Elliott
302e48068d
Update stackage snapshots
2017-03-13 14:23:25 -07:00
Brian Huffman
4c45e1ba62
Update haddock comments
2017-03-09 11:24:09 -08:00
Brian Huffman
f8290af910
Fix haddock parse errors
2017-03-09 10:58:55 -08:00
Brian Huffman
fd4415803a
Fix compiler warnings
2017-03-09 10:27:20 -08:00
Iavor S. Diatchki
fddcd60d10
Merge branch 'master' of github.com:GaloisInc/cryptol
2017-02-23 15:22:40 -08:00
Iavor S. Diatchki
174bb3c20a
Remove ECast
...
The invariant that this used to ensure does not hold anymore, so
it was more confusing than not to have it.
2017-02-23 15:18:05 -08:00
Iavor S. Diatchki
1d8f2576c8
Add a deriving Eq on Schemas.
...
The equality is completely syntactic.
2017-02-17 11:38:51 -08:00
Iavor S. Diatchki
41131fe7ed
Redo the export to SMT story in a much simpler way.
2017-02-16 16:46:38 -08:00
Iavor S. Diatchki
de770d5aed
Remove warnings.
2017-02-15 11:31:30 -08:00
Iavor S. Diatchki
866722956b
Fall back to old solver, if all else fails.
2017-02-15 11:29:03 -08:00
Iavor S. Diatchki
27eaec689d
Fix test. There is indeed defaulting that should be happening here.
2017-02-15 10:02:15 -08:00
Iavor S. Diatchki
e30b1e7cd3
Wibble
2017-02-15 10:01:57 -08:00
Iavor S. Diatchki
68303fb958
Prefere errors that do not mention unificaion variables.
2017-02-15 09:08:38 -08:00
Iavor S. Diatchki
5e1a3b6f5a
This one works now.
2017-02-15 09:08:15 -08:00
Iavor S. Diatchki
ec58bec6aa
Add .cryptolsrc files
2017-02-15 09:08:02 -08:00
Brian Huffman
091894fc9d
Update reference interpreter to handle run-time errors explicitly
...
The :eval command should never throw an actual run-time exception;
instead, errors are represented alongside bits in the value datatype,
and errors are printed wherever they appear inside the result value.
2017-02-10 13:35:15 -08:00
Iavor S. Diatchki
9d9f9a8de7
Hack, hack. Pass context to solver after defaulting.
...
The structure of all this should be fixed.
2017-02-08 19:00:00 -08:00
Iavor S. Diatchki
f6a4aef4cc
A more readable version of (possibly?) the same code
2017-02-08 18:59:24 -08:00
Iavor S. Diatchki
a8ddf035f2
Lookup variables in the interval map
2017-02-08 18:59:05 -08:00
Iavor S. Diatchki
2c3145a417
Fix some of the broken tests.
2017-02-08 17:24:15 -08:00
