Brian Huffman
a5a7a393be
Add definitions of SHAKE128 and SHAKE256 to keccak.cry
2017-10-04 10:39:10 -07:00
Iavor Diatchki
f74ad3c29d
Fix haddock comment, should restore build process.
2017-10-04 10:09:01 -07:00
brianhuffman
73de3f787f
Merge pull request #453 from GaloisInc/blocks-padding
...
Implement `blocks` and `padding` operators for numeric types.
2017-10-04 07:11:19 -07:00
Brian Huffman
9773782ba4
Tweak correctness property to match keccak documentation.
2017-10-04 07:02:55 -07:00
Brian Huffman
16e949b0d7
Fix bugs/warnings in keccak.cry, and add test vectors and other properties.
...
The switch to Cryptol 2 introduced some endianness bugs.
Also, the original version omitted the 0b01 "suffix" that is
specified by SHA3.
2017-10-03 18:06:52 -07:00
Rob Dockins
2df09a428a
Change how test coverage statistics are computed.
...
This formulation accounts for the fact that test vectors
are chosen randomly with replacement.
Fixes #461
2017-10-03 17:37:48 -07:00
robdockins
fc4fe4dc1e
Merge pull request #309 from clinty/cast5
...
CAST5 example
2017-10-03 15:27:30 -07:00
Iavor Diatchki
dac4c2e5a3
Merge branch 'master' of github.com:GaloisInc/cryptol
2017-10-03 14:04:36 -07:00
Iavor Diatchki
866a1142da
Try out a new logo. Stuff that matters :-)
2017-10-03 14:04:29 -07:00
Brian Huffman
7802747a1e
Simplify keccak.cry using new type operators for padding.
2017-10-03 13:57:16 -07:00
Brian Huffman
3b03545552
Merge branch 'master' into blocks-padding
2017-10-03 13:44:32 -07:00
Brian Huffman
96bff5c4a8
Update keccak.cry example to work with Cryptol 2.x
...
Fixes #458 .
2017-10-03 13:41:07 -07:00
Iavor S. Diatchki
cad6e1fe77
Merge pull request #459 from GaloisInc/rwd/linear-unifier
...
Add a rule to the numeric solver for "linear unifiers"
2017-10-03 13:17:15 -07:00
Rob Dockins
9785ed1e32
Add a rule to the numeric solver for "linear unifiers"
...
Check for situations where a unification variable is involved in
a sum of terms not containing additional unification variables,
and replace it with a solution and an inequality.
`s1 = ?a + s2 ~~> (?a = s1 - s2, s1 >= s2)`
Fixes #212
2017-10-03 12:49:17 -07:00
Brian Huffman
b107e606a2
Update example cryptol code to use infix syntax.
2017-10-03 12:31:37 -07:00
Rob Dockins
b1c6ae22c7
Add MD5 example
2017-10-03 11:27:15 -07:00
Rob Dockins
f1161dd282
Add a Karatsuba multiplier to the examples
2017-10-03 11:27:15 -07:00
Iavor Diatchki
a9edd7a389
Merge branch 'master' of github.com:GaloisInc/cryptol
2017-10-03 10:53:45 -07:00
Iavor Diatchki
234615e7b2
Add some comments
2017-10-03 10:53:40 -07:00
Rob Dockins
f02a3c783b
Bump simple-smt version bounds to pull in a bug fix.
...
Fixes #457
2017-10-03 10:20:15 -07:00
Rob Dockins
d32f3324c9
Update syntax reference with new fixity information for (||) and (&&)
2017-10-02 18:17:38 -07:00
Rob Dockins
e7d3ed02f9
Add testcase for issue #389 .
...
Recent improvements to the numeric solver have fixed this issue.
Fixes #389 .
2017-10-02 18:15:02 -07:00
Rob Dockins
42064dd9f2
Add testcase for issue #325 .
2017-10-02 17:49:12 -07:00
Rob Dockins
37f9dc4c4f
Add test for issue #78 .
...
Fixes #78 .
2017-10-02 15:48:51 -07:00
Iavor Diatchki
a233084db8
Merge branch 'master' of github.com:GaloisInc/cryptol
2017-10-02 15:47:23 -07:00
Rob Dockins
d5bfb1b648
Minor update to test suite
2017-10-02 15:40:46 -07:00
Rob Dockins
c0699e2d62
Change the fixity levels of (||) and (&&).
...
This advances the next step in the plan described in issue #241 .
2017-10-02 14:56:33 -07:00
Rob Dockins
2894a1fdef
Make solver startup/shutdown exception-safe.
2017-10-02 14:06:44 -07:00
Rob Dockins
12ac2c383a
Revert "Remove the Data.Sequence-based representation of unpacked bitsequences."
...
This may improve performace on some examples.
This reverts commit d4b70a039a
2017-10-02 11:12:50 -07:00
Brian Huffman
940b9c80ec
Merge branch 'integer'
2017-09-29 14:23:28 -07:00
Brian Huffman
5e4d094eb3
Fix test output due to counterexample printing change.
2017-09-29 14:23:18 -07:00
Aaron Tomb
da1ff8f225
Merge pull request #454 from madnight/patch-1
...
Update copyright notice year from 2016 to 2017
2017-09-29 10:59:16 -07:00
Brian Huffman
3fb74f7f60
Make :check and :exhaust print counterexamples the same way :prove does.
...
This addresses the first part of issue #449 .
2017-09-29 10:19:56 -07:00
Iavor Diatchki
fe88d98213
Merge branch 'master' of github.com:GaloisInc/cryptol
2017-09-29 09:44:42 -07:00
Brian Huffman
7be06d803e
Fix typo in error message.
2017-09-29 09:28:46 -07:00
Iavor S. Diatchki
75ca6b7fa2
Say something if name does not refer to anything
2017-09-28 15:47:23 -07:00
Iavor S. Diatchki
aa44dd7860
Add support for docstrings on type things
...
See #456
2017-09-28 14:39:22 -07:00
Brian Huffman
d9cbfd62d1
Add instance Zero Integer.
2017-09-28 13:26:01 -07:00
Brian Huffman
cce32a4868
Merge branch 'master' into integer
...
This brings the Logic and Zero type classes into the integer branch.
2017-09-28 13:18:27 -07:00
Brian Huffman
7e34c25e4d
Switch to infix syntax for blocks and padding operators.
...
"x /^ y" is x/y rounded up, i.e. the least n such that x <= y*n.
"x %^ y" is the least k such that x+k is a multiple of y.
For comparison,
"x / y" is x/y rounded down, i.e. the greatest n such that x >= y*n.
"x % y" is the least k such that x-k is a multiple of y.
The new syntax is much more suggestive of the relation to "/" and "%".
2017-09-28 10:26:31 -07:00
Brian Huffman
defadf8730
Fix cut-and-paste error.
2017-09-28 09:45:40 -07:00
Brian Huffman
1e41541405
Let type checker discharge fin (blocks x y) and fin (padding x y).
...
Both of these type operators are always either finite or undefined.
2017-09-28 09:28:07 -07:00
Fabian Beuke
ab75f152d1
Update copyright notice year from 2016 to 2017
2017-09-28 16:18:00 +02:00
Brian Huffman
f04908a551
Adapt example code to use new blocks and padding operators.
2017-09-27 13:55:55 -07:00
Brian Huffman
9bc6d02019
Implement blocks and padding operators for numeric types.
...
The design is as described in issue #96 :
blocks msgLen blockSize = the least n such that msgLen <= blockSize * n
padding msgLen blockSize = least k such that msgLen + k divides blockSize
or alternatively:
msgLen + padding msgLen blockSize = blocks msgLen blockSize * blockSize
2017-09-27 13:43:26 -07:00
Iavor Diatchki
aab03be26a
More wibbles
2017-09-27 10:24:30 -07:00
Iavor Diatchki
208119fbbf
Merge branch 'master' of github.com:GaloisInc/cryptol
2017-09-27 10:17:06 -07:00
Iavor Diatchki
6018af3537
Just documentation
2017-09-27 10:16:58 -07:00
brianhuffman
c32d68dade
Merge pull request #445 from GaloisInc/logic-class
...
Introduce a `Logic` class for bitwise logical operations
2017-09-27 09:10:47 -07:00
Brian Huffman
1ed5640339
Merge branch 'master' into logic-class
...
# Conflicts:
# tests/mono-binds/test05.icry.stdout
2017-09-26 16:50:53 -07:00
