diff --git a/kore/kore.cabal b/kore/kore.cabal index 190b4e2356..c7039a1cea 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..2ffe90713b --- /dev/null +++ b/kore/src/GraphTraversal.hs @@ -0,0 +1,312 @@ +{-# LANGUAGE MultiWayIf #-} + +{- | +Copyright : (c) Runtime Verification, 2018-2022 +License : BSD-3-Clause +Maintainer : jost.berthold@runtimeverification.com +-} +module GraphTraversal ( + module GraphTraversal, +) where + +import Control.Monad (foldM) +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.Generics qualified as GHC +import GHC.Natural +import Kore.Rewrite.Strategy ( + GraphSearchOrder (..), + LimitExceeded (..), + TransitionT (..), + runTransitionT, + unfoldSearchOrder, + ) +import Kore.Simplify.Data (Simplifier) +import Prelude.Kore +import Pretty + +data TransitionResult a + = -- | straight-line execution + StraightLine 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 + | -- | 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 + -- "terminal" rule) Needs to return that RHS + 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] -- TODO(JB) Could use `Stopped` if "next states" were added there + deriving stock (Eq, Show, GHC.Generic) + +instance Functor TransitionResult where + fmap f = \case + StraightLine a -> StraightLine $ f a + 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) + +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. + +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 +isTerminal _ = False +isCut (Cut _ _) = True +isCut _ = False + +extractNext :: TransitionResult a -> [a] +extractNext = \case + StraightLine a -> [a] + Branch _ as -> NE.toList as + Stuck _ -> [] + Final _ -> [] + Stopped _ -> [] + Terminal _ -> [] + Cut _ as -> as + +extractState :: TransitionResult a -> Maybe a +extractState = \case + StraightLine _ -> Nothing + Branch a _ -> Just a + Stuck a -> Just a + Final a -> Just a + Stopped a -> Just a + Terminal a -> Just a + Cut a _ -> Just a + +type Step prim = [prim] + +---------------------------------------- +transitionLeaves :: + 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 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 + + -- | BreadthFirst, DepthFirst + GraphSearchOrder -> + -- | breadth limit, essentially a natural number + Limit Natural -> + -- | transition function + (([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 prim], c) -> + Simplifier (TraversalResult c) +transitionLeaves + stopCriteria + direction + breadthLimit + transit + maxCounterExamples + start = + enqueue [start] Seq.empty + >>= either + (pure . const (GotStuck 0 [Stopped $ snd start])) + (\q -> checkLeftUnproven <$> evalStateT (worker q) []) + where + enqueue' = unfoldSearchOrder direction + + 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 $ + if exceedsLimit newQ + then Left (LimitExceeded newQ) + else Right newQ + + exceedsLimit :: Seq ([Step prim], c) -> Bool + exceedsLimit = not . withinLimit breadthLimit . fromIntegral . Seq.length + + shouldStop :: TransitionResult ([Step prim], c) -> Bool + shouldStop result = any ($ result) stopCriteria + + maxStuck = fromIntegral maxCounterExamples + + 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 + 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 lastState queue -> do + pure $ Aborted (Seq.length queue) [lastState] + -- TODO could add current state to return value ^^^^^^^ + step :: + ([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) + then pure (Output next q) + else + let abort (LimitExceeded queue) = Abort next queue + in either abort Continue <$> enqueue (extractNext next) q + + checkLeftUnproven :: + TraversalResult ([Step prim], c) -> TraversalResult c + checkLeftUnproven = \case + 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 -> fmap snd other + +data StepResult 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) + -- 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. Caller should extract + -- following states from the result. + Aborted Int [TransitionResult a] + | -- | 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 + 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) + Aborted n rs -> Aborted n (ffmap f rs) + Ended rs -> Ended (ffmap f rs) + where + ffmap = map . fmap + +---------------------------------------- +-- constructing transition functions (for caller) + +simpleTransition :: + forall config m prim rule. + Monad m => + -- | primitive strategy rule + (prim -> config -> TransitionT rule m config) -> + -- | converter to interpret the config (claim state or program state) + (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)) +simpleTransition applyPrim mapToResult = uncurry tt + where + tt :: [Step prim] -> config -> m (TransitionResult ([Step prim], config)) + tt [] config = + pure $ fmap ([],) $ mapToResult config [] + tt ([] : iss) config = + tt iss config + tt (is : iss) config = + (fmap (iss,) . mapToResult config . map fst) + <$> runTransitionT (applyGroup is config) + + applyGroup :: Step prim -> config -> TransitionT rule m config + applyGroup is c = foldM (flip applyPrim) c is diff --git a/kore/src/Kore/Exec.hs b/kore/src/Kore/Exec.hs index 72e1ee29af..abe97029fa 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 ( @@ -168,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, @@ -281,41 +284,113 @@ 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 - transit instr config = - Strategy.transitionRule - ( transitionRule rewriteGroups strategy - & profTransitionRule - & trackExecDepth + -- 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 :: + ( [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.Stopped prior + Remaining _ -> X.Final prior + Kore.Rewrite.Bottom -> X.Stopped prior -- should not happen + 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 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)) let finalConfigs' = @@ -328,17 +403,16 @@ 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 (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 :: @@ -494,7 +568,7 @@ prove :: Limit Natural -> Limit Natural -> Natural -> - FinalNodeType -> + Strategy.FinalNodeType -> -- | The main module VerifiedModule StepperAttributes -> -- | The spec module diff --git a/kore/src/Kore/Reachability/Prove.hs b/kore/src/Kore/Reachability/Prove.hs index 54c3fed29b..cadda4de7a 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 @@ -58,6 +56,7 @@ import Data.Text ( ) 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 ( @@ -85,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 @@ -97,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 @@ -120,16 +118,13 @@ 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 import Log ( MonadLog (..), ) -import Logic ( - LogicT, - ) -import Logic qualified import Numeric.Natural ( Natural, ) @@ -162,10 +157,10 @@ 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) +type VerifierT m = ExceptT StuckClaims m newtype AllClaims claim = AllClaims {getAllClaims :: [claim]} newtype Axioms claim = Axioms {getAxioms :: [Rule claim]} @@ -196,10 +191,6 @@ data ProveClaimsResult = ProveClaimsResult } proveClaims :: - forall simplifier. - MonadMask simplifier => - MonadSimplify simplifier => - MonadProf simplifier => Maybe MinDepth -> StuckCheck -> Limit Natural -> @@ -212,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 @@ -260,10 +251,6 @@ proveClaims else Left claim proveClaimsWorker :: - forall simplifier. - MonadSimplify simplifier => - MonadMask simplifier => - MonadProf simplifier => Maybe MinDepth -> StuckCheck -> Limit Natural -> @@ -275,7 +262,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 @@ -290,29 +277,32 @@ proveClaimsWorker where verifyWorker :: (SomeClaim, Limit Natural) -> - ExceptT StuckClaims (StateT ProvenClaims simplifier) () - verifyWorker unprovenClaim@(claim, _) = do - debugBeginClaim claim - proveClaim - maybeMinDepth - stuckCheck - breadthLimit - searchOrder - maxCounterexamples - finalNodeType - claims - axioms - unprovenClaim - addProvenClaim claim + VerifierT (StateT ProvenClaims Simplifier) () + verifyWorker unprovenClaim@(claim, _) = + traceExceptT D_OnePath_verifyClaim [debugArg "rule" claim] $ do + debugBeginClaim claim + result <- + lift . lift $ + 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)) 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) -> - ExceptT StuckClaims simplifier () + Simplifier (Either StuckClaims ()) proveClaim maybeMinDepth stuckCheck @@ -332,93 +322,106 @@ 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) - 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) - proofDepths <- - Strategy.leavesM - finalNodeType - updateQueue - (Strategy.unfoldTransition transit) - (limitedStrategy, (ProofDepth 0, startGoal)) - & fmap discardStrategy - & throwUnproven - & handle handleLimitExceeded - & (\s -> evalStateT s mempty) - let maxProofDepth = sconcat (ProofDepth 0 :| proofDepths) - 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 - 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 - ) + ------------------------------- + -- brought in from Claim.hs to remove Strategy type + infinite :: [X.Step Prim] + ~infinite = stepNoClaims : repeat stepWithClaims + + withMinDepth :: MinDepth -> [X.Step Prim] + withMinDepth d = + noCheckSteps <> repeat stepWithClaims 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 - updateSuckClaimsState 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 instr config = - Strategy.transitionRule - ( transitionRule' stuckCheck claims axioms - & trackProofDepth - & throwStuckClaims maxCounterexamples - ) - instr - config - & runTransitionT - & fmap discardAppliedRules - & traceProf ":transit" - & lift + 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 Prim], (ProofDepth, ClaimState SomeClaim)) -> + Simplifier (X.TransitionResult ([X.Step Prim], (ProofDepth, ClaimState SomeClaim))) + transition = + X.simpleTransition + (trackProofDepth $ transitionRule' stuckCheck claims axioms) + 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 @@ -567,42 +570,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' - updateSuckClaimsState unproven maxCounterexamples - return state' - _ -> return state' - -updateSuckClaimsState :: - Monad m => - SomeClaim -> - Natural -> - VerifierT m () -updateSuckClaimsState 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. diff --git a/kore/src/Kore/Rewrite/Strategy.hs b/kore/src/Kore/Rewrite/Strategy.hs index 1ec3d167ef..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': @@ -461,8 +358,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)) -> @@ -563,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) @@ -572,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 @@ -587,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) diff --git a/nix/kore-ghc8107.nix.d/kore.nix b/nix/kore-ghc8107.nix.d/kore.nix index 2c202ba849..effc85f7ce 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"