Merge pull request #1911 from GaloisInc/bb/constraint-guards

Add support for translating Cryptol constraint guards

Author: mergify[bot]

CHANGES.md

@@ -1,3 +1,8 @@
+# Nightly
+
+## New Features
+* SAW now supports loading and reasoning about Cryptol declarations that make use of numeric constraint guards.  For more information on numeric constraint guards, see the [relavent section of the Cryptol reference manual](https://galoisinc.github.io/cryptol/master/BasicSyntax.html#numeric-constraint-guards).
+
 # Version 1.0 -- 2023-06-26
 
 ## New Features

cryptol-saw-core/saw/Cryptol.sawcore

@@ -39,6 +39,10 @@ Num_rec : (p: Num -> sort 1) -> ((n:Nat) -> p (TCNum n)) -> p TCInf ->
            (n:Num) -> p n;
 Num_rec p f1 f2 n = Num#rec p f1 f2 n;
 
+-- Check whether a 'Num' is finite
+tcFin : Num -> Bool;
+tcFin n = Num#rec (\ (n:Num) -> Bool) (\ (n:Nat) -> True) False n;
+
 -- Helper function: take a Num that we expect to be finite, and extract its Nat,
 -- raising an error if that Num is not finite
 getFinNat : (n:Num) -> Nat;
@@ -182,6 +186,33 @@ tcLenFromThenTo_Nat x y z =
 tcLenFromThenTo : Num -> Num -> Num -> Num;
 tcLenFromThenTo = ternaryNumFun tcLenFromThenTo_Nat TCInf;
 
+-- Build a binary predicate on Nums by lifting a binary predicate on Nats (the
+-- first argument) and using additional cases for: when the first argument is a
+-- Nat and the second is infinite; when the second is a Nat and the first is
+-- infinite; and when both are infinite
+binaryNumPred : (Nat -> Nat -> Bool) ->
+                (Nat -> Bool) ->
+                (Nat -> Bool) ->
+                Bool ->
+                Num -> Num -> Bool;
+binaryNumPred f1 f2 f3 f4 num1 num2 =
+  Num#rec (\ (num1':Num) -> Bool)
+          (\ (n1:Nat) ->
+             Num#rec (\ (num2':Num) -> Bool)
+                     (\ (n2:Nat) -> f1 n1 n2)
+                     (f2 n1)
+                     num2)
+          (Num#rec (\ (num2':Num) -> Bool) f3 f4 num2)
+          num1;
+
+-- Check two 'Num's for equality.
+tcEqual : Num -> Num -> Bool;
+tcEqual =
+  binaryNumPred equalNat (\ (x:Nat) -> False) (\ (y:Nat) -> False) True;
+
+-- Check that the first 'Num' is strictly less than the second 'Num'.
+tcLt : Num -> Num -> Bool;
+tcLt = binaryNumPred ltNat (\ (x:Nat) -> True) (\ (y:Nat) -> False) True;
 
 --------------------------------------------------------------------------------
 -- Possibly infinite sequences

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

@@ -332,6 +332,44 @@ isErasedProp prop =
     C.TCon (C.PC C.PLiteralLessThan) _ -> False
     _ -> True
 
+-- | Translate a 'Prop' containing a numeric constraint to a 'Term' that tests
+-- if the 'Prop' holds. This function will 'panic' for 'Prop's that are not
+-- numeric constraints, such as @Integral@. In other words, this function
+-- supports the same set of 'Prop's that constraint guards do.
+importNumericConstraintAsBool :: SharedContext -> Env -> C.Prop -> IO Term
+importNumericConstraintAsBool sc env prop =
+  case prop of
+    C.TCon (C.PC C.PEqual) [lhs, rhs] -> eqTerm lhs rhs
+    C.TCon (C.PC C.PNeq) [lhs, rhs] -> eqTerm lhs rhs >>= scNot sc
+    C.TCon (C.PC C.PGeq) [lhs, rhs] -> do
+      -- Convert 'lhs >= rhs' into '(rhs < lhs) \/ (rhs == lhs)'
+      lhs' <- importType sc env lhs
+      rhs' <- importType sc env rhs
+      lt <- scGlobalApply sc "Cryptol.tcLt" [rhs', lhs']
+      eq <- scGlobalApply sc "Cryptol.tcEqual" [rhs', lhs']
+      scOr sc lt eq
+    C.TCon (C.PC C.PFin) [x] -> do
+      x' <- importType sc env x
+      scGlobalApply sc "Cryptol.tcFin" [x']
+    C.TCon (C.PC C.PAnd) [lhs, rhs] -> do
+      lhs' <- importType sc env lhs
+      rhs' <- importType sc env rhs
+      scAnd sc lhs' rhs'
+    C.TCon (C.PC C.PTrue) [] -> scBool sc True
+    C.TUser _ _ t -> importNumericConstraintAsBool sc env t
+    _ -> panic
+      "importNumericConstraintAsBool"
+      [ "importNumericConstraintAsBool called with non-numeric constraint:"
+      , pretty prop
+      ]
+  where
+    -- | Construct a term for equality of two types
+    eqTerm :: C.Type -> C.Type -> IO Term
+    eqTerm lhs rhs = do
+      lhs' <- importType sc env lhs
+      rhs' <- importType sc env rhs
+      scGlobalApply sc "Cryptol.tcEqual" [lhs', rhs']
+
 importPropsType :: SharedContext -> Env -> [C.Prop] -> C.Type -> IO Term
 importPropsType sc env [] ty = importType sc env ty
 importPropsType sc env (prop : props) ty
@@ -1076,25 +1114,56 @@ importExpr sc env expr =
     C.ELocated _ e ->
       importExpr sc env e
 
-    C.EPropGuards {} ->
-      error "Using contsraint guards is not yet supported by SAW."
+    C.EPropGuards arms typ -> do
+      -- Convert prop guards to nested if-then-elses
+      typ' <- importType sc env typ
+      errMsg <- scString sc "No constraints satisfied in constraint guard"
+      err <- scGlobalApply sc "Prelude.error" [typ', errMsg]
+      -- NOTE: Must use a right fold to maintain order of prop guards in
+      -- generated if-then-else
+      Fold.foldrM (propGuardToIte typ') err arms
 
   where
     the :: String -> Maybe a -> IO a
     the what = maybe (panic "importExpr" ["internal type error", what]) return
 
+    -- | Translate an erased 'Prop' to a term and return the conjunction of the
+    -- translated term and 'mt' if 'mt' is 'Just'. Otherwise, return the
+    -- translated 'Prop'.  This function is intended to be used in a fold,
+    -- taking a 'Maybe' in the first argument to avoid creating an unnecessary
+    -- conjunction over singleton lists.
+    conjoinErasedProps :: Maybe Term -> C.Prop -> IO (Maybe Term)
+    conjoinErasedProps mt p = do
+      p' <- importNumericConstraintAsBool sc env p
+      case mt of
+        Just t -> Just <$> scAnd sc t p'
+        Nothing -> pure $ Just p'
+
+    -- | A helper function to be used in a fold converting a prop guard to an
+    -- if-then-else. In order, the arguments of the function are:
+    -- 1. The type of the prop guard
+    -- 2. An arm of the prop guard
+    -- 3. A term representing the else branch of the if-then-else
+    propGuardToIte :: Term -> ([C.Prop], C.Expr) -> Term -> IO Term
+    propGuardToIte typ (props, body) falseBranch = do
+      mCondition <- Fold.foldlM conjoinErasedProps Nothing props
+      condition <- maybe (scBool sc True) pure mCondition
+      trueBranch <- importExpr sc env body
+      scGlobalApply sc "Prelude.ite" [typ, condition, trueBranch, falseBranch]
+
 
 -- | Convert a Cryptol expression with the given type schema to a
 -- SAW-Core term. Calling 'scTypeOf' on the result of @'importExpr''
 -- sc env schema expr@ must yield a type that is equivalent (i.e.
 -- convertible) with the one returned by @'importSchema' sc env
 -- schema@.
+--
+-- Essentially, this function should be used when the expression's type is known
+-- (such as with a type annotation), and 'importExpr' should be used when the
+-- type must be inferred.
 importExpr' :: SharedContext -> Env -> C.Schema -> C.Expr -> IO Term
 importExpr' sc env schema expr =
   case expr of
-    C.EPropGuards {} ->
-      error "Using contsraint guards is not yet supported by SAW."
-
     C.ETuple es ->
       do ty <- the "Expected a mono type in ETuple" (C.isMono schema)
          ts <- the "Expected a tuple type in ETuple" (C.tIsTuple ty)
@@ -1168,6 +1237,7 @@ importExpr' sc env schema expr =
     C.EApp      {} -> fallback
     C.ETApp     {} -> fallback
     C.EProofApp {} -> fallback
+    C.EPropGuards {} -> fallback
 
   where
     go :: C.Type -> C.Expr -> IO Term

intTests/test_constraint_guards/Test.cry

@@ -0,0 +1,21 @@
+module Test where
+
+// Exhaustive constraint guards with some overlapping branches
+guard : {w} [w] -> Integer
+guard x
+  | (w == 32) => 0
+  | (w >= 32) => 1
+  | (w < 8) => 2
+  | (w != 8, w != 9) => 3
+  | () => 4
+
+// Non-exhaustive constraint guard
+incomplete : {w} [w] -> Bool
+incomplete x
+  | (w == 32) => True
+
+// More dependently typed case
+dependent : {n} [n]
+dependent
+  | n == 1 => [True]
+  | ()     => repeat False

intTests/test_constraint_guards/test.saw

@@ -0,0 +1,18 @@
+import "Test.cry";
+
+// Test exhaustive constraint guards
+prove_print z3 {{ \(x : [32])  -> guard x == 0 }};
+prove_print z3 {{ \(x : [34])  -> guard x == 1 }};
+prove_print z3 {{ \(x : [4])   -> guard x == 2 }};
+prove_print z3 {{ \(x : [16])  -> guard x == 3 }};
+prove_print z3 {{ \(x : [8])   -> guard x == 4}};
+prove_print z3 {{ \(x : [9])   -> guard x == 4}};
+
+// Test non-exhaustive constraint guards
+prove_print z3 {{ \(x : [32]) -> incomplete x }};
+fails (prove_print z3 {{ \(x : [64]) -> incomplete x }});
+
+// Test more dependently typed constraint guards
+prove_print z3 {{ dependent`{1} == [True] }};
+prove_print z3 {{ dependent`{3} == [False, False, False] }};
+prove_print z3 {{ dependent`{0} == [] }};

intTests/test_constraint_guards/test.sh

@@ -0,0 +1,3 @@
+set -e
+
+$SAW test.saw