GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-12-17 04:44:39 +03:00
Code Issues Projects Releases Wiki Activity
200 Commits 68 Branches 28 Tags 95 MiB
99c3547a08
Commit Graph

200 Commits

This Branch
This Branch
All Branches
Author SHA1 Message Date
Adam C. Foltzer
156771a5d5 bind counterexamples and satisfying assignments to it 
If the solver returns values for :sat or :prove, we now bind them at
the repl to `it`. If more than one argument is part of the cex/sat
answer, we tuple up/uncurry the arguments.
 2014-08-18 19:19:22 -07:00
Adam C. Foltzer
cf1774bbbc change repl syntax to be more like ghci 
Since :let was clashing with :load for :l, and for consistency with
ghci, you can now enter bare let expressions at the repl:

> let x = 5

Also, the grammar for the repl parser disallows type bindings, which
were possible in the previous :let.

Semicolons no longer needed, though we can only bind one thing at a
time.
 2014-08-18 19:17:27 -07:00
Adam C. Foltzer
33f9012cda restricted grammar of :let commands 
For now, you can only enter one binding at a time at the REPL, and can
only enter expression bindings rather than type signatures or type
synonyms. It wouldn't be too hard to add type synonyms, but the value
is questionable.
 2014-08-18 14:48:44 -07:00
Adam C. Foltzer
62f38192e9 added it to the REPL 2014-08-18 14:14:37 -07:00
Adam C. Foltzer
1dedf6d693 refactor dynamic environment into ModuleEnv 
This just makes for a more consistent API; the "dynamic" environment
as extended by REPL commands is now part of the ModuleEnv. It's
actually more general than just for the REPL. We can use it in general
to add bindings on top of a loaded module context.
 2014-08-18 13:28:21 -07:00
Brian Huffman
fdaff29e9d Support for loading multiple source files simultaneously 
- track source filepath for each loaded module
- raise error when different loaded files use same module name
 2014-08-15 16:18:14 -07:00
Adam C. Foltzer
b2e83f8e27 getVars processes interactively-bound names better 
This change fixes the issue where `getVars` in the REPL would return
names with the `#Uniq_...` prefix. This was confusing, and also
messing up tab-completion.
 2014-08-14 17:06:00 -07:00
Adam C. Foltzer
f125947117 additional support for let-bound variables at the repl 
Let-bound identifiers now show up in `:browse`, get unloaded whenever
we load a new module context, and can be sent to `:sat` and `:prove`.
 2014-08-14 16:31:47 -07:00
Adam C. Foltzer
bed85a6b78 initial :let implementation 
This works by adding an extended environment to some of the
ModuleSystem functions. This extended environment contains
declarations entered interactively, a naming environment that maps
parsed names to the unique names we use to ensure lexical scope, and
an evaluation environment containing the values of the let-bound
expressions.
 2014-08-14 13:14:22 -07:00
Adam C. Foltzer
2b1380beed Add extended environment, support for typechecking and evaluating decls 
This is a checkpoint; it builds but doesn't yet work correctly!
 2014-08-13 17:51:17 -07:00
Sam Anklesaria
bede37a436 Merge branch 'newsbv' 2014-08-07 10:57:10 -07:00
Sam Anklesaria
8e54775642 exposing low level uninterpreted interface 2014-08-07 10:54:40 -07:00
Sam Anklesaria
5fca89f8b1 Revert "mkUninterpret function added to sbv Model" 
This reverts commit b73620a63b.
 2014-08-06 10:25:20 -07:00
Joey Dodds
d3d714018a Merge branch 'master' of https://github.com/GaloisInc/cryptol 2014-08-06 10:17:39 -07:00
Joey Dodds
7300f29606 changed collision properties to require inputs to be different 2014-08-06 10:16:14 -07:00
Sam Anklesaria
b73620a63b mkUninterpret function added to sbv Model 2014-08-06 10:14:53 -07:00
Aaron Tomb
abe336d907 Added SignCast instance and exported sbv 
Changes necessary for SAWCore's use of SBV. Ultimately, these should be
merged into the upstream SBV package.
 2014-08-06 09:49:19 -07:00
Joey Dodds
72fefff367 added malicious sha example 2014-08-05 14:08:30 -07:00
Sam Anklesaria
739adffb67 added SignCast instance and exported sbv 2014-08-04 23:39:47 -07:00
Joey Dodds
d248b50b40 finished test vectors 
created function AeadConstruction that is used to generate tags in
AEAD encryption and decryption
 2014-08-04 10:52:50 -07:00
Joey Dodds
2636a0ca9e Merge branch 'master' of https://github.com/GaloisInc/cryptol 2014-08-01 09:16:52 -07:00
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