From f2587604eca2e061282ecd89b94b84bde523f46e Mon Sep 17 00:00:00 2001
From: Brian Huffman <huffman@galois.com>
Date: Tue, 29 Sep 2020 16:40:33 -0700
Subject: [PATCH] Adapt to Literal instance for type Bit in
 GaloisInc/cryptol#914.

---
 cryptol-saw-core/saw/Cryptol.sawcore         | 3 +++
 cryptol-saw-core/src/Verifier/SAW/Cryptol.hs | 3 +++
 cryptol-saw-core/test/instance.cry           | 4 ++++
 3 files changed, 10 insertions(+)

diff --git a/cryptol-saw-core/saw/Cryptol.sawcore b/cryptol-saw-core/saw/Cryptol.sawcore
index 06937b83..4f50a9d5 100644
--- a/cryptol-saw-core/saw/Cryptol.sawcore
+++ b/cryptol-saw-core/saw/Cryptol.sawcore
@@ -936,6 +936,9 @@ PLiteralSeqBool n =
   Num#rec (\ (n : Num) -> PLiteral (seq n Bool)) bvNat
           (error (PLiteral (Stream Bool)) "PLiteralSeqBool: no instance for streams") n;
 
+PLiteralBit : PLiteral Bool;
+PLiteralBit = Nat_cases Bool False (\ (n:Nat) -> \ (b:Bool) -> True);
+
 PLiteralInteger : PLiteral Integer;
 PLiteralInteger = natToInt;
 
diff --git a/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs b/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs
index 929219e2..aa36d380 100644
--- a/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs
+++ b/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs
@@ -574,6 +574,9 @@ proveProp sc env prop =
         (C.pIsSignedCmp -> Just (C.tIsRec -> Just fm))
           -> do proveProp sc env (C.pSignedCmp (C.tTuple (map snd (C.canonicalFields fm))))
 
+        -- instance Literal val Bit
+        (C.pIsLiteral -> Just (_, C.tIsBit -> True))
+          -> do scGlobalApply sc "Cryptol.PLiteralBit" []
         -- instance Literal val Integer
         (C.pIsLiteral -> Just (_, C.tIsInteger -> True))
           -> do scGlobalApply sc "Cryptol.PLiteralInteger" []
diff --git a/cryptol-saw-core/test/instance.cry b/cryptol-saw-core/test/instance.cry
index 42a2f511..237c53f3 100644
--- a/cryptol-saw-core/test/instance.cry
+++ b/cryptol-saw-core/test/instance.cry
@@ -338,6 +338,10 @@ signedCmpRecord = (<$)
 ////////////////////////////////////////////////////////////////////////////////
 // Literal
 
+/* instance (1 >= val) => Literal val Bit */
+literalBit : {val} (1 >= val) => Bit
+literalBit = `val
+
 /* instance (fin val) => Literal val Integer */
 literalInteger : {val} (fin val) => Integer
 literalInteger = `val