Merge pull request #1455 from GaloisInc/update-deps

Update submodule versions.
GaloisInc · Sep 15, 2021 · 55ca13b · 55ca13b
2 parents 33fdd18 + ee6629f
commit 55ca13b
Show file tree

Hide file tree

Showing 9 changed files with 15 additions and 7 deletions.
diff --git a/cryptol-saw-core/saw/Cryptol.sawcore b/cryptol-saw-core/saw/Cryptol.sawcore
@@ -1073,6 +1073,12 @@ ecSMod n =
     (error (Stream Bool -> Stream Bool -> Stream Bool) "ecSMod: expected finite word")
     n;
 
+toSignedInteger : (n : Num) -> seq n Bool -> Integer;
+toSignedInteger n =
+  Num#rec (\ (n:Num) -> seq n Bool -> Integer)
+    sbvToInt
+    (error (Stream Bool -> Integer) "toSignedInteger: expected finite word")
+    n;
 
 -- Eq
 ecEq : (a : sort 0) -> PEq a -> a -> a -> Bool;

diff --git a/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs b/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs
@@ -745,6 +745,8 @@ prelPrims =
   , ("%$",           flip scGlobalDef "Cryptol.ecSMod")        -- {n} (fin n, n>=1) => [n] -> [n] -> [n]
   , ("lg2",          flip scGlobalDef "Cryptol.ecLg2")         -- {n} (fin n) => [n] -> [n]
   , (">>$",          flip scGlobalDef "Cryptol.ecSShiftR")     -- {n, ix} (fin n, n >= 1, Integral ix) => [n] -> ix -> [n]
+  , ("toSignedInteger",
+                     flip scGlobalDef "Cryptol.toSignedInteger") -- {n} (fin n, n >= 1) => [n] -> Integer
 
     -- -- Rational primitives
   , ("ratio",        flip scGlobalDef "Cryptol.ecRatio")       -- Integer -> Integer -> Rational

