Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Explicit stride #1391

Merged
merged 3 commits into from
Jul 29, 2021
Merged

Explicit stride #1391

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
9300efc
Bump What4 and Cryptol submodules.
robdockins Jul 21, 2021
19c75e5
Provided saw-core implementations of the new enumeration primitives.
robdockins Jul 21, 2021
45fa137
whitespace: remove tabs
robdockins Jul 21, 2021
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
174 changes: 129 additions & 45 deletions cryptol-saw-core/saw/Cryptol.sawcore
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -128,7 +128,6 @@ tcDiv =
(\ (y:Nat) -> TCInf)
-- infinity / infinity = 1
(TCNum 1);

tcMod : Num -> Num -> Num;
tcMod =
binaryNumFun (\ (x:Nat) -> \ (y:Nat) -> modNat x y)
Expand Down Expand Up @@ -170,7 +169,7 @@ tcCeilDiv =

tcCeilMod : Num -> Num -> Num;
tcCeilMod =
binaryNumFun ceilModNat (\ (x:Nat) -> TCNum 0) (\ (y:Nat) -> TCInf) TCInf;
binaryNumFun ceilModNat (\ (x:Nat) -> TCNum 0) (\ (y:Nat) -> TCNum 0) TCInf;

tcLenFromThenTo_Nat : Nat -> Nat -> Nat -> Nat;
tcLenFromThenTo_Nat x y z =
Expand Down Expand Up @@ -848,9 +847,9 @@ PIntegral a =
, toInt : a -> Integer
, posNegCases :
(r : sort 0) ->
(Nat -> r) ->
(Nat -> r) ->
a -> r
(Nat -> r) ->
(Nat -> r) ->
a -> r
};

PIntegralInteger : PIntegral Integer;
Expand Down Expand Up @@ -879,7 +878,7 @@ PIntegralSeqBool n =
Num#rec (\ (n:Num) -> PIntegral (seq n Bool))
(\ (n:Nat) -> PIntegralWord n)
(error (PIntegral (Stream Bool)) "PIntegralSeqBool: no instance for streams")
n;
n;


-- Field class
Expand Down Expand Up @@ -928,12 +927,12 @@ PRound a =

PRoundRational : PRound Rational;
PRoundRational =
{ roundField = PFieldRational
, roundCmp = PCmpRational
, floor = \(x : Rational) -> error Integer "Unimplemented: floor Rational"
, ceiling = \(x : Rational) -> error Integer "Unimplemented: ceiling Rational"
, trunc = \(x : Rational) -> error Integer "Unimplemented: trunc Rational"
, roundAway = \(x : Rational) -> error Integer "Unimplemented: roundAway Rational"
{ roundField = PFieldRational
, roundCmp = PCmpRational
, floor = \(x : Rational) -> error Integer "Unimplemented: floor Rational"
, ceiling = \(x : Rational) -> error Integer "Unimplemented: ceiling Rational"
, trunc = \(x : Rational) -> error Integer "Unimplemented: trunc Rational"
, roundAway = \(x : Rational) -> error Integer "Unimplemented: roundAway Rational"
, roundToEven = \(x : Rational) -> error Integer "Unimplemented: roundToEven Rational"
};

Expand Down Expand Up @@ -986,8 +985,8 @@ ecFromZ : (n : Num) -> IntModNum n -> Integer;
ecFromZ n =
Num#rec (\ (n : Num) -> IntModNum n -> Integer)
fromIntMod
(\ (x : Integer) -> x)
n;
(\ (x : Integer) -> x)
n;

-- Ring
ecFromInteger : (a : sort 0) -> PRing a -> Integer -> a;
Expand Down Expand Up @@ -1131,15 +1130,15 @@ ecShiftL m =
-- Case for (TCNum m)
(\ (m:Nat) -> \ (ix:sort 0) -> \ (a:sort 0) -> \ (pix : PIntegral ix) -> \ (pz:PZero a) -> \ (xs:Vec m a) ->
pix.posNegCases (Vec m a)
(shiftL m a (ecZero a pz) xs)
(shiftR m a (ecZero a pz) xs))
(shiftL m a (ecZero a pz) xs)
(shiftR m a (ecZero a pz) xs))

