Merge pull request #1698 from GaloisInc/rwd/congruence

Term utilities

Author: robdockins

cryptol-saw-core/src/Verifier/SAW/TypedTerm.hs

@@ -23,6 +23,7 @@ import Verifier.SAW.Cryptol (scCryptolType)
 import Verifier.SAW.FiniteValue
 import Verifier.SAW.Recognizer (asExtCns)
 import Verifier.SAW.SharedTerm
+import Verifier.SAW.SCTypeCheck (scTypeCheckError)
 
 -- Typed terms -----------------------------------------------------------------
 
@@ -67,22 +68,31 @@ mkTypedTerm sc trm = do
         Just (Right t) -> TypedTermSchema (C.tMono t)
   return (TypedTerm ttt trm)
 
--- | Apply a function-typed 'TypedTerm' to an argument. This operation
--- fails if the first 'TypedTerm' does not have a monomorphic function
--- type.
+-- | Apply a function-typed 'TypedTerm' to an argument.
+--   This operation fails if the type of the argument does
+--   not match the function.
 applyTypedTerm :: SharedContext -> TypedTerm -> TypedTerm -> IO TypedTerm
-applyTypedTerm sc (TypedTerm tp t1) (TypedTerm _ t2)
-  | Just (_,cty') <- C.tIsFun =<< ttIsMono tp
-  = TypedTerm (TypedTermSchema (C.tMono cty')) <$> scApply sc t1 t2
-
--- TODO? extend this to allow explicit application of types?
-applyTypedTerm _ _ _ = fail "applyTypedTerm: not a (monomorphic) function type"
+applyTypedTerm sc x y = applyTypedTerms sc x [y]
 
 -- | Apply a 'TypedTerm' to a list of arguments. This operation fails
 -- if the first 'TypedTerm' does not have a function type of
--- sufficient arity.
+-- sufficient arity, or if the types of the arguments do not match
+-- the type of the function.
 applyTypedTerms :: SharedContext -> TypedTerm -> [TypedTerm] -> IO TypedTerm
-applyTypedTerms sc = foldM (applyTypedTerm sc)
+applyTypedTerms sc (TypedTerm _ fn) args =
+  do trm <- foldM (scApply sc) fn (map ttTerm args)
+     ty <- scTypeCheckError sc trm
+     -- NB, scCryptolType can behave in strange ways due to the non-injectivity
+     -- of the mapping from Cryptol to SAWCore types. Perhaps we would be better
+     -- to combine the incoming type information instead of applying and then
+     -- reconstructing here.
+     ct <- scCryptolType sc ty
+     let ttt = case ct of
+           Nothing        -> TypedTermOther ty
+           Just (Left k)  -> TypedTermKind k
+           Just (Right t) -> TypedTermSchema (C.tMono t)
+     return (TypedTerm ttt trm)
+
 
 -- | Create an abstract defined constant with the specified name and body.
 defineTypedTerm :: SharedContext -> Text -> TypedTerm -> IO TypedTerm

intTests/test_congruence/README

@@ -0,0 +1,5 @@
+This is a simple test of the "congruence_for" primitive.
+
+We define a simple cryptol function, ask the system to
+automatically define a congruence rule for it; prove
+it is true, and then use it in another proof.

intTests/test_congruence/test.saw

@@ -0,0 +1,24 @@
+enable_experimental;
+
+let {{
+  f : [32] -> [100][12] -> Integer
+  f x ys = foldl (\i y -> i + toInteger y) (toInteger x) ys
+
+}};
+
+f_cong_term <- congruence_for {{ f }};
+f_cong_thm  <- prove_extcore (w4_unint_z3 ["f"]) f_cong_term;
+
+thm <- prove_print
+       do {
+         goal_intro "x";
+	 goal_intro "y";
+	 unfolding ["ecEq"];
+	 simplify (cryptol_ss ());
+	 goal_apply f_cong_thm;
+	 z3;
+	 z3;
+       }
+       {{ \x y -> f (x+y) zero == f (y+x) zero }};
+
+print thm;

intTests/test_congruence/test.sh

@@ -0,0 +1,2 @@
+#!/bin/sh
+$SAW test.saw

saw-core-coq/src/Verifier/SAW/Translation/Coq/SpecialTreatment.hs

@@ -217,6 +217,7 @@ sawCorePreludeSpecialTreatmentMap configuration =
   ++
   [ ("error",             mapsTo sawDefinitionsModule "error")
   , ("fix",               skip)
+  , ("fix_unfold",        skip)
   , ("unsafeAssert",      replaceDropArgs 3 $ Coq.Ltac "solveUnsafeAssert")
   , ("unsafeAssertBVULt", replaceDropArgs 3 $ Coq.Ltac "solveUnsafeAssertBVULt")
   , ("unsafeAssertBVULe", replaceDropArgs 3 $ Coq.Ltac "solveUnsafeAssertBVULe")

saw-core/prelude/Prelude.sawcore

@@ -158,6 +158,29 @@ eq_inv_map a b a1 a2 eq_a f1 f2 eq_f =
     (trans b (f1 a2) (f2 a2) (f2 a1) eq_f
            (eq_cong a a2 a1 (sym a a1 a2 eq_a) b f2));
 
+
+-- Basic axiom about the behavior of "fix"
+axiom fix_unfold :
+  (a : sort 1) ->
+  (f : a -> a) ->
+  Eq a (fix a f) (f (fix a f));
+
+inverse_eta_rule :
+  (a : sort 1) ->
+  (b : sort 1) ->
+  (f : a -> b) ->
+  (g : a -> b) ->
+  (Eq (a -> b) f g) ->
+  (x : a) ->
+  Eq b (f x) (g x);
+inverse_eta_rule a b f g H =
+  Eq__rec (a -> b) f
+    ( \ (g' : a -> b) -> \ (H':Eq (a -> b) f g') ->
+        ( x : a ) -> Eq b (f x) (g' x))
+    (\ (x:a) -> Refl b (f x))
+    g H;
+
+
 -- Unchecked assertion that two types are equal.
 axiom unsafeAssert : (a : sort 1) -> (x : a) -> (y : a) -> Eq a x y;
 

src/SAWScript/Builtins.hs

@@ -72,6 +72,7 @@ import Verifier.SAW.SATQuery
 import Verifier.SAW.SCTypeCheck hiding (TypedTerm)
 import qualified Verifier.SAW.SCTypeCheck as TC (TypedTerm(..))
 import Verifier.SAW.Recognizer
+import Verifier.SAW.Prelude (scEq)
 import Verifier.SAW.SharedTerm
 import Verifier.SAW.TypedTerm
 import qualified Verifier.SAW.Simulator.Concrete as Concrete
@@ -636,6 +637,58 @@ extract_uninterp unints opaques tt =
      pure (tt', replList)
 
 
+congruence_for :: TypedTerm -> TopLevel TypedTerm
+congruence_for tt =
+  do sc <- getSharedContext
+     congTm <- io $ build_congruence sc (ttTerm tt)
+     io $ mkTypedTerm sc congTm
+
+-- | Given an input term, construct another term that
+--   represents a congruence law for that term.
+--   This term will be a Curry-Howard style theorem statement
+--   that can be dispatched to solvers, and should have
+--   type "Prop".
+--
+--   This will only work for terms that represent non-dependent
+--   functions.
+build_congruence :: SharedContext -> Term -> IO Term
+build_congruence sc tm =
+  do ty <- scTypeOf sc tm
+     case asPiList ty of
+       ([],_) -> fail "congruence_for: Term is not a function"
+       (pis, body) ->
+         if looseVars body == emptyBitSet then
+           loop pis []
+         else
+           fail "congruence_for: cannot build congruence for dependent functions"
+ where
+  loop ((nm,tp):pis) vars =
+    if looseVars tp == emptyBitSet then
+      do l <- scFreshEC sc (nm <> "_1") tp
+         r <- scFreshEC sc (nm <> "_2") tp
+         loop pis ((l,r):vars)
+     else
+       fail "congruence_for: cannot build congruence for dependent functions"
+
+  loop [] vars =
+    do lvars <- mapM (scExtCns sc . fst) (reverse vars)
+       rvars <- mapM (scExtCns sc . snd) (reverse vars)
+       let allVars = concat [ [l,r] | (l,r) <- reverse vars ]
+
+       basel <- scApplyAll sc tm lvars
+       baser <- scApplyAll sc tm rvars
+       baseeq <- scEqTrue sc =<< scEq sc basel baser
+
+       let f x (l,r) =
+             do l' <- scExtCns sc l
+                r' <- scExtCns sc r
+                eq <- scEqTrue sc =<< scEq sc l' r'
+                scFun sc eq x
+       finalEq <- foldM f baseeq vars
+
+       scGeneralizeExts sc allVars finalEq
+
+
 filterCryTerms :: SharedContext -> [Term] -> IO [TypedTerm]
 filterCryTerms sc = loop
   where
@@ -1201,6 +1254,11 @@ abstractSymbolicPrim (TypedTerm _ t) = do
 bindAllExts :: SharedContext -> Term -> IO Term
 bindAllExts sc body = scAbstractExts sc (getAllExts body) body
 
+term_apply :: TypedTerm -> [TypedTerm] -> TopLevel TypedTerm
+term_apply fn args =
+  do sc <- getSharedContext
+     io $ applyTypedTerms sc fn args
+
 lambda :: TypedTerm -> TypedTerm -> TopLevel TypedTerm
 lambda x = lambdas [x]
 
@@ -1464,6 +1522,44 @@ eval_size s =
         Right _        -> fail "eval_size: not a numeric type"
     _ -> fail "eval_size: unsupported polymorphic type"
 
+int_to_term :: Int -> TopLevel TypedTerm
+int_to_term i
+  | i < 0 =
+     do sc  <- getSharedContext
+        tm  <- io (scNat sc (fromInteger (negate (toInteger i))))
+        tm' <- io (scIntNeg sc =<< scNatToInt sc tm)
+        io (mkTypedTerm sc tm')
+  | otherwise =
+     do sc  <- getSharedContext
+        tm  <- io (scNat sc (fromIntegral i))
+        tm' <- io (scNatToInt sc tm)
+        io (mkTypedTerm sc tm')
+
+nat_to_term :: Int -> TopLevel TypedTerm
+nat_to_term i
+  | i >= 0 =
+      do sc <- getSharedContext
+         tm <- io $ scNat sc (fromIntegral i)
+         io $ mkTypedTerm sc tm
+
+  | otherwise =
+      fail ("nat_to_term: negative value " ++ show i)
+
+
+size_to_term :: C.Schema -> TopLevel TypedTerm
+size_to_term s =
+  do sc <- getSharedContext
+     tm <- io $ case s of
+                  C.Forall [] [] t ->
+                    case C.evalType mempty t of
+                      Left (C.Nat x) | x >= 0 ->
+                        scCtorApp sc "Cryptol.TCNum" =<< sequence [scNat sc (fromInteger x)]
+                      Left C.Inf -> scCtorApp sc "Cryptol.TCInf" []
+                      _ -> fail "size_to_term: not a numeric type"
+                  _ -> fail "size_to_term: unsupported polymorphic type"
+
+     return (TypedTerm (TypedTermKind C.KNum) tm)
+
 nthPrim :: [a] -> Int -> TopLevel a
 nthPrim [] _ = fail "nth: index too large"
 nthPrim (x : _) 0 = return x

src/SAWScript/Interpreter.hs

@@ -1075,6 +1075,13 @@ primitives = Map.fromList
     , "is used only for pretty-printing."
     ]
 
+  , prim "term_apply"          "Term -> [Term] -> Term"
+    (funVal2 term_apply)
+    Current
+    [ "Build a term application node that applies the first term"
+    , "(which much be a term representing a function) to given list of arguments."
+    ]
+
   , prim "lambda"              "Term -> Term -> Term"
     (funVal2 lambda)
     Current
@@ -1090,6 +1097,22 @@ primitives = Map.fromList
     , "variables."
     ]
 
+  , prim "size_to_term"      "Type -> Term"
+    (funVal1 size_to_term)
+    Current
+    [ "Convert a Cryptol size type into a Term representation."
+    ]
+
+  , prim "int_to_term"      "Int -> Term"
+    (funVal1 int_to_term)
+    Current
+    [ "Convert a concrete integer value into an integer term." ]
+
+  , prim "nat_to_term"      "Int -> Term"
+    (funVal1 nat_to_term)
+    Current
+    [ "Convert a non-negative integer value into a natural number term." ]
+
   , prim "term_theories" "[String] -> Term -> [String]"
     (funVal2 term_theories)
     Experimental
@@ -1111,6 +1134,14 @@ primitives = Map.fromList
     Experimental
     [ "Apply Cryptol defaulting rules to the given term." ]
 
+  , prim "congruence_for" "Term -> TopLevel Term"
+    (pureVal congruence_for)
+    Experimental
+    [ "Given a term representing a (nondependent) function, attempt"
+    , "to automatically construct the statement of a congruence lemma"
+    , "for the function."
+    ]
+
   , prim "extract_uninterp" "[String] -> [String] -> Term -> TopLevel (Term, [(String,[(Term, Term)])])"
     (pureVal extract_uninterp)
     Experimental