From cf80114140d8f26a06b7538a8cb4aed41daf354d Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Fri, 15 Jul 2022 16:00:50 +1000 Subject: [PATCH 01/33] Adjust function name so it does not suck, small tweaks --- kore/src/Kore/Reachability/Prove.hs | 18 ++++++++++++------ kore/src/Kore/Rewrite/Strategy.hs | 3 +-- 2 files changed, 13 insertions(+), 8 deletions(-) diff --git a/kore/src/Kore/Reachability/Prove.hs b/kore/src/Kore/Reachability/Prove.hs index 54c3fed29b..980a97c482 100644 --- a/kore/src/Kore/Reachability/Prove.hs +++ b/kore/src/Kore/Reachability/Prove.hs @@ -162,8 +162,8 @@ lhsClaimStateTransformer sort = {- | @Verifer a@ is a 'Simplifier'-based action which returns an @a@. -The action may throw an exception if the proof fails; the exception is a single -@'Pattern' 'VariableName'@, the first unprovable configuration. +The action may throw an exception if the proof fails; the exception is a +@'MultiAnd'@ of unprovable configuration. -} type VerifierT m = StateT StuckClaims (ExceptT StuckClaims m) @@ -390,7 +390,7 @@ proveClaim let maybeUnproven = extractUnproven proofState for_ maybeUnproven $ \unproven -> lift $ do infoUnprovenDepth proofDepth - updateSuckClaimsState unproven maxCounterexamples + updateStuckClaimsState unproven maxCounterexamples pure proofDepth & Logic.observeAllT >>= checkLeftUnproven @@ -407,6 +407,12 @@ proveClaim discardAppliedRules = map fst + transit :: + Strategy Prim -> + (ProofDepth, ClaimState SomeClaim) -> + LogicT + (VerifierT simplifier) + [(ProofDepth, ClaimState SomeClaim)] transit instr config = Strategy.transitionRule ( transitionRule' stuckCheck claims axioms @@ -586,16 +592,16 @@ throwStuckClaims maxCounterexamples rule prim state = do ClaimState.Stuck unproven -> do lift $ do infoUnprovenDepth proofDepth' - updateSuckClaimsState unproven maxCounterexamples + updateStuckClaimsState unproven maxCounterexamples return state' _ -> return state' -updateSuckClaimsState :: +updateStuckClaimsState :: Monad m => SomeClaim -> Natural -> VerifierT m () -updateSuckClaimsState unproven maxCounterexamples = do +updateStuckClaimsState unproven maxCounterexamples = do stuckClaims <- State.get let updatedStuck = MultiAnd.singleton (StuckClaim unproven) <> stuckClaims diff --git a/kore/src/Kore/Rewrite/Strategy.hs b/kore/src/Kore/Rewrite/Strategy.hs index 1ec3d167ef..e24ffcbe7f 100644 --- a/kore/src/Kore/Rewrite/Strategy.hs +++ b/kore/src/Kore/Rewrite/Strategy.hs @@ -461,8 +461,7 @@ The queue updating function should be 'unfoldBreadthFirst' or -} leavesM :: forall m a. - Monad m => - Alternative m => + (Monad m, Alternative m) => FinalNodeType -> -- | queue updating function ([a] -> Seq a -> m (Seq a)) -> From 8bf8ed8f868141e6212d1052c1d84d5fa87e46d4 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Mon, 18 Jul 2022 17:05:40 +1000 Subject: [PATCH 02/33] add signature to exec transit function --- kore/src/Kore/Exec.hs | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/kore/src/Kore/Exec.hs b/kore/src/Kore/Exec.hs index 724ee2e3a0..088cbc7932 100644 --- a/kore/src/Kore/Exec.hs +++ b/kore/src/Kore/Exec.hs @@ -319,6 +319,12 @@ exec breadthLimit dropStrategy rewriteGroups = groupRewritesByPriority rewriteRules + + transit :: Strategy Prim + -> (ExecDepth, ProgramState (Pattern RewritingVariableName)) + -> LogicT + (Simplifier.SimplifierT smt) + [(ExecDepth, ProgramState (Pattern RewritingVariableName))] transit instr config = Strategy.transitionRule ( transitionRule rewriteGroups strategy From 591b71829ae8b5892068c20fe044a9f4349dff0c Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Wed, 20 Jul 2022 17:39:14 +1000 Subject: [PATCH 03/33] WIP draft code for graph traversal without exceptions --- kore/kore.cabal | 1 + kore/src/GraphTraversal.hs | 196 +++++++++++++++++++++++++++++++++++++ 2 files changed, 197 insertions(+) create mode 100644 kore/src/GraphTraversal.hs diff --git a/kore/kore.cabal b/kore/kore.cabal index e972ef05c5..0c0301eb10 100644 --- a/kore/kore.cabal +++ b/kore/kore.cabal @@ -209,6 +209,7 @@ library ErrorContext From GlobalMain + GraphTraversal Injection Kore.AST.ApplicativeKore Kore.AST.AstWithLocation diff --git a/kore/src/GraphTraversal.hs b/kore/src/GraphTraversal.hs new file mode 100644 index 0000000000..aa66d205df --- /dev/null +++ b/kore/src/GraphTraversal.hs @@ -0,0 +1,196 @@ +module GraphTraversal ( + module GraphTraversal, +) where + +import Control.Monad.Logic +import Control.Monad.Trans.State +import Data.Limit +import Data.List.NonEmpty qualified as NE +import Data.Sequence (Seq (..)) +import Data.Sequence qualified as Seq +import GHC.Natural +import Kore.Rewrite.Strategy ( + GraphSearchOrder (..), + LimitExceeded (..), + TransitionT (..), + runTransitionT, + unfoldSearchOrder, + ) +import Prelude.Kore + +data TransitionResult a + = -- | straight-line execution + StraightLine a + | -- | branch point + Branch (NonEmpty a) + | -- | no next state but not final (e.g., not goal state, or side + -- conditions do not hold) + Stuck a + | -- | final state (e.g., goal state reached, side conditions hold) + Final a + | -- Future work: + + -- | config matches a terminal pattern (or: is RHS of a + -- "terminal" rule) Needs to return that RHS + Terminal a + | -- | config matches a cut pattern ( aka: is LHS of a "cut" rule) + -- The respective RHS (or RHSs) are returned (if any) + Cut a [a] + +-- Graph traversal would always stop at Terminal/Cut, and _may_ stop +-- at Branch, depending on configuration. + +isStuck, isFinal, isTerminal, isCut, isBranch :: TransitionResult a -> Bool +isStuck (Stuck _) = True +isStuck _ = False +isFinal (Final _) = True +isFinal _ = False +isBranch (Branch _) = True +isBranch _ = False +isTerminal (Terminal _) = True +isTerminal _ = False +isCut (Cut _ _) = True +isCut _ = False + +extractNext :: TransitionResult a -> [a] +extractNext = \case + StraightLine a -> [a] + Branch as -> NE.toList as + Stuck _ -> [] + Final _ -> [] + Terminal _ -> [] + Cut _ as -> as + +extractState :: TransitionResult a -> Maybe a +extractState = \case + StraightLine _ -> Nothing + Branch _ -> Nothing + Stuck a -> Just a + Final a -> Just a + Terminal a -> Just a + Cut a _ -> Just a + +---------------------------------------- +transitionLeaves :: + forall m a. + (Monad m) => + -- | Stop critera, in terms of 'TransitionResult's. The algorithm + -- will _always_ stop on 'Stuck' and 'Final', so [isTerminal, + -- isCut, isBranch] could be used here. Could simplify this to + -- FinalNodeType + [TransitionResult a -> Bool] -> + -- queue updating parameters, + -- we construct enqueue :: [a] -> Seq a -> m (Either LimitExceeded (Seq a)) from it + -- m is probably only there for logging purposes + + -- | BreadthFirst, DepthFirst + GraphSearchOrder -> + -- | breadth limit, essentially a natural number + Limit Natural -> + -- | transition function + (a -> m (TransitionResult a)) -> + -- again, m is probably only for logging + + -- | + Natural -> + -- | initial node + a -> + m (TraversalResult a) +transitionLeaves + stopCriteria + direction + breadthLimit + transit + maxCounterExamples + start = + evalStateT (worker $ Seq.singleton start) [] + where + enqueue' = unfoldSearchOrder direction + + enqueue :: [a] -> Seq a -> m (Either (LimitExceeded a) (Seq a)) + enqueue as q = do + newQ <- enqueue' as q + pure $ + if exceedsLimit newQ + then Left (LimitExceeded newQ) + else Right newQ + + exceedsLimit :: Seq a -> Bool + exceedsLimit = not . withinLimit breadthLimit . fromIntegral . Seq.length + + shouldStop :: TransitionResult a -> Bool + shouldStop result = any ($ result) stopCriteria + + maxStuck = fromIntegral maxCounterExamples + + worker :: Seq a -> StateT [TransitionResult a] m (TraversalResult a) + worker Seq.Empty = Ended <$> get + worker (a :<| as) = do + result <- lift $ step a as + case result of + Continue nextQ -> worker nextQ + Output oneResult nextQ -> do + modify (oneResult :) + if not (isStuck oneResult) + then worker nextQ + else do + stuck <- gets (filter isStuck) + if length stuck >= maxStuck + then + pure $ + GotStuck (Seq.length nextQ) stuck + else worker nextQ + Abort results queue -> do + pure $ Aborted (Seq.length queue) results -- FIXME ??? results ??? + step :: + a -> + Seq a -> + m (StepResult a) + step a q = do + next <- transit a + if (isStuck next || isFinal next || shouldStop next) + then pure (Output next q) + else + either (\(LimitExceeded longQ) -> Abort [next] longQ) Continue + <$> enqueue (extractNext next) q + +data StepResult a + = Continue (Seq a) + | Output (TransitionResult a) (Seq a) + | Abort [TransitionResult a] (Seq a) + +data TraversalResult a + = -- | remaining queue length and all stuck states + GotStuck Int [TransitionResult a] + | -- | remaining queue length (limit exceeded) and results so far + Aborted Int [TransitionResult a] + | -- queue ran empty, results returned + Ended [TransitionResult a] + +---------------------------------------- +-- constructing transition functions (for caller) + +-- transition without terminal or cut rules +simpleTransition :: + forall instr config m rule. + Monad m => + -- | primitive strategy rule + (instr -> config -> TransitionT rule m config) -> + -- final transition function + ([instr], config) -> + m (TransitionResult ([instr], config)) +simpleTransition applyPrim = transit + where + tt :: [instr] -> config -> m [([instr], config)] + tt [] _config = pure [] + tt (i : is) config = + map ((is,) . fst) <$> runTransitionT (applyPrim i config) + + transit :: ([instr], config) -> m (TransitionResult ([instr], config)) + transit x = do + results <- uncurry tt x + pure $ case results of + -- FIXME how to distinguish final from stuck here? + [] -> Stuck x + [one] -> StraightLine one + (r : rs) -> Branch (r NE.:| rs) From 8cf6bf42fbaa06c0cb0583bdf66145eaae8fa864 Mon Sep 17 00:00:00 2001 From: github-actions Date: Wed, 20 Jul 2022 07:42:49 +0000 Subject: [PATCH 04/33] Format with fourmolu --- kore/src/Kore/Exec.hs | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/kore/src/Kore/Exec.hs b/kore/src/Kore/Exec.hs index 088cbc7932..ac88750a29 100644 --- a/kore/src/Kore/Exec.hs +++ b/kore/src/Kore/Exec.hs @@ -320,11 +320,12 @@ exec dropStrategy rewriteGroups = groupRewritesByPriority rewriteRules - transit :: Strategy Prim - -> (ExecDepth, ProgramState (Pattern RewritingVariableName)) - -> LogicT - (Simplifier.SimplifierT smt) - [(ExecDepth, ProgramState (Pattern RewritingVariableName))] + transit :: + Strategy Prim -> + (ExecDepth, ProgramState (Pattern RewritingVariableName)) -> + LogicT + (Simplifier.SimplifierT smt) + [(ExecDepth, ProgramState (Pattern RewritingVariableName))] transit instr config = Strategy.transitionRule ( transitionRule rewriteGroups strategy From 9c39325c91fd7fff65fb9716621873274d96133c Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Wed, 20 Jul 2022 17:54:33 +1000 Subject: [PATCH 05/33] comment --- kore/src/GraphTraversal.hs | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/kore/src/GraphTraversal.hs b/kore/src/GraphTraversal.hs index aa66d205df..d6034b8557 100644 --- a/kore/src/GraphTraversal.hs +++ b/kore/src/GraphTraversal.hs @@ -90,8 +90,7 @@ transitionLeaves :: -- | transition function (a -> m (TransitionResult a)) -> -- again, m is probably only for logging - - -- | + -- | max-counterexamples, included in the internal logic Natural -> -- | initial node a -> From 6d6f247da5b4e780bc44034b555d53e21df48068 Mon Sep 17 00:00:00 2001 From: github-actions Date: Wed, 20 Jul 2022 07:56:22 +0000 Subject: [PATCH 06/33] Materialize Nix expressions --- nix/kore-ghc8107.nix.d/kore.nix | 1 + 1 file changed, 1 insertion(+) diff --git a/nix/kore-ghc8107.nix.d/kore.nix b/nix/kore-ghc8107.nix.d/kore.nix index 40b596626a..99ecfec833 100644 --- a/nix/kore-ghc8107.nix.d/kore.nix +++ b/nix/kore-ghc8107.nix.d/kore.nix @@ -115,6 +115,7 @@ "ErrorContext" "From" "GlobalMain" + "GraphTraversal" "Injection" "Kore/AST/ApplicativeKore" "Kore/AST/AstWithLocation" From fa7fd2fad77217475fce9f8197c762067fa798e2 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Thu, 21 Jul 2022 09:40:23 +1000 Subject: [PATCH 07/33] WIP note about parameter function for transition construction --- kore/src/GraphTraversal.hs | 16 +++++++++------- 1 file changed, 9 insertions(+), 7 deletions(-) diff --git a/kore/src/GraphTraversal.hs b/kore/src/GraphTraversal.hs index d6034b8557..052facb23a 100644 --- a/kore/src/GraphTraversal.hs +++ b/kore/src/GraphTraversal.hs @@ -175,10 +175,12 @@ simpleTransition :: Monad m => -- | primitive strategy rule (instr -> config -> TransitionT rule m config) -> + -- | converter + ([config] -> TransitionResult config) -> -- final transition function ([instr], config) -> m (TransitionResult ([instr], config)) -simpleTransition applyPrim = transit +simpleTransition applyPrim mapToResult = transit where tt :: [instr] -> config -> m [([instr], config)] tt [] _config = pure [] @@ -187,9 +189,9 @@ simpleTransition applyPrim = transit transit :: ([instr], config) -> m (TransitionResult ([instr], config)) transit x = do - results <- uncurry tt x - pure $ case results of - -- FIXME how to distinguish final from stuck here? - [] -> Stuck x - [one] -> StraightLine one - (r : rs) -> Branch (r NE.:| rs) + mapToResult <$> uncurry tt x + -- pure $ case results of + -- -- FIXME how to distinguish final from stuck here? + -- [] -> Stuck x + -- [one] -> StraightLine one + -- (r : rs) -> Branch (r NE.:| rs) From 0b110ea9557a7f2411b86d819a492b631df4c01e Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Thu, 21 Jul 2022 10:34:39 +1000 Subject: [PATCH 08/33] add result interpretation as parameter function --- kore/src/GraphTraversal.hs | 34 +++++++++++++++++++--------------- kore/src/Kore/Exec.hs | 2 +- 2 files changed, 20 insertions(+), 16 deletions(-) diff --git a/kore/src/GraphTraversal.hs b/kore/src/GraphTraversal.hs index 052facb23a..710daab2e1 100644 --- a/kore/src/GraphTraversal.hs +++ b/kore/src/GraphTraversal.hs @@ -8,6 +8,7 @@ import Data.Limit import Data.List.NonEmpty qualified as NE import Data.Sequence (Seq (..)) import Data.Sequence qualified as Seq +import GHC.Generics qualified as GHC import GHC.Natural import Kore.Rewrite.Strategy ( GraphSearchOrder (..), @@ -36,6 +37,16 @@ data TransitionResult a | -- | config matches a cut pattern ( aka: is LHS of a "cut" rule) -- The respective RHS (or RHSs) are returned (if any) Cut a [a] + deriving stock (Eq, Show, GHC.Generic) + +instance Functor TransitionResult where + fmap f = \case + StraightLine a -> StraightLine $ f a + Branch as -> Branch $ NE.map f as + Stuck a -> Stuck $ f a + Final a -> Final $ f a + Terminal a -> Terminal $ f a + Cut a as -> Cut (f a) (map f as) -- Graph traversal would always stop at Terminal/Cut, and _may_ stop -- at Branch, depending on configuration. @@ -90,6 +101,7 @@ transitionLeaves :: -- | transition function (a -> m (TransitionResult a)) -> -- again, m is probably only for logging + -- | max-counterexamples, included in the internal logic Natural -> -- | initial node @@ -169,29 +181,21 @@ data TraversalResult a ---------------------------------------- -- constructing transition functions (for caller) --- transition without terminal or cut rules simpleTransition :: forall instr config m rule. Monad m => -- | primitive strategy rule (instr -> config -> TransitionT rule m config) -> - -- | converter + -- | converter to interpret the config (claim state or program state) ([config] -> TransitionResult config) -> -- final transition function ([instr], config) -> m (TransitionResult ([instr], config)) -simpleTransition applyPrim mapToResult = transit +simpleTransition applyPrim mapToResult = uncurry tt where - tt :: [instr] -> config -> m [([instr], config)] - tt [] _config = pure [] + tt :: [instr] -> config -> m (TransitionResult ([instr], config)) + tt [] config = + pure . fmap ([],) . mapToResult $ [config] tt (i : is) config = - map ((is,) . fst) <$> runTransitionT (applyPrim i config) - - transit :: ([instr], config) -> m (TransitionResult ([instr], config)) - transit x = do - mapToResult <$> uncurry tt x - -- pure $ case results of - -- -- FIXME how to distinguish final from stuck here? - -- [] -> Stuck x - -- [one] -> StraightLine one - -- (r : rs) -> Branch (r NE.:| rs) + (fmap (is,) . mapToResult . map fst) + <$> runTransitionT (applyPrim i config) diff --git a/kore/src/Kore/Exec.hs b/kore/src/Kore/Exec.hs index 0ecd827ec2..b2d193e456 100644 --- a/kore/src/Kore/Exec.hs +++ b/kore/src/Kore/Exec.hs @@ -303,7 +303,7 @@ exec Strategy Prim -> (ExecDepth, ProgramState (Pattern RewritingVariableName)) -> LogicT - (Simplifier.SimplifierT smt) + Simplifier.Simplifier [(ExecDepth, ProgramState (Pattern RewritingVariableName))] transit instr config = Strategy.transitionRule From ed163571456c662ebb40ddc7e8b7aa65547a591c Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Thu, 21 Jul 2022 11:38:03 +1000 Subject: [PATCH 09/33] result interpretation function for prover call site --- kore/src/GraphTraversal.hs | 6 +++--- kore/src/Kore/Reachability/Prove.hs | 26 ++++++++++++++++++++++++++ 2 files changed, 29 insertions(+), 3 deletions(-) diff --git a/kore/src/GraphTraversal.hs b/kore/src/GraphTraversal.hs index 710daab2e1..d4bd5db772 100644 --- a/kore/src/GraphTraversal.hs +++ b/kore/src/GraphTraversal.hs @@ -187,7 +187,7 @@ simpleTransition :: -- | primitive strategy rule (instr -> config -> TransitionT rule m config) -> -- | converter to interpret the config (claim state or program state) - ([config] -> TransitionResult config) -> + (config -> [config] -> TransitionResult config) -> -- final transition function ([instr], config) -> m (TransitionResult ([instr], config)) @@ -195,7 +195,7 @@ simpleTransition applyPrim mapToResult = uncurry tt where tt :: [instr] -> config -> m (TransitionResult ([instr], config)) tt [] config = - pure . fmap ([],) . mapToResult $ [config] + pure . fmap ([],) . (mapToResult config) $ [config] tt (i : is) config = - (fmap (is,) . mapToResult . map fst) + (fmap (is,) . mapToResult config . map fst) <$> runTransitionT (applyPrim i config) diff --git a/kore/src/Kore/Reachability/Prove.hs b/kore/src/Kore/Reachability/Prove.hs index 980a97c482..a7edb029b9 100644 --- a/kore/src/Kore/Reachability/Prove.hs +++ b/kore/src/Kore/Reachability/Prove.hs @@ -56,8 +56,11 @@ import Data.List.Extra ( import Data.Text ( Text, ) + +-- FIXME temporary import GHC.Generics qualified as GHC import Generics.SOP qualified as SOP +import GraphTraversal qualified as X import Kore.Attribute.Axiom qualified as Attribute.Axiom import Kore.Debug import Kore.Internal.Conditional ( @@ -486,6 +489,29 @@ proveClaimStep _ stuckCheck claims axioms executionGraph node = | otherwise = transitionRule' stuckCheck claims axioms prim state +-- | result interpretation for GraphTraversal.simpleTransition +toTransitionResult :: + Show c => + -- | prior state, needed for [] and Proven cases + ClaimState c -> + [ClaimState c] -> + X.TransitionResult (ClaimState c) +toTransitionResult prior = \case + [] -> X.Stuck prior + [c@ClaimState.Claimed{}] -> X.StraightLine c + [c@ClaimState.Rewritten{}] -> X.StraightLine c + [c@ClaimState.Remaining{}] -> X.StraightLine c + [c@ClaimState.Stuck{}] -> X.Stuck c + [ClaimState.Proven] -> X.Final prior + cs@(c : cs') + | noneStuck cs -> X.Branch (c :| cs') + | otherwise -> + -- FIXME Is it possible to get one stuck and one non-stuck? + error $ "toTransitionResult: " <> show (prior, cs) + where + noneStuck :: [ClaimState c] -> Bool + noneStuck = null . mapMaybe ClaimState.extractStuck + transitionRule' :: MonadSimplify simplifier => MonadProf simplifier => From 618fbe6d240b697639925c2365716b801308cf73 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Thu, 21 Jul 2022 16:38:28 +1000 Subject: [PATCH 10/33] Debugging and fixing traversal --- kore/src/GraphTraversal.hs | 79 ++++++++++++++++++++++++++------------ 1 file changed, 54 insertions(+), 25 deletions(-) diff --git a/kore/src/GraphTraversal.hs b/kore/src/GraphTraversal.hs index d4bd5db772..399d766b7b 100644 --- a/kore/src/GraphTraversal.hs +++ b/kore/src/GraphTraversal.hs @@ -17,6 +17,7 @@ import Kore.Rewrite.Strategy ( runTransitionT, unfoldSearchOrder, ) +import Kore.Reachability.Prim (Prim) import Prelude.Kore data TransitionResult a @@ -81,15 +82,17 @@ extractState = \case Terminal a -> Just a Cut a _ -> Just a +type Step = [Prim] + ---------------------------------------- transitionLeaves :: - forall m a. + forall m c . (Monad m) => -- | Stop critera, in terms of 'TransitionResult's. The algorithm -- will _always_ stop on 'Stuck' and 'Final', so [isTerminal, -- isCut, isBranch] could be used here. Could simplify this to -- FinalNodeType - [TransitionResult a -> Bool] -> + [TransitionResult ([Step], c) -> Bool] -> -- queue updating parameters, -- we construct enqueue :: [a] -> Seq a -> m (Either LimitExceeded (Seq a)) from it -- m is probably only there for logging purposes @@ -99,14 +102,14 @@ transitionLeaves :: -- | breadth limit, essentially a natural number Limit Natural -> -- | transition function - (a -> m (TransitionResult a)) -> + (([Step], c) -> m (TransitionResult ([Step], c))) -> -- again, m is probably only for logging -- | max-counterexamples, included in the internal logic Natural -> -- | initial node - a -> - m (TraversalResult a) + ([Step], c) -> + m (TraversalResult c) transitionLeaves stopCriteria direction @@ -114,11 +117,12 @@ transitionLeaves transit maxCounterExamples start = - evalStateT (worker $ Seq.singleton start) [] + evalStateT (worker (Seq.singleton start) >>= checkLeftUnproven) [] + where enqueue' = unfoldSearchOrder direction - enqueue :: [a] -> Seq a -> m (Either (LimitExceeded a) (Seq a)) + enqueue :: [([Step], c)] -> Seq ([Step], c) -> m (Either (LimitExceeded ([Step], c)) (Seq ([Step], c))) enqueue as q = do newQ <- enqueue' as q pure $ @@ -126,15 +130,15 @@ transitionLeaves then Left (LimitExceeded newQ) else Right newQ - exceedsLimit :: Seq a -> Bool + exceedsLimit :: Seq ([Step], c) -> Bool exceedsLimit = not . withinLimit breadthLimit . fromIntegral . Seq.length - shouldStop :: TransitionResult a -> Bool + shouldStop :: TransitionResult ([Step], c) -> Bool shouldStop result = any ($ result) stopCriteria maxStuck = fromIntegral maxCounterExamples - worker :: Seq a -> StateT [TransitionResult a] m (TraversalResult a) + worker :: Seq ([Step], c) -> StateT [TransitionResult ([Step], c)] m (TraversalResult ([Step], c)) worker Seq.Empty = Ended <$> get worker (a :<| as) = do result <- lift $ step a as @@ -154,21 +158,32 @@ transitionLeaves Abort results queue -> do pure $ Aborted (Seq.length queue) results -- FIXME ??? results ??? step :: - a -> - Seq a -> - m (StepResult a) + ([Step], c) -> + Seq ([Step], c) -> + m (StepResult ([Step], c)) step a q = do next <- transit a if (isStuck next || isFinal next || shouldStop next) then pure (Output next q) - else - either (\(LimitExceeded longQ) -> Abort [next] longQ) Continue - <$> enqueue (extractNext next) q + else either (\(LimitExceeded longQ) -> Abort [next] longQ) Continue + <$> enqueue (extractNext next) q + + checkLeftUnproven :: + TraversalResult ([Step], c) -> + StateT [TransitionResult ([Step], c)] m (TraversalResult c) + checkLeftUnproven result = do + stuck <- gets (map (fmap snd) . filter isStuck) + pure $ + if null stuck + then fmap snd result + else GotStuck 0 stuck + data StepResult a = Continue (Seq a) | Output (TransitionResult a) (Seq a) | Abort [TransitionResult a] (Seq a) + deriving stock (Eq, Show, GHC.Generic) data TraversalResult a = -- | remaining queue length and all stuck states @@ -177,25 +192,39 @@ data TraversalResult a Aborted Int [TransitionResult a] | -- queue ran empty, results returned Ended [TransitionResult a] + deriving stock (Eq, Show, GHC.Generic) + +instance Functor TraversalResult where + fmap f = \case + GotStuck n rs -> GotStuck n (ffmap f rs) + Aborted n rs -> GotStuck n (ffmap f rs) + Ended rs -> Ended (ffmap f rs) + where + ffmap = map . fmap ---------------------------------------- -- constructing transition functions (for caller) simpleTransition :: - forall instr config m rule. + forall config m rule. Monad m => -- | primitive strategy rule - (instr -> config -> TransitionT rule m config) -> + (Prim -> config -> TransitionT rule m config) -> -- | converter to interpret the config (claim state or program state) (config -> [config] -> TransitionResult config) -> -- final transition function - ([instr], config) -> - m (TransitionResult ([instr], config)) + ([Step], config) -> + m (TransitionResult ([Step], config)) simpleTransition applyPrim mapToResult = uncurry tt where - tt :: [instr] -> config -> m (TransitionResult ([instr], config)) + tt :: [Step] -> config -> m (TransitionResult ([Step], config)) tt [] config = - pure . fmap ([],) . (mapToResult config) $ [config] - tt (i : is) config = - (fmap (is,) . mapToResult config . map fst) - <$> runTransitionT (applyPrim i config) + pure $ Final ([], config) + tt ([] : iss) config = + tt iss config + tt (is : iss) config = + (fmap (iss,) . mapToResult config . map fst) + <$> runTransitionT (applyGroup is config) + + applyGroup :: Step -> config -> TransitionT rule m config + applyGroup is c = foldM (flip applyPrim) c is From 648b52a1bb827a72b6f0b0a82a873a44afa3beb5 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Thu, 21 Jul 2022 18:17:31 +1000 Subject: [PATCH 11/33] connected new traversal to existing proveClaim call, more debugging WIP --- kore/src/GraphTraversal.hs | 23 ++++---- kore/src/Kore/Reachability/Prove.hs | 87 ++++++++++++++++++++++++++++- 2 files changed, 96 insertions(+), 14 deletions(-) diff --git a/kore/src/GraphTraversal.hs b/kore/src/GraphTraversal.hs index 399d766b7b..5c291d7ff1 100644 --- a/kore/src/GraphTraversal.hs +++ b/kore/src/GraphTraversal.hs @@ -10,6 +10,7 @@ import Data.Sequence (Seq (..)) import Data.Sequence qualified as Seq import GHC.Generics qualified as GHC import GHC.Natural +import Kore.Reachability.Prim (Prim) import Kore.Rewrite.Strategy ( GraphSearchOrder (..), LimitExceeded (..), @@ -17,14 +18,13 @@ import Kore.Rewrite.Strategy ( runTransitionT, unfoldSearchOrder, ) -import Kore.Reachability.Prim (Prim) import Prelude.Kore data TransitionResult a = -- | straight-line execution StraightLine a - | -- | branch point - Branch (NonEmpty a) + | -- | branch point (1st arg), branching into 2nd arg elements + Branch a (NonEmpty a) | -- | no next state but not final (e.g., not goal state, or side -- conditions do not hold) Stuck a @@ -43,7 +43,7 @@ data TransitionResult a instance Functor TransitionResult where fmap f = \case StraightLine a -> StraightLine $ f a - Branch as -> Branch $ NE.map f as + Branch a as -> Branch (f a) $ NE.map f as Stuck a -> Stuck $ f a Final a -> Final $ f a Terminal a -> Terminal $ f a @@ -57,7 +57,7 @@ isStuck (Stuck _) = True isStuck _ = False isFinal (Final _) = True isFinal _ = False -isBranch (Branch _) = True +isBranch (Branch _ _) = True isBranch _ = False isTerminal (Terminal _) = True isTerminal _ = False @@ -67,7 +67,7 @@ isCut _ = False extractNext :: TransitionResult a -> [a] extractNext = \case StraightLine a -> [a] - Branch as -> NE.toList as + Branch _ as -> NE.toList as Stuck _ -> [] Final _ -> [] Terminal _ -> [] @@ -76,7 +76,7 @@ extractNext = \case extractState :: TransitionResult a -> Maybe a extractState = \case StraightLine _ -> Nothing - Branch _ -> Nothing + Branch a _ -> Just a Stuck a -> Just a Final a -> Just a Terminal a -> Just a @@ -86,7 +86,7 @@ type Step = [Prim] ---------------------------------------- transitionLeaves :: - forall m c . + forall m c. (Monad m) => -- | Stop critera, in terms of 'TransitionResult's. The algorithm -- will _always_ stop on 'Stuck' and 'Final', so [isTerminal, @@ -118,7 +118,6 @@ transitionLeaves maxCounterExamples start = evalStateT (worker (Seq.singleton start) >>= checkLeftUnproven) [] - where enqueue' = unfoldSearchOrder direction @@ -165,8 +164,9 @@ transitionLeaves next <- transit a if (isStuck next || isFinal next || shouldStop next) then pure (Output next q) - else either (\(LimitExceeded longQ) -> Abort [next] longQ) Continue - <$> enqueue (extractNext next) q + else + either (\(LimitExceeded longQ) -> Abort [next] longQ) Continue + <$> enqueue (extractNext next) q checkLeftUnproven :: TraversalResult ([Step], c) -> @@ -178,7 +178,6 @@ transitionLeaves then fmap snd result else GotStuck 0 stuck - data StepResult a = Continue (Seq a) | Output (TransitionResult a) (Seq a) diff --git a/kore/src/Kore/Reachability/Prove.hs b/kore/src/Kore/Reachability/Prove.hs index a7edb029b9..07ba7338c3 100644 --- a/kore/src/Kore/Reachability/Prove.hs +++ b/kore/src/Kore/Reachability/Prove.hs @@ -347,7 +347,8 @@ proveClaim adding an additional CheckImplication step at the end. -} & (`snoc` reachabilityCheckOnly) - proofDepths <- + -- OLD, somehow needed to disambiguate some types + _proofDepths <- Strategy.leavesM finalNodeType updateQueue @@ -357,6 +358,65 @@ proveClaim & throwUnproven & handle handleLimitExceeded & (\s -> evalStateT s mempty) + + -- NEW + let strategyToList :: Show prim => Strategy prim -> [prim] + strategyToList (Strategy.Seq a b) = strategyToList a <> strategyToList b + strategyToList (Strategy.Apply p) = [p] + strategyToList Strategy.Continue = [] + strategyToList other = error $ "strategyToList: " <> show other + + limitedStrategyList = + ( map strategyToList $ + Limit.takeWithin depthLimit $ + toList pickStrategy + ) + `snoc` (strategyToList reachabilityCheckOnly) + + stopOnBranches = \case + Strategy.Leaf -> const False + Strategy.LeafOrBranching -> X.isBranch + + transition :: + ([X.Step], (ProofDepth, ClaimState SomeClaim)) -> + ExceptT + StuckClaims + simplifier + ( X.TransitionResult + ([X.Step], (ProofDepth, ClaimState SomeClaim)) + ) + transition = + ( X.simpleTransition + ( trackProofDepth $ + transitionRule' stuckCheck claims axioms + ) + toTransitionResultWithDepth + ) + + traversalResult <- + X.transitionLeaves + [stopOnBranches finalNodeType, X.isTerminal, X.isCut] -- future work + searchOrder + breadthLimit + transition + maxCounterexamples + (limitedStrategyList, (ProofDepth 0, startGoal)) + -- traceM $ show traversalResult + + let mkStuckClaims = + MultiAnd.make + . map StuckClaim + . mapMaybe (X.extractState >=> extractStuck . snd) + proofDepths <- + case traversalResult of + X.GotStuck _n rs -> do + -- assert (length rs == fromIntegral maxCounterexamples) + Monad.Except.throwError $ mkStuckClaims rs + X.Aborted _n rs -> + Monad.Except.throwError $ mkStuckClaims rs + X.Ended results -> + pure (mapMaybe (fmap fst . X.extractState) results) + let maxProofDepth = sconcat (ProofDepth 0 :| proofDepths) infoProvenDepth maxProofDepth warnProvenClaimZeroDepth maxProofDepth goal @@ -504,7 +564,30 @@ toTransitionResult prior = \case [c@ClaimState.Stuck{}] -> X.Stuck c [ClaimState.Proven] -> X.Final prior cs@(c : cs') - | noneStuck cs -> X.Branch (c :| cs') + | noneStuck cs -> X.Branch prior (c :| cs') + | otherwise -> + -- FIXME Is it possible to get one stuck and one non-stuck? + error $ "toTransitionResult: " <> show (prior, cs) + where + noneStuck :: [ClaimState c] -> Bool + noneStuck = null . mapMaybe ClaimState.extractStuck + +-- could be solved with Data.Tuple.Extra.secondM if there wasn't the prior state +toTransitionResultWithDepth :: + Show c => + -- | prior state, needed for [] and Proven cases + (ProofDepth, ClaimState c) -> + [(ProofDepth, ClaimState c)] -> + X.TransitionResult (ProofDepth, ClaimState c) +toTransitionResultWithDepth prior = \case + [] -> X.Stuck prior + [c@(_, ClaimState.Claimed{})] -> X.StraightLine c + [c@(_, ClaimState.Rewritten{})] -> X.StraightLine c + [c@(_, ClaimState.Remaining{})] -> X.StraightLine c + [c@(_, ClaimState.Stuck{})] -> X.Stuck c + [(_, ClaimState.Proven)] -> X.Final prior + cs@(c : cs') + | noneStuck (map snd cs) -> X.Branch prior (c :| cs') | otherwise -> -- FIXME Is it possible to get one stuck and one non-stuck? error $ "toTransitionResult: " <> show (prior, cs) From 8e05e0f08d69f091564ac9d70b6456fa2b866527 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Thu, 21 Jul 2022 18:22:56 +1000 Subject: [PATCH 12/33] previous version removed, currently 16/68 tests failing --- kore/src/Kore/Reachability/Prove.hs | 38 ++++++++++++++--------------- 1 file changed, 19 insertions(+), 19 deletions(-) diff --git a/kore/src/Kore/Reachability/Prove.hs b/kore/src/Kore/Reachability/Prove.hs index 07ba7338c3..1cadd932f3 100644 --- a/kore/src/Kore/Reachability/Prove.hs +++ b/kore/src/Kore/Reachability/Prove.hs @@ -348,16 +348,16 @@ proveClaim -} & (`snoc` reachabilityCheckOnly) -- OLD, somehow needed to disambiguate some types - _proofDepths <- - Strategy.leavesM - finalNodeType - updateQueue - (Strategy.unfoldTransition transit) - (limitedStrategy, (ProofDepth 0, startGoal)) - & fmap discardStrategy - & throwUnproven - & handle handleLimitExceeded - & (\s -> evalStateT s mempty) + -- _proofDepths <- + -- Strategy.leavesM + -- finalNodeType + -- updateQueue + -- (Strategy.unfoldTransition transit) + -- (limitedStrategy, (ProofDepth 0, startGoal)) + -- & fmap discardStrategy + -- & throwUnproven + -- & handle handleLimitExceeded + -- & (\s -> evalStateT s mempty) -- NEW let strategyToList :: Show prim => Strategy prim -> [prim] @@ -434,15 +434,15 @@ proveClaim stuckClaims = mapMaybe extractStuckClaim states Monad.Except.throwError (MultiAnd.make $ toList stuckClaims) - updateQueue = \as -> - Strategy.unfoldSearchOrder searchOrder as - >=> lift . Strategy.applyBreadthLimit breadthLimit discardStrategy - >=> ( \queue -> - infoExecBreadth (ExecBreadth $ genericLength queue) - >> return queue - ) - where - genericLength = fromIntegral . length + -- updateQueue = \as -> + -- Strategy.unfoldSearchOrder searchOrder as + -- >=> lift . Strategy.applyBreadthLimit breadthLimit discardStrategy + -- >=> ( \queue -> + -- infoExecBreadth (ExecBreadth $ genericLength queue) + -- >> return queue + -- ) + -- where + -- genericLength = fromIntegral . length throwUnproven :: LogicT (VerifierT simplifier) (ProofDepth, CommonClaimState) -> From 2d97bb4261928f39e930e1679617cdcf900eb166 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Thu, 21 Jul 2022 20:48:34 +1000 Subject: [PATCH 13/33] Distinguish final from stopped results --- kore/src/GraphTraversal.hs | 33 +++++++++++++++++++++-------- kore/src/Kore/Reachability/Prove.hs | 8 ++++--- 2 files changed, 29 insertions(+), 12 deletions(-) diff --git a/kore/src/GraphTraversal.hs b/kore/src/GraphTraversal.hs index 5c291d7ff1..d6cd156c3c 100644 --- a/kore/src/GraphTraversal.hs +++ b/kore/src/GraphTraversal.hs @@ -1,3 +1,5 @@ +{-# LANGUAGE MultiWayIf #-} + module GraphTraversal ( module GraphTraversal, ) where @@ -30,6 +32,9 @@ data TransitionResult a Stuck a | -- | final state (e.g., goal state reached, side conditions hold) Final a + | -- | not stuck, but also not final (maximum depth reached before + -- finishing the proof) + Stopped a | -- Future work: -- | config matches a terminal pattern (or: is RHS of a @@ -46,17 +51,20 @@ instance Functor TransitionResult where Branch a as -> Branch (f a) $ NE.map f as Stuck a -> Stuck $ f a Final a -> Final $ f a + Stopped a -> Stopped $ f a Terminal a -> Terminal $ f a Cut a as -> Cut (f a) (map f as) -- Graph traversal would always stop at Terminal/Cut, and _may_ stop -- at Branch, depending on configuration. -isStuck, isFinal, isTerminal, isCut, isBranch :: TransitionResult a -> Bool +isStuck, isFinal, isStopped, isTerminal, isCut, isBranch :: TransitionResult a -> Bool isStuck (Stuck _) = True isStuck _ = False isFinal (Final _) = True isFinal _ = False +isStopped (Stopped _) = True +isStopped _ = False isBranch (Branch _ _) = True isBranch _ = False isTerminal (Terminal _) = True @@ -70,6 +78,7 @@ extractNext = \case Branch _ as -> NE.toList as Stuck _ -> [] Final _ -> [] + Stopped _ -> [] Terminal _ -> [] Cut _ as -> as @@ -79,6 +88,7 @@ extractState = \case Branch a _ -> Just a Stuck a -> Just a Final a -> Just a + Stopped a -> Just a Terminal a -> Just a Cut a _ -> Just a @@ -162,7 +172,7 @@ transitionLeaves m (StepResult ([Step], c)) step a q = do next <- transit a - if (isStuck next || isFinal next || shouldStop next) + if (isStuck next || isFinal next || isStopped next || shouldStop next) then pure (Output next q) else either (\(LimitExceeded longQ) -> Abort [next] longQ) Continue @@ -171,12 +181,17 @@ transitionLeaves checkLeftUnproven :: TraversalResult ([Step], c) -> StateT [TransitionResult ([Step], c)] m (TraversalResult c) - checkLeftUnproven result = do - stuck <- gets (map (fmap snd) . filter isStuck) - pure $ - if null stuck - then fmap snd result - else GotStuck 0 stuck + checkLeftUnproven = \case + result@Ended{} -> do + stuck <- gets (map (fmap snd) . filter isStuck) + -- some states may be unfinished but not stuck (Stopped) + unproven <- gets (map (fmap snd) . filter isStopped) + pure $ + if + | (not $ null stuck) -> GotStuck 0 stuck + | not $ null unproven -> Aborted 0 unproven -- ??? + | otherwise -> fmap snd result + other -> pure (fmap snd other) data StepResult a = Continue (Seq a) @@ -218,7 +233,7 @@ simpleTransition applyPrim mapToResult = uncurry tt where tt :: [Step] -> config -> m (TransitionResult ([Step], config)) tt [] config = - pure $ Final ([], config) + pure $ fmap ([],) $ mapToResult config [] tt ([] : iss) config = tt iss config tt (is : iss) config = diff --git a/kore/src/Kore/Reachability/Prove.hs b/kore/src/Kore/Reachability/Prove.hs index 1cadd932f3..d96ab3bacc 100644 --- a/kore/src/Kore/Reachability/Prove.hs +++ b/kore/src/Kore/Reachability/Prove.hs @@ -406,11 +406,10 @@ proveClaim let mkStuckClaims = MultiAnd.make . map StuckClaim - . mapMaybe (X.extractState >=> extractStuck . snd) + . mapMaybe (X.extractState >=> extractUnproven . snd) proofDepths <- case traversalResult of X.GotStuck _n rs -> do - -- assert (length rs == fromIntegral maxCounterexamples) Monad.Except.throwError $ mkStuckClaims rs X.Aborted _n rs -> Monad.Except.throwError $ mkStuckClaims rs @@ -580,7 +579,10 @@ toTransitionResultWithDepth :: [(ProofDepth, ClaimState c)] -> X.TransitionResult (ProofDepth, ClaimState c) toTransitionResultWithDepth prior = \case - [] -> X.Stuck prior + [] + | isJust (extractStuck $ snd prior) -> X.Stuck prior + | isJust (extractUnproven $ snd prior) -> X.Stopped prior + | otherwise -> X.Final prior -- FIXME ??? [c@(_, ClaimState.Claimed{})] -> X.StraightLine c [c@(_, ClaimState.Rewritten{})] -> X.StraightLine c [c@(_, ClaimState.Remaining{})] -> X.StraightLine c From b5c1c3fd7839895e00340962269de2063dc5ad3a Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Thu, 21 Jul 2022 23:05:45 +1000 Subject: [PATCH 14/33] catch corner case of breadthLimit 0 --- kore/src/GraphTraversal.hs | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/kore/src/GraphTraversal.hs b/kore/src/GraphTraversal.hs index d6cd156c3c..bd53fde20f 100644 --- a/kore/src/GraphTraversal.hs +++ b/kore/src/GraphTraversal.hs @@ -127,7 +127,10 @@ transitionLeaves transit maxCounterExamples start = - evalStateT (worker (Seq.singleton start) >>= checkLeftUnproven) [] + enqueue [start] Seq.empty + >>= either + (pure . const (Aborted 0 [Stopped $ snd start])) + (\q -> evalStateT (worker q >>= checkLeftUnproven) []) where enqueue' = unfoldSearchOrder direction From 964b9bb4cb2051aaef679d2171fe9dae8db42599 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Fri, 22 Jul 2022 10:44:02 +1000 Subject: [PATCH 15/33] Pretty instances for better debugging --- kore/src/GraphTraversal.hs | 37 +++++++++++++++++++++++++++++++++++++ 1 file changed, 37 insertions(+) diff --git a/kore/src/GraphTraversal.hs b/kore/src/GraphTraversal.hs index bd53fde20f..4efef790f0 100644 --- a/kore/src/GraphTraversal.hs +++ b/kore/src/GraphTraversal.hs @@ -21,6 +21,7 @@ import Kore.Rewrite.Strategy ( unfoldSearchOrder, ) import Prelude.Kore +import Pretty data TransitionResult a = -- | straight-line execution @@ -55,6 +56,30 @@ instance Functor TransitionResult where Terminal a -> Terminal $ f a Cut a as -> Cut (f a) (map f as) +instance Pretty a => Pretty (TransitionResult a) where + pretty = \case + StraightLine a -> single "StraightLine" a + Branch a as -> multi "Branch" "node" a "successors" (NE.toList as) + Stuck a -> single "Stuck" a + Final a -> single "Final" a + Stopped a -> single "Stopped" a + Terminal a -> single "Terminal" a + Cut a as -> multi "Cut" "node" a "successors" as + where + single :: Doc x -> a -> Doc x + single lbl a = + Pretty.vsep [lbl, Pretty.indent 4 $ Pretty.pretty a] + + multi :: Doc x -> Doc x -> a -> Doc x -> [a] -> Doc x + multi lbl lbl1 a lbl2 as = + Pretty.vsep $ + [ lbl + , Pretty.indent 2 $ "- " <> lbl1 + , Pretty.indent 4 $ Pretty.pretty a + , Pretty.indent 2 $ "- " <> lbl2 + ] + <> map (Pretty.indent 4 . Pretty.pretty) as + -- Graph traversal would always stop at Terminal/Cut, and _may_ stop -- at Branch, depending on configuration. @@ -211,6 +236,18 @@ data TraversalResult a Ended [TransitionResult a] deriving stock (Eq, Show, GHC.Generic) +instance Pretty a => Pretty (TraversalResult a) where + pretty = \case + GotStuck n as -> + Pretty.hang 4 $ + Pretty.vsep $ ("Got stuck with queue of " <> Pretty.pretty n) : map Pretty.pretty as + Aborted n as -> + Pretty.hang 4 $ + Pretty.vsep $ ("Aborted with queue of " <> Pretty.pretty n) : map Pretty.pretty as + Ended as -> + Pretty.hang 4 $ + Pretty.vsep $ "Ended" : map Pretty.pretty as + instance Functor TraversalResult where fmap f = \case GotStuck n rs -> GotStuck n (ffmap f rs) From 6f73ec663692f216cf43723d7c6f4ae9855ffee9 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Fri, 22 Jul 2022 10:48:00 +1000 Subject: [PATCH 16/33] style --- kore/src/Kore/Reachability/Prove.hs | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/kore/src/Kore/Reachability/Prove.hs b/kore/src/Kore/Reachability/Prove.hs index d96ab3bacc..a709c305cf 100644 --- a/kore/src/Kore/Reachability/Prove.hs +++ b/kore/src/Kore/Reachability/Prove.hs @@ -367,10 +367,7 @@ proveClaim strategyToList other = error $ "strategyToList: " <> show other limitedStrategyList = - ( map strategyToList $ - Limit.takeWithin depthLimit $ - toList pickStrategy - ) + map strategyToList (Limit.takeWithin depthLimit $ toList pickStrategy) `snoc` (strategyToList reachabilityCheckOnly) stopOnBranches = \case From 556c63f2c12fe3889a9d250e95ec9ab71fcaf644 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Fri, 22 Jul 2022 11:12:19 +1000 Subject: [PATCH 17/33] fix limit-exceeded case and copy pasta Semantics of TraversalResult (failure cases): - When `GotStuck` is returned, the returned results are considered stuck and thrown as an exception; - when `Aborted` is returned, the returned results are _analysed_ and their _next_ states (to enqueue) are considered stuck and thrown. --- kore/src/GraphTraversal.hs | 10 +++++----- kore/src/Kore/Reachability/Prove.hs | 28 ++++++++++++++++++++-------- 2 files changed, 25 insertions(+), 13 deletions(-) diff --git a/kore/src/GraphTraversal.hs b/kore/src/GraphTraversal.hs index 4efef790f0..dbb11f4a4a 100644 --- a/kore/src/GraphTraversal.hs +++ b/kore/src/GraphTraversal.hs @@ -193,7 +193,7 @@ transitionLeaves GotStuck (Seq.length nextQ) stuck else worker nextQ Abort results queue -> do - pure $ Aborted (Seq.length queue) results -- FIXME ??? results ??? + pure $ Aborted (Seq.length queue) results step :: ([Step], c) -> Seq ([Step], c) -> @@ -203,8 +203,8 @@ transitionLeaves if (isStuck next || isFinal next || isStopped next || shouldStop next) then pure (Output next q) else - either (\(LimitExceeded longQ) -> Abort [next] longQ) Continue - <$> enqueue (extractNext next) q + let abort (LimitExceeded queue) = Abort [next] queue + in either abort Continue <$> enqueue (extractNext next) q checkLeftUnproven :: TraversalResult ([Step], c) -> @@ -217,7 +217,7 @@ transitionLeaves pure $ if | (not $ null stuck) -> GotStuck 0 stuck - | not $ null unproven -> Aborted 0 unproven -- ??? + | not $ null unproven -> GotStuck 0 unproven | otherwise -> fmap snd result other -> pure (fmap snd other) @@ -251,7 +251,7 @@ instance Pretty a => Pretty (TraversalResult a) where instance Functor TraversalResult where fmap f = \case GotStuck n rs -> GotStuck n (ffmap f rs) - Aborted n rs -> GotStuck n (ffmap f rs) + Aborted n rs -> Aborted n (ffmap f rs) Ended rs -> Ended (ffmap f rs) where ffmap = map . fmap diff --git a/kore/src/Kore/Reachability/Prove.hs b/kore/src/Kore/Reachability/Prove.hs index a709c305cf..5059916978 100644 --- a/kore/src/Kore/Reachability/Prove.hs +++ b/kore/src/Kore/Reachability/Prove.hs @@ -398,18 +398,30 @@ proveClaim transition maxCounterexamples (limitedStrategyList, (ProofDepth 0, startGoal)) - -- traceM $ show traversalResult - let mkStuckClaims = - MultiAnd.make - . map StuckClaim - . mapMaybe (X.extractState >=> extractUnproven . snd) + -- traceM + -- . Pretty.renderString + -- . Pretty.layoutPretty Pretty.defaultLayoutOptions + -- $ Pretty.pretty traversalResult + + let throwStuckClaims = + Monad.Except.throwError . MultiAnd.make . map StuckClaim proofDepths <- + -- Semantics of TraversalResult (failure cases): + -- - When `GotStuck` is returned, the returned results + -- are considered stuck and thrown as an exception; + -- - when `Aborted` is returned, the returned results + -- are _analysed_ and their _next_ states (to + -- enqueue) are considered stuck and thrown. case traversalResult of - X.GotStuck _n rs -> do - Monad.Except.throwError $ mkStuckClaims rs + X.GotStuck _n rs -> + throwStuckClaims $ + mapMaybe (X.extractState >=> extractUnproven . snd) rs + -- return _given_ states (considered stuck) when GotStuck X.Aborted _n rs -> - Monad.Except.throwError $ mkStuckClaims rs + throwStuckClaims $ + -- return _next_ states when Aborted + concatMap (mapMaybe (extractUnproven . snd) . X.extractNext) rs X.Ended results -> pure (mapMaybe (fmap fst . X.extractState) results) From 59eb56c7d348fe61ca78beb4d221016f8f65dc19 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Fri, 22 Jul 2022 11:21:56 +1000 Subject: [PATCH 18/33] fix breadthLimit = 0 corner case (again) --- kore/src/GraphTraversal.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kore/src/GraphTraversal.hs b/kore/src/GraphTraversal.hs index dbb11f4a4a..c8b069382b 100644 --- a/kore/src/GraphTraversal.hs +++ b/kore/src/GraphTraversal.hs @@ -154,7 +154,7 @@ transitionLeaves start = enqueue [start] Seq.empty >>= either - (pure . const (Aborted 0 [Stopped $ snd start])) + (pure . const (GotStuck 0 [Stopped $ snd start])) (\q -> evalStateT (worker q >>= checkLeftUnproven) []) where enqueue' = unfoldSearchOrder direction From d994ae4046dfdb38b78cc35579f12e2e235682e9 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Fri, 22 Jul 2022 11:28:07 +1000 Subject: [PATCH 19/33] format my life... --- kore/src/GraphTraversal.hs | 2 +- kore/src/Kore/Reachability/Prove.hs | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/kore/src/GraphTraversal.hs b/kore/src/GraphTraversal.hs index c8b069382b..c34581ef72 100644 --- a/kore/src/GraphTraversal.hs +++ b/kore/src/GraphTraversal.hs @@ -204,7 +204,7 @@ transitionLeaves then pure (Output next q) else let abort (LimitExceeded queue) = Abort [next] queue - in either abort Continue <$> enqueue (extractNext next) q + in either abort Continue <$> enqueue (extractNext next) q checkLeftUnproven :: TraversalResult ([Step], c) -> diff --git a/kore/src/Kore/Reachability/Prove.hs b/kore/src/Kore/Reachability/Prove.hs index 5059916978..9a1db49c92 100644 --- a/kore/src/Kore/Reachability/Prove.hs +++ b/kore/src/Kore/Reachability/Prove.hs @@ -416,8 +416,8 @@ proveClaim case traversalResult of X.GotStuck _n rs -> throwStuckClaims $ - mapMaybe (X.extractState >=> extractUnproven . snd) rs -- return _given_ states (considered stuck) when GotStuck + mapMaybe (X.extractState >=> extractUnproven . snd) rs X.Aborted _n rs -> throwStuckClaims $ -- return _next_ states when Aborted From 0769e1164677dda2607906b7c54e72905d64a813 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Fri, 22 Jul 2022 11:42:06 +1000 Subject: [PATCH 20/33] fix state count when stopped before stuck/final --- kore/src/GraphTraversal.hs | 22 +++++++++++----------- 1 file changed, 11 insertions(+), 11 deletions(-) diff --git a/kore/src/GraphTraversal.hs b/kore/src/GraphTraversal.hs index c34581ef72..5058fea93a 100644 --- a/kore/src/GraphTraversal.hs +++ b/kore/src/GraphTraversal.hs @@ -155,7 +155,7 @@ transitionLeaves enqueue [start] Seq.empty >>= either (pure . const (GotStuck 0 [Stopped $ snd start])) - (\q -> evalStateT (worker q >>= checkLeftUnproven) []) + (\q -> checkLeftUnproven <$> evalStateT (worker q) []) where enqueue' = unfoldSearchOrder direction @@ -176,7 +176,7 @@ transitionLeaves maxStuck = fromIntegral maxCounterExamples worker :: Seq ([Step], c) -> StateT [TransitionResult ([Step], c)] m (TraversalResult ([Step], c)) - worker Seq.Empty = Ended <$> get + worker Seq.Empty = Ended . reverse <$> get worker (a :<| as) = do result <- lift $ step a as case result of @@ -207,19 +207,19 @@ transitionLeaves in either abort Continue <$> enqueue (extractNext next) q checkLeftUnproven :: - TraversalResult ([Step], c) -> - StateT [TransitionResult ([Step], c)] m (TraversalResult c) + TraversalResult ([Step], c) -> TraversalResult c checkLeftUnproven = \case - result@Ended{} -> do - stuck <- gets (map (fmap snd) . filter isStuck) - -- some states may be unfinished but not stuck (Stopped) - unproven <- gets (map (fmap snd) . filter isStopped) - pure $ - if + result@(Ended results) -> + let -- we collect a maximum of 'maxCounterExamples' Stuck states + stuck = map (fmap snd) $ filter isStuck results + -- Other states may be unfinished but not stuck (Stopped) + -- Only provide the requested amount of states (maxCounterExamples) + unproven = take maxStuck . map (fmap snd) $ filter isStopped results + in if | (not $ null stuck) -> GotStuck 0 stuck | not $ null unproven -> GotStuck 0 unproven | otherwise -> fmap snd result - other -> pure (fmap snd other) + other -> fmap snd other data StepResult a = Continue (Seq a) From c6b411e776be2891129bb95034092292392f9789 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Fri, 22 Jul 2022 16:35:13 +1000 Subject: [PATCH 21/33] clean-up and comments GraphTraversal --- kore/src/GraphTraversal.hs | 37 ++++++++++++++++++++++++------------- 1 file changed, 24 insertions(+), 13 deletions(-) diff --git a/kore/src/GraphTraversal.hs b/kore/src/GraphTraversal.hs index 5058fea93a..41cf79e00e 100644 --- a/kore/src/GraphTraversal.hs +++ b/kore/src/GraphTraversal.hs @@ -1,5 +1,10 @@ {-# LANGUAGE MultiWayIf #-} +{- | +Copyright : (c) Runtime Verification, 2018-2022 +License : BSD-3-Clause +Maintainer : jost.berthold@runtimeverification.com +-} module GraphTraversal ( module GraphTraversal, ) where @@ -192,8 +197,9 @@ transitionLeaves pure $ GotStuck (Seq.length nextQ) stuck else worker nextQ - Abort results queue -> do - pure $ Aborted (Seq.length queue) results + Abort lastState queue -> do + pure $ Aborted (Seq.length queue) [lastState] + -- TODO could add current state to return value ^^^^^^^ step :: ([Step], c) -> Seq ([Step], c) -> @@ -203,7 +209,7 @@ transitionLeaves if (isStuck next || isFinal next || isStopped next || shouldStop next) then pure (Output next q) else - let abort (LimitExceeded queue) = Abort [next] queue + let abort (LimitExceeded queue) = Abort next queue in either abort Continue <$> enqueue (extractNext next) q checkLeftUnproven :: @@ -224,29 +230,33 @@ transitionLeaves data StepResult a = Continue (Seq a) | Output (TransitionResult a) (Seq a) - | Abort [TransitionResult a] (Seq a) + | Abort (TransitionResult a) (Seq a) deriving stock (Eq, Show, GHC.Generic) data TraversalResult a - = -- | remaining queue length and all stuck states + = -- | remaining queue length and stuck or stopped (unproven) + -- states (always at most maxCounterExamples many) GotStuck Int [TransitionResult a] - | -- | remaining queue length (limit exceeded) and results so far + | -- | queue length (exceeding the limit) and result(s) of the + -- last step that led to stopping Aborted Int [TransitionResult a] - | -- queue ran empty, results returned + | -- | queue empty, results returned Ended [TransitionResult a] deriving stock (Eq, Show, GHC.Generic) instance Pretty a => Pretty (TraversalResult a) where pretty = \case GotStuck n as -> - Pretty.hang 4 $ - Pretty.vsep $ ("Got stuck with queue of " <> Pretty.pretty n) : map Pretty.pretty as + Pretty.hang 4 . Pretty.vsep $ + ("Got stuck with queue of " <> Pretty.pretty n) : + map Pretty.pretty as Aborted n as -> - Pretty.hang 4 $ - Pretty.vsep $ ("Aborted with queue of " <> Pretty.pretty n) : map Pretty.pretty as + Pretty.hang 4 . Pretty.vsep $ + ("Aborted with queue of " <> Pretty.pretty n) : + map Pretty.pretty as Ended as -> - Pretty.hang 4 $ - Pretty.vsep $ "Ended" : map Pretty.pretty as + Pretty.hang 4 . Pretty.vsep $ + "Ended" : map Pretty.pretty as instance Functor TraversalResult where fmap f = \case @@ -265,6 +275,7 @@ simpleTransition :: -- | primitive strategy rule (Prim -> config -> TransitionT rule m config) -> -- | converter to interpret the config (claim state or program state) + -- TODO should also consider the applied rule(s) (for Terminal/Cut) (config -> [config] -> TransitionResult config) -> -- final transition function ([Step], config) -> From 14af3bbd65c122362530073aeeaa4a2f5cf09fc4 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Fri, 22 Jul 2022 17:07:24 +1000 Subject: [PATCH 22/33] clean up Prove module (call site) --- kore/src/Kore/Reachability/Prove.hs | 267 ++++++---------------------- 1 file changed, 55 insertions(+), 212 deletions(-) diff --git a/kore/src/Kore/Reachability/Prove.hs b/kore/src/Kore/Reachability/Prove.hs index 9a1db49c92..ae9bbaa81a 100644 --- a/kore/src/Kore/Reachability/Prove.hs +++ b/kore/src/Kore/Reachability/Prove.hs @@ -29,7 +29,6 @@ import Control.Monad ( import Control.Monad.Catch ( MonadCatch, MonadMask, - handle, handleAll, throwM, ) @@ -40,7 +39,6 @@ import Control.Monad.Except ( import Control.Monad.Except qualified as Monad.Except import Control.Monad.State.Strict ( StateT, - evalStateT, runStateT, ) import Control.Monad.State.Strict qualified as State @@ -56,8 +54,6 @@ import Data.List.Extra ( import Data.Text ( Text, ) - --- FIXME temporary import GHC.Generics qualified as GHC import Generics.SOP qualified as SOP import GraphTraversal qualified as X @@ -88,7 +84,6 @@ import Kore.Log.DebugTransition ( debugBeforeTransition, debugFinalTransition, ) -import Kore.Log.InfoExecBreadth import Kore.Log.InfoProofDepth import Kore.Log.WarnStuckClaimState import Kore.Log.WarnTrivialClaim @@ -129,10 +124,6 @@ import Kore.Unparser import Log ( MonadLog (..), ) -import Logic ( - LogicT, - ) -import Logic qualified import Numeric.Natural ( Natural, ) @@ -168,7 +159,7 @@ lhsClaimStateTransformer sort = The action may throw an exception if the proof fails; the exception is a @'MultiAnd'@ of unprovable configuration. -} -type VerifierT m = StateT StuckClaims (ExceptT StuckClaims m) +type VerifierT m = ExceptT StuckClaims m newtype AllClaims claim = AllClaims {getAllClaims :: [claim]} newtype Axioms claim = Axioms {getAxioms :: [Rule claim]} @@ -278,7 +269,7 @@ proveClaimsWorker :: -- | List of claims, together with a maximum number of verification steps -- for each. ToProve SomeClaim -> - ExceptT StuckClaims (StateT ProvenClaims simplifier) () + VerifierT (StateT ProvenClaims simplifier) () proveClaimsWorker maybeMinDepth stuckCheck @@ -293,7 +284,7 @@ proveClaimsWorker where verifyWorker :: (SomeClaim, Limit Natural) -> - ExceptT StuckClaims (StateT ProvenClaims simplifier) () + VerifierT (StateT ProvenClaims simplifier) () verifyWorker unprovenClaim@(claim, _) = do debugBeginClaim claim proveClaim @@ -325,7 +316,7 @@ proveClaim :: AllClaims SomeClaim -> Axioms SomeClaim -> (SomeClaim, Limit Natural) -> - ExceptT StuckClaims simplifier () + VerifierT simplifier () proveClaim maybeMinDepth stuckCheck @@ -338,33 +329,9 @@ proveClaim (goal, depthLimit) = traceExceptT D_OnePath_verifyClaim [debugArg "rule" goal] $ do let startGoal = ClaimState.Claimed (Lens.over lensClaimPattern mkGoal goal) - limitedStrategy = - pickStrategy - & toList - & Limit.takeWithin depthLimit - {- With a non-Unlimited 'depthLimit', ensure that we - discharge proofs which hold at the depth bound by - adding an additional CheckImplication step at the end. - -} - & (`snoc` reachabilityCheckOnly) - -- OLD, somehow needed to disambiguate some types - -- _proofDepths <- - -- Strategy.leavesM - -- finalNodeType - -- updateQueue - -- (Strategy.unfoldTransition transit) - -- (limitedStrategy, (ProofDepth 0, startGoal)) - -- & fmap discardStrategy - -- & throwUnproven - -- & handle handleLimitExceeded - -- & (\s -> evalStateT s mempty) - - -- NEW - let strategyToList :: Show prim => Strategy prim -> [prim] - strategyToList (Strategy.Seq a b) = strategyToList a <> strategyToList b - strategyToList (Strategy.Apply p) = [p] - strategyToList Strategy.Continue = [] - strategyToList other = error $ "strategyToList: " <> show other + + pickStrategy = + maybe strategy strategyWithMinDepth maybeMinDepth limitedStrategyList = map strategyToList (Limit.takeWithin depthLimit $ toList pickStrategy) @@ -374,22 +341,6 @@ proveClaim Strategy.Leaf -> const False Strategy.LeafOrBranching -> X.isBranch - transition :: - ([X.Step], (ProofDepth, ClaimState SomeClaim)) -> - ExceptT - StuckClaims - simplifier - ( X.TransitionResult - ([X.Step], (ProofDepth, ClaimState SomeClaim)) - ) - transition = - ( X.simpleTransition - ( trackProofDepth $ - transitionRule' stuckCheck claims axioms - ) - toTransitionResultWithDepth - ) - traversalResult <- X.transitionLeaves [stopOnBranches finalNodeType, X.isTerminal, X.isCut] -- future work @@ -399,11 +350,6 @@ proveClaim maxCounterexamples (limitedStrategyList, (ProofDepth 0, startGoal)) - -- traceM - -- . Pretty.renderString - -- . Pretty.layoutPretty Pretty.defaultLayoutOptions - -- $ Pretty.pretty traversalResult - let throwStuckClaims = Monad.Except.throwError . MultiAnd.make . map StuckClaim proofDepths <- @@ -429,73 +375,55 @@ proveClaim infoProvenDepth maxProofDepth warnProvenClaimZeroDepth maxProofDepth goal where - pickStrategy = - maybe strategy strategyWithMinDepth maybeMinDepth - - discardStrategy = snd - - handleLimitExceeded :: - Strategy.LimitExceeded (ProofDepth, CommonClaimState) -> - VerifierT simplifier a - handleLimitExceeded (Strategy.LimitExceeded states) = do - let extractStuckClaim = fmap StuckClaim . extractUnproven . snd - stuckClaims = mapMaybe extractStuckClaim states - Monad.Except.throwError (MultiAnd.make $ toList stuckClaims) - - -- updateQueue = \as -> - -- Strategy.unfoldSearchOrder searchOrder as - -- >=> lift . Strategy.applyBreadthLimit breadthLimit discardStrategy - -- >=> ( \queue -> - -- infoExecBreadth (ExecBreadth $ genericLength queue) - -- >> return queue - -- ) - -- where - -- genericLength = fromIntegral . length - - throwUnproven :: - LogicT (VerifierT simplifier) (ProofDepth, CommonClaimState) -> - VerifierT simplifier [ProofDepth] - throwUnproven acts = - do - (proofDepth, proofState) <- acts - let maybeUnproven = extractUnproven proofState - for_ maybeUnproven $ \unproven -> lift $ do - infoUnprovenDepth proofDepth - updateStuckClaimsState unproven maxCounterexamples - pure proofDepth - & Logic.observeAllT - >>= checkLeftUnproven - - checkLeftUnproven :: - [ProofDepth] -> - VerifierT simplifier [ProofDepth] - checkLeftUnproven depths = - do - stuck <- State.get - if (null stuck) - then pure depths - else Monad.Except.throwError stuck - - discardAppliedRules = map fst - - transit :: - Strategy Prim -> - (ProofDepth, ClaimState SomeClaim) -> - LogicT - (VerifierT simplifier) - [(ProofDepth, ClaimState SomeClaim)] - transit instr config = - Strategy.transitionRule - ( transitionRule' stuckCheck claims axioms - & trackProofDepth - & throwStuckClaims maxCounterexamples + -- TODO remove use of "Strategy", use stream/list directly + strategyToList :: Show prim => Strategy prim -> [prim] + strategyToList (Strategy.Seq a b) = strategyToList a <> strategyToList b + strategyToList (Strategy.Apply p) = [p] + strategyToList Strategy.Continue = [] + strategyToList other = error $ "strategyToList: " <> show other + + transition :: + ([X.Step], (ProofDepth, ClaimState SomeClaim)) -> + ExceptT + StuckClaims + simplifier + ( X.TransitionResult + ([X.Step], (ProofDepth, ClaimState SomeClaim)) + ) + transition = + ( X.simpleTransition + ( trackProofDepth $ + transitionRule' stuckCheck claims axioms ) - instr - config - & runTransitionT - & fmap discardAppliedRules - & traceProf ":transit" - & lift + toTransitionResultWithDepth + ) + + -- result interpretation for GraphTraversal.simpleTransition + toTransitionResultWithDepth :: + Show c => + -- | prior state, needed for [] and Proven cases + (ProofDepth, ClaimState c) -> + [(ProofDepth, ClaimState c)] -> + X.TransitionResult (ProofDepth, ClaimState c) + toTransitionResultWithDepth prior = \case + [] + | isJust (extractStuck $ snd prior) -> X.Stuck prior + | isJust (extractUnproven $ snd prior) -> X.Stopped prior + | otherwise -> X.Final prior -- FIXME ??? + [c@(_, ClaimState.Claimed{})] -> X.StraightLine c + [c@(_, ClaimState.Rewritten{})] -> X.StraightLine c + [c@(_, ClaimState.Remaining{})] -> X.StraightLine c + [c@(_, ClaimState.Stuck{})] -> X.Stuck c + [(_, ClaimState.Proven)] -> X.Final prior + cs@(c : cs') + | noneStuck (map snd cs) -> X.Branch prior (c :| cs') + | otherwise -> + -- FIXME Is it possible to get one stuck and one + -- non-stuck? + error $ "toTransitionResult: " <> show (prior, cs) + where + noneStuck :: [ClaimState c] -> Bool + noneStuck = null . mapMaybe ClaimState.extractStuck {- | Attempts to perform a single proof step, starting at the configuration in the execution graph designated by the provided node. Re-constructs the @@ -557,55 +485,6 @@ proveClaimStep _ stuckCheck claims axioms executionGraph node = | otherwise = transitionRule' stuckCheck claims axioms prim state --- | result interpretation for GraphTraversal.simpleTransition -toTransitionResult :: - Show c => - -- | prior state, needed for [] and Proven cases - ClaimState c -> - [ClaimState c] -> - X.TransitionResult (ClaimState c) -toTransitionResult prior = \case - [] -> X.Stuck prior - [c@ClaimState.Claimed{}] -> X.StraightLine c - [c@ClaimState.Rewritten{}] -> X.StraightLine c - [c@ClaimState.Remaining{}] -> X.StraightLine c - [c@ClaimState.Stuck{}] -> X.Stuck c - [ClaimState.Proven] -> X.Final prior - cs@(c : cs') - | noneStuck cs -> X.Branch prior (c :| cs') - | otherwise -> - -- FIXME Is it possible to get one stuck and one non-stuck? - error $ "toTransitionResult: " <> show (prior, cs) - where - noneStuck :: [ClaimState c] -> Bool - noneStuck = null . mapMaybe ClaimState.extractStuck - --- could be solved with Data.Tuple.Extra.secondM if there wasn't the prior state -toTransitionResultWithDepth :: - Show c => - -- | prior state, needed for [] and Proven cases - (ProofDepth, ClaimState c) -> - [(ProofDepth, ClaimState c)] -> - X.TransitionResult (ProofDepth, ClaimState c) -toTransitionResultWithDepth prior = \case - [] - | isJust (extractStuck $ snd prior) -> X.Stuck prior - | isJust (extractUnproven $ snd prior) -> X.Stopped prior - | otherwise -> X.Final prior -- FIXME ??? - [c@(_, ClaimState.Claimed{})] -> X.StraightLine c - [c@(_, ClaimState.Rewritten{})] -> X.StraightLine c - [c@(_, ClaimState.Remaining{})] -> X.StraightLine c - [c@(_, ClaimState.Stuck{})] -> X.Stuck c - [(_, ClaimState.Proven)] -> X.Final prior - cs@(c : cs') - | noneStuck (map snd cs) -> X.Branch prior (c :| cs') - | otherwise -> - -- FIXME Is it possible to get one stuck and one non-stuck? - error $ "toTransitionResult: " <> show (prior, cs) - where - noneStuck :: [ClaimState c] -> Bool - noneStuck = null . mapMaybe ClaimState.extractStuck - transitionRule' :: MonadSimplify simplifier => MonadProf simplifier => @@ -693,42 +572,6 @@ checkStuckConfiguration rule prim proofState = do isNot_Ceil_ (PredicateNot (PredicateCeil _)) = True isNot_Ceil_ _ = False --- | Terminate the prover after 'maxCounterexamples' stuck steps. -throwStuckClaims :: - forall m rule. - MonadLog m => - Natural -> - TransitionRule - (VerifierT m) - rule - (ProofDepth, ClaimState SomeClaim) -> - TransitionRule - (VerifierT m) - rule - (ProofDepth, ClaimState SomeClaim) -throwStuckClaims maxCounterexamples rule prim state = do - state'@(proofDepth', proofState') <- rule prim state - case proofState' of - ClaimState.Stuck unproven -> do - lift $ do - infoUnprovenDepth proofDepth' - updateStuckClaimsState unproven maxCounterexamples - return state' - _ -> return state' - -updateStuckClaimsState :: - Monad m => - SomeClaim -> - Natural -> - VerifierT m () -updateStuckClaimsState unproven maxCounterexamples = do - stuckClaims <- State.get - let updatedStuck = - MultiAnd.singleton (StuckClaim unproven) <> stuckClaims - when (MultiAnd.size updatedStuck >= maxCounterexamples) $ do - Monad.Except.throwError updatedStuck - State.put updatedStuck - -- | Modify a 'TransitionRule' to track the depth of a proof. trackProofDepth :: forall m rule goal. From 10910404a709cb4e0e0bd61aae057fa5ec05ba17 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Mon, 25 Jul 2022 11:50:47 +1000 Subject: [PATCH 23/33] remove Strategy.And and Strategy.Or, unused --- kore/src/Kore/Reachability/Prove.hs | 1 - kore/src/Kore/Rewrite/Strategy.hs | 122 ------------------------ kore/test/Test/Kore/Rewrite.hs | 7 -- kore/test/Test/Kore/Rewrite/Strategy.hs | 95 +----------------- 4 files changed, 1 insertion(+), 224 deletions(-) diff --git a/kore/src/Kore/Reachability/Prove.hs b/kore/src/Kore/Reachability/Prove.hs index ae9bbaa81a..2efd239fc0 100644 --- a/kore/src/Kore/Reachability/Prove.hs +++ b/kore/src/Kore/Reachability/Prove.hs @@ -380,7 +380,6 @@ proveClaim strategyToList (Strategy.Seq a b) = strategyToList a <> strategyToList b strategyToList (Strategy.Apply p) = [p] strategyToList Strategy.Continue = [] - strategyToList other = error $ "strategyToList: " <> show other transition :: ([X.Step], (ProofDepth, ClaimState SomeClaim)) -> diff --git a/kore/src/Kore/Rewrite/Strategy.hs b/kore/src/Kore/Rewrite/Strategy.hs index e24ffcbe7f..c21de2caff 100644 --- a/kore/src/Kore/Rewrite/Strategy.hs +++ b/kore/src/Kore/Rewrite/Strategy.hs @@ -13,18 +13,9 @@ import Kore.Rewrite.Strategy qualified as Strategy module Kore.Rewrite.Strategy ( -- * Strategies Strategy (..), - and, - all, - or, - try, - first, - any, - many, - some, apply, seq, sequence, - stuck, continue, -- * Running strategies @@ -93,14 +84,8 @@ import GHC.Generics qualified as GHC import Kore.Rewrite.Transition import Numeric.Natural import Prelude.Kore hiding ( - all, - and, - any, - many, - or, seq, sequence, - some, ) {- | An execution strategy. @@ -108,25 +93,11 @@ import Prelude.Kore hiding ( @Strategy prim@ represents a strategy for execution by applying rewrite axioms of type @prim@. -} - --- TODO (thomas.tuegel): This could be implemented as an algebra so that a --- strategy is a free monad over the primitive rule type and the result of --- execution is not a generic tree, but a cofree comonad with exactly the --- branching structure described by the strategy algebra. data Strategy prim where - -- The recursive arguments of these constructors are /intentionally/ lazy to - -- allow strategies to loop. - -- | Apply two strategies in sequence. Seq :: Strategy prim -> Strategy prim -> Strategy prim - -- | Apply both strategies to the same configuration, i.e. in parallel. - And :: Strategy prim -> Strategy prim -> Strategy prim - -- | Apply the second strategy if the first fails to produce children. - Or :: Strategy prim -> Strategy prim -> Strategy prim -- | Apply the rewrite rule, then advance to the next strategy. Apply :: !prim -> Strategy prim - -- | @Stuck@ produces no children. - Stuck :: Strategy prim -- | @Continue@ produces one child identical to its parent. Continue :: Strategy prim deriving stock (Eq, Show, Functor) @@ -148,54 +119,6 @@ sequence [] === continue sequence :: [Strategy prim] -> Strategy prim sequence = foldr seq continue --- | Apply both strategies to the same configuration, i.e. in parallel. -and :: Strategy prim -> Strategy prim -> Strategy prim -and = And - -{- | Apply all of the strategies in parallel. - -@ -all [] === stuck -@ --} -all :: [Strategy prim] -> Strategy prim -all = foldr and stuck - -{- | Apply the second strategy if the first fails immediately. - -A strategy is considered successful if it produces any children. --} -or :: Strategy prim -> Strategy prim -> Strategy prim -or = Or - -{- | Apply the given strategies in order until one succeeds. - -A strategy is considered successful if it produces any children. - -@ -any [] === stuck -@ --} -first :: [Strategy prim] -> Strategy prim -first = foldr or stuck - -any :: [Strategy prim] -> Strategy prim -any = first - --- | Attempt the given strategy once. -try :: Strategy prim -> Strategy prim -try strategy = or strategy continue - --- | Apply the strategy zero or more times. -many :: Strategy prim -> Strategy prim -many strategy = many0 - where - many0 = or (seq strategy many0) continue - --- | Apply the strategy one or more times. -some :: Strategy prim -> Strategy prim -some strategy = seq strategy (many strategy) - -- | Apply the rewrite rule, then advance to the next strategy. apply :: -- | rule @@ -203,32 +126,6 @@ apply :: Strategy prim apply = Apply -{- | Produce no children; the end of all strategies. - -@stuck@ does not necessarily indicate unsuccessful termination, but it -is not generally possible to determine if one branch of execution is -successful without looking at all the branches. - -@stuck@ is the annihilator of 'seq': -@ -seq stuck a === stuck -seq a stuck === stuck -@ - -@stuck@ is the identity of 'and': -@ -and stuck a === a -and a stuck === a -@ - -@stuck@ is the left-identity of 'or': -@ -or stuck a === a -@ --} -stuck :: Strategy prim -stuck = Stuck - {- | Produce one child identical to its parent. @continue@ is the identity of 'seq': @@ -562,7 +459,6 @@ unfoldTransition transit (instrs, config) = -- | Transition rule for running a 'Strategy'. transitionRule :: - Monad m => -- | Primitive strategy rule (prim -> config -> TransitionT rule m config) -> (Strategy prim -> config -> TransitionT rule m config) @@ -571,14 +467,8 @@ transitionRule applyPrim = transitionRule0 transitionRule0 = \case Seq instr1 instr2 -> transitionSeq instr1 instr2 - And instr1 instr2 -> transitionAnd instr1 instr2 - Or instr1 instr2 -> transitionOr instr1 instr2 Apply prim -> transitionApply prim Continue -> transitionContinue - Stuck -> transitionStuck - - -- End execution. - transitionStuck _ = empty transitionContinue result = return result @@ -586,18 +476,6 @@ transitionRule applyPrim = transitionRule0 transitionSeq instr1 instr2 = transitionRule0 instr1 >=> transitionRule0 instr2 - -- Attempt both instructions, i.e. create a branch for each. - transitionAnd instr1 instr2 config = - transitionRule0 instr1 config <|> transitionRule0 instr2 config - - -- Attempt the first instruction. Fall back to the second if it is - -- unsuccessful. - transitionOr instr1 instr2 config = do - results <- tryTransitionT (transitionRule0 instr1 config) - case results of - [] -> transitionRule0 instr2 config - _ -> scatter results - -- Apply a primitive rule. Throw an exception if the rule is not successful. transitionApply = applyPrim diff --git a/kore/test/Test/Kore/Rewrite.hs b/kore/test/Test/Kore/Rewrite.hs index ff5ee22580..7767dc2435 100644 --- a/kore/test/Test/Kore/Rewrite.hs +++ b/kore/test/Test/Kore/Rewrite.hs @@ -317,21 +317,14 @@ test_executionStrategy = hasRewrite :: Strategy Prim -> Bool hasRewrite = \case Strategy.Seq s1 s2 -> hasRewrite s1 || hasRewrite s2 - Strategy.And s1 s2 -> hasRewrite s1 || hasRewrite s2 - Strategy.Or s1 s2 -> hasRewrite s1 || hasRewrite s2 Strategy.Apply p -> p == Rewrite - Strategy.Stuck -> False Strategy.Continue -> False isLastSimplify :: Strategy Prim -> Bool isLastSimplify = \case Strategy.Seq s Strategy.Continue -> isLastSimplify s - Strategy.Seq s Strategy.Stuck -> isLastSimplify s Strategy.Seq _ s -> isLastSimplify s - Strategy.And s1 s2 -> isLastSimplify s1 && isLastSimplify s2 - Strategy.Or s1 s2 -> isLastSimplify s1 && isLastSimplify s2 Strategy.Apply p -> p == Simplify - Strategy.Stuck -> False Strategy.Continue -> False simpleRewrite :: diff --git a/kore/test/Test/Kore/Rewrite/Strategy.hs b/kore/test/Test/Kore/Rewrite/Strategy.hs index 4f9b598f34..8f15caecb7 100644 --- a/kore/test/Test/Kore/Rewrite/Strategy.hs +++ b/kore/test/Test/Kore/Rewrite/Strategy.hs @@ -3,13 +3,7 @@ module Test.Kore.Rewrite.Strategy ( prop_SeqContinueIdentity, - prop_SeqStuckDominate, - prop_AndStuckIdentity, - prop_OrStuckIdentity, - prop_Stuck, prop_Continue, - test_And, - test_Or, prop_depthLimit, prop_pickLongest, prop_pickFinal, @@ -44,8 +38,6 @@ import Prelude.Kore hiding ( seq, ) import Test.QuickCheck.Instances () -import Test.Tasty -import Test.Tasty.HUnit import Test.Tasty.QuickCheck data Prim @@ -67,10 +59,8 @@ instance Arbitrary Prim where instance Arbitrary prim => Arbitrary (Strategy prim) where arbitrary = do ~s <- Strategy.seq <$> arbitrary <*> arbitrary - ~a <- Strategy.and <$> arbitrary <*> arbitrary - ~o <- Strategy.or <$> arbitrary <*> arbitrary ~p <- Strategy.apply <$> arbitrary - elements [s, a, o, p, Strategy.stuck, Strategy.continue] + elements [s, p, Strategy.continue] shrink = \case @@ -78,16 +68,7 @@ instance Arbitrary prim => Arbitrary (Strategy prim) where [a, b] ++ (Strategy.Seq <$> shrink a <*> pure b) ++ (Strategy.Seq a <$> shrink b) - Strategy.And a b -> - [a, b] - ++ (Strategy.And <$> shrink a <*> pure b) - ++ (Strategy.And a <$> shrink b) - Strategy.Or a b -> - [a, b] - ++ (Strategy.Or <$> shrink a <*> pure b) - ++ (Strategy.Or a <$> shrink b) Strategy.Apply _ -> [] - Strategy.Stuck -> [] Strategy.Continue -> [] transitionPrim :: Prim -> Natural -> TransitionT Prim Catch Natural @@ -104,24 +85,9 @@ apply = Strategy.apply seq :: Strategy Prim -> Strategy Prim -> Strategy Prim seq = Strategy.seq -and :: Strategy Prim -> Strategy Prim -> Strategy Prim -and = Strategy.and - -or :: Strategy Prim -> Strategy Prim -> Strategy Prim -or = Strategy.or - -stuck :: Strategy Prim -stuck = Strategy.stuck - continue :: Strategy Prim continue = Strategy.continue -throw :: Strategy Prim -throw = apply Throw - -const :: Natural -> Strategy Prim -const = apply . Const - succ_ :: Strategy Prim succ_ = apply Succ @@ -141,33 +107,6 @@ prop_SeqContinueIdentity a n = right = runStrategy [seq a continue] n in (expect === left) .&&. (expect === right) -prop_SeqStuckDominate :: Strategy Prim -> Natural -> Property -prop_SeqStuckDominate a n = - let expect = runStrategy [stuck] n - left = runStrategy [seq stuck a] n - right = runStrategy [seq a stuck] n - in (expect === left) .&&. (expect === right) - -prop_AndStuckIdentity :: Strategy Prim -> Natural -> Property -prop_AndStuckIdentity a n = - let expect = runStrategy [a] n - left = runStrategy [and stuck a] n - right = runStrategy [and a stuck] n - in (expect === left) .&&. (expect === right) - -prop_OrStuckIdentity :: Strategy Prim -> Natural -> Property -prop_OrStuckIdentity a n = - let expect = runStrategy [a] n - left = runStrategy [or stuck a] n - right = runStrategy [or a stuck] n - in (expect === left) .&&. (expect === right) - -prop_Stuck :: Natural -> Property -prop_Stuck n = - let expect = Graph.mkGraph [(0, n)] [] - actual = Strategy.graph $ runStrategy [stuck] n - in expect === actual - prop_Continue :: Natural -> Property prop_Continue n = let expect = @@ -177,38 +116,6 @@ prop_Continue n = actual = Strategy.graph $ runStrategy [continue] n in expect === actual -test_And :: [TestTree] -test_And = - let expect = - Graph.mkGraph - [(0, 0), (1, 1)] - [(0, 1, Seq.fromList [Const 1])] - in [ testCase "Stuck on left" $ do - let strategy = [and stuck (const 1)] - actual = Strategy.graph $ runStrategy strategy 0 - expect @=? actual - , testCase "Stuck on right" $ do - let strategy = [and (const 1) stuck] - actual = Strategy.graph $ runStrategy strategy 0 - expect @=? actual - ] - -test_Or :: [TestTree] -test_Or = - let expect = - Graph.mkGraph - [(0, 0), (1, 1)] - [(0, 1, Seq.fromList [Const 1])] - in [ testCase "Throw on left" $ do - let strategy = [or throw (const 1)] - actual = Strategy.graph $ runStrategy strategy 0 - expect @=? actual - , testCase "Throw on right" $ do - let strategy = [or (const 1) throw] - actual = Strategy.graph $ runStrategy strategy 0 - expect @=? actual - ] - prop_depthLimit :: Integer -> Property prop_depthLimit i = (i >= 0) ==> (expect === actual) From 69dcea7642cd397785649839413ef5dde0da2085 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Mon, 25 Jul 2022 12:03:18 +1000 Subject: [PATCH 24/33] rearrange end of ProofClaim --- kore/src/Kore/Reachability/Prove.hs | 42 ++++++++++++++--------------- 1 file changed, 20 insertions(+), 22 deletions(-) diff --git a/kore/src/Kore/Reachability/Prove.hs b/kore/src/Kore/Reachability/Prove.hs index 2efd239fc0..743f25198f 100644 --- a/kore/src/Kore/Reachability/Prove.hs +++ b/kore/src/Kore/Reachability/Prove.hs @@ -352,28 +352,26 @@ proveClaim let throwStuckClaims = Monad.Except.throwError . MultiAnd.make . map StuckClaim - proofDepths <- - -- Semantics of TraversalResult (failure cases): - -- - When `GotStuck` is returned, the returned results - -- are considered stuck and thrown as an exception; - -- - when `Aborted` is returned, the returned results - -- are _analysed_ and their _next_ states (to - -- enqueue) are considered stuck and thrown. - case traversalResult of - X.GotStuck _n rs -> - throwStuckClaims $ - -- return _given_ states (considered stuck) when GotStuck - mapMaybe (X.extractState >=> extractUnproven . snd) rs - X.Aborted _n rs -> - throwStuckClaims $ - -- return _next_ states when Aborted - concatMap (mapMaybe (extractUnproven . snd) . X.extractNext) rs - X.Ended results -> - pure (mapMaybe (fmap fst . X.extractState) results) - - let maxProofDepth = sconcat (ProofDepth 0 :| proofDepths) - infoProvenDepth maxProofDepth - warnProvenClaimZeroDepth maxProofDepth goal + -- Semantics of TraversalResult (failure cases): + -- - When `GotStuck` is returned, the returned results + -- are considered stuck and thrown as an exception; + -- - when `Aborted` is returned, the returned results + -- are _analysed_ and their _next_ states (to + -- enqueue) are considered stuck and thrown. + case traversalResult of + X.GotStuck _n rs -> + throwStuckClaims $ + -- return _given_ states (considered stuck) when GotStuck + mapMaybe (X.extractState >=> extractUnproven . snd) rs + X.Aborted _n rs -> + throwStuckClaims $ + -- return _next_ states when Aborted + concatMap (mapMaybe (extractUnproven . snd) . X.extractNext) rs + X.Ended results -> do + let depths = mapMaybe (fmap fst . X.extractState) results + maxProofDepth = sconcat (ProofDepth 0 :| depths) + infoProvenDepth maxProofDepth + warnProvenClaimZeroDepth maxProofDepth goal where -- TODO remove use of "Strategy", use stream/list directly strategyToList :: Show prim => Strategy prim -> [prim] From b79fa99e47baa49cb2a0ffadfa3d99c44f42735d Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Mon, 25 Jul 2022 12:29:22 +1000 Subject: [PATCH 25/33] throw out Strategy type for new traversal --- kore/src/Kore/Reachability/Prove.hs | 36 ++++++++++++++++++++--------- 1 file changed, 25 insertions(+), 11 deletions(-) diff --git a/kore/src/Kore/Reachability/Prove.hs b/kore/src/Kore/Reachability/Prove.hs index 743f25198f..7ae4fa9b8d 100644 --- a/kore/src/Kore/Reachability/Prove.hs +++ b/kore/src/Kore/Reachability/Prove.hs @@ -95,7 +95,7 @@ import Kore.Reachability.ClaimState ( extractUnproven, ) import Kore.Reachability.ClaimState qualified as ClaimState -import Kore.Reachability.Prim qualified as Prim ( +import Kore.Reachability.Prim as Prim ( Prim (..), ) import Kore.Reachability.SomeClaim @@ -330,12 +330,11 @@ proveClaim traceExceptT D_OnePath_verifyClaim [debugArg "rule" goal] $ do let startGoal = ClaimState.Claimed (Lens.over lensClaimPattern mkGoal goal) - pickStrategy = - maybe strategy strategyWithMinDepth maybeMinDepth - limitedStrategyList = - map strategyToList (Limit.takeWithin depthLimit $ toList pickStrategy) - `snoc` (strategyToList reachabilityCheckOnly) + Limit.takeWithin + depthLimit + (maybe infinite withMinDepth maybeMinDepth) + `snoc` [Begin, CheckImplication] -- last step of limited step stopOnBranches = \case Strategy.Leaf -> const False @@ -373,11 +372,26 @@ proveClaim infoProvenDepth maxProofDepth warnProvenClaimZeroDepth maxProofDepth goal where - -- TODO remove use of "Strategy", use stream/list directly - strategyToList :: Show prim => Strategy prim -> [prim] - strategyToList (Strategy.Seq a b) = strategyToList a <> strategyToList b - strategyToList (Strategy.Apply p) = [p] - strategyToList Strategy.Continue = [] + ------------------------------- + -- brought in from Claim.hs to remove Strategy type + infinite :: [X.Step] + ~infinite = stepNoClaims : repeat stepWithClaims + + withMinDepth :: MinDepth -> [X.Step] + withMinDepth d = + noCheckSteps <> repeat stepWithClaims + where + noCheckSteps = + [Begin, Simplify, ApplyAxioms, Simplify] : + replicate + (getMinDepth d - 1) + [Begin, Simplify, ApplyAxioms, ApplyClaims, Simplify] + + stepNoClaims = + [Begin, Simplify, CheckImplication, ApplyAxioms, Simplify] + stepWithClaims = + [Begin, Simplify, CheckImplication, ApplyClaims, ApplyAxioms, Simplify] + ------------------------------- transition :: ([X.Step], (ProofDepth, ClaimState SomeClaim)) -> From c06ac839f6601c9947af683bfcb0a443d9da9fa9 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Mon, 25 Jul 2022 13:11:15 +1000 Subject: [PATCH 26/33] remove ExceptT from proveClaim graph traversal --- kore/src/Kore/Reachability/Prove.hs | 137 ++++++++++++++-------------- 1 file changed, 67 insertions(+), 70 deletions(-) diff --git a/kore/src/Kore/Reachability/Prove.hs b/kore/src/Kore/Reachability/Prove.hs index 7ae4fa9b8d..d04b91a6fa 100644 --- a/kore/src/Kore/Reachability/Prove.hs +++ b/kore/src/Kore/Reachability/Prove.hs @@ -285,19 +285,25 @@ proveClaimsWorker verifyWorker :: (SomeClaim, Limit Natural) -> VerifierT (StateT ProvenClaims simplifier) () - verifyWorker unprovenClaim@(claim, _) = do - debugBeginClaim claim - proveClaim - maybeMinDepth - stuckCheck - breadthLimit - searchOrder - maxCounterexamples - finalNodeType - claims - axioms - unprovenClaim - addProvenClaim claim + verifyWorker unprovenClaim@(claim, _) = + traceExceptT D_OnePath_verifyClaim [debugArg "rule" claim] $ do + debugBeginClaim claim + result <- + proveClaim + maybeMinDepth + stuckCheck + breadthLimit + searchOrder + maxCounterexamples + finalNodeType + claims + axioms + unprovenClaim + either + -- throw stuck claims, ending the traversal + Monad.Except.throwError + (const $ addProvenClaim claim) + result addProvenClaim claim = State.modify' (mappend (MultiAnd.singleton claim)) @@ -316,7 +322,7 @@ proveClaim :: AllClaims SomeClaim -> Axioms SomeClaim -> (SomeClaim, Limit Natural) -> - VerifierT simplifier () + simplifier (Either StuckClaims ()) proveClaim maybeMinDepth stuckCheck @@ -326,51 +332,50 @@ proveClaim finalNodeType (AllClaims claims) (Axioms axioms) - (goal, depthLimit) = - traceExceptT D_OnePath_verifyClaim [debugArg "rule" goal] $ do - let startGoal = ClaimState.Claimed (Lens.over lensClaimPattern mkGoal goal) - - limitedStrategyList = - Limit.takeWithin - depthLimit - (maybe infinite withMinDepth maybeMinDepth) - `snoc` [Begin, CheckImplication] -- last step of limited step - - stopOnBranches = \case - Strategy.Leaf -> const False - Strategy.LeafOrBranching -> X.isBranch - - traversalResult <- - X.transitionLeaves - [stopOnBranches finalNodeType, X.isTerminal, X.isCut] -- future work - searchOrder - breadthLimit - transition - maxCounterexamples - (limitedStrategyList, (ProofDepth 0, startGoal)) - - let throwStuckClaims = - Monad.Except.throwError . MultiAnd.make . map StuckClaim - -- Semantics of TraversalResult (failure cases): - -- - When `GotStuck` is returned, the returned results - -- are considered stuck and thrown as an exception; - -- - when `Aborted` is returned, the returned results - -- are _analysed_ and their _next_ states (to - -- enqueue) are considered stuck and thrown. - case traversalResult of - X.GotStuck _n rs -> - throwStuckClaims $ - -- return _given_ states (considered stuck) when GotStuck - mapMaybe (X.extractState >=> extractUnproven . snd) rs - X.Aborted _n rs -> - throwStuckClaims $ - -- return _next_ states when Aborted - concatMap (mapMaybe (extractUnproven . snd) . X.extractNext) rs - X.Ended results -> do - let depths = mapMaybe (fmap fst . X.extractState) results - maxProofDepth = sconcat (ProofDepth 0 :| depths) - infoProvenDepth maxProofDepth - warnProvenClaimZeroDepth maxProofDepth goal + (goal, depthLimit) = do + let startGoal = ClaimState.Claimed (Lens.over lensClaimPattern mkGoal goal) + + limitedStrategyList = + Limit.takeWithin + depthLimit + (maybe infinite withMinDepth maybeMinDepth) + `snoc` [Begin, CheckImplication] -- last step of limited step + stopOnBranches = \case + Strategy.Leaf -> const False + Strategy.LeafOrBranching -> X.isBranch + + traversalResult <- + X.transitionLeaves + [stopOnBranches finalNodeType, X.isTerminal, X.isCut] -- future work + searchOrder + breadthLimit + transition + maxCounterexamples + (limitedStrategyList, (ProofDepth 0, startGoal)) + + let returnStuckClaims = + pure . Left . MultiAnd.make . map StuckClaim + -- Semantics of TraversalResult (failure cases): + -- - When `GotStuck` is returned, the returned results + -- are considered stuck and thrown as an exception; + -- - when `Aborted` is returned, the returned results + -- are _analysed_ and their _next_ states (to + -- enqueue) are considered stuck and thrown. + case traversalResult of + X.GotStuck _n rs -> + returnStuckClaims $ + -- return _given_ states (considered stuck) when GotStuck + mapMaybe (X.extractState >=> extractUnproven . snd) rs + X.Aborted _n rs -> + returnStuckClaims $ + -- return _next_ states when Aborted + concatMap (mapMaybe (extractUnproven . snd) . X.extractNext) rs + X.Ended results -> do + let depths = mapMaybe (fmap fst . X.extractState) results + maxProofDepth = sconcat (ProofDepth 0 :| depths) + infoProvenDepth maxProofDepth + warnProvenClaimZeroDepth maxProofDepth goal + pure $ Right () where ------------------------------- -- brought in from Claim.hs to remove Strategy type @@ -395,19 +400,11 @@ proveClaim transition :: ([X.Step], (ProofDepth, ClaimState SomeClaim)) -> - ExceptT - StuckClaims - simplifier - ( X.TransitionResult - ([X.Step], (ProofDepth, ClaimState SomeClaim)) - ) + simplifier (X.TransitionResult ([X.Step], (ProofDepth, ClaimState SomeClaim))) transition = - ( X.simpleTransition - ( trackProofDepth $ - transitionRule' stuckCheck claims axioms - ) + X.simpleTransition + (trackProofDepth $ transitionRule' stuckCheck claims axioms) toTransitionResultWithDepth - ) -- result interpretation for GraphTraversal.simpleTransition toTransitionResultWithDepth :: From 3d7080dadca4670e3517b381b9ae79b2d4e134f3 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Mon, 25 Jul 2022 13:24:34 +1000 Subject: [PATCH 27/33] use Simplifier monad directly in Prove.hs --- kore/src/Kore/Reachability/Prove.hs | 44 +++++++++++------------------ 1 file changed, 17 insertions(+), 27 deletions(-) diff --git a/kore/src/Kore/Reachability/Prove.hs b/kore/src/Kore/Reachability/Prove.hs index d04b91a6fa..5ccce92256 100644 --- a/kore/src/Kore/Reachability/Prove.hs +++ b/kore/src/Kore/Reachability/Prove.hs @@ -118,6 +118,7 @@ import Kore.Rewrite.Transition ( runTransitionT, ) import Kore.Rewrite.Transition qualified as Transition +import Kore.Simplify.Data (Simplifier) import Kore.Simplify.Simplify import Kore.TopBottom import Kore.Unparser @@ -190,10 +191,6 @@ data ProveClaimsResult = ProveClaimsResult } proveClaims :: - forall simplifier. - MonadMask simplifier => - MonadSimplify simplifier => - MonadProf simplifier => Maybe MinDepth -> StuckCheck -> Limit Natural -> @@ -206,7 +203,7 @@ proveClaims :: -- | List of claims, together with a maximum number of verification steps -- for each. ToProve SomeClaim -> - simplifier ProveClaimsResult + Simplifier ProveClaimsResult proveClaims maybeMinDepth stuckCheck @@ -254,10 +251,6 @@ proveClaims else Left claim proveClaimsWorker :: - forall simplifier. - MonadSimplify simplifier => - MonadMask simplifier => - MonadProf simplifier => Maybe MinDepth -> StuckCheck -> Limit Natural -> @@ -269,7 +262,7 @@ proveClaimsWorker :: -- | List of claims, together with a maximum number of verification steps -- for each. ToProve SomeClaim -> - VerifierT (StateT ProvenClaims simplifier) () + VerifierT (StateT ProvenClaims Simplifier) () proveClaimsWorker maybeMinDepth stuckCheck @@ -284,21 +277,22 @@ proveClaimsWorker where verifyWorker :: (SomeClaim, Limit Natural) -> - VerifierT (StateT ProvenClaims simplifier) () + VerifierT (StateT ProvenClaims Simplifier) () verifyWorker unprovenClaim@(claim, _) = traceExceptT D_OnePath_verifyClaim [debugArg "rule" claim] $ do debugBeginClaim claim result <- - proveClaim - maybeMinDepth - stuckCheck - breadthLimit - searchOrder - maxCounterexamples - finalNodeType - claims - axioms - unprovenClaim + lift . lift $ + proveClaim + maybeMinDepth + stuckCheck + breadthLimit + searchOrder + maxCounterexamples + finalNodeType + claims + axioms + unprovenClaim either -- throw stuck claims, ending the traversal Monad.Except.throwError @@ -309,10 +303,6 @@ proveClaimsWorker State.modify' (mappend (MultiAnd.singleton claim)) proveClaim :: - forall simplifier. - MonadSimplify simplifier => - MonadMask simplifier => - MonadProf simplifier => Maybe MinDepth -> StuckCheck -> Limit Natural -> @@ -322,7 +312,7 @@ proveClaim :: AllClaims SomeClaim -> Axioms SomeClaim -> (SomeClaim, Limit Natural) -> - simplifier (Either StuckClaims ()) + Simplifier (Either StuckClaims ()) proveClaim maybeMinDepth stuckCheck @@ -400,7 +390,7 @@ proveClaim transition :: ([X.Step], (ProofDepth, ClaimState SomeClaim)) -> - simplifier (X.TransitionResult ([X.Step], (ProofDepth, ClaimState SomeClaim))) + Simplifier (X.TransitionResult ([X.Step], (ProofDepth, ClaimState SomeClaim))) transition = X.simpleTransition (trackProofDepth $ transitionRule' stuckCheck claims axioms) From 3719858c6c6ab128db628632ae26e30c8f61d88e Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Mon, 25 Jul 2022 13:28:40 +1000 Subject: [PATCH 28/33] specialise GraphTraversal to Simplifer monad --- kore/src/GraphTraversal.hs | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/kore/src/GraphTraversal.hs b/kore/src/GraphTraversal.hs index 41cf79e00e..ba231ac29d 100644 --- a/kore/src/GraphTraversal.hs +++ b/kore/src/GraphTraversal.hs @@ -25,6 +25,7 @@ import Kore.Rewrite.Strategy ( runTransitionT, unfoldSearchOrder, ) +import Kore.Simplify.Data (Simplifier) import Prelude.Kore import Pretty @@ -126,8 +127,7 @@ type Step = [Prim] ---------------------------------------- transitionLeaves :: - forall m c. - (Monad m) => + forall c. -- | Stop critera, in terms of 'TransitionResult's. The algorithm -- will _always_ stop on 'Stuck' and 'Final', so [isTerminal, -- isCut, isBranch] could be used here. Could simplify this to @@ -142,14 +142,14 @@ transitionLeaves :: -- | breadth limit, essentially a natural number Limit Natural -> -- | transition function - (([Step], c) -> m (TransitionResult ([Step], c))) -> + (([Step], c) -> Simplifier (TransitionResult ([Step], c))) -> -- again, m is probably only for logging -- | max-counterexamples, included in the internal logic Natural -> -- | initial node ([Step], c) -> - m (TraversalResult c) + Simplifier (TraversalResult c) transitionLeaves stopCriteria direction @@ -164,7 +164,7 @@ transitionLeaves where enqueue' = unfoldSearchOrder direction - enqueue :: [([Step], c)] -> Seq ([Step], c) -> m (Either (LimitExceeded ([Step], c)) (Seq ([Step], c))) + enqueue :: [([Step], c)] -> Seq ([Step], c) -> Simplifier (Either (LimitExceeded ([Step], c)) (Seq ([Step], c))) enqueue as q = do newQ <- enqueue' as q pure $ @@ -180,7 +180,7 @@ transitionLeaves maxStuck = fromIntegral maxCounterExamples - worker :: Seq ([Step], c) -> StateT [TransitionResult ([Step], c)] m (TraversalResult ([Step], c)) + worker :: Seq ([Step], c) -> StateT [TransitionResult ([Step], c)] Simplifier (TraversalResult ([Step], c)) worker Seq.Empty = Ended . reverse <$> get worker (a :<| as) = do result <- lift $ step a as @@ -203,7 +203,7 @@ transitionLeaves step :: ([Step], c) -> Seq ([Step], c) -> - m (StepResult ([Step], c)) + Simplifier (StepResult ([Step], c)) step a q = do next <- transit a if (isStuck next || isFinal next || isStopped next || shouldStop next) From 85cd6c153abca4ed2f250629176e8026b7489a94 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Mon, 25 Jul 2022 17:36:54 +1000 Subject: [PATCH 29/33] Generalise primitive "strategy" (step atom) for use in Exec --- kore/src/GraphTraversal.hs | 47 +++++++++++++++++------------ kore/src/Kore/Reachability/Prove.hs | 8 ++--- 2 files changed, 32 insertions(+), 23 deletions(-) diff --git a/kore/src/GraphTraversal.hs b/kore/src/GraphTraversal.hs index ba231ac29d..55b8314267 100644 --- a/kore/src/GraphTraversal.hs +++ b/kore/src/GraphTraversal.hs @@ -9,6 +9,7 @@ module GraphTraversal ( module GraphTraversal, ) where +import Control.Monad (foldM) import Control.Monad.Logic import Control.Monad.Trans.State import Data.Limit @@ -123,16 +124,16 @@ extractState = \case Terminal a -> Just a Cut a _ -> Just a -type Step = [Prim] +type Step prim = [prim] ---------------------------------------- transitionLeaves :: - forall c. + forall c prim. -- | Stop critera, in terms of 'TransitionResult's. The algorithm -- will _always_ stop on 'Stuck' and 'Final', so [isTerminal, -- isCut, isBranch] could be used here. Could simplify this to -- FinalNodeType - [TransitionResult ([Step], c) -> Bool] -> + [TransitionResult ([Step prim], c) -> Bool] -> -- queue updating parameters, -- we construct enqueue :: [a] -> Seq a -> m (Either LimitExceeded (Seq a)) from it -- m is probably only there for logging purposes @@ -142,13 +143,13 @@ transitionLeaves :: -- | breadth limit, essentially a natural number Limit Natural -> -- | transition function - (([Step], c) -> Simplifier (TransitionResult ([Step], c))) -> + (([Step prim], c) -> Simplifier (TransitionResult ([Step prim], c))) -> -- again, m is probably only for logging -- | max-counterexamples, included in the internal logic Natural -> -- | initial node - ([Step], c) -> + ([Step prim], c) -> Simplifier (TraversalResult c) transitionLeaves stopCriteria @@ -164,7 +165,10 @@ transitionLeaves where enqueue' = unfoldSearchOrder direction - enqueue :: [([Step], c)] -> Seq ([Step], c) -> Simplifier (Either (LimitExceeded ([Step], c)) (Seq ([Step], c))) + enqueue :: + [([Step prim], c)] -> + Seq ([Step prim], c) -> + Simplifier (Either (LimitExceeded ([Step prim], c)) (Seq ([Step prim], c))) enqueue as q = do newQ <- enqueue' as q pure $ @@ -172,15 +176,20 @@ transitionLeaves then Left (LimitExceeded newQ) else Right newQ - exceedsLimit :: Seq ([Step], c) -> Bool + exceedsLimit :: Seq ([Step prim], c) -> Bool exceedsLimit = not . withinLimit breadthLimit . fromIntegral . Seq.length - shouldStop :: TransitionResult ([Step], c) -> Bool + shouldStop :: TransitionResult ([Step prim], c) -> Bool shouldStop result = any ($ result) stopCriteria maxStuck = fromIntegral maxCounterExamples - worker :: Seq ([Step], c) -> StateT [TransitionResult ([Step], c)] Simplifier (TraversalResult ([Step], c)) + worker :: + Seq ([Step prim], c) -> + StateT + [TransitionResult ([Step prim], c)] + Simplifier + (TraversalResult ([Step prim], c)) worker Seq.Empty = Ended . reverse <$> get worker (a :<| as) = do result <- lift $ step a as @@ -201,9 +210,9 @@ transitionLeaves pure $ Aborted (Seq.length queue) [lastState] -- TODO could add current state to return value ^^^^^^^ step :: - ([Step], c) -> - Seq ([Step], c) -> - Simplifier (StepResult ([Step], c)) + ([Step prim], c) -> + Seq ([Step prim], c) -> + Simplifier (StepResult ([Step prim], c)) step a q = do next <- transit a if (isStuck next || isFinal next || isStopped next || shouldStop next) @@ -213,7 +222,7 @@ transitionLeaves in either abort Continue <$> enqueue (extractNext next) q checkLeftUnproven :: - TraversalResult ([Step], c) -> TraversalResult c + TraversalResult ([Step prim], c) -> TraversalResult c checkLeftUnproven = \case result@(Ended results) -> let -- we collect a maximum of 'maxCounterExamples' Stuck states @@ -270,19 +279,19 @@ instance Functor TraversalResult where -- constructing transition functions (for caller) simpleTransition :: - forall config m rule. + forall config m prim rule. Monad m => -- | primitive strategy rule - (Prim -> config -> TransitionT rule m config) -> + (prim -> config -> TransitionT rule m config) -> -- | converter to interpret the config (claim state or program state) -- TODO should also consider the applied rule(s) (for Terminal/Cut) (config -> [config] -> TransitionResult config) -> -- final transition function - ([Step], config) -> - m (TransitionResult ([Step], config)) + ([Step prim], config) -> + m (TransitionResult ([Step prim], config)) simpleTransition applyPrim mapToResult = uncurry tt where - tt :: [Step] -> config -> m (TransitionResult ([Step], config)) + tt :: [Step prim] -> config -> m (TransitionResult ([Step prim], config)) tt [] config = pure $ fmap ([],) $ mapToResult config [] tt ([] : iss) config = @@ -291,5 +300,5 @@ simpleTransition applyPrim mapToResult = uncurry tt (fmap (iss,) . mapToResult config . map fst) <$> runTransitionT (applyGroup is config) - applyGroup :: Step -> config -> TransitionT rule m config + applyGroup :: Step prim -> config -> TransitionT rule m config applyGroup is c = foldM (flip applyPrim) c is diff --git a/kore/src/Kore/Reachability/Prove.hs b/kore/src/Kore/Reachability/Prove.hs index 5ccce92256..cadda4de7a 100644 --- a/kore/src/Kore/Reachability/Prove.hs +++ b/kore/src/Kore/Reachability/Prove.hs @@ -369,10 +369,10 @@ proveClaim where ------------------------------- -- brought in from Claim.hs to remove Strategy type - infinite :: [X.Step] + infinite :: [X.Step Prim] ~infinite = stepNoClaims : repeat stepWithClaims - withMinDepth :: MinDepth -> [X.Step] + withMinDepth :: MinDepth -> [X.Step Prim] withMinDepth d = noCheckSteps <> repeat stepWithClaims where @@ -389,8 +389,8 @@ proveClaim ------------------------------- transition :: - ([X.Step], (ProofDepth, ClaimState SomeClaim)) -> - Simplifier (X.TransitionResult ([X.Step], (ProofDepth, ClaimState SomeClaim))) + ([X.Step Prim], (ProofDepth, ClaimState SomeClaim)) -> + Simplifier (X.TransitionResult ([X.Step Prim], (ProofDepth, ClaimState SomeClaim))) transition = X.simpleTransition (trackProofDepth $ transitionRule' stuckCheck claims axioms) From e156b190b028232c1f23de9bc760a0b62d3371fa Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Mon, 25 Jul 2022 17:37:21 +1000 Subject: [PATCH 30/33] WIP draft code, exec using new graph traversal --- kore/src/Kore/Exec.hs | 145 ++++++++++++++++++++++++++++++------------ 1 file changed, 106 insertions(+), 39 deletions(-) diff --git a/kore/src/Kore/Exec.hs b/kore/src/Kore/Exec.hs index 95fc821f03..d9d1b0dcae 100644 --- a/kore/src/Kore/Exec.hs +++ b/kore/src/Kore/Exec.hs @@ -40,8 +40,9 @@ import Control.Monad.Trans.Maybe (runMaybeT) import Data.Coerce ( coerce, ) -import Data.Limit ( +import Data.Limit as Limit ( Limit (..), + takeWithin, ) import Data.List ( tails, @@ -51,6 +52,9 @@ import Data.Map.Strict ( ) import Data.Map.Strict qualified as Map import GHC.Generics qualified as GHC + +-- temporary +import GraphTraversal qualified as X import Kore.Attribute.Axiom qualified as Attribute import Kore.Attribute.Definition import Kore.Attribute.Symbol ( @@ -281,48 +285,110 @@ exec , rewrites , equations } - strategy + execMode (mkRewritingTerm -> initialTerm) = evalSimplifier simplifierx verifiedModule' sortGraph overloadGraph metadataTools equations $ do let Initialized{rewriteRules} = rewrites finals <- - getFinalConfigsOf $ do - initialConfig <- - Pattern.simplify - (Pattern.fromTermLike initialTerm) - >>= Logic.scatter - let updateQueue = \as -> - Strategy.unfoldDepthFirst as - >=> lift - . Strategy.applyBreadthLimit - breadthLimit - dropStrategy - rewriteGroups = groupRewritesByPriority rewriteRules + -- getFinalConfigsOf $ do + -- initialConfig <- + -- Pattern.simplify + -- (Pattern.fromTermLike initialTerm) + -- >>= Logic.scatter + -- let updateQueue = \as -> + -- Strategy.unfoldDepthFirst as + -- >=> lift + -- . Strategy.applyBreadthLimit + -- breadthLimit + -- dropStrategy + -- rewriteGroups = groupRewritesByPriority rewriteRules + + -- transit :: + -- Strategy Prim -> + -- (ExecDepth, ProgramState (Pattern RewritingVariableName)) -> + -- LogicT + -- Simplifier.Simplifier + -- [(ExecDepth, ProgramState (Pattern RewritingVariableName))] + -- transit instr config = + -- Strategy.transitionRule + -- ( transitionRule rewriteGroups strategy + -- & profTransitionRule + -- & trackExecDepth + -- ) + -- instr + -- config + -- & runTransitionT + -- & fmap (map fst) + -- & lift + -- Strategy.leavesM + -- Leaf + -- updateQueue + -- (unfoldTransition transit) + -- ( limitedExecutionStrategy depthLimit + -- , (ExecDepth 0, Start initialConfig) + -- ) + --------------------- + do + -- FIXME wrong, and maybe not even required? + -- (step 1 simplifies first thing) + let initialConfig = Pattern.fromTermLike initialTerm + let rewriteGroups = groupRewritesByPriority rewriteRules + + execStrategy :: [X.Step Prim] + execStrategy = + Limit.takeWithin depthLimit $ + [Begin, Simplify, Rewrite, Simplify] : + repeat [Begin, Rewrite, Simplify] transit :: - Strategy Prim -> - (ExecDepth, ProgramState (Pattern RewritingVariableName)) -> - LogicT - Simplifier.Simplifier - [(ExecDepth, ProgramState (Pattern RewritingVariableName))] - transit instr config = - Strategy.transitionRule - ( transitionRule rewriteGroups strategy - & profTransitionRule - & trackExecDepth + ( [X.Step Prim] + , (ExecDepth, ProgramState (Pattern RewritingVariableName)) + ) -> + Simplifier.Simplifier + ( X.TransitionResult + ([X.Step Prim], (ExecDepth, ProgramState (Pattern RewritingVariableName))) ) - instr - config - & runTransitionT - & fmap (map fst) - & lift - Strategy.leavesM - Leaf - updateQueue - (unfoldTransition transit) - ( limitedExecutionStrategy depthLimit - , (ExecDepth 0, Start initialConfig) - ) + transit = + X.simpleTransition + ( trackExecDepth . profTransitionRule $ + transitionRule rewriteGroups execMode + ) + toTransitionResult + + toTransitionResult :: + (ExecDepth, ProgramState p) -> + [(ExecDepth, ProgramState p)] -> + (X.TransitionResult (ExecDepth, ProgramState p)) + toTransitionResult prior [] = + case snd prior of + Start _ -> X.Stuck prior -- ??? + Rewritten _ -> X.Final prior + Remaining _ -> X.Final prior + Kore.Rewrite.Bottom -> error "what now?" + toTransitionResult prior [next] = + case snd next of + Start _ -> X.StraightLine next -- should not happen! + Rewritten _ -> X.StraightLine next + Remaining _ -> X.Stuck prior -- ??? + Kore.Rewrite.Bottom -> X.Stuck prior + toTransitionResult prior (s : ss) = + X.Branch prior (s :| ss) + + result <- + X.transitionLeaves + [X.isTerminal, X.isCut] -- future work + Strategy.DepthFirst + breadthLimit + transit + 123 -- FIXME! + (execStrategy, (ExecDepth 0, Start initialConfig)) + case result of + X.Ended results -> pure $ mapMaybe X.extractState results + X.GotStuck _ results -> pure $ mapMaybe X.extractState results + X.Aborted _ results -> do + forM_ depthLimit warnDepthLimitExceeded -- FIXME debug this! + pure $ mapMaybe X.extractState results + let (depths, finalConfigs) = unzip finals infoExecDepth (maximum (ExecDepth 0 : depths)) let finalConfigs' = @@ -343,9 +409,10 @@ exec (Builtin.internalize metadataTools) verifiedModule initialSort = termLikeSort initialTerm - unfoldTransition transit (instrs, config) = do - when (null instrs) $ forM_ depthLimit warnDepthLimitExceeded - Strategy.unfoldTransition transit (instrs, config) + +-- unfoldTransition transit (instrs, config) = do +-- when (null instrs) $ forM_ depthLimit warnDepthLimitExceeded +-- Strategy.unfoldTransition transit (instrs, config) -- | Modify a 'TransitionRule' to track the depth of the execution graph. trackExecDepth :: From a5a25e7038721aea9e847858c70fe64fa4232f69 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Mon, 25 Jul 2022 21:16:17 +1000 Subject: [PATCH 31/33] fix up depth limit warning in exec --- kore/src/Kore/Exec.hs | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) diff --git a/kore/src/Kore/Exec.hs b/kore/src/Kore/Exec.hs index d9d1b0dcae..d2cbc9e09b 100644 --- a/kore/src/Kore/Exec.hs +++ b/kore/src/Kore/Exec.hs @@ -362,9 +362,9 @@ exec toTransitionResult prior [] = case snd prior of Start _ -> X.Stuck prior -- ??? - Rewritten _ -> X.Final prior + Rewritten _ -> X.Stopped prior Remaining _ -> X.Final prior - Kore.Rewrite.Bottom -> error "what now?" + Kore.Rewrite.Bottom -> X.Stopped prior -- should not happen toTransitionResult prior [next] = case snd next of Start _ -> X.StraightLine next -- should not happen! @@ -384,10 +384,13 @@ exec (execStrategy, (ExecDepth 0, Start initialConfig)) case result of X.Ended results -> pure $ mapMaybe X.extractState results - X.GotStuck _ results -> pure $ mapMaybe X.extractState results - X.Aborted _ results -> do - forM_ depthLimit warnDepthLimitExceeded -- FIXME debug this! + X.GotStuck n results -> do + when (n == 0 && any (not . X.isStuck) results) $ + forM_ depthLimit warnDepthLimitExceeded pure $ mapMaybe X.extractState results + X.Aborted n results -> do + when (n == 0) $ forM_ depthLimit warnDepthLimitExceeded + pure $ concatMap X.extractNext results let (depths, finalConfigs) = unzip finals infoExecDepth (maximum (ExecDepth 0 : depths)) From 96821753ecb7bb3499c6847d16e8a8f6a08ab670 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Tue, 26 Jul 2022 11:40:42 +1000 Subject: [PATCH 32/33] clean up unused imports to make the build happy --- kore/src/GraphTraversal.hs | 2 -- kore/src/Kore/Exec.hs | 5 +---- 2 files changed, 1 insertion(+), 6 deletions(-) diff --git a/kore/src/GraphTraversal.hs b/kore/src/GraphTraversal.hs index 55b8314267..d9fb86478d 100644 --- a/kore/src/GraphTraversal.hs +++ b/kore/src/GraphTraversal.hs @@ -10,7 +10,6 @@ module GraphTraversal ( ) where import Control.Monad (foldM) -import Control.Monad.Logic import Control.Monad.Trans.State import Data.Limit import Data.List.NonEmpty qualified as NE @@ -18,7 +17,6 @@ import Data.Sequence (Seq (..)) import Data.Sequence qualified as Seq import GHC.Generics qualified as GHC import GHC.Natural -import Kore.Reachability.Prim (Prim) import Kore.Rewrite.Strategy ( GraphSearchOrder (..), LimitExceeded (..), diff --git a/kore/src/Kore/Exec.hs b/kore/src/Kore/Exec.hs index d2cbc9e09b..abe97029fa 100644 --- a/kore/src/Kore/Exec.hs +++ b/kore/src/Kore/Exec.hs @@ -172,7 +172,6 @@ import Kore.Rewrite.Search ( searchGraph, ) import Kore.Rewrite.Search qualified as Search -import Kore.Rewrite.Strategy (FinalNodeType (Leaf)) import Kore.Rewrite.Strategy qualified as Strategy import Kore.Rewrite.Transition ( runTransitionT, @@ -404,8 +403,6 @@ exec & sameTermLikeSort initialSort return (exitCode, finalTerm) where - dropStrategy = snd - getFinalConfigsOf act = observeAllT $ fmap snd act verifiedModule' = IndexedModule.mapAliasPatterns -- TODO (thomas.tuegel): Move this into Kore.Builtin @@ -571,7 +568,7 @@ prove :: Limit Natural -> Limit Natural -> Natural -> - FinalNodeType -> + Strategy.FinalNodeType -> -- | The main module VerifiedModule StepperAttributes -> -- | The spec module From 9b6f62fe8d0c59fa2920fa5c68cf8df73a116261 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Tue, 26 Jul 2022 11:40:55 +1000 Subject: [PATCH 33/33] descriptive comments and notes about desired refactorings --- kore/src/GraphTraversal.hs | 26 ++++++++++++++++++-------- 1 file changed, 18 insertions(+), 8 deletions(-) diff --git a/kore/src/GraphTraversal.hs b/kore/src/GraphTraversal.hs index d9fb86478d..2ffe90713b 100644 --- a/kore/src/GraphTraversal.hs +++ b/kore/src/GraphTraversal.hs @@ -45,10 +45,10 @@ data TransitionResult a -- | config matches a terminal pattern (or: is RHS of a -- "terminal" rule) Needs to return that RHS - Terminal a + Terminal a -- TODO(JB) obsolete, can use `Stopped` | -- | config matches a cut pattern ( aka: is LHS of a "cut" rule) -- The respective RHS (or RHSs) are returned (if any) - Cut a [a] + Cut a [a] -- TODO(JB) Could use `Stopped` if "next states" were added there deriving stock (Eq, Show, GHC.Generic) instance Functor TransitionResult where @@ -235,17 +235,27 @@ transitionLeaves other -> fmap snd other data StepResult a - = Continue (Seq a) - | Output (TransitionResult a) (Seq a) - | Abort (TransitionResult a) (Seq a) + = -- | Traversal continues with given queue. + Continue (Seq a) + | -- | Traversal produced a result and continues with given queue. + -- Typically a final or stuck state (or a "stop" state), and the + -- queue is the remaining work. + Output (TransitionResult a) (Seq a) + | -- | Traversal exceeded the breadth limit and should not + -- continue. The last state and the current queue are provided + -- for analysis. + Abort (TransitionResult a) (Seq a) deriving stock (Eq, Show, GHC.Generic) +-- TODO(JB) extract and return states instead of TransitionResults data TraversalResult a = -- | remaining queue length and stuck or stopped (unproven) - -- states (always at most maxCounterExamples many) + -- results (always at most maxCounterExamples many). Caller + -- should extract current states from returned results. GotStuck Int [TransitionResult a] | -- | queue length (exceeding the limit) and result(s) of the - -- last step that led to stopping + -- last step that led to stopping. Caller should extract + -- following states from the result. Aborted Int [TransitionResult a] | -- | queue empty, results returned Ended [TransitionResult a] @@ -282,8 +292,8 @@ simpleTransition :: -- | primitive strategy rule (prim -> config -> TransitionT rule m config) -> -- | converter to interpret the config (claim state or program state) - -- TODO should also consider the applied rule(s) (for Terminal/Cut) (config -> [config] -> TransitionResult config) -> + -- TODO(JB) should also consider the applied rule(s) (for Terminal/Cut) -- final transition function ([Step prim], config) -> m (TransitionResult ([Step prim], config))