Skip to content

Commit

Permalink
Bump What4 and Cryptol submodules.
Browse files Browse the repository at this point in the history
Add stub implementations of the new enumeration primitives
from GaloisInc/cryptol#1227, and fix up the type of `ecFromTo`,
which also changed slightly in that PR.
  • Loading branch information
robdockins committed Jul 21, 2021
1 parent 14c2f75 commit 61bf878
Show file tree
Hide file tree
Showing 4 changed files with 64 additions and 21 deletions.
39 changes: 33 additions & 6 deletions cryptol-saw-core/saw/Cryptol.sawcore
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 @@ -1349,17 +1348,17 @@ ecAt 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,34 @@ 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 first last stride a PLit =
error (seq (tcAdd (TCNum 1) (tcDiv (tcSub last first) stride)) a)
"TODO implement ecFromToBy";

ecFromToByLessThan :
(first bound stride : Num) -> (a : sort 0) -> PLiteralLessThan a ->
seq (tcCeilDiv (tcSub bound first) stride) a;
ecFromToByLessThan first bound stride a PLit =
error (seq (tcCeilDiv (tcSub bound first) stride) a)
"TODO implement ecFromToByLessThan";

ecFromToDownBy :
(first last stride : Num) -> (a : sort 0) -> PLiteral a ->
seq (tcAdd (TCNum 1) (tcDiv (tcSub first last) stride)) a;
ecFromToDownBy first last stride a PLit =
error (seq (tcAdd (TCNum 1) (tcDiv (tcSub first last) stride)) a)
"TODO implement ecFromToDownBy";

ecFromToDownByGreaterThan :
(first bound stride : Num) -> (a : sort 0) -> PLiteral a ->
seq (tcCeilDiv (tcSub first bound) stride) a;
ecFromToDownByGreaterThan first bound stride a PLit =
error (seq (tcCeilDiv (tcSub first bound) stride) a)
"TODO implement ecFromToDownByGreaterThan";

-- Infinite word sequences
ecInfFrom : (a : sort 0) -> PIntegral a -> a -> seq TCInf a;
ecInfFrom a pa x =
Expand Down
42 changes: 29 additions & 13 deletions cryptol-saw-core/src/Verifier/SAW/Cryptol.hs
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
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

0 comments on commit 61bf878

Please sign in to comment.