-- Case for (infinity)
(\ (ix:sort 0) -> \ (a:sort 0) -> \ (pix : PIntegral ix) -> \ (pz:PZero a) ->
\ (xs:Stream a) ->
pix.posNegCases (Stream a)
(streamShiftL a xs)
(streamShiftR a pz xs))
(streamShiftL a xs)
(streamShiftR a pz xs))
m;

ecShiftR : (m : Num) -> (ix a : sort 0) -> PIntegral ix -> PZero a ->
Expand All @@ -1151,14 +1150,14 @@ ecShiftR m =
-- Case for (TCNum m)
(\ (m:Nat) -> \ (ix:sort 0) -> \ (a:sort 0) -> \ (pix : PIntegral ix) -> \ (pz:PZero a) -> \ (xs:Vec m a) ->
pix.posNegCases (Vec m a)
(shiftR m a (ecZero a pz) xs)
(shiftL m a (ecZero a pz) xs))
(shiftR m a (ecZero a pz) xs)
(shiftL m a (ecZero a pz) xs))

-- Case for (infinity)
(\ (ix:sort 0) -> \ (a:sort 0) -> \ (pix : PIntegral ix) -> \ (pz:PZero a) -> \ (xs:Stream a) ->
pix.posNegCases (Stream a)
(streamShiftR a pz xs)
(streamShiftL a xs))
(streamShiftR a pz xs)
(streamShiftL a xs))
m;

ecSShiftR : (n : Num) -> (ix : sort 0) -> PIntegral ix -> seq n Bool -> ix -> seq n Bool;
Expand All @@ -1172,8 +1171,8 @@ ecSShiftR =
(\ (xs : Vec 0 Bool) -> \ (_ : ix) -> xs)
(\ (w : Nat) -> \ (xs : Vec (Succ w) Bool) ->
pix.posNegCases (Vec (Succ w) Bool)
(bvSShr w xs)
(bvShl (Succ w) xs))
(bvSShr w xs)
(bvShl (Succ w) xs))
n));

ecRotL : (m : Num) -> (ix a : sort 0) -> PIntegral ix -> seq m a -> ix -> seq m a;
Expand All @@ -1183,7 +1182,7 @@ ecRotL =
(\ (m:Nat) -> \ (ix:sort 0) -> \ (a:sort 0) -> \ (pix:PIntegral ix) -> \ (xs:Vec m a) ->
pix.posNegCases (Vec m a)
(rotateL m a xs)
(rotateR m a xs));
(rotateR m a xs));

ecRotR : (m : Num) -> (ix a : sort 0) -> PIntegral ix -> seq m a -> ix -> seq m a;
ecRotR =
Expand All @@ -1192,7 +1191,7 @@ ecRotR =
(\ (m:Nat) -> \ (ix:sort 0) -> \ (a:sort 0) -> \ (pix:PIntegral ix) -> \ (xs:Vec m a) ->
pix.posNegCases (Vec m a)
(rotateR m a xs)
(rotateL m a xs));
(rotateL m a xs));

ecCat : (m n : Num) -> (a : sort 0) -> seq m a -> seq n a -> seq (tcAdd m n) a;
ecCat =
Expand Down Expand Up @@ -1224,9 +1223,9 @@ ecTake =
(Num_rec
(\ (n:Num) -> (a:sort 0) -> seq (tcAdd TCInf n) a -> Stream a)
-- The case (TCInf, TCNum n)
(\ (n:Nat) -> \ (a:sort 0) -> \ (xs:Stream a) -> xs)
-- The case (TCInf, TCInf)
(\ (a:sort 0) -> \ (xs:Stream a) -> xs));
(\ (n:Nat) -> \ (a:sort 0) -> \ (xs:Stream a) -> xs)
-- The case (TCInf, TCInf)
(\ (a:sort 0) -> \ (xs:Stream a) -> xs));

