Merge pull request #30 from GaloisInc/check-cryptol-prelude

Make test binary load, translate, and typecheck `Cryptol.cry`.

cryptol-verifier.cabal

@@ -85,5 +85,9 @@ test-suite cryptol-verifier-tc-test
 
   build-depends:
     base,
+    bytestring,
+    containers,
+    cryptol,
     cryptol-verifier,
+    heredoc >= 0.2,
     saw-core

saw/Cryptol.sawcore

@@ -221,6 +221,26 @@ Rational = #();
 ecRatio : Integer -> Integer -> Rational;
 ecRatio x y = ();
 
+eqRational : Rational -> Rational -> Bool;
+eqRational x y = error Bool "Unimplemented: (==) Rational";
+
+ltRational : Rational -> Rational -> Bool;
+ltRational x y = error Bool "Unimplemented: (<) Rational";
+
+addRational : Rational -> Rational -> Rational;
+addRational x y = error Rational "Unimplemented: (+) Rational";
+
+subRational : Rational -> Rational -> Rational;
+subRational x y = error Rational "Unimplemented: (-) Rational";
+
+mulRational : Rational -> Rational -> Rational;
+mulRational x y = error Rational "Unimplemented: (*) Rational";
+
+negRational : Rational -> Rational;
+negRational x = error Rational "Unimplemented: negate Rational";
+
+integerToRational : Integer -> Rational;
+integerToRational x = error Rational "Unimplemented: fromInteger Rational";
 
 --------------------------------------------------------------------------------
 -- Parmap (Experimental)
@@ -428,6 +448,9 @@ boolCmp x y k = ite Bool x (and y k) (or y k);
 integerCmp : Integer -> Integer -> Bool -> Bool;
 integerCmp x y k = or (intLt x y) (and (intEq x y) k);
 
+rationalCmp : Rational -> Rational -> Bool -> Bool;
+rationalCmp x y k = or (ltRational x y) (and (eqRational x y) k);
+
 bvCmp : (n : Nat) -> bitvector n -> bitvector n -> Bool -> Bool;
 bvCmp n x y k = or (bvult n x y) (and (bvEq n x y) k);
 
@@ -467,6 +490,9 @@ PEqBit = { eq = boolEq };
 PEqInteger : PEq Integer;
 PEqInteger = { eq = intEq };
 
+PEqRational : PEq Rational;
+PEqRational = { eq = eqRational };
+
 PEqIntMod : (n : Nat) -> PEq (IntMod n);
 PEqIntMod n = { eq = intModEq n };
 
@@ -515,6 +541,9 @@ PCmpBit = { cmpEq = PEqBit, cmp = boolCmp };
 PCmpInteger : PCmp Integer;
 PCmpInteger = { cmpEq = PEqInteger, cmp = integerCmp };
 
+PCmpRational : PCmp Rational;
+PCmpRational = { cmpEq = PEqRational, cmp = rationalCmp };
+
 PCmpVec : (n : Nat) -> (a : sort 0) -> PCmp a -> PCmp (Vec n a);
 PCmpVec n a pa = { cmpEq = PEqVec n a pa.cmpEq, cmp = vecCmp n a pa.cmp };
 
@@ -568,6 +597,13 @@ PSignedCmpSeq n =
 PSignedCmpWord : (n : Nat) -> PSignedCmp (Vec n Bool);
 PSignedCmpWord n = { signedCmpEq = PEqWord n, scmp = bvSCmp n };
 
+PSignedCmpSeqBool : (n : Num) -> PSignedCmp (seq n Bool);
+PSignedCmpSeqBool n =
+  Num#rec (\ (n : Num) -> PSignedCmp (seq n Bool))
+          (\ (n:Nat) -> PSignedCmpWord n)
+          (error (PSignedCmp (Stream Bool)) "invalid SignedCmp instance")
+          n;
+
 PSignedCmpUnit : PSignedCmp #();
 PSignedCmpUnit = { signedCmpEq = PEqUnit, scmp = unitCmp };
 
@@ -592,6 +628,9 @@ PZeroInteger = natToInt 0;
 PZeroIntMod : (n : Nat) -> PZero (IntMod n);
 PZeroIntMod n = toIntMod n (natToInt 0);
 
+PZeroRational : PZero Rational;
+PZeroRational = integerToRational (natToInt 0);
+
 PZeroIntModNum : (num : Num) -> PZero (IntModNum num);
 PZeroIntModNum num = Num#rec (\ (n : Num) -> PZero (IntModNum n)) PZeroIntMod PZeroInteger num;
 
@@ -728,6 +767,16 @@ PRingIntModNum : (num : Num) -> PRing (IntModNum num);
 PRingIntModNum num =
   Num#rec (\ (n : Num) -> PRing (IntModNum n)) PRingIntMod PRingInteger num;
 