diff --git a/deps/argo b/deps/argo
diff --git a/deps/crucible b/deps/crucible
diff --git a/deps/cryptol b/deps/cryptol
diff --git a/deps/cryptol-specs b/deps/cryptol-specs
diff --git a/deps/llvm-pretty b/deps/llvm-pretty
diff --git a/deps/parameterized-utils b/deps/parameterized-utils
diff --git a/deps/what4 b/deps/what4
+131 −31		argo/src/Argo.hs
+10 −0		python/CHANGELOG.md
+9 −3		python/argo_client/connection.py
+5 −3		python/argo_client/interaction.py
+1 −1		python/setup.py
+22 −0		python/tests/test_file_echo_api.py
+3 −3		python/tests/test_file_echo_interaction.py
+7 −0		crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics.hs
+31 −4		crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/LLVM.hs
+58 −0		crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Libc.hs
+22 −8		crucible-llvm/src/Lang/Crucible/LLVM/MemModel.hs
+3 −3		crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Common.hs
+3 −3		crucible-llvm/src/Lang/Crucible/LLVM/QQ.hs
+10 −0		crux-llvm/README.md
+41 −2		crux-llvm/src/Crux/LLVM/Config.hs
+1 −0		crux-llvm/src/Crux/LLVM/Overrides.hs
+92 −16		crux-llvm/src/Crux/LLVM/Simulate.hs
+5 −3		crux-llvm/svcomp/Main.hs
+4 −4		crux-llvm/svcomp/README.md
+3 −0		crux-llvm/svcomp/config-files/README.md
+26 −0		crux-llvm/svcomp/config-files/no-overflow.config
+1 −0		crux-llvm/svcomp/config-files/unreach-call.config
+22 −0		crux-llvm/svcomp/def-files/README.md
+86 −0		crux-llvm/svcomp/def-files/crux.py
+171 −0		crux-llvm/svcomp/def-files/crux.xml
+1 −1		crux-llvm/svcomp/mk-svcomp-bindist.sh
+7 −0		crux-llvm/test-data/golden/T812.c
+1 −0		crux-llvm/test-data/golden/T812.config
+1 −0		crux-llvm/test-data/golden/T812.good
+16 −0		crux-llvm/test-data/golden/T816.c
+2 −0		crux-llvm/test-data/golden/T816.good
+10 −0		crux-llvm/test-data/golden/T828.c
+1 −0		crux-llvm/test-data/golden/T828.config
+1 −0		crux-llvm/test-data/golden/T828.good
+5 −0		crux-llvm/test-data/golden/T838.c
+1 −0		crux-llvm/test-data/golden/T838.good
+17 −0		crux-llvm/test-data/golden/golden/T840.c.orig
+1 −0		crux-llvm/test-data/golden/golden/T840.good
+134 −0		crux-llvm/test-data/golden/golden/T840.ll
+1 −1		dependencies/llvm-pretty
+14 −15		uc-crux-llvm/README.md
+3 −3		uc-crux-llvm/src/UCCrux/LLVM/Classify.hs
+10 −9		uc-crux-llvm/src/UCCrux/LLVM/Constraints.hs
+7 −10		uc-crux-llvm/src/UCCrux/LLVM/Context/Function.hs
+69 −63		uc-crux-llvm/src/UCCrux/LLVM/Context/Module.hs
+4 −4		uc-crux-llvm/src/UCCrux/LLVM/Cursor.hs
+28 −9		uc-crux-llvm/src/UCCrux/LLVM/Equivalence.hs
+34 −0		uc-crux-llvm/src/UCCrux/LLVM/Equivalence/Config.hs
+37 −225		uc-crux-llvm/src/UCCrux/LLVM/FullType/Translation.hs
+20 −4		uc-crux-llvm/src/UCCrux/LLVM/FullType/Type.hs
+94 −56		uc-crux-llvm/src/UCCrux/LLVM/Main.hs
+119 −30		uc-crux-llvm/src/UCCrux/LLVM/Main/Config/FromEnv.hs
+39 −0		uc-crux-llvm/src/UCCrux/LLVM/Main/Config/Type.hs
+420 −0		uc-crux-llvm/src/UCCrux/LLVM/Module.hs
+22 −0		uc-crux-llvm/src/UCCrux/LLVM/Newtypes/FunctionName.hs
+28 −0		uc-crux-llvm/src/UCCrux/LLVM/Newtypes/Seconds.hs
+14 −13		uc-crux-llvm/src/UCCrux/LLVM/Overrides/Skip.hs
+65 −0		uc-crux-llvm/src/UCCrux/LLVM/Run/EntryPoints.hs
+45 −20		uc-crux-llvm/src/UCCrux/LLVM/Run/Explore.hs
+27 −0		uc-crux-llvm/src/UCCrux/LLVM/Run/Explore/Config.hs
+45 −36		uc-crux-llvm/src/UCCrux/LLVM/Run/Loop.hs
+4 −3		uc-crux-llvm/src/UCCrux/LLVM/Run/Simulate.hs
+4 −4		uc-crux-llvm/src/UCCrux/LLVM/Setup.hs
+44 −23		uc-crux-llvm/test/Test.hs
+9 −1		uc-crux-llvm/uc-crux-llvm.cabal
+4 −4		cryptol-remote-api/python/poetry.lock
+1 −1		cryptol-remote-api/python/tests/cryptol/test_CplxQNewtype.py
+2 −2		cryptol-remote-api/python/tests/cryptol/test_cryptol_api.py
+2 −2		cryptol-remote-api/python/tests/cryptol_eval/test_basics.py
+1 −1		deps/argo
+3 −3		docs/ProgrammingCryptol/crashCourse/CrashCourse.tex
+5 −0		lib/Cryptol.cry
+6 −0		src/Cryptol/Backend.hs
+1 −0		src/Cryptol/Backend/Concrete.hs
+1 −0		src/Cryptol/Backend/SBV.hs
+1 −0		src/Cryptol/Backend/What4.hs
+10 −0		src/Cryptol/Eval/Generic.hs
+8 −2		src/Cryptol/Utils/PP.hs
+4 −4		tests/issues/T146.icry.stdout
+6 −6		tests/issues/issue1024.icry.stdout
+1 −1		tests/issues/issue103.icry.stdout
+3 −2		tests/issues/issue226.icry.stdout
+6 −6		tests/issues/issue268.icry.stdout
+2 −2		tests/issues/issue290v2.icry.stdout
+4 −3		tests/issues/issue407.icry.stdout
+2 −2		tests/issues/issue723.icry.stdout
+2 −2		tests/issues/padding.icry.stdout
+1 −1		tests/modsys/T16.icry.stdout
+4 −4		tests/regression/rec-update.icry.stdout
+1 −1		tests/regression/safety.icry.stdout
+4 −4		tests/regression/sort.icry.stdout
+4 −4		tests/regression/tc-errors.icry.stdout
+5 −5		Primitive/Asymmetric/Signature/Dilithium/Round2/DilithiumRecommended.cry
+5 −5		Primitive/Asymmetric/Signature/Dilithium/Round2/DilithiumVeryhigh.cry
+5 −5		Primitive/Asymmetric/Signature/Dilithium/Round2/DilithiumWeak.cry
+8 −0		Primitive/Keyless/Hash/SHA3/SHA3.cry
+29 −0		Primitive/Keyless/Hash/SHA3/SHA3_224.cry
+21 −0		Primitive/Keyless/Hash/SHA3/SHA3_256.cry
+17 −0		Primitive/Keyless/Hash/SHA3/SHA3_384.cry
+21 −0		Primitive/Keyless/Hash/SHA3/SHA3_512.cry
+9 −0		Primitive/Keyless/Hash/SHAKE/SHAKE.cry
+19 −0		Primitive/Keyless/Hash/SHAKE/SHAKE128.cry
+16 −0		Primitive/Keyless/Hash/SHAKE/SHAKE256.cry
+0 −74		Primitive/Keyless/Hash/keccak.cry
+8 −0		Primitive/Keyless/Hash/utils.cry
+3 −0		.github/workflows/test.yml
+11 −0		Changelog.md
+1 −0		parameterized-utils.cabal
+48 −0		src/Data/Parameterized/Axiom.hs
+2 −1		src/Data/Parameterized/Context/Unsafe.hs
+3 −3		src/Data/Parameterized/Ctx/Proofs.hs
+13 −12		src/Data/Parameterized/NatRepr.hs
+3 −2		src/Data/Parameterized/NatRepr/Internal.hs
+2 −2		src/Data/Parameterized/Nonce.hs
+2 −1		src/Data/Parameterized/Nonce/Unsafe.hs
+6 −5		src/Data/Parameterized/Peano.hs
+2 −1		src/Data/Parameterized/SymbolRepr.hs
+13 −7		what4/src/What4/Concrete.hs
+9 −8		what4/src/What4/Interface.hs