Brian Huffman
9584fdb54d
Remove some duplicate files from /examples that were also in cryptol-specs.
...
See #571 .
2019-03-01 18:34:23 -08:00
Brian Huffman
acafb2952d
Add cryptol-specs as git submodule under /examples.
2019-03-01 18:05:28 -08:00
Brian Huffman
c387dbe5fd
Remove all uses of [x..] syntax from examples and tests.
2019-02-27 16:25:53 -08:00
Aaron Tomb
bf3aa4dc01
Adapt Travis to new scripts
2018-12-13 08:39:04 -08:00
Brian Huffman
20b9b1c193
Rename prelude function width to length, and generalize its type.
...
Fixes #550 .
2018-10-10 16:21:38 -07:00
Brian Huffman
d58aebcee8
Fix shadowing warnings in example cryptol code.
...
Shadowing a name from the Cryptol prelude produces an unpredictable
warning message with a temporary file name, which is not good for our
regression test suite.
2018-07-19 14:48:12 -07:00
Brian Huffman
48e0e1989b
Fix examples/param_modules/Common/AES_GCM_SIV.cry.
...
Some types had been renamed in a module that it imports.
2018-07-19 09:55:18 -07:00
Brian Huffman
b812241481
Fix type error in examples/Karatsuba.cry.
...
The error was caused by the recent change of the type of `demote`
when class `Literal` was introduced.
2018-07-19 09:37:51 -07:00
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
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
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
Aaron Tomb
99f3fdbf37
Merge Cryptol/Extras.cry with Cryptol.cry
...
Closes #427 .
2018-05-23 15:55:05 -07:00
Iavor Diatchki
f4d306f1ee
Add a TBox based AES
2018-01-04 14:52:41 -08:00
Iavor Diatchki
31d6a5d5a7
Split up AES algorithm into multiple modules.
2018-01-03 15:58:10 -08:00
Iavor Diatchki
173ca8702f
Parametrize polyval by a starting value.
...
This makes it easier to continue hashing:
polyvalFrom H (xs # ys) start = polyvalFrom H ys (polyvalFrom H xs start)
2017-11-28 16:10:48 -08:00
Iavor Diatchki
07029f95c3
Factor out the counter modding part.
...
This is convenient in a proof I am working on.
2017-11-28 11:37:10 -08:00
Iavor Diatchki
93c56ea428
Add support for working directly with key schedules.
...
This is useful for code that uses the same key multiple times.
2017-11-28 11:10:34 -08:00
Iavor S. Diatchki
5421340d26
Move parameterized module to the Common sub-directory
2017-11-09 10:30:07 -08:00
Iavor Diatchki
5dcaf27dbc
Implement AES_GCM_SIV mode
2017-11-08 15:51:20 -08:00
Iavor Diatchki
1f82b8f7df
Rename 'Flavor' to 'Mode'
2017-11-08 15:51:08 -08:00
Iavor Diatchki
4b6013e68e
Remove empty record parameters.
2017-11-08 15:50:58 -08:00
Iavor Diatchki
31c680d49d
AES and GCM using parameterized modules.
2017-11-07 13:59:22 -08:00
Aaron Tomb
8c6af8632b
Fix order of counter in Salsa20 example
2017-11-03 07:24:30 -07:00
Iavor Diatchki
ee1871dc4c
Add an example of module instantiation.
2017-10-27 15:07:04 -07:00
Iavor S. Diatchki
8627945ade
Fix up transformation
2017-10-26 11:50:36 -07:00
Iavor Diatchki
1f86f4c3b3
Some examples.
2017-10-25 17:00:23 -07:00
Iavor Diatchki
d52c5f5938
Merge remote-tracking branch 'origin/master' into abstract-types
...
# Conflicts:
# src/Cryptol/Parser/ParserUtils.hs
2017-10-20 14:07:47 -07:00
Iavor Diatchki
1e17bd03cf
Make parser use strict text (XXX: does this affect performance +ve or -ve)
...
Also makes module names into their own newtype
2017-10-20 12:00:00 -07:00
Iavor S. Diatchki
7dc7be45bb
Merge remote-tracking branch 'origin/master' into abstract-types
...
# Conflicts:
# src/Cryptol/REPL/Monad.hs
2017-10-13 10:45:35 -07:00
Brian Huffman
a5a7a393be
Add definitions of SHAKE128 and SHAKE256 to keccak.cry
2017-10-04 10:39:10 -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
robdockins
fc4fe4dc1e
Merge pull request #309 from clinty/cast5
...
CAST5 example
2017-10-03 15:27:30 -07:00
Iavor Diatchki
1d4ada07c7
Merge branch 'master' into abstract-types
2017-10-03 14:10: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 Diatchki
2ef0a67d9b
Merge branch 'master' into abstract-types
2017-10-03 13:35:57 -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
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
f04908a551
Adapt example code to use new blocks and padding operators.
2017-09-27 13:55:55 -07:00
Iavor Diatchki
920cb58ad0
Some cleanup and doubt that I've enconded the algorithm correctly
2017-09-27 09:50:47 -07:00
Iavor Diatchki
b8707033d7
Add module parameters as extra vars---prints nicer error messages.
2017-09-26 15:29:23 -07:00
Iavor Diatchki
83d0132e50
Add module-level constraints to assumptions when proving implications.
2017-09-26 15:21:40 -07:00
Iavor Diatchki
ccc4b828c2
Represent type parameters as just type variables.
2017-09-25 11:41:00 -07:00
Iavor S. Diatchki
d1abac0cec
Update design; handle numeric type parameters in type checking SMT
2017-09-21 14:57:53 -07:00
Iavor Diatchki
f7e1a941e2
checkpoint
2017-09-21 09:28:01 -07:00
