Iavor Diatchki
01b72ce0f9
When a test fails, print a suggestion how to make the output gold.
2017-12-21 10:14:44 -08:00
Iavor Diatchki
32fb511ced
Add location more generally.
2017-12-15 14:12:38 -08:00
Iavor Diatchki
7db18e817c
Improve error message for ambiguous types.
2017-12-15 14:05:15 -08:00
Iavor Diatchki
2272a59314
Rename type synonyms properly.
2017-12-01 10:29:42 -08:00
Iavor Diatchki
3443331f06
Add a test
2017-12-01 09:51:43 -08:00
Iavor Diatchki
5cd90d0045
Fix up scoping when instantiating modules.
2017-12-01 09:51:28 -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
f658f0244d
Add another test.
2017-11-28 14:26:12 -08:00
Iavor Diatchki
c0b4ddd608
Keep track of the order in which type parameters are declared in the file.
2017-11-28 14:07:14 -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 Diatchki
9de90e5752
Slightly better parser messages.
2017-11-15 15:36:45 -08:00
Brian Huffman
951eebb8e2
Add more documentation of Cryptol prelude primitives.
2017-11-15 11:37:06 -08:00
Brian Huffman
79fbb61aa7
Require doc-strings to start with "/**" with exactly 2 asterisks.
...
Things like "/******* WARNING ********/" are now parsed as ordinary
comments. See #438 .
2017-11-15 11:36:25 -08:00
Brian Huffman
511e97767f
Disallow spaces inside qualified names (e.g. Foo::x). Fixes #381 .
2017-11-15 10:52:36 -08:00
Iavor Diatchki
8700ad6832
Run warning check whenever we do some renaming, instead of just in the module.
...
Hopefully this fixes #483 properly this time.
2017-11-14 16:11:00 -08:00
Iavor Diatchki
5ccb0bb4ad
Warn for unused type names.
...
Fixes #483 .
2017-11-14 15:57:15 -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
c4b156e499
Don't add an empty record, if the module has not value parameters.
...
Fixes #484
2017-11-08 14:19:40 -08:00
Iavor Diatchki
a8d5c5c602
Add some better cancellation of common constants.
2017-11-08 14:13:49 -08:00
Iavor Diatchki
7e964aa1cd
Add a simplification rule for subtraction.
2017-11-07 15:51:05 -08:00
Iavor Diatchki
e1b9e0b5bf
Merge branch 'master' of github.com:GaloisInc/cryptol
2017-11-07 13:59:28 -08:00
Iavor Diatchki
31c680d49d
AES and GCM using parameterized modules.
2017-11-07 13:59:22 -08:00
Iavor Diatchki
0adcddb792
Remember edit path.
2017-11-07 11:27:50 -08:00
Iavor Diatchki
f71ba16345
Fix order of type applications.
2017-11-07 11:27:37 -08:00
Brian Huffman
30b7d2918a
Implement signed operators (/$) and (%$) in reference interpreter.
...
This partially addresses ticket #469 .
2017-11-06 16:55:32 -08:00
Brian Huffman
8f94daf783
Catch calls to error coming from SBV library. Fixes #479 .
2017-11-06 14:10:01 -08:00
Aaron Tomb
8c6af8632b
Fix order of counter in Salsa20 example
2017-11-03 07:24:30 -07:00
Brian Huffman
c587d3fcb4
Allow underscores in numeric literals. Implements #477 .
...
The implementation allows any number of underscores between
digits, or between the base specifier and digits. Underscores
are not allowed at the beginning or end of a numeric literal.
0x1234_5678 (OK)
0b_0110_1001 (OK)
0xff______ff (OK)
5_000_000 (OK)
2_________3 (OK)
0_x1234 (BAD)
_0xff (BAD)
52_ (BAD)
_5 (BAD)
2017-11-02 17:00:46 -07:00
Iavor Diatchki
d6d8ab1d35
Try to shrink the model, when defaulting at the REPL. Fixes #476
2017-10-30 17:26:18 -07:00
Iavor Diatchki
d7d1f21434
Cancel out finite positive variables.
2017-10-30 14:25:15 -07:00
Iavor Diatchki
c5e0540a0f
Fix test.
2017-10-30 14:24:47 -07:00
Iavor Diatchki
2bf932045d
Fix benchmarking code
2017-10-30 13:20:50 -07:00
Iavor Diatchki
07eac47989
Merge remote-tracking branch 'origin/abstract-types'
2017-10-27 15:12:22 -07:00
Iavor Diatchki
3f8a8b8874
Add forgotten file
2017-10-27 15:07:15 -07:00
Iavor Diatchki
ee1871dc4c
Add an example of module instantiation.
2017-10-27 15:07:04 -07:00
Iavor Diatchki
2d3e146766
Allow evaluation in parameterized module, as long as parameters are not used.
2017-10-27 14:59:32 -07:00
Iavor Diatchki
4cf83a3c3d
Keep track of the file that cause an error.
...
Also, now we automatically switch to working on this file, which
is sometimes nice, and sometimes confusing...
2017-10-27 11:02:08 -07:00
Brian Huffman
bc5fe0e4c9
Add combinators tIsRec and aRec for matching record types (TRec).
2017-10-27 10:54:32 -07:00
Iavor Diatchki
35a3843685
Remember the path when editing.
2017-10-27 10:21:50 -07:00
Iavor S. Diatchki
2faa44e17b
Add some documentation for the module system.
2017-10-26 16:34:08 -07:00
Iavor S. Diatchki
65ebbb5956
Extend core linter with support for parameterized modules.
2017-10-26 14:20:29 -07:00
Iavor S. Diatchki
26240742a4
Pretty print when panicing, makes it easier to see
2017-10-26 11:50:48 -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
b87f387d38
Add param in the correct place, but there's still something wrong.
2017-10-25 17:00:11 -07:00
Iavor Diatchki
3f4cc570cf
Use a record for all module parameters at the value level. Also improve PP
2017-10-25 16:39:29 -07:00
