Use entire goal in proof strategy (#1936)

* Breadth limit: handle for prove

* Strategy.Verification: replace Pattern with OrPattern

* Remove redundant constraints

* Remove unused import

* Fix tests

* Remove unused imports

* Add unit tests

* Add integration tests

* Clean-up

* Address review comments

* Regenerate golden file

* Strategies.Verification: replace (Pattern Variable) with ReachabilityRule in CommonProofState

* kore-repl: keep entire goal in execution graph

* Strategies.Verification: remove redundant function

* Repl: use stored goal instead of generating claims

* Clean-up

* Clean-up

* Repl: add dest (destination) command

* Clean-up

* Address review comment

* Address review comments

* Revert + fix

* Verification.verifyClaimStep: remove target argument

Author: ana-pantilie

kore/src/Kore/Repl.hs

@@ -251,19 +251,18 @@ runRepl
     firstClaimExecutionGraph = emptyExecutionGraph firstClaim
 
     stepper0
-        :: ReachabilityRule
-        -> [ReachabilityRule]
+        :: [ReachabilityRule]
         -> [Axiom]
         -> ExecutionGraph Axiom
         -> ReplNode
         -> m (ExecutionGraph Axiom)
-    stepper0 claim claims axioms graph rnode = do
+    stepper0 claims axioms graph rnode = do
         let node = unReplNode rnode
         if Graph.outdeg (Strategy.graph graph) node == 0
             then
                 catchEverything graph
                 $ catchInterruptWithDefault graph
-                $ verifyClaimStep claim claims axioms graph node
+                $ verifyClaimStep claims axioms graph node
             else pure graph
 
     catchInterruptWithDefault :: a -> m a -> m a

kore/src/Kore/Repl/Data.hs

@@ -229,6 +229,8 @@ data ReplCommand
     -- ^ Select a different node in the graph.
     | ShowConfig !(Maybe ReplNode)
     -- ^ Show the configuration from the current node.
+    | ShowDest !(Maybe ReplNode)
+    -- ^ Show the destination from the current node.
     | OmitCell !(Maybe String)
     -- ^ Adds or removes cell to omit list, or shows current omit list.
     | ShowLeafs
@@ -334,6 +336,8 @@ helpText =
     \select <n>                               select node id 'n' from the graph\n\
     \config [n]                               shows the config for node 'n'\
                                               \ (defaults to current node)\n\
+    \dest [n]                                 shows the destination for node 'n'\
+                                              \ (defaults to current node)\n\
     \omit [cell]                              adds or removes cell to omit list\
                                               \ (defaults to showing the omit\
                                               \ list)\n\
@@ -493,13 +497,12 @@ data ReplState = ReplState
 -- | Configuration environment for the repl.
 data Config m = Config
     { stepper
-        :: Claim
-        -> [Claim]
+        :: [Claim]
         -> [Axiom]
         -> ExecutionGraph Axiom
         -> ReplNode
         -> m (ExecutionGraph Axiom)
-    -- ^ Stepper function, it is a partially applied 'verifyClaimStep'
+    -- ^ Stepper function
     , unifier
         :: SideCondition VariableName
         -> TermLike VariableName

kore/src/Kore/Repl/Interpreter.hs

@@ -178,6 +178,7 @@ import Kore.Step.RulePattern
     ( ReachabilityRule (..)
     , RulePattern (..)
     , ToRulePattern (..)
+    , rhsToPattern
     )
 import Kore.Step.Simplification.Data
     ( MonadSimplify
@@ -186,12 +187,12 @@ import qualified Kore.Step.Strategy as Strategy
 import Kore.Strategies.Goal
 import Kore.Strategies.ProofState
     ( ProofStateTransformer (ProofStateTransformer)
+    , extractUnproven
     , proofState
     )
 import qualified Kore.Strategies.ProofState as ProofState.DoNotUse
 import Kore.Strategies.Verification
     ( CommonProofState
-    , commonProofStateTransformer
     )
 import Kore.Syntax.Application
 import qualified Kore.Syntax.Id as Id
@@ -248,6 +249,7 @@ replInterpreter0 printAux printKore replCmd = do
                 ProveStepsF n         -> proveStepsF n           $> Continue
                 SelectNode i          -> selectNode i            $> Continue
                 ShowConfig mc         -> showConfig mc           $> Continue
+                ShowDest mc           -> showDest mc             $> Continue
                 OmitCell c            -> omitCell c              $> Continue
                 ShowLeafs             -> showLeafs               $> Continue
                 ShowRule   mc         -> showRule mc             $> Continue
@@ -521,14 +523,37 @@ showConfig
     => Maybe ReplNode
     -- ^ 'Nothing' for current node, or @Just n@ for a specific node identifier
     -> ReplM m ()
-showConfig configNode = do
-    maybeConfig <- getConfigAt configNode
-    case maybeConfig of
+showConfig =
+    showProofStateComponent "Config" getConfiguration
+
+-- | Shows destination at node 'n', or current node if 'Nothing' is passed.
+showDest
+    :: Monad m
+    => Maybe ReplNode
+    -- ^ 'Nothing' for current node, or @Just n@ for a specific node identifier
+    -> ReplM m ()
+showDest =
+    showProofStateComponent "Destination" (rhsToPattern . getDestination)
+
+showProofStateComponent
+    :: Monad m
+    => String
+    -- ^ component name
+    -> (ReachabilityRule -> Pattern VariableName)
+    -> Maybe ReplNode
+    -> ReplM m ()
+showProofStateComponent name transformer maybeNode = do
+    maybeProofState <- getProofStateAt maybeNode
+    case maybeProofState of
         Nothing -> putStrLn' "Invalid node!"
         Just (ReplNode node, config) -> do
             omit <- Lens.use (field @"omit")
-            putStrLn' $ "Config at node " <> show node <> " is:"
-            tell $ unparseStrategy omit config
+            putStrLn' $ name <> " at node " <> show node <> " is:"
+            unparseProofStateComponent
+                transformer
+                omit
+                config
+                & tell
 
 -- | Shows current omit list if passed 'Nothing'. Adds/removes from the list
 -- depending on whether the string already exists in the list or not.
@@ -846,7 +871,7 @@ tryAxiomClaimWorker mode ref = do
         -> ReplM m ()
     showUnificationFailure axiomOrClaim' node = do
         let first = extractLeftPattern axiomOrClaim'
-        maybeSecond <- getConfigAt (Just node)
+        maybeSecond <- getProofStateAt (Just node)
         case maybeSecond of
             Nothing -> putStrLn' "Unexpected error getting current config."
             Just (_, second) ->
@@ -858,7 +883,7 @@ tryAxiomClaimWorker mode ref = do
                         , goalRewrittenTransformer = patternUnifier
                         , goalStuckTransformer = patternUnifier
                         }
-                    second
+                    (getConfiguration <$> second)
               where
                 patternUnifier :: Pattern VariableName -> ReplM m ()
                 patternUnifier
@@ -964,30 +989,25 @@ savePartialProof
     -> FilePath
     -> ReplM m ()
 savePartialProof maybeNatural file = do
-    currentClaim <- Lens.use (field @"claim")
     currentIndex <- Lens.use (field @"claimIndex")
     claims <- Lens.use (field @"claims")
     Config { mainModuleName } <- ask
-    maybeConfig <- getConfigAt maybeNode
-    case maybeConfig of
+    maybeConfig <- getProofStateAt maybeNode
+    case (fmap . fmap) extractUnproven maybeConfig of
         Nothing -> putStrLn' "Invalid node!"
-        Just (currentNode, currentProofState) -> do
-            let config = unwrapConfig currentProofState
-                newClaim = createClaim currentClaim config
-                newTrustedClaims =
+        Just (_, Nothing) -> putStrLn' "Goal is proven."
+        Just (currentNode, Just currentGoal) -> do
+            let newTrustedClaims =
                     makeTrusted
                     <$> removeIfRoot currentNode currentIndex claims
                 newDefinition =
                     createNewDefinition
                         mainModuleName
                         (makeModuleName file)
-                        $ newClaim : newTrustedClaims
+                        $ currentGoal : newTrustedClaims
             saveUnparsedDefinitionToFile (unparse newDefinition)
             putStrLn' "Done."
   where
-    unwrapConfig :: CommonProofState -> Pattern VariableName
-    unwrapConfig = proofState commonProofStateTransformer
-
     saveUnparsedDefinitionToFile
         :: Pretty.Doc ann
         -> ReplM m ()
@@ -1203,26 +1223,30 @@ showRewriteRule rule =
     <> makeAuxReplOutput (show . Pretty.pretty . from @_ @SourceLocation $ rule)
 
 -- | Unparses a strategy node, using an omit list to hide specified children.
-unparseStrategy
-    :: Set String
+unparseProofStateComponent
+    :: (ReachabilityRule -> Pattern VariableName)
+    -> Set String
     -- ^ omit list
     -> CommonProofState
     -- ^ pattern
     -> ReplOutput
-unparseStrategy omitList =
+unparseProofStateComponent transformation omitList =
     proofState ProofStateTransformer
-        { goalTransformer = makeKoreReplOutput . unparseToString . fmap hide
-        , goalRemainderTransformer = \pat ->
+        { goalTransformer =
+            makeKoreReplOutput . unparseComponent
+        , goalRemainderTransformer = \goal ->
             makeAuxReplOutput "Stuck: \n"
-            <> makeKoreReplOutput (unparseToString $ fmap hide pat)
+            <> makeKoreReplOutput (unparseComponent goal)
         , goalRewrittenTransformer =
-            makeKoreReplOutput . unparseToString . fmap hide
-        , goalStuckTransformer = \pat ->
+            makeKoreReplOutput . unparseComponent
+        , goalStuckTransformer = \goal ->
             makeAuxReplOutput "Stuck: \n"
-            <> makeKoreReplOutput (unparseToString $ fmap hide pat)
+            <> makeKoreReplOutput (unparseComponent goal)
         , provenValue = makeAuxReplOutput "Reached bottom"
         }
   where
+    unparseComponent =
+        unparseToString . fmap hide . transformation
     hide :: TermLike VariableName -> TermLike VariableName
     hide =
         Recursive.unfold $ \termLike ->

kore/src/Kore/Repl/Parser.hs

@@ -105,6 +105,7 @@ nonRecursiveCommand =
         , proveSteps
         , selectNode
         , showConfig
+        , showDest
         , omitCell
         , showLeafs
         , showRule
@@ -188,6 +189,11 @@ showConfig = do
     dec <- literal "config" *> maybeDecimal
     return $ ShowConfig (fmap ReplNode dec)
 
+showDest :: Parser ReplCommand
+showDest = do
+    dec <- literal "dest" *> maybeDecimal
+    return $ ShowDest (fmap ReplNode dec)
+
 omitCell :: Parser ReplCommand
 omitCell = OmitCell <$$> literal "omit" *> maybeWord