From 077a98b632bcc99feacc7b780f4dd661de123a9d Mon Sep 17 00:00:00 2001 From: Andrei Date: Sun, 14 Jan 2024 07:17:15 +0000 Subject: [PATCH 1/3] Add unfolding_fix_once. --- intTests/test_unfold_fix_once/test.saw | 12 ++++++++++++ intTests/test_unfold_fix_once/test.sh | 4 ++++ saw-core/src/Verifier/SAW/SharedTerm.hs | 26 +++++++++++++++++++++++++ src/SAWScript/Builtins.hs | 8 ++++++++ src/SAWScript/Interpreter.hs | 5 +++++ src/SAWScript/Proof.hs | 18 +++++++++++++++++ 6 files changed, 73 insertions(+) create mode 100644 intTests/test_unfold_fix_once/test.saw create mode 100755 intTests/test_unfold_fix_once/test.sh diff --git a/intTests/test_unfold_fix_once/test.saw b/intTests/test_unfold_fix_once/test.saw new file mode 100644 index 0000000000..908766f3ac --- /dev/null +++ b/intTests/test_unfold_fix_once/test.saw @@ -0,0 +1,12 @@ +let {{ + f : [64] -> [64] + f x = if x <$ 0 then 0 else 2 * (f (x + 1)) +}}; + +prove_print + (do { + unfolding_fix_once ["f"]; + w4_unint_z3 ["f"]; + }) + {{ \x -> (f x) % 2 == 0 }}; + diff --git a/intTests/test_unfold_fix_once/test.sh b/intTests/test_unfold_fix_once/test.sh new file mode 100755 index 0000000000..d0c501894a --- /dev/null +++ b/intTests/test_unfold_fix_once/test.sh @@ -0,0 +1,4 @@ +set -e + +$SAW test.saw + diff --git a/saw-core/src/Verifier/SAW/SharedTerm.hs b/saw-core/src/Verifier/SAW/SharedTerm.hs index b9da0f1c5f..3a1cf7d029 100644 --- a/saw-core/src/Verifier/SAW/SharedTerm.hs +++ b/saw-core/src/Verifier/SAW/SharedTerm.hs @@ -270,6 +270,7 @@ module Verifier.SAW.SharedTerm , scUnfoldConstants' , scUnfoldConstantSet , scUnfoldConstantSet' + , scUnfoldOnceFixConstantSet , scSharedSize , scSharedSizeAux , scSharedSizeMany @@ -2622,6 +2623,31 @@ scUnfoldConstantSet sc b names t0 = do _ -> scTermF sc =<< traverse go tf go t0 +scUnfoldOnceFixConstantSet :: SharedContext + -> Bool -- ^ True: unfold constants in set. False: unfold constants NOT in set + -> Set VarIndex -- ^ Set of constant names + -> Term + -> IO Term +scUnfoldOnceFixConstantSet sc b names t0 = do + cache <- newCache + let go :: Term -> IO Term + go t@(Unshared tf) = + case tf of + Constant (EC idx _ _) (Just rhs) + | Set.member idx names == b + , (isGlobalDef "Prelude.fix" -> Just (), [_, f]) <- asApplyAll rhs -> + betaNormalize sc =<< scApply sc f t + | otherwise -> return t + _ -> Unshared <$> traverse go tf + go t@(STApp{ stAppIndex = idx, stAppTermF = tf }) = useCache cache idx $ + case tf of + Constant (EC ecidx _ _) (Just rhs) + | Set.member ecidx names == b + , (isGlobalDef "Prelude.fix" -> Just (), [_, f]) <- asApplyAll rhs -> + betaNormalize sc =<< scApply sc f t + | otherwise -> return t + _ -> scTermF sc =<< traverse go tf + go t0 -- | TODO: test whether this version is slower or faster. scUnfoldConstantSet' :: SharedContext diff --git a/src/SAWScript/Builtins.hs b/src/SAWScript/Builtins.hs index dc41073628..eb3ed0d806 100644 --- a/src/SAWScript/Builtins.hs +++ b/src/SAWScript/Builtins.hs @@ -672,6 +672,14 @@ unfoldGoal unints = sqt' <- traverseSequentWithFocus (io . unfoldProp sc unints') (goalSequent goal) return (sqt', UnfoldEvidence unints') +unfoldFixOnceGoal :: [String] -> ProofScript () +unfoldFixOnceGoal unints = + execTactic $ tacticChange $ \goal -> + do sc <- getSharedContext + unints' <- resolveNames unints + sqt' <- traverseSequentWithFocus (io . unfoldFixOnceProp sc unints') (goalSequent goal) + return (sqt', UnfoldFixOnceEvidence unints') + simplifyGoal :: SV.SAWSimpset -> ProofScript () simplifyGoal ss = execTactic $ tacticChange $ \goal -> diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs index c8e360f3e6..2e052120bd 100644 --- a/src/SAWScript/Interpreter.hs +++ b/src/SAWScript/Interpreter.hs @@ -1732,6 +1732,11 @@ primitives = Map.fromList Current [ "Unfold the named subterm(s) within the current goal." ] + , prim "unfolding_fix_once" "[String] -> ProofScript ()" + (pureVal unfoldFixOnceGoal) + Current + [ "Unfold the fixpoint constant definitions once within the current goal." ] + , prim "simplify" "Simpset -> ProofScript ()" (pureVal simplifyGoal) Current diff --git a/src/SAWScript/Proof.hs b/src/SAWScript/Proof.hs index f75cf0b0db..5dd14ed04a 100644 --- a/src/SAWScript/Proof.hs +++ b/src/SAWScript/Proof.hs @@ -18,6 +18,7 @@ module SAWScript.Proof , splitConj , splitDisj , unfoldProp + , unfoldFixOnceProp , simplifyProp , hoistIfsInProp , evalProp @@ -378,6 +379,13 @@ unfoldProp sc unints (Prop tm) = do tm' <- scUnfoldConstantSet sc True unints tm return (Prop tm') +-- | Unfold all the constants appearing in the proposition +-- whose VarIndex is found in the given set. +unfoldFixOnceProp :: SharedContext -> Set VarIndex -> Prop -> IO Prop +unfoldFixOnceProp sc unints (Prop tm) = + do tm' <- scUnfoldOnceFixConstantSet sc True unints tm + return (Prop tm') + -- | Rewrite the proposition using the provided Simpset simplifyProp :: Ord a => SharedContext -> Simpset a -> Prop -> IO (Set a, Prop) simplifyProp sc ss (Prop tm) = @@ -1040,6 +1048,12 @@ data Evidence -- evidence is used to check the modified sequent. | UnfoldEvidence !(Set VarIndex) !Evidence + -- | This type of evidence is used to modify a sequent via unfolding fixpoint + -- constant definitions once. The sequent is modified by unfolding + -- constants identified via the given set of @VarIndex@; then the provided + -- evidence is used to check the modified sequent. + | UnfoldFixOnceEvidence !(Set VarIndex) !Evidence + -- | This type of evidence is used to modify a sequent via evaluation -- into the the What4 formula representation. During evaluation, the -- constants identified by the given set of @VarIndex@ are held @@ -1649,6 +1663,10 @@ checkEvidence sc = \e p -> do nenv <- scGetNamingEnv sc do sqt' <- traverseSequentWithFocus (unfoldProp sc vars) sqt check nenv e' sqt' + UnfoldFixOnceEvidence vars e' -> + do sqt' <- traverseSequentWithFocus (unfoldFixOnceProp sc vars) sqt + check nenv e' sqt' + NormalizePropEvidence opqueSet e' -> do modmap <- scGetModuleMap sc sqt' <- traverseSequentWithFocus (normalizeProp sc modmap opqueSet) sqt From 362ac43a16a6a4130403dd78cd1209ad2afafa84 Mon Sep 17 00:00:00 2001 From: Andrei Date: Tue, 16 Jan 2024 06:38:10 +0000 Subject: [PATCH 2/3] Address comments. --- saw-core/src/Verifier/SAW/SharedTerm.hs | 5 +++++ src/SAWScript/Proof.hs | 4 ++-- 2 files changed, 7 insertions(+), 2 deletions(-) diff --git a/saw-core/src/Verifier/SAW/SharedTerm.hs b/saw-core/src/Verifier/SAW/SharedTerm.hs index 3a1cf7d029..75f84c2386 100644 --- a/saw-core/src/Verifier/SAW/SharedTerm.hs +++ b/saw-core/src/Verifier/SAW/SharedTerm.hs @@ -2623,6 +2623,11 @@ scUnfoldConstantSet sc b names t0 = do _ -> scTermF sc =<< traverse go tf go t0 +-- | Unfold one time fixpoint constants. +-- +-- Specifically, if 'c = fix a f', then replace 'c' with 'f c', that is replace +-- '(fix a f)' with 'f (fix a f)' while preserving the constant name. The +-- signature of 'fix' if 'primitive fix : (a : sort 1) -> (a -> a) -> a;'. scUnfoldOnceFixConstantSet :: SharedContext -> Bool -- ^ True: unfold constants in set. False: unfold constants NOT in set -> Set VarIndex -- ^ Set of constant names diff --git a/src/SAWScript/Proof.hs b/src/SAWScript/Proof.hs index 5dd14ed04a..cb685c2889 100644 --- a/src/SAWScript/Proof.hs +++ b/src/SAWScript/Proof.hs @@ -379,8 +379,8 @@ unfoldProp sc unints (Prop tm) = do tm' <- scUnfoldConstantSet sc True unints tm return (Prop tm') --- | Unfold all the constants appearing in the proposition --- whose VarIndex is found in the given set. +-- | Unfold one time all the fixpoint constants appearing in the proposition +-- whose VarIndex is found in the given set. unfoldFixOnceProp :: SharedContext -> Set VarIndex -> Prop -> IO Prop unfoldFixOnceProp sc unints (Prop tm) = do tm' <- scUnfoldOnceFixConstantSet sc True unints tm From adc9b4bbfd7963bba200ee43f7cd739ffcd44555 Mon Sep 17 00:00:00 2001 From: Andrei Date: Tue, 16 Jan 2024 07:04:50 +0000 Subject: [PATCH 3/3] Address comments. --- saw-core/src/Verifier/SAW/SharedTerm.hs | 24 +++++++++++------------- src/SAWScript/Interpreter.hs | 5 ++++- 2 files changed, 15 insertions(+), 14 deletions(-) diff --git a/saw-core/src/Verifier/SAW/SharedTerm.hs b/saw-core/src/Verifier/SAW/SharedTerm.hs index 75f84c2386..b7a439dbdc 100644 --- a/saw-core/src/Verifier/SAW/SharedTerm.hs +++ b/saw-core/src/Verifier/SAW/SharedTerm.hs @@ -2625,9 +2625,9 @@ scUnfoldConstantSet sc b names t0 = do -- | Unfold one time fixpoint constants. -- --- Specifically, if 'c = fix a f', then replace 'c' with 'f c', that is replace --- '(fix a f)' with 'f (fix a f)' while preserving the constant name. The --- signature of 'fix' if 'primitive fix : (a : sort 1) -> (a -> a) -> a;'. +-- Specifically, if @c = fix a f@, then replace @c@ with @f c@, that is replace +-- @(fix a f)@ with @f (fix a f)@ while preserving the constant name. The +-- signature of @fix@ is @primitive fix : (a : sort 1) -> (a -> a) -> a;@. scUnfoldOnceFixConstantSet :: SharedContext -> Bool -- ^ True: unfold constants in set. False: unfold constants NOT in set -> Set VarIndex -- ^ Set of constant names @@ -2635,22 +2635,20 @@ scUnfoldOnceFixConstantSet :: SharedContext -> IO Term scUnfoldOnceFixConstantSet sc b names t0 = do cache <- newCache + let unfold t idx rhs + | Set.member idx names == b + , (isGlobalDef "Prelude.fix" -> Just (), [_, f]) <- asApplyAll rhs = + betaNormalize sc =<< scApply sc f t + | otherwise = + return t let go :: Term -> IO Term go t@(Unshared tf) = case tf of - Constant (EC idx _ _) (Just rhs) - | Set.member idx names == b - , (isGlobalDef "Prelude.fix" -> Just (), [_, f]) <- asApplyAll rhs -> - betaNormalize sc =<< scApply sc f t - | otherwise -> return t + Constant (EC idx _ _) (Just rhs) -> unfold t idx rhs _ -> Unshared <$> traverse go tf go t@(STApp{ stAppIndex = idx, stAppTermF = tf }) = useCache cache idx $ case tf of - Constant (EC ecidx _ _) (Just rhs) - | Set.member ecidx names == b - , (isGlobalDef "Prelude.fix" -> Just (), [_, f]) <- asApplyAll rhs -> - betaNormalize sc =<< scApply sc f t - | otherwise -> return t + Constant (EC ecidx _ _) (Just rhs) -> unfold t ecidx rhs _ -> scTermF sc =<< traverse go tf go t0 diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs index 2e052120bd..0f6816836f 100644 --- a/src/SAWScript/Interpreter.hs +++ b/src/SAWScript/Interpreter.hs @@ -1735,7 +1735,10 @@ primitives = Map.fromList , prim "unfolding_fix_once" "[String] -> ProofScript ()" (pureVal unfoldFixOnceGoal) Current - [ "Unfold the fixpoint constant definitions once within the current goal." ] + [ "Unfold the named recursive constants once within the current goal." + , "Like `unfolding`, except that the recursive constants are unfolded" + , "only once, avoiding possible infinite evaluation." + ] , prim "simplify" "Simpset -> ProofScript ()" (pureVal simplifyGoal)