GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-12-18 13:31:50 +03:00
Code Issues Projects Releases Wiki Activity
329 Commits 67 Branches 28 Tags 95 MiB
cdf1afd261
Commit Graph

329 Commits

This Branch
This Branch
All Branches
Author SHA1 Message Date
Joey Dodds
72c870cb12 small fixes for push 2014-08-01 09:15:58 -07:00
Brian Huffman
8a37dac522 Add "boolector" and "mathsat" as possible prover settings. 
Support for these provers was added in SBV version 3.
 2014-07-31 16:38:04 -07:00
Trevor Elliott
67a28f4e73 Change the panic message 
Switch from requesting bug reports to "cryptol-bugs@galois.com" to the github
issue tracker.
 2014-07-30 17:08:24 -07:00
Joey Dodds
00ad314681 added most of the test cases 2014-07-29 16:39:50 -07:00
Dylan McNamee
5faf927b3e Initial (incomplete, but mostly working) version of ChaChaPoly IETF draft. 
Original document: https://datatracker.ietf.org/doc/draft-irtf-cfrg-chacha20-poly1305/
 2014-07-29 09:32:14 -07:00
Adam C. Foltzer
09974fbc64 add makefile target for cryptolnb executable 2014-07-29 09:02:22 -07:00
Adam C. Foltzer
ab39a74c98 fix #67 
The python side of the notebook needed to be updated to expect a
.cabal-sandbox rather than cabal-dev sandbox. Also added a -fnotebook
flag to the cabal file to build the Haskell side of it.
 2014-07-29 08:53:44 -07:00
Brian Huffman
aa935996b9 Reimplement "logicUnary" so that complement works on infinite streams of bits 2014-07-28 12:08:15 -07:00
Brian Huffman
c8a80b4186 Remove more no-longer-necessary local additions to SBV 2014-07-23 10:25:59 -07:00
Brian Huffman
7e876be060 Remove additions to local fork of SBV that are no longer necessary 2014-07-23 10:10:54 -07:00
Brian Huffman
6bb2cd796d Unify Value datatypes for interpreter and symbolic simulator 
Some Value constructors and destructors are now polymorphic as well.
 2014-07-22 17:35:06 -07:00
Brian Huffman
ca53f226e5 Factor out separate type "BV" for words in evaluator's Value datatype 
Instead of constructor VWord Integer Integer, we use VWord BV,
where data BV = BV !Integer !Integer.
 2014-07-22 16:26:33 -07:00
Brian Huffman
c8abc76fd1 Remove unused length tag from interpreter tuple values 2014-07-22 15:43:29 -07:00
Brian Huffman
6a99eb99dd Modify symbolic Value type to match the interpreter's Value type 
This is a step towards unifying the two modules.
 2014-07-22 15:32:26 -07:00
Brian Huffman
907e4b55a9 Fix typo in comment 2014-07-22 15:16:00 -07:00
Brian Huffman
c5a14e388d Rewrite symbolic simulator in pure functional style 
We now take advantage of new features of SBV 3.1, including
the "sBranch" mechanism for evaluating reachability of conditional
branches.
 2014-07-22 13:44:17 -07:00
Brian Huffman
c2859d579b Update output for regression test 226 2014-07-21 16:18:47 -07:00
Brian Huffman
c8b3b8c134 Update output for regression test 086. 
(cf. revision 0ee396d434)
 2014-07-21 16:13:56 -07:00
Brian Huffman
ffebd5c330 Update output for regression test number 290 2014-07-21 16:02:38 -07:00
Brian Huffman
ec0395e9d0 Update regression test number 289, which now runs successfully. 
This test works as of revision db08bfafa9.

Versions of SBV prior to 3.1 did not distinguish the boolean type from
the size-1 bitvector type; this example uses literals like "0b0" and
"0b1", so it triggered the SBV bug, which manifested as a type error from
the external SMT solver.
 2014-07-21 16:01:43 -07:00
Brian Huffman
db08bfafa9 Merge changes from SBV release version 3.1 2014-07-21 15:23:34 -07:00
Brian Huffman
11d5c884b7 prove/sat commands avoid generating SBV bitvector variables of zero width 2014-07-21 14:59:33 -07:00
Brian Huffman
010d930638 Optimize symbolic "extract" to produce literal value if result has width 0 2014-07-21 11:28:40 -07:00
Brian Huffman
733c7932c5 Fix compiler warnings 2014-07-21 10:38:21 -07:00
Brian Huffman
ca14cff93a Pretty-print hex literals in parser AST using lowercase "abcdef". 
This makes the Cryptol.Parser.AST pretty printer consistent with the
one for values in Cryptol.Eval.Value.
 2014-07-15 16:43:20 -07:00
Brian Huffman
4f28f4bfed Update regression tests for :prove and :sat output 
As of ee8685e4f2, :sat and :prove now
parse and then pretty print the given predicate with appropriate
parenthesization.
 2014-07-15 16:26:37 -07:00