+PRingRational : PRing Rational;
+PRingRational =
+  { ringZero = PZeroRational
+  , add = addRational
+  , sub = subRational
+  , mul = mulRational
+  , neg = negRational
+  , int = integerToRational
+  };
+
 PRingVec : (n : Nat) -> (a : sort 0) -> PRing a -> PRing (Vec n a);
 PRingVec n a pa =
   { ringZero = replicate n a pa.ringZero
@@ -845,6 +894,7 @@ PIntegralSeqBool n =
           (error (PIntegral (Stream Bool)) "PIntegralSeqBool: no instance for streams")
 	  n;
 
+
 -- Field class
 
 PField : sort 0 -> sort 1;
@@ -854,7 +904,12 @@ PField a =
    , fieldDiv  : a -> a -> a
    };
 
--- TODO Field class instances
+PFieldRational : PField Rational;
+PFieldRational =
+  { fieldRing = PRingRational
+  , recip     = \(x : Rational) -> error Rational "Unimplemented: recip Rational"
+  , fieldDiv  = \(x y : Rational) -> error Rational "Unimplemented: (/.) Rational"
+  };
 
 
 -- Round class
@@ -870,7 +925,16 @@ PRound a =
    , roundToEven : a -> Integer
    };
 
--- TODO Round class instances
+PRoundRational : PRound Rational;
+PRoundRational =
+  { roundField	= PFieldRational
+  , roundCmp	= PCmpRational
+  , floor	= \(x : Rational) -> error Integer "Unimplemented: floor Rational"
+  , ceiling	= \(x : Rational) -> error Integer "Unimplemented: ceiling Rational"
+  , trunc	= \(x : Rational) -> error Integer "Unimplemented: trunc Rational"
+  , roundAway	= \(x : Rational) -> error Integer "Unimplemented: roundAway Rational"
+  , roundToEven = \(x : Rational) -> error Integer "Unimplemented: roundToEven Rational"
+  };
 
 
 -- Literal class
@@ -895,6 +959,9 @@ PLiteralIntModNum : (num : Num) -> PLiteral (IntModNum num);
 PLiteralIntModNum num =
   Num#rec (\ (n : Num) -> PLiteral (IntModNum n)) PLiteralIntMod PLiteralInteger num;
 
+PLiteralRational : PLiteral Rational;
+PLiteralRational = \ (x : Nat) -> error Rational "Unimplemented: Literal Rational";
+
 -- TODO: FLiteral class
 
 
@@ -1324,6 +1391,15 @@ ecTrace _ _ _ _ _ x = x;
 TCFloat : Num -> Num -> sort 0;
 TCFloat _ _ = #();
 
+PEqFloat : (e p : Num) -> PEq (TCFloat e p);
+PEqFloat e p = { eq = \(x y : TCFloat e p) -> error Bool "Unimplemented: (==) Float" };
+
+PCmpFloat : (e p : Num) -> PCmp (TCFloat e p);
+PCmpFloat e p =
+  { cmpEq = PEqFloat e p
+  , cmp = \(x y : TCFloat e p) (k : Bool) -> error Bool "Unimplemented: Cmp Float"
+  };
+
 PZeroFloat : (e p : Num) -> PZero (TCFloat e p);
 PZeroFloat e p = error (TCFloat e p) "Unimplemented: Zero Float";
 
@@ -1337,6 +1413,24 @@ PRingFloat e p =
   , int = \ (i : Integer) -> error (TCFloat e p) "Unimplemented: toInteger Float"
   };
 
+PFieldFloat : (e p : Num) -> PField (TCFloat e p);
+PFieldFloat e p =
+  { fieldRing = PRingFloat e p
+  , recip     = \(x : TCFloat e p) -> error (TCFloat e p) "Unimplemented: recip Float"
+  , fieldDiv  = \(x y : TCFloat e p) -> error (TCFloat e p) "Unimplemented: (/.) Float"
+  };
+
+PRoundFloat : (e p : Num) -> PRound (TCFloat e p);
+PRoundFloat e p =
+  { roundField  = PFieldFloat e p
+  , roundCmp    = PCmpFloat e p
+  , floor       = \(x : TCFloat e p) -> error Integer "Unimplemented: floor Float"
+  , ceiling     = \(x : TCFloat e p) -> error Integer "Unimplemented: ceiling Float"
+  , trunc       = \(x : TCFloat e p) -> error Integer "Unimplemented: trunc Float"
+  , roundAway   = \(x : TCFloat e p) -> error Integer "Unimplemented: roundAway Float"
+  , roundToEven = \(x : TCFloat e p) -> error Integer "Unimplemented: roundToEven Float"
+  };
+
 ecFpNaN : (e : Num) -> (p : Num) -> TCFloat e p;
 ecFpNaN e p = error (TCFloat e p) "Unimplemented: fpNaN";
 
