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
Iavor S. Diatchki
424d02eb27
Fix copy-paste error in normalization of LenFromThenTo
2017-02-08 16:30:04 -08:00
Iavor S. Diatchki
568a26b9aa
Restore functionality of Panic
2017-02-08 16:29:45 -08:00
Iavor S. Diatchki
3c15d086d1
Merge branch 'master' into wip/solver
2017-02-08 16:24:46 -08:00
Iavor S. Diatchki
8c19abb452
Merge branch 'master' of github.com:GaloisInc/cryptol
2017-02-08 16:19:00 -08:00
Iavor S. Diatchki
6bef779780
Add a flag to control if batch execution stops on the first error or not.
...
This is off by default.
2017-02-08 16:18:50 -08:00
Iavor S. Diatchki
fa37734956
Add a flag to control if we show prover timing stats or not.
2017-02-08 16:08:20 -08:00
Iavor S. Diatchki
3c2c9a857a
Fix test to account for printing of operators' precedences.
2017-02-08 16:07:54 -08:00
Iavor S. Diatchki
710355176a
More rules and things; external solver disabled; we can at least load ChaCha
2017-02-08 15:08:50 -08:00
Iavor S. Diatchki
90c6adbfcd
Goals as Sets works again.
2017-02-03 17:10:50 -08:00
Iavor S. Diatchki
336ea625b0
In InferM types don't contain thunks.
2017-02-03 15:56:19 -08:00
Iavor S. Diatchki
44085b4c5d
Keep maintaining evaluated invariant
2017-02-03 14:21:24 -08:00
Iavor S. Diatchki
5ebf13212a
Remove extra layer of simplification.
...
We should not be inferring unevaluated types.
XXX: The whole ECast story is probably broken now, as we evaluate substitutions
directly, but we don't do the corresponding rewrites on terms.
XXX: Do we need ECast at all?
2017-02-03 13:52:33 -08:00