Brian Huffman
ee8685e4f2 REPL handles printing of :sat/prove results; parenthesize predicates as appropriate 2014-07-15 15:35:37 -07:00
Brian Huffman
f0ab651157 :sat and :prove print counterexamples in the user-configured number base 2014-07-15 14:32:14 -07:00
Thomas M. DuBuisson
97488c0cc1 Add an FNV-1a example (non-cryptographic hash). 2014-05-29 22:13:28 -07:00
Brian Huffman
62cdfd453f Cryptol REPL prints a hint if the user omits "=" on a ":set" command. 
Old behavior:
Cryptol> :set base 16
base 16 = 10

New behavior:
Cryptol> :set base 16
Unknown user option: `base 16`
Did you mean: `:set base = 16`?
 2014-05-27 15:46:42 -07:00
Brian Huffman
0ee396d434 Pretty printer for Cryptol.Parser.AST.Expr parenthesizes infix operators. 
(The printer for Cryptol.TypeCheck.AST.Expr already does this.)

Previously:
Cryptol> :t (+)
+ : {a} (Arith a) => a -> a -> a

Now:
Cryptol> :t (+)
(+) : {a} (Arith a) => a -> a -> a
 2014-05-15 14:41:22 -07:00
Brian Huffman
682c130b11 Add "fin" constraint on index size for (@), (!) and (!!), like (@@) has. 
Prior to this changeset, any of the following three expressions

[1,2,3] @ (zero : [inf])
[1,2,3] ! (zero : [inf])
[1,2,3] !! [zero : [inf]]

would produce the following error:

  Location:  [Eval] fromVWord
  Message:   not a word
             [False, False, False, False, False, ...]
 2014-05-13 13:38:55 -07:00
Brian Huffman
b304eb2ef0 New module Cryptol.TypeCheck.TypeOf has functions to compute Type of an Expr 2014-05-09 16:27:07 -07:00
Brian Huffman
a6077dd59a Add more destructor functions for TypeCheck.AST.Type 2014-05-09 16:26:31 -07:00
Trevor Elliott
28043c395c Only print Loading when the module is going to be loaded 
Looks like we were re-loading everything afterall!  This closes #10
 2014-05-06 14:32:17 -07:00
Trevor Elliott
25f17d0202 Some bug fixes related to fenced code in markdown 
``` as cryptol wasn't supported, and fenced code blocks that weren't
understood were having their internals processed as markdown
 2014-05-06 14:29:51 -07:00
Trevor Elliott
f1f1991ce0 No plans to allow indented code fence blocks 
Support for the indented blocks isn't consistent, so it seems easier to just
avoid trying to support this feature.
 2014-05-06 10:59:29 -07:00
Sergei Trofimovich
b713a8ac9f Setup.hs: unbreak 'runhaskell Setup configure' building mode 
Otherwise default hook won't generate src/GitRev.hs file.

Signed-off-by: Sergei Trofimovich <slyfox@gentoo.org>
 2014-05-02 15:28:11 +03:00
Dylan McNamee
87042d4604 fixing lone bad reference in doc, added syntax chapter, replaced Salsa spec 
PDF with pointer to it, fixed table in section 1.2.2
 2014-04-30 11:37:15 -07:00
Adam C. Foltzer
3919ebeab7 fix expected output for tests after fix in #10 2014-04-29 11:43:19 -07:00
Dylan McNamee
3188a212b5 Fixing a type constraint solver bug submitted by Jaak Randmets, 
verified by Iavor. Regression tests passed.
 2014-04-28 10:17:11 -07:00
Adam C. Foltzer
8ad498ca57 disable email notifications for travis 2014-04-27 21:54:18 -07:00
Adam C. Foltzer
924de3f152 install the Cabal library before starting the Travis build 2014-04-27 21:33:38 -07:00
Adam C. Foltzer
2b6642457b add travis.yml 2014-04-27 21:27:57 -07:00
Adam C. Foltzer
2cf71679c6 Merge branch 'master' into devel 2014-04-27 20:51:56 -07:00
Dylan McNamee
3e0ce32888 document that four failing tests is expected (for now) 2014-04-27 11:29:52 -07:00
Dylan McNamee
3e22966c1c spelling in README 2014-04-27 11:26:37 -07:00
Trevor Elliott
1dac36494a Only print Loading when the module is going to be loaded 
Looks like we were re-loading everything afterall!  This closes #10
 2014-04-25 11:15:08 -07:00
Dylan McNamee
62acc96f97 Fixing makefile to be compatible with David Lazar's speck fix 2014-04-24 18:07:47 -07:00
Dylan McNamee
203b2c8596 Merge branch 'master' of https://github.com/davidlazar/cryptol into davidlazar-master 2014-04-24 18:01:46 -07:00