From 6a70cdd97048ae0459314cf820567097d8cb1678 Mon Sep 17 00:00:00 2001
From: Brian Huffman <huffman@galois.com>
Date: Wed, 15 Sep 2021 06:23:26 -0700
Subject: [PATCH 1/2] Update submodule versions.

---
 deps/argo                | 2 +-
 deps/crucible            | 2 +-
 deps/cryptol             | 2 +-
 deps/cryptol-specs       | 2 +-
 deps/llvm-pretty         | 2 +-
 deps/parameterized-utils | 2 +-
 deps/what4               | 2 +-
 7 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/deps/argo b/deps/argo
index 101cad520f..72dc6f057d 160000
--- a/deps/argo
+++ b/deps/argo
@@ -1 +1 @@
-Subproject commit 101cad520fc353a8673f9ba9d71b70e2f9ec59d9
+Subproject commit 72dc6f057d609ddaee8d964c41984faaa97e4cf1
diff --git a/deps/crucible b/deps/crucible
index eebba271a5..59b1db2326 160000
--- a/deps/crucible
+++ b/deps/crucible
@@ -1 +1 @@
-Subproject commit eebba271a5571bf8c91e7049d8d5b4ad2e6c13f9
+Subproject commit 59b1db232641d7587563e86d56d4a78330baf28c
diff --git a/deps/cryptol b/deps/cryptol
index 0eea2cb7e9..5a668a4594 160000
--- a/deps/cryptol
+++ b/deps/cryptol
@@ -1 +1 @@
-Subproject commit 0eea2cb7e96dfaefb3237414233b9a7b1cc11696
+Subproject commit 5a668a4594e386a084f6f0ceb231c69946971a50
diff --git a/deps/cryptol-specs b/deps/cryptol-specs
index e8e3bde6f7..d15c5d0352 160000
--- a/deps/cryptol-specs
+++ b/deps/cryptol-specs
@@ -1 +1 @@
-Subproject commit e8e3bde6f7465b4a9207a4cf9deecade151af5a4
+Subproject commit d15c5d035266b6b68db44ff67a332885ff25be3d
diff --git a/deps/llvm-pretty b/deps/llvm-pretty
index 226e75264c..97fd46c51f 160000
--- a/deps/llvm-pretty
+++ b/deps/llvm-pretty
@@ -1 +1 @@
-Subproject commit 226e75264c7f5b40539fa792c99dcc2214b81c32
+Subproject commit 97fd46c51f59ba8aa836a00e04d59945b494a1d8
diff --git a/deps/parameterized-utils b/deps/parameterized-utils
index 13f367bc02..4b6562fdf3 160000
--- a/deps/parameterized-utils
+++ b/deps/parameterized-utils
@@ -1 +1 @@
-Subproject commit 13f367bc029de35f9ab4edec2bcd90bc638d30a7
+Subproject commit 4b6562fdf334849d63435442bbcd2a6d9bce34a7
diff --git a/deps/what4 b/deps/what4
index 95fd577a6b..26a47b8e11 160000
--- a/deps/what4
+++ b/deps/what4
@@ -1 +1 @@
-Subproject commit 95fd577a6b7e0d13158da97695c6b7750892f918
+Subproject commit 26a47b8e11031ff94b59b2d075086aef592a87d5

From ee6629ff1d5d1501fb74779dc5c2b5586ba7f305 Mon Sep 17 00:00:00 2001
From: Brian Huffman <huffman@galois.com>
Date: Wed, 15 Sep 2021 10:13:45 -0700
Subject: [PATCH 2/2] Update and adapt to GaloisInc/cryptol#1281
 "toSignedInteger".

---
 cryptol-saw-core/saw/Cryptol.sawcore         | 6 ++++++
 cryptol-saw-core/src/Verifier/SAW/Cryptol.hs | 2 ++
 deps/cryptol                                 | 2 +-
 3 files changed, 9 insertions(+), 1 deletion(-)

diff --git a/cryptol-saw-core/saw/Cryptol.sawcore b/cryptol-saw-core/saw/Cryptol.sawcore
index 3b244d890a..3b80d8306d 100644
--- 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
index 5e6a90a1e1..e4f5afa8c2 100644
--- 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/cryptol b/deps/cryptol
index 5a668a4594..cb240cdd31 160000
--- a/deps/cryptol
+++ b/deps/cryptol
@@ -1 +1 @@
-Subproject commit 5a668a4594e386a084f6f0ceb231c69946971a50
+Subproject commit cb240cdd31c864b298f181c0dac660e2f4e32aa5