GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-12-17 21:11:35 +03:00
Code Issues Projects Releases Wiki Activity
1,376 Commits 67 Branches 28 Tags 95 MiB
d32f3324c9
Commit Graph

1376 Commits

This Branch
This Branch
All Branches
Author SHA1 Message Date
Rob Dockins
d32f3324c9 Update syntax reference with new fixity information for (||) and (&&) 2017-10-02 18:17:38 -07:00
Rob Dockins
e7d3ed02f9 Add testcase for issue #389. 
Recent improvements to the numeric solver have fixed this issue.

Fixes #389.
 2017-10-02 18:15:02 -07:00
Rob Dockins
42064dd9f2 Add testcase for issue #325. 2017-10-02 17:49:12 -07:00
Rob Dockins
37f9dc4c4f Add test for issue #78. 
Fixes #78.
 2017-10-02 15:48:51 -07:00
Rob Dockins
d5bfb1b648 Minor update to test suite 2017-10-02 15:40:46 -07:00
Rob Dockins
c0699e2d62 Change the fixity levels of (||) and (&&). 
This advances the next step in the plan described in issue #241.
 2017-10-02 14:56:33 -07:00
Rob Dockins
2894a1fdef Make solver startup/shutdown exception-safe. 2017-10-02 14:06:44 -07:00
Rob Dockins
12ac2c383a Revert "Remove the Data.Sequence-based representation of unpacked bitsequences." 
This may improve performace on some examples.
This reverts commit d4b70a039a.
 2017-10-02 11:12:50 -07:00
Brian Huffman
940b9c80ec Merge branch 'integer' 2017-09-29 14:23:28 -07:00
Brian Huffman
5e4d094eb3 Fix test output due to counterexample printing change. 2017-09-29 14:23:18 -07:00
Aaron Tomb
da1ff8f225 Merge pull request #454 from madnight/patch-1 
Update copyright notice year from 2016 to 2017
 2017-09-29 10:59:16 -07:00
Brian Huffman
3fb74f7f60 Make :check and :exhaust print counterexamples the same way :prove does. 
This addresses the first part of issue #449.
 2017-09-29 10:19:56 -07:00
Brian Huffman
7be06d803e Fix typo in error message. 2017-09-29 09:28:46 -07:00
Iavor S. Diatchki
75ca6b7fa2 Say something if name does not refer to anything 2017-09-28 15:47:23 -07:00
Iavor S. Diatchki
aa44dd7860 Add support for docstrings on type things 
See #456
 2017-09-28 14:39:22 -07:00
Brian Huffman
d9cbfd62d1 Add instance Zero Integer. 2017-09-28 13:26:01 -07:00
Brian Huffman
cce32a4868 Merge branch 'master' into integer 
This brings the Logic and Zero type classes into the integer branch.
 2017-09-28 13:18:27 -07:00
Fabian Beuke
ab75f152d1 Update copyright notice year from 2016 to 2017 2017-09-28 16:18:00 +02:00
Iavor Diatchki
208119fbbf Merge branch 'master' of github.com:GaloisInc/cryptol 2017-09-27 10:17:06 -07:00
Iavor Diatchki
6018af3537 Just documentation 2017-09-27 10:16:58 -07:00
brianhuffman
c32d68dade Merge pull request #445 from GaloisInc/logic-class 
Introduce a `Logic` class for bitwise logical operations
 2017-09-27 09:10:47 -07:00
Brian Huffman
1ed5640339 Merge branch 'master' into logic-class 
# Conflicts:
#	tests/mono-binds/test05.icry.stdout
 2017-09-26 16:50:53 -07:00
Iavor Diatchki
60523d5986 Delete old solver stuff. 
The main user visible effect of this might be that sometime things on
the Cryptol command line are instantiated in a slightly different way:
we get `inf` sometimes when we got a finite example before.

We could work around this if it is an issue, but I am not sure which
behavior is more reasonable.
 2017-09-26 14:02:52 -07:00
Brian Huffman
36f8fff3ca Support Integer type in reference evaluator (:eval). 2017-09-22 15:45:43 -07:00
Iavor Diatchki
0cc5151e6d Correct the handling of TCAnd in the SMT translation 2017-09-22 10:43:02 -07:00
Brian Huffman
1d71fa141c Merge branch 'master' into integer 2017-09-21 17:05:00 -07:00
Brian Huffman
d545abceec Fix incomplete pattern match warning caused by merge. 2017-09-21 16:47:36 -07:00
Brian Huffman
2c4157ecd4 Merge branch 'master' into logic-class 2017-09-21 16:44:39 -07:00
Brian Huffman
2ce1ca3eca Change constraint synonym syntax from "constraint" to "type constraint". 
For example:

type constraint NonZero n = (fin n, 1 <= n)

last : {n, a} NonZero n => [n]a -> a
last xs = xs!0
 2017-09-21 13:21:51 -07:00
Brian Huffman
393a11e170 Implement constraint synonyms (#373). 
The syntax is just as described in ticket #373: We have a new
declaration form consisting of the keyword 'constraint' followed
by a identifier and optionally a list of type parameters; the
right-hand side is either a single constraint or a parenthesized,
comma-separated list of type constraints. For example:

constraint NonZero n = (fin n, 1 <= n)

last : {n, a} NonZero n => [n]a -> a
last xs = xs!0
 2017-09-21 09:40:22 -07:00
Brian Huffman
c4af07a053 Remove unused TokenKW constructors. 2017-09-20 11:38:36 -07:00
Brian Huffman
b4cf793e7f Adapt fastSchemaOf function to avoid simplifying when instantiating props. 
Previously, checking the type of e.g. "(&&) `{[2]b}" would not return
"(Logic [2]b) => [2]b -> [2]b -> [2]b" as expected, but
"Logic b => [2]b -> [2]b -> [2]b". This made it impossible to reconstruct
the instances necessary to produce the required Logic dictionary when
translating to saw-core.
 2017-09-18 15:54:35 -07:00
Brian Huffman
c6db409837 Add type-matching functions pIsZero and pIsLogic. 2017-09-15 21:50:21 -07:00
Brian Huffman
35423d0243 Update test output. 2017-09-15 16:38:03 -07:00
Brian Huffman
b03f1ae0c2 Add class Zero with zero :: {a} (Zero a) => a. 
Shift operators also have a `Zero` constraint on the element type.
 2017-09-15 16:37:44 -07:00
Brian Huffman
860060c085 Fix test output. 2017-09-15 14:05:27 -07:00
Brian Huffman
a52510e56b Add 'Logic' class constraints to Cryptol::Extras 2017-09-15 13:38:43 -07:00
Brian Huffman
d1305b2860 Add 'Logic' typeclass with operations complement, &&, ||, ^, zero. 
Left and right shift operations also gain a Logic constraint,
since they shift in zero values.
 2017-09-15 13:33:56 -07:00
Brian Huffman
571d186c6c Support toInteger/fromInteger with symbolic arguments in :prove/:sat. 2017-09-14 17:51:03 -07:00
Brian Huffman
5332d98261 Fix test output 2017-09-13 17:04:52 -07:00
Aaron Tomb
c05281d390 Fix spurious failures due to lazy I/O 
Regression test check31 was failing somewhat unpredictably due to the
use of lazy I/O when loading the Z3 prelude for the type checker. Using
the `strict` package seems to fix it.
 2017-09-13 15:31:43 -07:00
Brian Huffman
5d73b5d405 Merge branch 'master' into integer 
This involved plenty of non-trivial merge edits to fix compilation errors.

# Conflicts:
#	src/Cryptol/Eval.hs
#	src/Cryptol/Eval/Value.hs
#	src/Cryptol/Prims/Eval.hs
#	src/Cryptol/Symbolic/Prims.hs
#	src/Cryptol/Symbolic/Value.hs
#	src/Cryptol/TypeCheck/AST.hs
 2017-09-13 14:28:04 -07:00
Eric Mertens
28bc4f81de Work around happy bug by adding type signature on ipat 2017-09-11 10:36:59 -07:00
Eric Mertens
bf571569fa Add upper bound on happy 
A bug introduced in happy-1.19.6 causes incorrect type signatures
to be generated in the parser source file which lead to type
checker errors
 2017-09-11 10:20:22 -07:00
robdockins
bbcd39d400 Merge pull request #439 from GaloisInc/signed-arith 
Add operations for signed arithmetic, and carry condition testing.
 2017-08-17 10:27:18 -07:00
Robert Dockins
8333b81c16 Update CryptolPrims documentation 2017-08-16 18:26:40 -07:00
Robert Dockins
9550d1b8dd Update syntax documentation 2017-08-16 18:22:49 -07:00
Robert Dockins
ef047d3a19 Fix test breakage due to new operations in the Cryptol prelude. 2017-08-16 17:37:24 -07:00
Robert Dockins
cefc67a149 Implement signed division and remainder as methods of the Arith class. 
Clarify the documentation that division is "round toward 0" division.
 2017-08-16 17:34:22 -07:00
Robert Dockins
6a30560fc0 Implement the nested lexicographic order for signed comparisons. 
This commit reorganizes how lexicographic comparisons are done in
the concrete simulator to reuse the same combinator from the symbolic
simulator.  This makes it more straightforward to implement the new
signed comparison.
 2017-08-16 13:58:44 -07:00