@@ -1364,6 +1458,15 @@ ecFpMul e p _ _ _ = error (TCFloat e p) "Unimplemented: fpMul";
 ecFpDiv : (e : Num) -> (p : Num) -> bitvector 3 -> TCFloat e p -> TCFloat e p -> TCFloat e p;
 ecFpDiv e p _ _ _ = error (TCFloat e p) "Unimplemented: fpDiv";
 
+ecFpIsFinite : (e : Num) -> (p : Num) -> TCFloat e p -> Bool;
+ecFpIsFinite e p _ = error Bool "Unimplemented: fpIsFinite";
+
+ecFpToRational : (e : Num) -> (p : Num) -> TCFloat e p -> Rational;
+ecFpToRational e p _ = error Rational "Unimplemented: fpToRational";
+
+ecFpFromRational : (e : Num) -> (p : Num) -> bitvector 3 -> Rational -> TCFloat e p;
+ecFpFromRational e p _ _ = error (TCFloat e p) "Unimplemented: fpFromRational";
+
 
 --------------------------------------------------------------------------------
 -- Extra primitives

src/Verifier/SAW/Cryptol.hs

@@ -325,6 +325,9 @@ proveProp sc env prop =
         (C.pIsZero -> Just (C.tIsIntMod -> Just n))
           -> do n' <- importType sc env n
                 scGlobalApply sc "Cryptol.PZeroIntModNum" [n']
+        -- instance Zero Rational
+        (C.pIsZero -> Just (C.tIsRational -> True))
+          -> do scGlobalApply sc "Cryptol.PZeroRational" []
         -- instance Zero [n]
         (C.pIsZero -> Just (C.tIsSeq -> Just (n, C.tIsBit -> True)))
           -> do n' <- importType sc env n
@@ -396,6 +399,9 @@ proveProp sc env prop =
         (C.pIsRing -> Just (C.tIsIntMod -> Just n))
           -> do n' <- importType sc env n
                 scGlobalApply sc "Cryptol.PRingIntModNum" [n']
+        -- instance Ring Rational
+        (C.pIsRing -> Just (C.tIsRational -> True))
+          -> do scGlobalApply sc "Cryptol.PRingRational" []
         -- instance (fin n) => Ring [n]
         (C.pIsRing -> Just (C.tIsSeq -> Just (n, C.tIsBit -> True)))
           -> do n' <- importType sc env n
@@ -435,14 +441,29 @@ proveProp sc env prop =
 
         -- instance Integral Integer
         (C.pIsIntegral -> Just (C.tIsInteger -> True))
-          -> scGlobalApply sc "Cryptol.PIntegralInteger" []
+          -> do scGlobalApply sc "Cryptol.PIntegralInteger" []
         -- instance Integral [n]
         (C.pIsIntegral -> Just (C.tIsSeq -> (Just (n, C.tIsBit -> True))))
           -> do n' <- importType sc env n
                 scGlobalApply sc "Cryptol.PIntegralSeqBool" [n']
 
-        -- TODO, Field instances
-        -- TODO, Round instances
+        -- instance Field Rational
+        (C.pIsField -> Just (C.tIsRational -> True))
+          -> do scGlobalApply sc "Cryptol.PFieldRational" []
+        -- instance (ValidFloat e p) => Field (Float e p)
+        (C.pIsField -> Just (C.tIsFloat -> Just (e, p)))
+          -> do e' <- importType sc env e
+                p' <- importType sc env p
+                scGlobalApply sc "Cryptol.PFieldFloat" [e', p']
+
+        -- instance Round Rational
+        (C.pIsRound -> Just (C.tIsRational -> True))
+          -> do scGlobalApply sc "Cryptol.PRoundRational" []
+        -- instance (ValidFloat e p) => Round (Float e p)
+        (C.pIsRound -> Just (C.tIsFloat -> Just (e, p)))
+          -> do e' <- importType sc env e
+                p' <- importType sc env p
+                scGlobalApply sc "Cryptol.PRoundFloat" [e', p']
 
         -- instance Eq Bit
         (C.pIsEq -> Just (C.tIsBit -> True))
@@ -454,6 +475,14 @@ proveProp sc env prop =
         (C.pIsEq -> Just (C.tIsIntMod -> Just n))
           -> do n' <- importType sc env n
                 scGlobalApply sc "Cryptol.PEqIntModNum" [n']
+        -- instance Eq Rational
+        (C.pIsEq -> Just (C.tIsRational -> True))
+          -> do scGlobalApply sc "Cryptol.PEqRational" []
+        -- instance Eq (Float e p)
+        (C.pIsEq -> Just (C.tIsFloat -> Just (e, p)))
+          -> do e' <- importType sc env e
+                p' <- importType sc env p
+                scGlobalApply sc "Cryptol.PEqFloat" [e', p']
         -- instance (fin n) => Eq [n]
         (C.pIsEq -> Just (C.tIsSeq -> Just (n, C.tIsBit -> True)))
           -> do n' <- importType sc env n
@@ -486,6 +515,14 @@ proveProp sc env prop =
         -- instance Cmp Integer
         (C.pIsCmp -> Just (C.tIsInteger -> True))
           -> do scGlobalApply sc "Cryptol.PCmpInteger" []
+        -- instance Cmp Rational
+        (C.pIsCmp -> Just (C.tIsRational -> True))
+          -> do scGlobalApply sc "Cryptol.PCmpRational" []
+        -- instance Cmp (Float e p)
+        (C.pIsCmp -> Just (C.tIsFloat -> Just (e, p)))
+          -> do e' <- importType sc env e
+                p' <- importType sc env p
+                scGlobalApply sc "Cryptol.PCmpFloat" [e', p']
         -- instance (fin n) => Cmp [n]
         (C.pIsCmp -> Just (C.tIsSeq -> Just (n, C.tIsBit -> True)))
           -> do n' <- importType sc env n
@@ -515,7 +552,7 @@ proveProp sc env prop =
         -- instance (fin n) => SignedCmp [n]
         (C.pIsSignedCmp -> Just (C.tIsSeq -> Just (n, C.tIsBit -> True)))
           -> do n' <- importType sc env n
-                scGlobalApply sc "Cryptol.PSignedCmpWord" [n']
+                scGlobalApply sc "Cryptol.PSignedCmpSeqBool" [n']
         -- instance (fin n, SignedCmp a) => SignedCmp [n]a
         (C.pIsSignedCmp -> Just (C.tIsSeq -> Just (n, a)))
           -> do n' <- importType sc env n
@@ -545,6 +582,9 @@ proveProp sc env prop =
         (C.pIsLiteral -> Just (_, C.tIsIntMod -> Just n))
           -> do n' <- importType sc env n
                 scGlobalApply sc "Cryptol.PLiteralIntModNum" [n']
+        -- instance Literal val Rational
+        (C.pIsLiteral -> Just (_, C.tIsRational -> True))
+          -> do scGlobalApply sc "Cryptol.PLiteralRational" []
         -- instance (fin n, n >= width val) => Literal val [n]
         (C.pIsLiteral -> Just (_, C.tIsSeq -> Just (n, C.tIsBit -> True)))
           -> do n' <- importType sc env n
@@ -689,15 +729,18 @@ floatPrims :: Map C.PrimIdent (SharedContext -> IO Term)
 floatPrims =
   Map.fromList $
   first C.floatPrim <$>
-  [ ("fpNaN",      flip scGlobalDef "Cryptol.ecFpNaN")
-  , ("fpPosInf",   flip scGlobalDef "Cryptol.ecFpPosInf")
-  , ("fpFromBits", flip scGlobalDef "Cryptol.ecFpFromBits")
-  , ("fpToBits",   flip scGlobalDef "Cryptol.ecFpToBits")
-  , ("=.=",        flip scGlobalDef "Cryptol.ecFpEq")
-  , ("fpAdd",      flip scGlobalDef "Cryptol.ecFpAdd")
-  , ("fpSub",      flip scGlobalDef "Cryptol.ecFpSub")
-  , ("fpMul",      flip scGlobalDef "Cryptol.ecFpMul")
-  , ("fpDiv",      flip scGlobalDef "Cryptol.ecFpDiv")
+  [ ("fpNaN",          flip scGlobalDef "Cryptol.ecFpNaN")
+  , ("fpPosInf",       flip scGlobalDef "Cryptol.ecFpPosInf")
+  , ("fpFromBits",     flip scGlobalDef "Cryptol.ecFpFromBits")
+  , ("fpToBits",       flip scGlobalDef "Cryptol.ecFpToBits")
+  , ("=.=",            flip scGlobalDef "Cryptol.ecFpEq")
+  , ("fpAdd",          flip scGlobalDef "Cryptol.ecFpAdd")
+  , ("fpSub",          flip scGlobalDef "Cryptol.ecFpSub")
+  , ("fpMul",          flip scGlobalDef "Cryptol.ecFpMul")
+  , ("fpDiv",          flip scGlobalDef "Cryptol.ecFpDiv")
+  , ("fpIsFinite",     flip scGlobalDef "Cryptol.ecFpIsFinite")
+  , ("fpToRational",   flip scGlobalDef "Cryptol.ecFpToRational")
+  , ("fpFromRational", flip scGlobalDef "Cryptol.ecFpFromRational")
   ]