From 514b71215fdf1c9f44225193d97db645172d5697 Mon Sep 17 00:00:00 2001
From: Brian Huffman <huffman@galois.com>
Date: Wed, 21 Feb 2018 15:04:59 -0800
Subject: [PATCH] Add sign extension operator to `cryptol_prims`.

---
 deps/cryptol-verifier     | 2 +-
 src/SAWScript/Builtins.hs | 1 +
 2 files changed, 2 insertions(+), 1 deletion(-)

diff --git a/deps/cryptol-verifier b/deps/cryptol-verifier
index 6869f1e074..0e4adb2054 160000
--- a/deps/cryptol-verifier
+++ b/deps/cryptol-verifier
@@ -1 +1 @@
-Subproject commit 6869f1e074eebef2d608b5359bd9f46737c24e6f
+Subproject commit 0e4adb2054f728a13d9d45ba12533e345f54104b
diff --git a/src/SAWScript/Builtins.hs b/src/SAWScript/Builtins.hs
index e6107cf8f4..72a082daea 100644
--- a/src/SAWScript/Builtins.hs
+++ b/src/SAWScript/Builtins.hs
@@ -1341,6 +1341,7 @@ cryptol_prims = CryptolModule Map.empty <$> Map.fromList <$> traverse parsePrim
     prims =
       [ ("trunc", "Cryptol.ecTrunc" , "{m, n} (fin m, fin n) => [m+n] -> [n]")
       , ("uext" , "Cryptol.ecUExt"  , "{m, n} (fin m, fin n) => [n] -> [m+n]")
+      , ("sext" , "Cryptol.ecSExt"  , "{m, n} (fin m, fin n, n >= 1) => [n] -> [m+n]")
       , ("sgt"  , "Cryptol.ecSgt"   , "{n} (fin n) => [n] -> [n] -> Bit")
       , ("sge"  , "Cryptol.ecSge"   , "{n} (fin n) => [n] -> [n] -> Bit")
       , ("slt"  , "Cryptol.ecSlt"   , "{n} (fin n) => [n] -> [n] -> Bit")