Merge pull request #73 from GaloisInc/update-cryptol

Adapt to Literal instance for type Bit in GaloisInc/cryptol#914.
GaloisInc · Sep 29, 2020 · 920a014 · 920a014
2 parents 15b35b4 + f258760
commit 920a014
Show file tree

Hide file tree

Showing 3 changed files with 10 additions and 0 deletions.
diff --git 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
@@ -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
@@ -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