[3198] fix stopping prover on branches + logging unproven (#3199)

* The rewritten prover was returning a final instead of a stopped state when stopping at branches
* Proof depth for unproven claims was not logged at info level as before.

This fixes both problems, and adds a unit test for stopping at branches.

Fixes #3198

Author: jberthold

kore/src/Kore/Exec/GraphTraversal.hs

@@ -19,6 +19,7 @@ import Control.Monad (foldM)
 import Control.Monad.Trans.State
 import Data.Limit
 import Data.List.NonEmpty qualified as NE
+import Data.Maybe (maybeToList)
 import Data.Sequence (Seq (..))
 import Data.Sequence qualified as Seq
 import GHC.Natural
@@ -227,11 +228,14 @@ graphTraversal
         exceedsLimit =
             not . withinLimit breadthLimit . fromIntegral . Seq.length
 
-        shouldStop :: TransitionResult (TState instr config) -> Bool
-        shouldStop =
-            case stopOn of
-                Leaf -> const False
-                LeafOrBranching -> isBranch
+        -- when stopping at branches, turn a 'Branch' result into a 'Stopped'
+        branchStop :: TransitionResult (TState i c) -> TransitionResult (TState i c)
+        branchStop result
+            | isBranch result =
+                case stopOn of
+                    Leaf -> result
+                    LeafOrBranching -> Stopped (maybeToList $ extractState result)
+            | otherwise = result
 
         worker ::
             Seq (TState instr config) ->
@@ -263,8 +267,8 @@ graphTraversal
             Seq (TState instr config) ->
             Simplifier (StepResult (TState instr config))
         step a q = do
-            next <- transit a
-            if (isStuck next || isFinal next || isStopped next || shouldStop next)
+            next <- branchStop <$> transit a
+            if (isStuck next || isFinal next || isStopped next)
                 then pure (Output next q)
                 else
                     let abort (LimitExceeded queue) = Abort next queue

kore/src/Kore/Reachability/Prove.hs

@@ -340,13 +340,15 @@ proveClaim
                 limitedStrategyList
                 (ProofDepth 0, startGoal)
 
-        let returnUnprovenClaims n =
+        let returnUnprovenClaims n unproven = do
+                mapM_ (infoUnprovenDepth . fst) unproven
                 pure
                     . Left
                     . (,fromIntegral n)
                     . MultiAnd.make
                     . map StuckClaim
                     . mapMaybe (extractUnproven . snd)
+                    $ unproven
 
         case traversalResult of
             GraphTraversal.GotStuck n rs ->

kore/test/Test/Kore/Reachability/Prove.hs

@@ -46,7 +46,7 @@ import Kore.Rewrite.RulePattern (
     rulePattern,
  )
 import Kore.Rewrite.Strategy (
-    FinalNodeType (Leaf),
+    FinalNodeType (..),
     GraphSearchOrder (..),
  )
 import Kore.Rewrite.Transition (runTransitionT)
@@ -780,6 +780,7 @@ test_proveClaims =
                             Unlimited
                             Unlimited
                             1
+                            Leaf
                             axioms
                             [mkSimpleClaim Mock.a Mock.d]
                             []
@@ -795,6 +796,44 @@ test_proveClaims =
          in [ mkTest "OnePath" simpleOnePathClaim
             , mkTest "AllPath" simpleAllPathClaim
             ]
+    , testGroup "returns branch state when stopping at branch points" $
+        let axioms =
+                [ simpleAxiom Mock.a Mock.d
+                , simpleAxiom Mock.d (mkOr Mock.b Mock.c)
+                ]
+            mkTest name mkSimpleClaim mkSomeClaim =
+                testCase name $ do
+                    actual <-
+                        Test.Kore.Reachability.Prove.proveClaims
+                            Unlimited
+                            Unlimited
+                            1
+                            LeafOrBranching
+                            axioms
+                            [mkSimpleClaim Mock.a $ mkOr Mock.b Mock.c]
+                            []
+                    let stuck =
+                            mkSomeClaim
+                                (Pattern.fromTermLike Mock.d)
+                                ( OrPattern.fromPatterns $
+                                    map
+                                        Pattern.fromTermLike
+                                        [ Mock.b
+                                        , Mock.c
+                                        ]
+                                )
+                                []
+                        expect =
+                            ProveClaimsResult
+                                { stuckClaims = MultiAnd.singleton $ StuckClaim stuck
+                                , provenClaims = MultiAnd.top
+                                , unexplored = 0
+                                }
+                    assertEqual "count" (unexplored expect) (unexplored actual)
+                    assertEqual "claim" (stuckClaims expect) (stuckClaims actual)
+         in [ mkTest "OnePath" simpleOnePathClaim mkSomeClaimOnePath
+            , mkTest "AllPath" simpleAllPathClaim mkSomeClaimAllPath
+            ]
     ]
 
 test_transitionRule :: TestTree
@@ -892,6 +931,7 @@ proveClaims ::
     Limit Natural ->
     Limit Natural ->
     Natural ->
+    FinalNodeType ->
     [Rule SomeClaim] ->
     [SomeClaim] ->
     [SomeClaim] ->
@@ -900,6 +940,7 @@ proveClaims
     breadthLimit
     depthLimit
     maxCounterexamples
+    finalNodeType
     axioms
     claims
     alreadyProven =
@@ -909,7 +950,7 @@ proveClaims
             breadthLimit
             BreadthFirst
             maxCounterexamples
-            Leaf
+            finalNodeType
             (AllClaims claims)
             (Axioms axioms)
             (AlreadyProven (map unparseToText2 alreadyProven))
@@ -941,6 +982,7 @@ proveClaimsMaxCounterexamples_
                     breadthLimit
                     depthLimit
                     maxCounterexamples
+                    Leaf
                     axioms
                     claims
                     alreadyProven