ecDrop : (m n : Num) -> (a : sort 0) -> seq (tcAdd m n) a -> seq n a;
ecDrop =
Expand Down Expand Up @@ -1336,30 +1335,30 @@ ecAt n =
(\ (n:Num) -> (a ix: sort 0) -> PIntegral ix -> seq n a -> ix -> a)
(\ (n:Nat) -> \ (a:sort 0) -> \ (ix:sort 0) -> \ (pix:PIntegral ix) -> \ (xs:Vec n a) ->
pix.posNegCases a
(at n a xs)
(\ (_:Nat) -> at n a xs 0))
-- (error (Nat -> a) "ecAt : negative index"))
(at n a xs)
(\ (_:Nat) -> at n a xs 0))
-- (error (Nat -> a) "ecAt : negative index"))
(\ (a:sort 0) -> \ (ix:sort 0) -> \ (pix:PIntegral ix) -> \ (xs:Stream a) ->
pix.posNegCases a
(streamGet a xs)
(\ (_:Nat) -> streamGet a xs 0))
-- (error (Nat -> a) "ecAt : negative index"))
(streamGet a xs)
(\ (_:Nat) -> streamGet a xs 0))
-- (error (Nat -> a) "ecAt : negative index"))
n;

ecAtBack : (n : Num) -> (a ix : sort 0) -> PIntegral ix -> seq n a -> ix -> a;
ecAtBack n a ix pix xs = ecAt n a ix pix (ecReverse n a xs);

ecFromTo : (first last : Num) -> (a : sort 0) -> PLiteral a -> PLiteral a ->
ecFromTo : (first last : Num) -> (a : sort 0) -> PLiteral a ->
seq (tcAdd (TCNum 1) (tcSub last first)) a;
ecFromTo =
finNumRec
(\ (first:Num) -> (last:Num) -> (a : sort 0) -> PLiteral a -> PLiteral a ->
(\ (first:Num) -> (last:Num) -> (a : sort 0) -> PLiteral a ->
seq (tcAdd (TCNum 1) (tcSub last first)) a)
(\ (first:Nat) ->
finNumRec
(\ (last:Num) -> (a : sort 0) -> PLiteral a -> PLiteral a ->
(\ (last:Num) -> (a : sort 0) -> PLiteral a ->
seq (tcAdd (TCNum 1) (tcSub last (TCNum first))) a)
(\ (last:Nat) -> \ (a : sort 0) -> \ (pa : PLiteral a) -> \ (_ : PLiteral a) ->
(\ (last:Nat) -> \ (a : sort 0) -> \ (pa : PLiteral a) ->
gen (addNat 1 (subNat last first)) a
(\ (i : Nat) -> pa (addNat i first))));

Expand Down Expand Up @@ -1394,6 +1393,91 @@ ecFromThenTo first next _ a =
(mulNat i (getFinNat next)))
(mulNat i (getFinNat first)))));

ecFromToBy :
(first last stride : Num) -> (a : sort 0) -> PLiteral a ->
seq (tcAdd (TCNum 1) (tcDiv (tcSub last first) stride)) a;
ecFromToBy =
finNumRec
(\ (first:Num) -> (last:Num) -> (stride : Num) -> (a : sort 0) -> PLiteral a ->
seq (tcAdd (TCNum 1) (tcDiv (tcSub last first) stride)) a)
(\ (first:Nat) ->
finNumRec
(\ (last:Num) -> (stride : Num) -> (a : sort 0) -> PLiteral a ->
seq (tcAdd (TCNum 1) (tcDiv (tcSub last (TCNum first)) stride)) a)
(\ (last:Nat) ->
finNumRec
(\ (stride:Num) -> (a : sort 0) -> PLiteral a ->
seq (tcAdd (TCNum 1) (tcDiv (TCNum (subNat last first)) stride)) a)
(\ (stride:Nat) -> \ (a : sort 0) -> \ (pa : PLiteral a) ->
gen (addNat 1 (divNat (subNat last first) stride)) a
(\ (i : Nat) -> pa (addNat first (mulNat i stride))))));

