From 918305bd6f9f3e84da666f00070aefa39c902ed7 Mon Sep 17 00:00:00 2001 From: Brett Boston Date: Wed, 2 Aug 2023 14:05:16 -0700 Subject: [PATCH 1/9] Add support for translating Cryptol constraint guards Closes #1897. This change adds support for translating Cryptol constraint guards into nested if-then-else expressions so that they may be reasoned about in SAW. --- cryptol-saw-core/saw/Cryptol.sawcore | 31 ++++++++ cryptol-saw-core/src/Verifier/SAW/Cryptol.hs | 81 ++++++++++++++++++-- intTests/test_constraint_guards/Test.cry | 14 ++++ intTests/test_constraint_guards/test.saw | 12 +++ intTests/test_constraint_guards/test.sh | 3 + 5 files changed, 136 insertions(+), 5 deletions(-) create mode 100644 intTests/test_constraint_guards/Test.cry create mode 100644 intTests/test_constraint_guards/test.saw create mode 100644 intTests/test_constraint_guards/test.sh diff --git a/cryptol-saw-core/saw/Cryptol.sawcore b/cryptol-saw-core/saw/Cryptol.sawcore index 2841e44b15..233e59077e 100644 --- a/cryptol-saw-core/saw/Cryptol.sawcore +++ b/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 : (n: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) False; -------------------------------------------------------------------------------- -- Possibly infinite sequences diff --git a/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs b/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs index 37501375a9..2d8a093595 100644 --- a/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs +++ b/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs @@ -332,6 +332,45 @@ isErasedProp prop = C.TCon (C.PC C.PLiteralLessThan) _ -> False _ -> True +-- | Translate an erased 'Prop' to a 'Term' +importErasedProp :: SharedContext -> Env -> C.Prop -> IO Term +importErasedProp 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 + _ -> if isErasedProp prop + then error $ + concat [ "importErasedProp does not support erased props of type '" + , show prop + , "'" + ] + else panic "importErasedProp" + [ "imporErasedProp called with non-erased prop:" + , show 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 +1115,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' <- importErasedProp 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 +1238,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 diff --git a/intTests/test_constraint_guards/Test.cry b/intTests/test_constraint_guards/Test.cry new file mode 100644 index 0000000000..6cf83c42ee --- /dev/null +++ b/intTests/test_constraint_guards/Test.cry @@ -0,0 +1,14 @@ +module Test where + +// Exhaustive constraint guards with some overlapping branches +guard : {w} [w] -> Integer +guard x + | (w == 32) => 0 + | (w >= 32) => 1 + | (w != 8, w != 9) => 2 + | () => 3 + +// Non-exhaustive constraint guard +incomplete : {w} [w] -> Bool +incomplete x + | (w == 32) => True diff --git a/intTests/test_constraint_guards/test.saw b/intTests/test_constraint_guards/test.saw new file mode 100644 index 0000000000..91132e285c --- /dev/null +++ b/intTests/test_constraint_guards/test.saw @@ -0,0 +1,12 @@ +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 : [16]) -> guard x == 2 }}; +prove_print z3 {{ \(x : [8]) -> guard x == 3}}; +prove_print z3 {{ \(x : [9]) -> guard x == 3}}; + +// Test non-exhaustive constraint guards +prove_print z3 {{ \(x : [32]) -> incomplete x }}; +fails (prove_print z3 {{ \(x : [64]) -> incomplete x }}); diff --git a/intTests/test_constraint_guards/test.sh b/intTests/test_constraint_guards/test.sh new file mode 100644 index 0000000000..2315cc233c --- /dev/null +++ b/intTests/test_constraint_guards/test.sh @@ -0,0 +1,3 @@ +set -e + +$SAW test.saw From 5ddb65f60d9d289b34c91144eb1717916557faf9 Mon Sep 17 00:00:00 2001 From: Brett Boston Date: Wed, 16 Aug 2023 11:10:34 -0700 Subject: [PATCH 2/9] Add test for strict less than --- intTests/test_constraint_guards/Test.cry | 3 ++- intTests/test_constraint_guards/test.saw | 5 +++-- 2 files changed, 5 insertions(+), 3 deletions(-) diff --git a/intTests/test_constraint_guards/Test.cry b/intTests/test_constraint_guards/Test.cry index 6cf83c42ee..e749172dd3 100644 --- a/intTests/test_constraint_guards/Test.cry +++ b/intTests/test_constraint_guards/Test.cry @@ -6,7 +6,8 @@ guard x | (w == 32) => 0 | (w >= 32) => 1 | (w != 8, w != 9) => 2 - | () => 3 + | (w < 8) => 3 + | () => 4 // Non-exhaustive constraint guard incomplete : {w} [w] -> Bool diff --git a/intTests/test_constraint_guards/test.saw b/intTests/test_constraint_guards/test.saw index 91132e285c..6efc50fa18 100644 --- a/intTests/test_constraint_guards/test.saw +++ b/intTests/test_constraint_guards/test.saw @@ -4,8 +4,9 @@ import "Test.cry"; prove_print z3 {{ \(x : [32]) -> guard x == 0 }}; prove_print z3 {{ \(x : [34]) -> guard x == 1 }}; prove_print z3 {{ \(x : [16]) -> guard x == 2 }}; -prove_print z3 {{ \(x : [8]) -> guard x == 3}}; -prove_print z3 {{ \(x : [9]) -> guard x == 3}}; +prove_print z3 {{ \(x : [4]) -> 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 }}; From 728619a7e256a3b83d35030fe604d0db91984f78 Mon Sep 17 00:00:00 2001 From: Brett Boston Date: Wed, 16 Aug 2023 11:11:06 -0700 Subject: [PATCH 3/9] Update cryptol-saw-core/saw/Cryptol.sawcore Co-authored-by: Ryan Scott --- cryptol-saw-core/saw/Cryptol.sawcore | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/cryptol-saw-core/saw/Cryptol.sawcore b/cryptol-saw-core/saw/Cryptol.sawcore index 233e59077e..2188387642 100644 --- a/cryptol-saw-core/saw/Cryptol.sawcore +++ b/cryptol-saw-core/saw/Cryptol.sawcore @@ -40,7 +40,7 @@ Num_rec : (p: Num -> sort 1) -> ((n:Nat) -> p (TCNum n)) -> p TCInf -> Num_rec p f1 f2 n = Num#rec p f1 f2 n; -- Check whether a 'Num' is finite -tcFin : (n:Num) -> Bool; +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, From f53701040776ddb55cbda664413027193e14a523 Mon Sep 17 00:00:00 2001 From: Brett Boston Date: Wed, 16 Aug 2023 11:15:09 -0700 Subject: [PATCH 4/9] Pretty print props --- cryptol-saw-core/src/Verifier/SAW/Cryptol.hs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs b/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs index 2d8a093595..5aec249d79 100644 --- a/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs +++ b/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs @@ -356,12 +356,12 @@ importErasedProp sc env prop = _ -> if isErasedProp prop then error $ concat [ "importErasedProp does not support erased props of type '" - , show prop + , pretty prop , "'" ] else panic "importErasedProp" [ "imporErasedProp called with non-erased prop:" - , show prop + , pretty prop ] where -- | Construct a term for equality of two types From a02ba5deab8f85f5080791c78bf96a31ce7f5d1f Mon Sep 17 00:00:00 2001 From: Brett Boston Date: Wed, 16 Aug 2023 12:02:23 -0700 Subject: [PATCH 5/9] Handle user types --- cryptol-saw-core/src/Verifier/SAW/Cryptol.hs | 1 + intTests/test_constraint_guards/Test.cry | 4 ++-- intTests/test_constraint_guards/test.saw | 4 ++-- 3 files changed, 5 insertions(+), 4 deletions(-) diff --git a/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs b/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs index 5aec249d79..fb77e41563 100644 --- a/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs +++ b/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs @@ -353,6 +353,7 @@ importErasedProp sc env prop = rhs' <- importType sc env rhs scAnd sc lhs' rhs' C.TCon (C.PC C.PTrue) [] -> scBool sc True + C.TUser _ _ t -> importErasedProp sc env t _ -> if isErasedProp prop then error $ concat [ "importErasedProp does not support erased props of type '" diff --git a/intTests/test_constraint_guards/Test.cry b/intTests/test_constraint_guards/Test.cry index e749172dd3..5b659d119e 100644 --- a/intTests/test_constraint_guards/Test.cry +++ b/intTests/test_constraint_guards/Test.cry @@ -5,8 +5,8 @@ guard : {w} [w] -> Integer guard x | (w == 32) => 0 | (w >= 32) => 1 - | (w != 8, w != 9) => 2 - | (w < 8) => 3 + | (w < 8) => 2 + | (w != 8, w != 9) => 3 | () => 4 // Non-exhaustive constraint guard diff --git a/intTests/test_constraint_guards/test.saw b/intTests/test_constraint_guards/test.saw index 6efc50fa18..9a24e31de4 100644 --- a/intTests/test_constraint_guards/test.saw +++ b/intTests/test_constraint_guards/test.saw @@ -3,8 +3,8 @@ 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 : [16]) -> guard x == 2 }}; -prove_print z3 {{ \(x : [4]) -> guard x == 3 }}; +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}}; From 4f4f1a9167c7753cdd495582aecf83d3d76a322b Mon Sep 17 00:00:00 2001 From: Brett Boston Date: Wed, 16 Aug 2023 13:13:27 -0700 Subject: [PATCH 6/9] Add more dependently typed test --- intTests/test_constraint_guards/Test.cry | 6 ++++++ intTests/test_constraint_guards/test.saw | 5 +++++ 2 files changed, 11 insertions(+) diff --git a/intTests/test_constraint_guards/Test.cry b/intTests/test_constraint_guards/Test.cry index 5b659d119e..c92ee9ceb9 100644 --- a/intTests/test_constraint_guards/Test.cry +++ b/intTests/test_constraint_guards/Test.cry @@ -13,3 +13,9 @@ guard x incomplete : {w} [w] -> Bool incomplete x | (w == 32) => True + +// More dependently typed case +dependent : {n} [n] +dependent + | n == 1 => [True] + | () => repeat False \ No newline at end of file diff --git a/intTests/test_constraint_guards/test.saw b/intTests/test_constraint_guards/test.saw index 9a24e31de4..e2b443bb91 100644 --- a/intTests/test_constraint_guards/test.saw +++ b/intTests/test_constraint_guards/test.saw @@ -11,3 +11,8 @@ 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} == [] }}; From 3d441f244d6329043da0b3bd97f39aaf24755126 Mon Sep 17 00:00:00 2001 From: Brett Boston Date: Wed, 16 Aug 2023 15:34:50 -0700 Subject: [PATCH 7/9] importErasedTerm -> importNumericConstraintAsBool + docs --- cryptol-saw-core/src/Verifier/SAW/Cryptol.hs | 28 +++++++++----------- 1 file changed, 13 insertions(+), 15 deletions(-) diff --git a/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs b/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs index fb77e41563..3deafd0a90 100644 --- a/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs +++ b/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs @@ -332,9 +332,12 @@ isErasedProp prop = C.TCon (C.PC C.PLiteralLessThan) _ -> False _ -> True --- | Translate an erased 'Prop' to a 'Term' -importErasedProp :: SharedContext -> Env -> C.Prop -> IO Term -importErasedProp sc env prop = +-- | 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 @@ -353,17 +356,12 @@ importErasedProp sc env prop = rhs' <- importType sc env rhs scAnd sc lhs' rhs' C.TCon (C.PC C.PTrue) [] -> scBool sc True - C.TUser _ _ t -> importErasedProp sc env t - _ -> if isErasedProp prop - then error $ - concat [ "importErasedProp does not support erased props of type '" - , pretty prop - , "'" - ] - else panic "importErasedProp" - [ "imporErasedProp called with non-erased prop:" - , pretty prop - ] + 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 @@ -1136,7 +1134,7 @@ importExpr sc env expr = -- conjunction over singleton lists. conjoinErasedProps :: Maybe Term -> C.Prop -> IO (Maybe Term) conjoinErasedProps mt p = do - p' <- importErasedProp sc env p + p' <- importNumericConstraintAsBool sc env p case mt of Just t -> Just <$> scAnd sc t p' Nothing -> pure $ Just p' From 6292006b4951b95c5431b5f80cea45d7cfa6c114 Mon Sep 17 00:00:00 2001 From: Brett Boston Date: Wed, 16 Aug 2023 15:42:14 -0700 Subject: [PATCH 8/9] `inf < inf` now returns True --- cryptol-saw-core/saw/Cryptol.sawcore | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/cryptol-saw-core/saw/Cryptol.sawcore b/cryptol-saw-core/saw/Cryptol.sawcore index 2188387642..96b67a8925 100644 --- a/cryptol-saw-core/saw/Cryptol.sawcore +++ b/cryptol-saw-core/saw/Cryptol.sawcore @@ -212,7 +212,7 @@ tcEqual = -- 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) False; +tcLt = binaryNumPred ltNat (\ (x:Nat) -> True) (\ (y:Nat) -> False) True; -------------------------------------------------------------------------------- -- Possibly infinite sequences From 8b43a892e6b2b9a1a1d5baf8b08b6b7c1c2ad577 Mon Sep 17 00:00:00 2001 From: Brett Boston Date: Thu, 17 Aug 2023 14:59:56 -0700 Subject: [PATCH 9/9] Update changelog with info on numeric constraint guards --- CHANGES.md | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/CHANGES.md b/CHANGES.md index ceabca591d..c31d0bebd2 100644 --- a/CHANGES.md +++ b/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