GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-12-16 03:05:44 +03:00
Code Issues Projects Releases Wiki Activity
1,813 Commits 68 Branches 28 Tags 95 MiB
027037d6ee
Commit Graph

1813 Commits

This Branch
This Branch
All Branches
Author SHA1 Message Date
Iavor Diatchki
027037d6ee Fix test 2018-07-26 22:06:31 +03:00
Iavor Diatchki
6d789a1d64 Preserve prefix - and ~ until the renamer. 
This allows to print back expressions in a form that looks more like what
the user typed.  Fixes #541
 2018-07-26 22:04:45 +03:00
Iavor Diatchki
fb4080a22e Merge branch 'master' of github.com:GaloisInc/cryptol 2018-07-26 09:28:06 +03:00
Iavor Diatchki
96539178d4 Display help for built-in types in REPL. 
Fixes #504
 2018-07-26 09:27:11 +03:00
Iavor Diatchki
19c71fa4aa Move all built-in types to the same place; add precedence and documentaiton 2018-07-26 09:06:37 +03:00
Brian Huffman
4d84989b60 Edits to AES chapter of the book. 2018-07-25 15:12:13 -07:00
Brian Huffman
2f53f364b5 Add stderrLogger to go with stdoutLogger. 2018-07-25 10:10:52 -07:00
Iavor Diatchki
f4e7100e59 Merge branch 'master' of github.com:GaloisInc/cryptol 2018-07-25 13:27:14 +03:00
Iavor Diatchki
5a720e6695 Use proveModuleTopLevel instead simplifyAllConstraints. 
The difference is that the one does defaulting as well.  Fixes #540
 2018-07-25 13:27:01 +03:00
Brian Huffman
165674710b Fix typo in comment. 2018-07-24 15:42:16 -07:00
Brian Huffman
1af977873e Make :browse <interactive> work with tab-completion, no warnings. 2018-07-24 15:29:58 -07:00
Brian Huffman
951eacc8ff Fix some index entry names in the book. 2018-07-24 13:03:32 -07:00
Iavor Diatchki
e55436eaa7 Keep track of user vs. system names. 
This makes it possible to hide system names from the users,
as they are not really meaningful.  Fixes #535
 2018-07-24 18:19:17 +03:00
Iavor Diatchki
125a2a4d32 After defaulting, nub the resulting fin constraints. 
Fixes #531
 2018-07-24 16:52:15 +03:00
Iavor Diatchki
d1b5439b4c Remove defSu, this is already part of totSu, as we've extended it 2018-07-24 16:51:28 +03:00
Iavor Diatchki
83ece9e3fb Fixes #532 2018-07-24 16:00:55 +03:00
Iavor Diatchki
9f94dd0eba Merge branch 'master' of github.com:GaloisInc/cryptol 2018-07-24 15:29:27 +03:00
Iavor Diatchki
b6d6ead7f1 Fixes related to generalization in recursive groups, where some bindings are monomorphic. 
This is tricky stuff, hopefully this better.  Fixes #534
 2018-07-24 15:29:06 +03:00
Brian Huffman
3cee1b037e Memoize wordValLogicOp on BitsVal arguments. 
This fixes the exponential runtime for the example in #537.
 2018-07-23 14:44:48 -07:00
Aaron Tomb
35452a6a9e Add example of using the === operator 2018-07-23 13:19:13 -07:00
Iavor Diatchki
9a9e9c977c A bit of refactoring. 
This should help us hide top-level generated names that are
not of interest to the user.
 2018-07-23 03:34:04 -07:00
Iavor Diatchki
bd0d3ccf35 Remove unused code, add explicit exports 2018-07-23 03:32:31 -07:00
Iavor Diatchki
f398a68fad When applying a defaulting substitution, keep going even if value found. 
Since our substitutions are idempotent, normally this would be just wasted
work, but when we are defaulting, we must make sure that we default the
varibales in the looked up thing also.

This fixes #534
 2018-07-23 03:30:52 -07:00
Brian Huffman
863c165c66 Update syntax appendix of Cryptol book. 2018-07-20 18:13:15 -07:00
Brian Huffman
1eaabf87aa Miscellaneous edits to the book. 2018-07-20 15:48:46 -07:00
Brian Huffman
891b7fe914 Update exercises in chapter 1 of the book. 2018-07-20 15:48:10 -07:00
Brian Huffman
ed757860bf Fix typos in Cryptol prelude docstrings. 2018-07-20 15:34:13 -07:00
Aaron Tomb
69ec23e96b Make sure to use BASH on Travis 2018-07-20 14:46:45 -07:00
Aaron Tomb
7d2afb6c2a Run tests on Travis 2018-07-20 14:08:31 -07:00
Brian Huffman
317893a564 Updates to "High-assurance programming" chapter of the book. 2018-07-20 12:20:59 -07:00
Brian Huffman
72bc388663 Add regression test for #533. 2018-07-20 12:04:03 -07:00
Brian Huffman
09bb438021 Avoid type mismatch panic when printing counterexamples. Fixes #533. 2018-07-20 12:03:51 -07:00
Brian Huffman
5def499908 Capitalize sentences in output of :check and :exhaust. 2018-07-20 10:55:24 -07:00
Brian Huffman
409e544772 Restrict polynomial literals to bitvector types. Fixes #530. 2018-07-20 10:06:16 -07:00
Aaron Tomb
031b236e66 Update CI scripts 2018-07-20 10:05:44 -07:00
Aaron Tomb
0b46db36ce Fix capitalization of MiniLock in test 2018-07-20 10:04:11 -07:00
Brian Huffman
73a8c19b58 Update cryptol primitives appendix in the book. 2018-07-20 09:48:31 -07:00
Brian Huffman
eef8924dfe Update operator names in Cryptol book index. 2018-07-20 09:00:29 -07:00
Brian Huffman
6201415c66 Remove index entries and text about non-existent :i, :p commands. 2018-07-20 08:28:35 -07:00
Brian Huffman
dd2c4b6507 Introduce command for more uniform exercise references in the book. 2018-07-19 18:25:55 -07:00
Brian Huffman
abbce5405c Tweak fix for #494: it should never say an equation is unsolvable. 2018-07-19 18:01:12 -07:00
Brian Huffman
af6b830162 Use autoref command and lowercase section refs consistently in the book. 2018-07-19 18:00:17 -07:00
Brian Huffman
10f43b4279 Switch Cryptol book exercises to use split instead of groupBy. 2018-07-19 16:46:48 -07:00
Brian Huffman
5451683f4a Add regression test for #494. 2018-07-19 15:08:24 -07:00
Brian Huffman
b19cac5fab Add simplification rule: t1 == min (K + t1) t2 ~> t1 == t2, if K >= 1. 
Fixes #494.
 2018-07-19 15:07:21 -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
d803192b2b Add regression test that loads all modules from examples directory. 
This file should be updated every time a new module is added to
`examples`.

Fixes #529.
 2018-07-19 09:57:18 -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