ecFromToByLessThan :
(first bound stride : Num) -> (a : sort 0) -> PLiteralLessThan a ->
seq (tcCeilDiv (tcSub bound first) stride) a;
ecFromToByLessThan =
finNumRec
(\ (first:Num) -> (bound:Num) -> (stride:Num) -> (a : sort 0) -> PLiteralLessThan a ->
seq (tcCeilDiv (tcSub bound first) stride) a)
(\ (first:Nat) ->
Num_rec
(\ (bound:Num) -> (stride:Num) -> (a : sort 0) -> PLiteralLessThan a ->
seq (tcCeilDiv (tcSub bound (TCNum first)) stride) a)

-- bound is finite case
(\ (bound:Nat) ->
finNumRec
(\ (stride:Num) -> (a : sort 0) -> PLiteralLessThan a ->
seq (tcCeilDiv (TCNum (subNat bound first)) stride) a)
(\ (stride:Nat) -> \ (a:sort 0) -> \ (pa:PLiteralLessThan a) ->
gen (ceilDivNat (subNat bound first) stride) a
(\ (i:Nat) -> pa (addNat first (mulNat i stride)))))

-- bound is infinite case
(finNumRec
(\ (stride:Num) -> (a : sort 0) -> PLiteralLessThan a ->
seq (tcCeilDiv TCInf stride) a)
(\ (stride:Nat) -> \ (a : sort 0) -> \ (pa:PLiteralLessThan a) ->
MkStream a (\ (i:Nat) -> pa (addNat first (mulNat i stride))))));

ecFromToDownBy :
(first last stride : Num) -> (a : sort 0) -> PLiteral a ->
seq (tcAdd (TCNum 1) (tcDiv (tcSub first last) stride)) a;
ecFromToDownBy =
finNumRec
(\ (first:Num) -> (last:Num) -> (stride:Num) -> (a : sort 0) -> PLiteral a ->
seq (tcAdd (TCNum 1) (tcDiv (tcSub first last) stride)) a)
(\ (first:Nat) ->
finNumRec
(\ (last:Num) -> (stride:Num) -> (a : sort 0) -> PLiteral a ->
seq (tcAdd (TCNum 1) (tcDiv (tcSub (TCNum first) last) stride)) a)
(\ (last:Nat) ->
finNumRec
(\ (stride:Num) -> (a : sort 0) -> PLiteral a ->
seq (tcAdd (TCNum 1) (tcDiv (TCNum (subNat first last)) stride)) a)
(\ (stride:Nat) -> \ (a : sort 0) -> \ (pa : PLiteral a) ->
gen (addNat 1 (divNat (subNat first last) stride)) a
(\ (i:Nat) -> pa (subNat first (mulNat i stride))))));

ecFromToDownByGreaterThan :
(first bound stride : Num) -> (a : sort 0) -> PLiteral a ->
seq (tcCeilDiv (tcSub first bound) stride) a;
ecFromToDownByGreaterThan =
finNumRec
(\ (first:Num) -> (bound:Num) -> (stride:Num) -> (a : sort 0) -> PLiteral a ->
seq (tcCeilDiv (tcSub first bound) stride) a)
(\ (first:Nat) ->
finNumRec
(\ (bound:Num) -> (stride:Num) -> (a : sort 0) -> PLiteral a ->
seq (tcCeilDiv (tcSub (TCNum first) bound) stride) a)
(\ (bound:Nat) ->
finNumRec
(\ (stride:Num) -> (a : sort 0) -> PLiteral a ->
seq (tcCeilDiv (TCNum (subNat first bound)) stride) a)
(\ (stride:Nat) -> \ (a : sort 0) -> \ (pa:PLiteral a) ->
gen (ceilDivNat (subNat first bound) stride) a
(\ (i:Nat) -> pa (subNat first (mulNat i stride))))));

