Create a Kore.Reachability context (#2141)

* mv Kore.Strategies.Goal Kore.Reachability.Claim

* Kore.Reachability.Claim: Remove unprovenNodes and proven

* Import Kore.Reachability.Claim as Claim

* Rename ReachabilityRule to ReachabilityClaim

* Kore.Repl.Data: Remove Claim type synonym

* Rename Goal to Claim

* Move data family Rule into Claim class

* Rename ProofState to ClaimState

The data type does not represent the state of the entire proof, but only the
state of a single claim.

* ClaimState: Rename constructors

* Extract Kore.Reachability.Prim from Kore.Reachability.ClaimState

* mv Kore.Strategies.Verification Kore.Reachability.Prove

* Kore.Reachability.Prove: rename verify to proveClaims

* mv Test.Kore.Strategies Test.Kore.Reachability

* Kore.Reachability: AllPathClaim, OnePathClaim, SomeClaim

* Rename ReachabilityClaim to SomeClaim

There are three types which represent reachability logic claims (AllPathClaim,
OnePathClaim, and SomeClaim) so it did not make sense to call out SomeClaim as
_the_ ReachabilityClaim. The prefix Some- matches the typical naming convention
of collecting multiple subtypes in a sum type.

* HLint cleanup

* kore-exec: fix build

* Test.Kore.Reachability: move all prove tests to Prove.hs, remove duplicates

* Test.Kore.Reachability.Prove: clean-up exports

* Move Test.Kore.Strategies.OnePath.Step

* Update kore/src/Kore/Reachability/ClaimState.hs

Co-authored-by: ana-pantilie <[email protected]>

* Kore.Reachability.ClaimState: Alignment

* OnePathClaim: Remove obsolete comment

* SentenceVerifier: Use extractClaim

* Add Test.Expect.expectJust

* QualifiedAxiomPattern: Remove reachability claims

* Remove Kore.Reachability.SomeClaim.toSentence

* MockAllPath: Rename Goal to MockClaim

* MockAllPath: HLint

Co-authored-by: ana-pantilie <[email protected]>
Co-authored-by: ana-pantilie <[email protected]>

Author: ttuegel

kore/app/exec/Main.hs

@@ -132,12 +132,13 @@ import Kore.Parser
     ( ParsedPattern
     , parseKorePattern
     )
+import Kore.Reachability
+    ( ProofStuck (..)
+    , SomeClaim
+    )
+import qualified Kore.Reachability.Claim as Claim
 import Kore.Rewriting.RewritingVariable
 import Kore.Step
-import Kore.Step.ClaimPattern
-    ( ReachabilityRule
-    , toSentence
-    )
 import Kore.Step.RulePattern
     ( RewriteRule
     )
@@ -149,10 +150,6 @@ import Kore.Step.SMT.Lemma
 import Kore.Step.Strategy
     ( GraphSearchOrder (..)
     )
-import qualified Kore.Strategies.Goal as Goal
-import Kore.Strategies.Verification
-    ( Stuck (..)
-    )
 import Kore.Syntax.Definition
     ( Definition (Definition)
     , Module (Module)
@@ -611,9 +608,9 @@ mainWithOptions execOptions = do
             Nothing -> errorException someException
         throwM someException
 
-    handleWithConfiguration :: Goal.WithConfiguration -> Main ExitCode
+    handleWithConfiguration :: Claim.WithConfiguration -> Main ExitCode
     handleWithConfiguration
-        (Goal.WithConfiguration lastConfiguration someException)
+        (Claim.WithConfiguration lastConfiguration someException)
       = do
         liftIO $ renderResult
             execOptions
@@ -697,7 +694,7 @@ koreProve execOptions proveOptions = do
             maybeAlreadyProvenModule
 
     (exitCode, final) <- case proveResult of
-        Left Stuck { stuckPatterns, provenClaims } -> do
+        Left ProofStuck { stuckPatterns, provenClaims } -> do
             maybe
                 (return ())
                 (lift . saveProven specModule provenClaims)
@@ -733,7 +730,7 @@ koreProve execOptions proveOptions = do
 
     saveProven
         :: VerifiedModule StepperAttributes
-        -> [ReachabilityRule]
+        -> [SomeClaim]
         -> FilePath
         -> IO ()
     saveProven specModule provenClaims outputFile =
@@ -753,13 +750,15 @@ koreProve execOptions proveOptions = do
         isNotAxiomOrClaim (SentenceSortSentence _) = True
         isNotAxiomOrClaim (SentenceHookSentence _) = True
 
+        provenClaimSentences = map (from @SomeClaim @(Sentence _)) provenClaims
         provenModule =
             Module
                 { moduleName = savedProofsModuleName
                 , moduleSentences =
-                    specModuleDefinitions <> fmap toSentence provenClaims
+                    specModuleDefinitions <> provenClaimSentences
                 , moduleAttributes = def
                 }
+
         provenDefinition = Definition
             { definitionAttributes = def
             , definitionModules = [provenModule]

kore/src/Kore/ASTVerifier/SentenceVerifier.hs

@@ -79,18 +79,17 @@ import qualified Kore.Internal.Symbol as Internal.Symbol
 import Kore.Internal.TermLike.TermLike
     ( freeVariables
     )
+import Kore.Reachability
+    ( SomeClaim
+    , extractClaim
+    , lensClaimPattern
+    )
 import Kore.Sort
 import Kore.Step.ClaimPattern
-    ( AllPathRule (..)
-    , ClaimPattern
-    , OnePathRule (..)
+    ( ClaimPattern
     , freeVariablesLeft
     , freeVariablesRight
     )
-import Kore.Step.Rule
-    ( QualifiedAxiomPattern (..)
-    , fromSentenceAxiom
-    )
 import Kore.Syntax.Definition
 import Kore.Syntax.Variable
 import qualified Kore.Verified as Verified
@@ -406,12 +405,11 @@ verifyClaimSentence sentence =
             (field @"indexedModuleClaims")
             ((attrs, verified) :)
     rejectClaim attrs verified =
-        case fromSentenceAxiom (attrs, verified) of
-            Right (OnePathClaimPattern (OnePathRule claimPattern))
-              | rejectClaimPattern claimPattern -> True
-            Right (AllPathClaimPattern (AllPathRule claimPattern))
-              | rejectClaimPattern claimPattern -> True
-            _ -> False
+        do
+            someClaim <- extractClaim @SomeClaim (attrs, SentenceClaim verified)
+            let claimPattern = Lens.view lensClaimPattern someClaim
+            pure (rejectClaimPattern claimPattern)
+        & fromMaybe False
     rejectClaimPattern :: ClaimPattern -> Bool
     rejectClaimPattern claimPattern =
         not $ Set.isSubsetOf freeRightVars freeLeftVars

kore/src/Kore/Exec.hs

@@ -105,14 +105,23 @@ import Kore.Log.KoreLogOptions
     )
 import Kore.Log.WarnTrivialClaim
 import qualified Kore.ModelChecker.Bounded as Bounded
+import Kore.Reachability
+    ( AllClaims (AllClaims)
+    , AlreadyProven (AlreadyProven)
+    , Axioms (Axioms)
+    , ProofStuck (..)
+    , Rule (ReachabilityRewriteRule)
+    , SomeClaim (..)
+    , ToProve (ToProve)
+    , extractClaims
+    , isTrusted
+    , lensClaimPattern
+    , proveClaims
+    )
 import qualified Kore.Repl as Repl
 import qualified Kore.Repl.Data as Repl.Data
 import Kore.Rewriting.RewritingVariable
 import Kore.Step
-import Kore.Step.ClaimPattern
-    ( ReachabilityRule (..)
-    , lensClaimPattern
-    )
 import Kore.Step.Rule
     ( extractImplicationClaims
     , extractRewriteAxioms
@@ -156,15 +165,6 @@ import qualified Kore.Step.Strategy as Strategy
 import Kore.Step.Transition
     ( runTransitionT
     )
-import qualified Kore.Strategies.Goal as Goal
-import Kore.Strategies.Verification
-    ( AllClaims (AllClaims)
-    , AlreadyProven (AlreadyProven)
-    , Axioms (Axioms)
-    , Stuck (..)
-    , ToProve (ToProve)
-    , verify
-    )
 import Kore.Syntax.Module
     ( ModuleName
     )
@@ -386,7 +386,7 @@ prove
     -- ^ The spec module
     -> Maybe (VerifiedModule StepperAttributes)
     -- ^ The module containing the claims that were proven in a previous run.
-    -> smt (Either Stuck ())
+    -> smt (Either ProofStuck ())
 prove
     searchOrder
     breadthLimit
@@ -402,7 +402,7 @@ prove
                 specModule
                 trustedModule
         let InitializedProver { axioms, claims, alreadyProven } = initialized
-        verify
+        proveClaims
             breadthLimit
             searchOrder
             (AllClaims claims)
@@ -415,8 +415,8 @@ prove
             )
             & runExceptT
   where
-    extractUntrustedClaims' :: [ReachabilityRule] -> [ReachabilityRule]
-    extractUntrustedClaims' = filter (not . Goal.isTrusted)
+    extractUntrustedClaims' :: [SomeClaim] -> [SomeClaim]
+    extractUntrustedClaims' = filter (not . isTrusted)
 
 -- | Initialize and run the repl with the main and spec modules. This will loop
 -- the repl until the user exits.
@@ -650,11 +650,11 @@ makeImplicationRule
 makeImplicationRule (attributes, ImplicationRule rulePattern) =
     ImplicationRule rulePattern { attributes }
 
-simplifyReachabilityRule
+simplifySomeClaim
     :: MonadSimplify simplifier
-    => ReachabilityRule
-    -> simplifier ReachabilityRule
-simplifyReachabilityRule rule = do
+    => SomeClaim
+    -> simplifier SomeClaim
+simplifySomeClaim rule = do
     let claim = Lens.view lensClaimPattern rule
     claim' <- Rule.simplifyClaimPattern claim
     return $ Lens.set lensClaimPattern claim' rule
@@ -684,9 +684,9 @@ initialize verifiedModule = do
 
 data InitializedProver =
     InitializedProver
-        { axioms :: ![Goal.Rule ReachabilityRule]
-        , claims :: ![ReachabilityRule]
-        , alreadyProven :: ![ReachabilityRule]
+        { axioms :: ![Rule SomeClaim]
+        , claims :: ![SomeClaim]
+        , alreadyProven :: ![SomeClaim]
         }
 
 data MaybeChanged a = Changed !a | Unchanged !a
@@ -707,39 +707,35 @@ initializeProver definitionModule specModule maybeTrustedModule = do
     initialized <- initialize definitionModule
     tools <- Simplifier.askMetadataTools
     let Initialized { rewriteRules } = initialized
-        changedSpecClaims :: [MaybeChanged ReachabilityRule]
-        changedSpecClaims =
-            expandClaim tools <$> Goal.extractClaims specModule
-        simplifyToList
-            :: ReachabilityRule
-            -> simplifier [ReachabilityRule]
+        changedSpecClaims :: [MaybeChanged SomeClaim]
+        changedSpecClaims = expandClaim tools <$> extractClaims specModule
+        simplifyToList :: SomeClaim -> simplifier [SomeClaim]
         simplifyToList rule = do
             simplified <- simplifyRuleLhs rule
             let result = MultiAnd.extractPatterns simplified
             when (null result) $ warnTrivialClaimRemoved rule
             return result
 
-        trustedClaims :: [ReachabilityRule]
-        trustedClaims =
-            fmap Goal.extractClaims maybeTrustedModule & fromMaybe []
+        trustedClaims :: [SomeClaim]
+        trustedClaims = fmap extractClaims maybeTrustedModule & fromMaybe []
 
     mapM_ logChangedClaim changedSpecClaims
 
-    let specClaims :: [ReachabilityRule]
+    let specClaims :: [SomeClaim]
         specClaims = map fromMaybeChanged changedSpecClaims
     -- This assertion should come before simplifying the claims,
     -- since simplification should remove all trivial claims.
     assertSomeClaims specClaims
     simplifiedSpecClaims <- mapM simplifyToList specClaims
-    claims <- traverse simplifyReachabilityRule (concat simplifiedSpecClaims)
+    claims <- traverse simplifySomeClaim (concat simplifiedSpecClaims)
     let axioms = coerce <$> rewriteRules
         alreadyProven = trustedClaims
     pure InitializedProver { axioms, claims, alreadyProven }
   where
     expandClaim
         :: SmtMetadataTools attributes
-        -> ReachabilityRule
-        -> MaybeChanged ReachabilityRule
+        -> SomeClaim
+        -> MaybeChanged SomeClaim
     expandClaim tools claim =
         if claim /= expanded
             then Changed expanded
@@ -748,7 +744,7 @@ initializeProver definitionModule specModule maybeTrustedModule = do
         expanded = expandSingleConstructors tools claim
 
     logChangedClaim
-        :: MaybeChanged ReachabilityRule
+        :: MaybeChanged SomeClaim
         -> simplifier ()
     logChangedClaim (Changed claim) =
         Log.logInfo ("Claim variables were expanded:\n" <> unparseToText claim)

kore/src/Kore/Log/DebugProofState.hs renamed to kore/src/Kore/Log/DebugClaimState.hs

@@ -3,36 +3,38 @@ Copyright   : (c) Runtime Verification, 2020
 License     : NCSA
 -}
 
-module Kore.Log.DebugProofState
-    ( DebugProofState (..)
+module Kore.Log.DebugClaimState
+    ( DebugClaimState (..)
     ) where
 
 import Prelude.Kore
 
-import Kore.Step.ClaimPattern
-    ( ReachabilityRule (..)
+import Kore.Reachability.ClaimState
+    ( ClaimState (..)
     )
-import Kore.Strategies.ProofState
+import Kore.Reachability.Prim
     ( Prim (..)
-    , ProofState (..)
+    )
+import Kore.Reachability.SomeClaim
+    ( SomeClaim (..)
     )
 import Log
 import Pretty
     ( Pretty (..)
     )
 import qualified Pretty
 
-data DebugProofState =
-    DebugProofState
-        { proofState :: ProofState ReachabilityRule
+data DebugClaimState =
+    DebugClaimState
+        { proofState :: ClaimState SomeClaim
         , transition :: Prim
-        , result :: Maybe (ProofState ReachabilityRule)
+        , result :: Maybe (ClaimState SomeClaim)
         }
     deriving (Show)
 
-instance Pretty DebugProofState where
+instance Pretty DebugClaimState where
     pretty
-        DebugProofState
+        DebugClaimState
             { proofState
             , transition
             , result
@@ -47,6 +49,6 @@ instance Pretty DebugProofState where
             , Pretty.indent 4 (maybe "Terminal state." pretty result)
             ]
 
-instance Entry DebugProofState where
+instance Entry DebugClaimState where
     entrySeverity _ = Debug
     helpDoc _ = "log proof state"

kore/src/Kore/Log/DebugProven.hs

@@ -9,16 +9,16 @@ module Kore.Log.DebugProven
 
 import Prelude.Kore
 
-import Kore.Step.ClaimPattern
-    ( ReachabilityRule (..)
+import Kore.Reachability.SomeClaim
+    ( SomeClaim (..)
     )
 import Log
 import Pretty
     ( Pretty (..)
     )
 import qualified Pretty
 
-newtype DebugProven = DebugProven { claim :: ReachabilityRule }
+newtype DebugProven = DebugProven { claim :: SomeClaim }
     deriving (Show)
 
 instance Pretty DebugProven where

kore/src/Kore/Log/InfoReachability.hs

@@ -10,9 +10,7 @@ module Kore.Log.InfoReachability
 
 import Prelude.Kore
 
-import Kore.Strategies.ProofState
-    ( Prim (..)
-    )
+import Kore.Reachability.Prim
 import Log
 import Pretty
     ( Doc