Add sign extension operator to cryptol_prims.

GaloisInc · Feb 21, 2018 · 514b712 · 514b712
1 parent 2a65b90
commit 514b712
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 1 deletion.
diff --git a/deps/cryptol-verifier b/deps/cryptol-verifier
diff --git 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")