3119 output unexplored leaf count when failing (#3177)

* 3119 Output count of unexplored branches when a proof fails

When a proof fails on one branch (or more, when using
`--max-counterexamples`), the prover indicates with a warning if any
other branches existed that were left unexplored.

* Materialize Nix expressions

* shut up hlint (log entries should be lazy)

* fix a strictness + formatter error

* add log entry to registry

* test case for unexplored branch count

Co-authored-by: github-actions <github-actions@github.com>

Author: jberthold

.hlint.yaml

@@ -157,6 +157,7 @@
     within:
       - GlobalMain
       - Kore.Log.InfoExecDepth
+      - Kore.Log.WarnUnexploredBranches
 
 - ignore: {name: "Redundant compare", within: [Kore.Syntax.Id]}
 

kore/app/exec/Main.hs

@@ -75,6 +75,9 @@ import Kore.Log.WarnBoundedModelChecker (
 import Kore.Log.WarnIfLowProductivity (
     warnIfLowProductivity,
  )
+import Kore.Log.WarnUnexploredBranches (
+    warnUnexploredBranches,
+ )
 import Kore.ModelChecker.Bounded qualified as Bounded (
     CheckResult (..),
  )
@@ -784,25 +787,25 @@ koreProve LocalOptions{execOptions, simplifierx} proveOptions = do
             specModule
             maybeAlreadyProvenModule
 
-    let ProveClaimsResult{stuckClaims, provenClaims} = proveResult
+    let ProveClaimsResult{stuckClaims, provenClaims, unexplored} = proveResult
     let (exitCode, final) =
             case foldFirst stuckClaims of
                 Nothing -> success -- stuckClaims is empty
                 Just claim ->
                     stuckPatterns
                         & OrPattern.toTermLike (getClaimPatternSort $ claimPattern claim)
                         & failure
-          where
-            stuckPatterns =
-                OrPattern.fromPatterns (MultiAnd.map getStuckConfig stuckClaims)
-            getStuckConfig =
-                getRewritingPattern . getConfiguration . getStuckClaim
-            claimPattern claim =
-                claim
-                    & getStuckClaim
-                    & Lens.view lensClaimPattern
+                  where
+                    stuckPatterns =
+                        OrPattern.fromPatterns (MultiAnd.map getStuckConfig stuckClaims)
+                    getStuckConfig =
+                        getRewritingPattern . getConfiguration . getStuckClaim
+                    claimPattern = Lens.view lensClaimPattern . getStuckClaim
+
     lift $ for_ saveProofs $ saveProven specModule provenClaims
     lift $ renderResult execOptions (unparse final)
+    when (unexplored /= 0) $
+        warnUnexploredBranches unexplored
     return (kFileLocations definition, exitCode)
   where
     failure pat = (ExitFailure 1, pat)

kore/kore.cabal

@@ -394,6 +394,7 @@ library
     Kore.Log.WarnStuckClaimState
     Kore.Log.WarnSymbolSMTRepresentation
     Kore.Log.WarnTrivialClaim
+    Kore.Log.WarnUnexploredBranches
     Kore.Log.WarnUnsimplified
     Kore.ModelChecker.Bounded
     Kore.ModelChecker.Simplification

kore/src/Kore/Log/Registry.hs

@@ -145,6 +145,9 @@ import Kore.Log.WarnSymbolSMTRepresentation (
 import Kore.Log.WarnTrivialClaim (
     WarnTrivialClaim,
  )
+import Kore.Log.WarnUnexploredBranches (
+    WarnUnexploredBranches,
+ )
 import Kore.Log.WarnUnsimplified (
     WarnUnsimplifiedCondition,
     WarnUnsimplifiedPredicate,
@@ -213,6 +216,7 @@ entryHelpDocsErr, entryHelpDocsNoErr :: [Pretty.Doc ()]
             , mk $ Proxy @WarnClaimRHSIsBottom
             , mk $ Proxy @WarnIfLowProductivity
             , mk $ Proxy @WarnTrivialClaim
+            , mk $ Proxy @WarnUnexploredBranches
             , mk $ Proxy @DebugRetrySolverQuery
             , mk $ Proxy @DebugUnifyBottom
             , mk $ Proxy @DebugEvaluateCondition

kore/src/Kore/Log/WarnUnexploredBranches.hs

@@ -0,0 +1,43 @@
+{-# LANGUAGE NoStrict #-}
+{-# LANGUAGE NoStrictData #-}
+
+{- |
+Copyright   : (c) Runtime Verification, 2019-2022
+License     : BSD-3-Clause
+-}
+module Kore.Log.WarnUnexploredBranches (
+    WarnUnexploredBranches (..),
+    warnUnexploredBranches,
+) where
+
+import Log
+import Numeric.Natural
+import Prelude.Kore
+import Pretty (
+    Pretty,
+ )
+import Pretty qualified
+
+{- | @WarnUnexploredBranches@ is emitted when a proof gets stuck. It
+   indicates how many other branches in the proof were left unexplored
+   (and may also be failing if explored).
+-}
+data WarnUnexploredBranches
+    = WarnUnexploredBranches Natural
+    deriving stock (Show)
+
+instance Pretty WarnUnexploredBranches where
+    pretty (WarnUnexploredBranches count) =
+        Pretty.pretty count
+            Pretty.<+> "branches were still unexplored when the action failed."
+
+instance Entry WarnUnexploredBranches where
+    entrySeverity _ = Warning
+    oneLineDoc (WarnUnexploredBranches count) =
+        Pretty.pretty count
+            Pretty.<+> "branches were still unexplored when the action failed."
+    helpDoc _ =
+        "indicate whether and how many unexplored branches existed when failing."
+
+warnUnexploredBranches :: MonadLog log => Natural -> log ()
+warnUnexploredBranches = logEntry . WarnUnexploredBranches

kore/src/Kore/Reachability/Prove.hs

@@ -152,10 +152,11 @@ 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
-@'MultiAnd'@ of unprovable configuration.
+The action may throw an exception if the proof fails; the exception is
+a @'MultiAnd'@ of unprovable configuration and a count of unexplored
+branches.
 -}
-type VerifierT m = ExceptT StuckClaims m
+type VerifierT m = ExceptT (StuckClaims, Natural) m
 
 newtype AllClaims claim = AllClaims {getAllClaims :: [claim]}
 newtype Axioms claim = Axioms {getAxioms :: [Rule claim]}
@@ -183,6 +184,8 @@ data ProveClaimsResult = ProveClaimsResult
       stuckClaims :: !StuckClaims
     , -- | The conjunction of all claims which were proven.
       provenClaims :: !ProvenClaims
+    , -- | A count of non-final states that were not explored further
+      unexplored :: Natural
     }
 
 proveClaims ::
@@ -224,10 +227,12 @@ proveClaims
                     unproven
                     & runExceptT
                     & flip runStateT (MultiAnd.make stillProven)
+            let (stuckClaims, unexplored) = fromLeft (MultiAnd.top, 0) result
             pure
                 ProveClaimsResult
-                    { stuckClaims = fromLeft MultiAnd.top result
+                    { stuckClaims
                     , provenClaims
+                    , unexplored
                     }
       where
         unproven :: ToProve SomeClaim
@@ -307,7 +312,7 @@ proveClaim ::
     AllClaims SomeClaim ->
     Axioms SomeClaim ->
     (SomeClaim, Limit Natural) ->
-    Simplifier (Either StuckClaims ())
+    Simplifier (Either (StuckClaims, Natural) ())
 proveClaim
     maybeMinDepth
     stuckCheck
@@ -335,18 +340,19 @@ proveClaim
                 limitedStrategyList
                 (ProofDepth 0, startGoal)
 
-        let returnUnprovenClaims =
+        let returnUnprovenClaims n =
                 pure
                     . Left
+                    . (,fromIntegral n)
                     . MultiAnd.make
                     . map StuckClaim
                     . mapMaybe (extractUnproven . snd)
 
         case traversalResult of
-            GraphTraversal.GotStuck _n rs ->
-                returnUnprovenClaims rs
-            GraphTraversal.Aborted _n rs ->
-                returnUnprovenClaims rs
+            GraphTraversal.GotStuck n rs ->
+                returnUnprovenClaims n rs
+            GraphTraversal.Aborted n rs ->
+                returnUnprovenClaims n rs
             GraphTraversal.Ended results -> do
                 let depths = map fst results
                     maxProofDepth = sconcat (ProofDepth 0 :| depths)

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

@@ -771,6 +771,30 @@ test_proveClaims =
          in [ mkTest "OnePath" simpleOnePathClaim
             , mkTest "AllPath" simpleAllPathClaim
             ]
+    , testGroup "warns about unexplored branch when one of several stuck claims returned" $
+        let axioms = [simpleAxiom Mock.a (mkOr Mock.b Mock.c)]
+            mkTest name mkSimpleClaim =
+                testCase name $ do
+                    actual <-
+                        Test.Kore.Reachability.Prove.proveClaims
+                            Unlimited
+                            Unlimited
+                            1
+                            axioms
+                            [mkSimpleClaim Mock.a Mock.d]
+                            []
+                    let stuck = mkSimpleClaim Mock.b Mock.d
+                        expect =
+                            ProveClaimsResult
+                                { stuckClaims = MultiAnd.singleton (StuckClaim stuck)
+                                , provenClaims = MultiAnd.top
+                                , unexplored = 1
+                                }
+                    assertEqual "count" (unexplored expect) (unexplored actual)
+                    assertEqual "claim" (stuckClaims expect) (stuckClaims actual)
+         in [ mkTest "OnePath" simpleOnePathClaim
+            , mkTest "AllPath" simpleAllPathClaim
+            ]
     ]
 
 test_transitionRule :: TestTree

nix/kore-ghc8107.nix.d/kore.nix

@@ -312,6 +312,7 @@
         "Kore/Log/WarnStuckClaimState"
         "Kore/Log/WarnSymbolSMTRepresentation"
         "Kore/Log/WarnTrivialClaim"
+        "Kore/Log/WarnUnexploredBranches"
         "Kore/Log/WarnUnsimplified"
         "Kore/ModelChecker/Bounded"
         "Kore/ModelChecker/Simplification"

nix/kore-ghc923.nix.d/kore.nix

@@ -312,6 +312,7 @@
         "Kore/Log/WarnStuckClaimState"
         "Kore/Log/WarnSymbolSMTRepresentation"
         "Kore/Log/WarnTrivialClaim"
+        "Kore/Log/WarnUnexploredBranches"
         "Kore/Log/WarnUnsimplified"
         "Kore/ModelChecker/Bounded"
         "Kore/ModelChecker/Simplification"