-- Infinite word sequences
ecInfFrom : (a : sort 0) -> PIntegral a -> a -> seq TCInf a;
ecInfFrom a pa x =
Expand Down Expand Up @@ -1582,13 +1666,13 @@ ecUpdate n =
-- Case for (TCNum n, TCNum w)
pix.posNegCases (a -> Vec n a)
(upd n a xs)
(\ (_:Nat) -> \ (_:a) -> xs))
-- (error (Nat -> a -> Vec n a) "ecUpdate: negative index"))
(\ (_:Nat) -> \ (_:a) -> xs))
-- (error (Nat -> a -> Vec n a) "ecUpdate: negative index"))
(\ (a:sort 0) -> \ (ix:sort 0) -> \ (pix:PIntegral ix) -> \ (xs : Stream a) ->
pix.posNegCases (a -> Stream a)
(streamUpd a xs)
(\ (_:Nat) -> \ (_:a) -> xs))
--(error (Nat -> a -> Stream a) "ecUpdate: negative index"))
(\ (_:Nat) -> \ (_:a) -> xs))
--(error (Nat -> a -> Stream a) "ecUpdate: negative index"))
n;


Expand All @@ -1599,8 +1683,8 @@ ecUpdateEnd =
(\ (n:Nat) -> \ (a:sort 0) -> \ (ix:sort 0) -> \ (pix:PIntegral ix) -> \ (xs:Vec n a) ->
pix.posNegCases (a -> Vec n a)
(\ (i:Nat) -> upd n a xs (subNat (subNat n 1) i))
(\ (_:Nat) -> \ (_:a) -> xs));
-- (error (Nat -> a -> Vec n a) "ecUpdateEnd: negative index"));
(\ (_:Nat) -> \ (_:a) -> xs));
-- (error (Nat -> a -> Vec n a) "ecUpdateEnd: negative index"));


-- Bitvector truncation
Expand Down
42 changes: 29 additions & 13 deletions cryptol-saw-core/src/Verifier/SAW/Cryptol.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -759,21 +759,37 @@ prelPrims =

-- -- Enumerations
, ("fromTo", flip scGlobalDef "Cryptol.ecFromTo")
-- -- fromTo : {first, last, bits, a}
-- -- ( fin last, fin bits, last >== first,
-- -- Literal first a, Literal last a)
-- -- => [1 + (last - first)]a
-- fromTo : {first, last, bits, a}
-- ( fin last, fin bits, last >== first,
-- Literal first a, Literal last a)
-- => [1 + (last - first)]a
, ("fromToLessThan", flip scGlobalDef "Cryptol.ecFromToLessThan")
-- -- fromToLessThan : {first, bound, a}
-- -- ( fin first, bound >= first,
-- -- LiteralLessThan bound a)
-- -- => [bound - first]a
-- fromToLessThan : {first, bound, a}
-- ( fin first, bound >= first,
-- LiteralLessThan bound a)
-- => [bound - first]a
, ("fromThenTo", flip scGlobalDef "Cryptol.ecFromThenTo")
-- -- fromThenTo : {first, next, last, a, len}
-- -- ( fin first, fin next, fin last
-- -- , Literal first a, Literal next a, Literal last a
-- -- , first != next
-- -- , lengthFromThenTo first next last == len) => [len]a
-- fromThenTo : {first, next, last, a, len}
-- ( fin first, fin next, fin last
-- , Literal first a, Literal next a, Literal last a
-- , first != next
-- , lengthFromThenTo first next last == len) => [len]a
, ("fromToBy", flip scGlobalDef "Cryptol.ecFromToBy")
-- fromToBy : {first, last, stride, a}
-- (fin last, fin stride, stride >= 1, last >= first, Literal last a) =>
-- [1 + (last - first)/stride]a
, ("fromToByLessThan", flip scGlobalDef "Cryptol.ecFromToByLessThan")
-- fromToByLessThan : {first, bound, stride, a}
-- (fin first, fin stride, stride >= 1, bound >= first, LiteralLessThan bound a) =>
-- [(bound - first)/^stride]a
, ("fromToDownBy", flip scGlobalDef "Cryptol.ecFromToDownBy")
-- fromToDownBy : {first, last, stride, a}
-- (fin first, fin stride, stride >= 1, first >= last, Literal first a) =>
-- [1 + (first - last)/stride]a
, ("fromToDownByGreaterThan", flip scGlobalDef "Cryptol.ecFromToDownByGreaterThan")
-- fromToDownByGreaterThan : {first, bound, stride, a}
-- (fin first, fin stride, stride >= 1, first >= bound, Literal first a) =>
-- [(first - bound)/^stride]a

