Save proofs even when successful (#2197)

* proveClaims: Return a ProveClaimsResult

* Kore.Reachability.Prove: Remove ProofStuck

* proveClaims: Clean up result

* kore-exec: Save proofs even when successful

* test/save-proofs: Save successful proofs

* mkClaimPattern: renamed from claimPattern

* Kore.Reachability: Export mkAllPathClaim and mkOnePathClaim

* proveClaims: Return entire stuck claims

Return the entire stuck claims, instead of the left-hand sides only.

Author: ttuegel

kore/app/exec/Main.hs

@@ -94,6 +94,10 @@ import Kore.IndexedModule.IndexedModule
 import qualified Kore.IndexedModule.MetadataToolsBuilder as MetadataTools
     ( build
     )
+import Kore.Internal.MultiAnd
+    ( MultiAnd
+    )
+import qualified Kore.Internal.MultiAnd as MultiAnd
 import qualified Kore.Internal.OrPattern as OrPattern
 import Kore.Internal.Pattern
     ( Conditional (..)
@@ -137,8 +141,10 @@ import Kore.Parser
     , parseKorePattern
     )
 import Kore.Reachability
-    ( ProofStuck (..)
+    ( ProveClaimsResult (..)
     , SomeClaim
+    , StuckClaim (..)
+    , getConfiguration
     )
 import qualified Kore.Reachability.Claim as Claim
 import Kore.Rewriting.RewritingVariable
@@ -161,6 +167,9 @@ import Kore.Syntax.Definition
     , Sentence (..)
     )
 import qualified Kore.Syntax.Definition as Definition.DoNotUse
+import Kore.TopBottom
+    ( isTop
+    )
 import Kore.Unparser
     ( unparse
     )
@@ -648,18 +657,20 @@ koreProve execOptions proveOptions = do
             specModule
             maybeAlreadyProvenModule
 
-    (exitCode, final) <- case proveResult of
-        Left ProofStuck { stuckPatterns, provenClaims } -> do
-            maybe
-                (return ())
-                (lift . saveProven specModule provenClaims)
-                saveProofs
+    let ProveClaimsResult { stuckClaims, provenClaims } = proveResult
+    let (exitCode, final)
+          | noStuckClaims = success
+          | otherwise =
             stuckPatterns
-                & OrPattern.toTermLike
-                & failure
-                & return
-        Right () -> return success
-
+            & OrPattern.toTermLike
+            & failure
+          where
+            noStuckClaims = isTop stuckClaims
+            stuckPatterns =
+                OrPattern.fromPatterns (MultiAnd.map getStuckConfig stuckClaims)
+            getStuckConfig =
+                getRewritingPattern . getConfiguration . getStuckClaim
+    lift $ Foldable.for_ saveProofs $ saveProven specModule provenClaims
     lift $ renderResult execOptions (unparse final)
     return exitCode
   where
@@ -685,10 +696,10 @@ koreProve execOptions proveOptions = do
 
     saveProven
         :: VerifiedModule StepperAttributes
-        -> [SomeClaim]
+        -> MultiAnd SomeClaim
         -> FilePath
         -> IO ()
-    saveProven specModule provenClaims outputFile =
+    saveProven specModule (Foldable.toList -> provenClaims) outputFile =
         withFile outputFile WriteMode
             (`hPutDoc` unparse provenDefinition)
       where

kore/src/Kore/Exec.hs

@@ -38,9 +38,6 @@ import Control.Monad
 import Control.Monad.Catch
     ( MonadMask
     )
-import Control.Monad.Trans.Except
-    ( runExceptT
-    )
 import Data.Coerce
     ( coerce
     )
@@ -106,7 +103,7 @@ import Kore.Reachability
     ( AllClaims (AllClaims)
     , AlreadyProven (AlreadyProven)
     , Axioms (Axioms)
-    , ProofStuck (..)
+    , ProveClaimsResult (..)
     , Rule (ReachabilityRewriteRule)
     , SomeClaim (..)
     , ToProve (ToProve)
@@ -383,7 +380,7 @@ prove
     -- ^ The spec module
     -> Maybe (VerifiedModule StepperAttributes)
     -- ^ The module containing the claims that were proven in a previous run.
-    -> smt (Either ProofStuck ())
+    -> smt ProveClaimsResult
 prove
     searchOrder
     breadthLimit
@@ -410,7 +407,6 @@ prove
                     (extractUntrustedClaims' claims)
                 )
             )
-            & runExceptT
   where
     extractUntrustedClaims' :: [SomeClaim] -> [SomeClaim]
     extractUntrustedClaims' = filter (not . isTrusted)

kore/src/Kore/Reachability.hs

@@ -6,10 +6,14 @@ License     : NCSA
 
 module Kore.Reachability
     ( AllPathClaim (..)
+    , mkAllPathClaim
     , allPathRuleToTerm
     , OnePathClaim (..)
+    , mkOnePathClaim
     , onePathRuleToTerm
     , SomeClaim (..)
+    , mkSomeClaimAllPath
+    , mkSomeClaimOnePath
     , makeTrusted
     , lensClaimPattern
     , getConfiguration

kore/src/Kore/Reachability/AllPathClaim.hs

@@ -6,6 +6,7 @@ License     : NCSA
 
 module Kore.Reachability.AllPathClaim
     ( AllPathClaim (..)
+    , mkAllPathClaim
     , allPathRuleToTerm
     , Rule (..)
     ) where
@@ -29,10 +30,17 @@ import Kore.Debug
 import Kore.Internal.Alias
     ( Alias (aliasConstructor)
     )
+import Kore.Internal.OrPattern
+    ( OrPattern
+    )
+import Kore.Internal.Pattern
+    ( Pattern
+    )
 import qualified Kore.Internal.Pattern as Pattern
 import qualified Kore.Internal.Predicate as Predicate
 import Kore.Internal.TermLike
-    ( Id (getId)
+    ( ElementVariable
+    , Id (getId)
     , TermLike
     , VariableName
     , weakAlwaysFinally
@@ -71,6 +79,14 @@ newtype AllPathClaim =
     deriving anyclass (SOP.Generic, SOP.HasDatatypeInfo)
     deriving anyclass (Debug, Diff)
 
+mkAllPathClaim
+    :: Pattern RewritingVariableName
+    -> OrPattern RewritingVariableName
+    -> [ElementVariable RewritingVariableName]
+    -> AllPathClaim
+mkAllPathClaim left right existentials =
+    AllPathClaim (mkClaimPattern left right existentials)
+
 instance Unparse AllPathClaim where
     unparse claimPattern' =
         unparse $ allPathRuleToTerm claimPattern'

kore/src/Kore/Reachability/OnePathClaim.hs

@@ -7,6 +7,7 @@ License     : NCSA
 module Kore.Reachability.OnePathClaim
     ( OnePathClaim (..)
     , onePathRuleToTerm
+    , mkOnePathClaim
     , Rule (..)
     ) where
 
@@ -26,10 +27,17 @@ import Kore.Debug
 import Kore.Internal.Alias
     ( Alias (aliasConstructor)
     )
+import Kore.Internal.OrPattern
+    ( OrPattern
+    )
+import Kore.Internal.Pattern
+    ( Pattern
+    )
 import qualified Kore.Internal.Pattern as Pattern
 import qualified Kore.Internal.Predicate as Predicate
 import Kore.Internal.TermLike
-    ( Id (getId)
+    ( ElementVariable
+    , Id (getId)
     , TermLike
     , VariableName
     , weakExistsFinally
@@ -76,6 +84,14 @@ onePathRuleToTerm :: OnePathClaim -> TermLike VariableName
 onePathRuleToTerm (OnePathClaim claimPattern') =
     claimPatternToTerm TermLike.WEF claimPattern'
 
+mkOnePathClaim
+    :: Pattern RewritingVariableName
+    -> OrPattern RewritingVariableName
+    -> [ElementVariable RewritingVariableName]
+    -> OnePathClaim
+mkOnePathClaim left right existentials =
+    OnePathClaim (mkClaimPattern left right existentials)
+
 instance Unparse OnePathClaim where
     unparse claimPattern' =
         unparse $ onePathRuleToTerm claimPattern'