Adam C. Foltzer
4c441898d9
remove a merge error from docs Makefile
2015-10-05 15:33:04 -07:00
Adam C. Foltzer
80daf82b8c
add threading by default for executables
2015-10-01 13:50:32 -07:00
Adam C. Foltzer
baddfcaab8
Merge branch 'heads/hotfixes/v2.2.5'
2015-10-01 10:56:30 -07:00
Adam C. Foltzer
7d81568555
remove iteSolver option for compat with sbv 5+
2015-09-30 14:24:21 -07:00
Adam C. Foltzer
243e051df3
bump version number, add SBV upper bound
...
Conflicts:
stackage.config
2015-09-29 11:28:30 -07:00
Adam C. Foltzer
c07f97a994
update to Stackage LTS 3.5
...
This snapshot requires GHC 7.10+, but since we're only copying over the
Stackage config on the Jenkins machines, we're not requiring 7.10-only
just yet. The newest 7.8.4 snapshot has a too-old version of SBV,
though, so builds for earlier than 7.8 are more of a wild west.
2015-09-18 16:05:31 -07:00
Adam C. Foltzer
4df92455e5
update stackage snapshot
2015-09-17 14:45:51 -07:00
Jenkins Builder
75539f9244
add \protect to fix error on Windows docs
2015-09-16 13:12:37 -07:00
Adam C. Foltzer
2ca0e6f732
switch back to non-latexmk for book (Windows)
...
Windows didn't like the latexmk solution from
5eb5f00d0a
2015-09-16 11:37:00 -07:00
Thomas M. DuBuisson
17abf37b7d
A rough cut at SIV.
2015-09-16 09:19:27 -07:00
Adam C. Foltzer
5eb5f00d0a
change how the book is built
2015-09-15 13:38:06 -07:00
Trevor Elliott
98c49b875c
Slight speedup in name comparison
2015-09-14 21:50:26 -07:00
Adam C. Foltzer
28461e7b72
update attribution on SHA512
2015-09-14 17:18:47 -07:00
Thomas M. DuBuisson
7643a17182
Fix #272 Don't full blocks in ChaChaPoly8675309
2015-08-28 15:22:03 -07:00
Brian Huffman
72d8794b9d
Change where integer masking is applied in the interpreter
...
In the Value datatype, we now maintain an invariant for
all packed bitvectors: The value must be within the range
0..2^width-1. Values are normalized when constructed, not
when they are scrutinized.
2015-08-28 13:47:17 -07:00
Aaron Tomb
44f8bcd310
Fix comment in Keccak example
...
Note: this is actually Cryptol 1 code. We should port it. I've started
the process, but don't have a complete port yet.
2015-08-28 09:49:29 -07:00
Adam C. Foltzer
9b6cde1f8d
reexport version number
2015-08-26 11:34:16 -07:00
Trevor Elliott
ec4fb4ab54
Fix #271
...
The renamer wasn't expecting to see anything but (==), (>=), or (<=) show up in
a case where that wasn't a valid assumption.
2015-08-25 10:50:35 -07:00
Brian Huffman
792f8e433f
Allow "-" in infix operator names
2015-08-21 11:00:46 -07:00
Adam C. Foltzer
50ca428018
add regression in #269 to benchmark suite
2015-08-20 15:49:06 -07:00
Adam C. Foltzer
3825ce84c8
update to use Text in Ident
2015-08-19 14:42:40 -07:00
Trevor Elliott
5cf2b9e47e
Warning removal
2015-08-14 17:43:02 -07:00
Trevor Elliott
9092492d6a
Improvement improvements
...
Integrate interval analysis into improvements to simplify fin constraints, and
rewriting of equality constraints.
2015-08-14 17:38:50 -07:00
Trevor Elliott
d71fd8a3ee
Issue #148 is fixed now
2015-08-14 17:38:50 -07:00
Adam C. Foltzer
dce6f994e8
Merge branch 'master' into feature/benchmarks
2015-08-14 16:23:10 -07:00
Adam C. Foltzer
ab9ccb50d7
make NFData deriving 7.8-compatible
2015-08-14 14:42:38 -07:00
Trevor Elliott
a4c3892002
Finish a comment
2015-08-13 23:08:00 -07:00
Trevor Elliott
0d4a5bf5d3
Warning removal
2015-08-13 22:50:23 -07:00
Trevor Elliott
6784125cfa
Add an intersection function for intervals
2015-08-13 22:49:54 -07:00
Iavor S. Diatchki
ad6f0fb8aa
Solving fin constraints direclty.
2015-08-13 16:38:48 -07:00
Iavor S. Diatchki
b6fa8d9473
Bufixes, and pass in info argument.
2015-08-13 16:38:34 -07:00
Trevor Elliott
f54a3b13ca
Remove debugging output
2015-08-13 14:44:29 -07:00
Trevor Elliott
82f8bbbe0d
Conservative use of fin constraints
2015-08-13 14:43:18 -07:00
Trevor Elliott
a21a646af2
Enable OverloadedStrings to fix a build error
2015-08-13 14:42:10 -07:00
Trevor Elliott
9fa56160f8
Only add subtraction in special cases during goal rewriting
...
It's only OK to subtract something if you know that it's finite. This change
adds a fairly conservative check when rewriting `a + b = r` to `a = r - b` that
`b` be finite.
2015-08-13 11:15:12 -07:00
Brian Huffman
dadc5e1781
Switch Name type to use Data.Text instead of String
...
This gives a few percent speedup in the interpreter.
2015-08-12 17:58:57 -07:00
Brian Huffman
4976a8db3e
Use abstract interface to module Cryptol.ModuleSystem.Name
...
This makes it possible to change the representation of
the Name type without breaking lots of other code.
2015-08-12 17:40:06 -07:00
Iavor S. Diatchki
c9e4fab6a8
Fix up tests.
2015-08-12 15:52:18 -07:00
Adam C. Foltzer
ef2fd808ee
add junit-style output for make bench target
2015-08-12 15:47:50 -07:00
Iavor S. Diatchki
1d69f4b67d
Merge remote-tracking branch 'origin/wip/goal-rewriting'
...
Conflicts:
src/Cryptol/TypeCheck/Solve.hs
2015-08-12 15:42:03 -07:00
Iavor S. Diatchki
44ef6930d7
Merge branch 'master' of github.com:GaloisInc/cryptol
2015-08-12 15:02:34 -07:00
Iavor S. Diatchki
31dd1125ec
Definitions of semantics for partial predicates.
2015-08-12 15:02:22 -07:00
Iavor S. Diatchki
c363d92c44
Clean up simplification of individual constraints, somewhat.
2015-08-12 15:01:51 -07:00
Adam C. Foltzer
32e55cc11f
add benchmark sources
2015-08-12 14:41:44 -07:00
Adam C. Foltzer
4e6dcaa026
add NFData instances for many cryptol types
...
add more benchmarks as well
2015-08-12 14:29:30 -07:00
Trevor Elliott
c10a92be84
First pass at goal rewriting
...
Attempt to normalize equality constraints involving a single unification
variable into a form where that variable is alone on one side of the equation.
Applying this normalization before attempting to simplify goals seems to clean
up some cases that the solver wasn't able to deal with.
2015-08-11 23:35:19 -07:00
Trevor Elliott
579b129c2f
Only import Traversable in < ghc 7.10
2015-08-11 17:16:57 -07:00
Trevor Elliott
77c69efe8d
Add the CPP pragma
2015-08-11 17:11:11 -07:00
Iavor S. Diatchki
306713a824
Checkpoint
2015-08-11 09:22:28 -07:00
Iavor S. Diatchki
d86c288928
More logging
2015-08-11 09:22:09 -07:00