-- Evaluation primitives: deepseq, parmap
, ("deepseq", flip scGlobalDef "Cryptol.ecDeepseq") -- {a, b} (Eq b) => a -> b -> b
Expand Down
2 changes: 1 addition & 1 deletion deps/cryptol
Open in desktop
Submodule cryptol updated 79 files
+3 −2 .github/ci.sh
+13 −9 .github/workflows/ci.yml
+30 −0 .gitpod.Dockerfile
+39 −0 .gitpod.yml
+11 −1 CHANGES.md
+4 −3 Dockerfile
+2 −0 README.md
+2 −0 cabal.GHC-8.10.2.config
+1 −1 cabal.GHC-8.10.3.config
+1 −1 cabal.GHC-8.6.5.config
+1 −1 cabal.GHC-8.8.4.config
+5 −0 cry
+9 −3 cryptol-remote-api/CHANGELOG.md
+14 −7 cryptol-remote-api/Dockerfile
+16 −6 cryptol-remote-api/cryptol-remote-api.cabal
+23 −15 cryptol-remote-api/docs/Cryptol.rst
+6 −0 cryptol-remote-api/python/CHANGELOG.md
+9 −6 cryptol-remote-api/python/cryptol/commands.py
+9 −3 cryptol-remote-api/python/cryptol/connection.py
+30 −2 cryptol-remote-api/python/cryptol/solver.py
+9 −9 cryptol-remote-api/python/poetry.lock
+2 −2 cryptol-remote-api/python/pyproject.toml
+1 −1 cryptol-remote-api/python/tests/cryptol/test_AES.py
+1 −1 cryptol-remote-api/python/tests/cryptol/test_CplxQNewtype.py
+5 −5 cryptol-remote-api/python/tests/cryptol/test_DES.py
+1 −1 cryptol-remote-api/python/tests/cryptol/test_EvenMansour.py
+1 −1 cryptol-remote-api/python/tests/cryptol/test_SHA256.py
+1 −1 cryptol-remote-api/python/tests/cryptol/test_basics.py
+71 −4 cryptol-remote-api/python/tests/cryptol/test_cryptol_api.py
+1 −1 cryptol-remote-api/python/tests/cryptol/test_low_level_ops.py
+176 −67 cryptol-remote-api/src/CryptolServer/Sat.hs
+3 −1 cryptol-remote-api/test-cryptol-remote-api.py
+10 −8 cryptol-remote-api/test_docker.sh
+7 −0 cryptol-remote-api/update_docs.sh
+1 −1 cryptol.cabal
+4 −10 cryptol/Main.hs
+1 −1 deps/argo
+2 −2 docs/ProgrammingCryptol/crashCourse/CrashCourse.tex
+63 −13 lib/Cryptol.cry
+10 −6 lib/CryptolTC.z3
+83 −17 src/Cryptol/Eval/Generic.hs
+19 −0 src/Cryptol/ModuleSystem/Renamer.hs
+13 −2 src/Cryptol/Parser.y
+17 −0 src/Cryptol/Parser/AST.hs
+6 −0 src/Cryptol/Parser/Lexer.x
+4 −0 src/Cryptol/Parser/Names.hs
+2 −0 src/Cryptol/Parser/NoPat.hs
+37 −0 src/Cryptol/Parser/ParserUtils.hs
+4 −1 src/Cryptol/Parser/Token.hs
+6 −2 src/Cryptol/REPL/Command.hs
+38 −1 src/Cryptol/REPL/Monad.hs
+20 −0 src/Cryptol/Symbolic.hs
+254 −85 src/Cryptol/Symbolic/What4.hs
+54 −0 src/Cryptol/TypeCheck/Infer.hs
+0 −2 src/Cryptol/TypeCheck/SimpType.hs
+9 −10 src/Cryptol/TypeCheck/Solver/InfNat.hs
+2 −2 src/Cryptol/TypeCheck/Solver/Numeric/Fin.hs
+4 −4 tests/issues/T146.icry.stdout
+2 −0 tests/issues/issue072.icry.stdout
+6 −6 tests/issues/issue1024.icry.stdout
+1 −1 tests/issues/issue103.icry.stdout
+15 −0 tests/issues/issue1210.cry
+6 −0 tests/issues/issue1210.icry
+31 −0 tests/issues/issue1210.icry.stdout
+4 −4 tests/issues/issue138.cry
+2 −2 tests/issues/issue138.icry
+17 −2 tests/issues/issue226.icry.stdout
+2 −2 tests/issues/issue290v2.icry.stdout
+2 −22 tests/issues/issue582.icry.stdout
+2 −2 tests/issues/issue723.icry.stdout
+1 −1 tests/modsys/T16.icry.stdout
+1 −1 tests/modsys/T16.icry.stdout.mingw32
+3 −0 tests/regression/allsat.cry
+9 −0 tests/regression/allsat.icry
+7 −0 tests/regression/allsat.icry.stdout
+12 −0 tests/regression/explicit-strides.icry
+30 −0 tests/regression/explicit-strides.icry.stdout
+1 −1 tests/regression/safety.icry.stdout
+4 −4 tests/regression/tc-errors.icry.stdout
2 changes: 1 addition & 1 deletion deps/what4
Open in desktop
Submodule what4 updated 34 files
+13 −3 .github/workflows/test.yml
+1 −1 dependencies/aig
+1 −1 dependencies/language-sally
+1 −1 what4-abc/what4-abc.cabal
+1 −1 what4-blt/what4-blt.cabal
+2 −2 what4-transition-system/what4-transition-system.cabal
+61 −2 what4/CHANGES.md
+25 −0 what4/doc/implementation.md
+3 −3 what4/src/What4/Config.hs
+1,323 −1,328 what4/src/What4/Expr/App.hs
+0 −2 what4/src/What4/Expr/Builder.hs
+32 −9 what4/src/What4/Interface.hs
+102 −19 what4/src/What4/Protocol/Online.hs
+7 −4 what4/src/What4/Protocol/SMTLib2.hs
+20 −9 what4/src/What4/Protocol/SMTLib2/Response.hs
+6 −5 what4/src/What4/Protocol/SMTWriter.hs
+22 −16 what4/src/What4/SWord.hs
+2 −0 what4/src/What4/Solver.hs
+18 −3 what4/src/What4/Solver/Boolector.hs
+3 −4 what4/src/What4/Solver/CVC4.hs
+18 −4 what4/src/What4/Solver/STP.hs
+32 −12 what4/src/What4/Solver/Yices.hs
+3 −4 what4/src/What4/Solver/Z3.hs
+19 −2 what4/src/What4/Utils/AbstractDomains.hs
+2 −1 what4/src/What4/Utils/Process.hs
+36 −17 what4/src/What4/Utils/StringLiteral.hs
+49 −22 what4/test/AdapterTest.hs
+141 −88 what4/test/ExprBuilderSMTLib2.hs
+310 −63 what4/test/OnlineSolverTest.hs
+1 −1 what4/test/TestTemplate.hs
+1 −9 what4/test/responses/err-behav-unrec.exp
+1 −8 what4/test/responses/minisat_verbose_success.strict.exp
+1 −9 what4/test/responses/rsnunk-bad.exp
+22 −4 what4/what4.cabal