Refactor reachability proof strategies (#1932)

* Rename "remove destination" to "check implication"

We would like to use the same terminology as the domain experts, which is "check
implication".

* Remove ProofState type family

The ProofState associated type family is always instantiated at the concrete
ProofState type, so this was a meaningless layer of indirection.

* Remove Prim type family

The associated type family Prim was only ever instantiated at a single type.

* checkImplication: Return CheckImplicationResult

The function checkImplication returns a CheckImplicationResult instead of a
ProofState. This follows a principle from domain-driven design: the function
indicates its own result (CheckImplicationResult) instead of telling the caller
what to do next (ProofState). The code is more flexible because checkImplication
now does not need to know anything about the caller.

* Move TransitionRuleTemplate into Goal class

* Move logTransitionRule to Kore.Strategies.Verification

This acts to separate the domain model from the application code.

* Move withDebugProofState to Kore.Strategies.Verification

This change extracts application code from the domain model.

* Extract transitionRule

Now, the only instance of transitionRule is the canonical instance. This
instance _defines_ reachability proving and the individual types of reachability
claims may only define how they implement each step.

* Move withConfiguration to Kore.Strategies.Verification

This change reinforces the separation between the application and domain model
code.

* Goal: Remove MonadCatch constraints

* Add applyClaims

* Add instance Foldable ProofState

* Add applyAxioms

* Remove redundant steps from one-path strategy

This makes the one-path strategy like the all-path strategy.

* Test.Kore.Strategies.AllPath.AllPath: Use ApplyAxioms and ApplyClaims

* Remove DerivePar and DeriveSeq

* TODO: ApplyResult

* Extract strategy from class Goal

The strategy belongs to and is common to all reachability proofs.

* Remove stray comment

* withConfiguration: Use extractUnproven

* rm test/imp/sum-breadth-limit-three-spec.k

Author: ttuegel

kore/src/Kore/Log/DebugProofState.hs

@@ -9,10 +9,8 @@ module Kore.Log.DebugProofState
 
 import Prelude.Kore
 
-import Kore.Rewriting.RewritingVariable
 import Kore.Step.RulePattern
     ( ReachabilityRule (..)
-    , RewriteRule (..)
     )
 import Kore.Strategies.ProofState
     ( Prim (..)
@@ -27,7 +25,7 @@ import qualified Pretty
 data DebugProofState =
     DebugProofState
         { proofState :: ProofState ReachabilityRule
-        , transition :: Prim (RewriteRule RewritingVariableName)
+        , transition :: Prim
         , result :: Maybe (ProofState ReachabilityRule)
         }
     deriving (Show)
@@ -44,14 +42,10 @@ instance Pretty DebugProofState where
             [ "Reached proof state with the following configuration:"
             , Pretty.indent 4 (pretty proofState)
             , "On which the following transition applies:"
-            , Pretty.indent 4 (prettyTransition transition)
+            , Pretty.indent 4 (pretty transition)
             , "Resulting in:"
             , Pretty.indent 4 (maybe "Terminal state." pretty result)
             ]
-      where
-        prettyTransition (DeriveSeq _) = "Transition DeriveSeq."
-        prettyTransition (DerivePar _) = "Transition DerivePar."
-        prettyTransition prim          = Pretty.pretty prim
 
 instance Entry DebugProofState where
     entrySeverity _ = Debug

kore/src/Kore/Log/InfoReachability.hs

@@ -6,7 +6,7 @@ License     : NCSA
 module Kore.Log.InfoReachability
     ( InfoReachability (..)
     , whileSimplify
-    , whileRemoveDestination
+    , whileCheckImplication
     , whileDeriveSeq
     , whileDerivePar
     ) where
@@ -19,7 +19,7 @@ import qualified Pretty
 
 data InfoReachability
     = InfoSimplify !ReachabilityRule
-    | InfoRemoveDestination !ReachabilityRule
+    | InfoCheckImplication !ReachabilityRule
     | InfoDeriveSeq ![Rule ReachabilityRule] !ReachabilityRule
     | InfoDerivePar ![Rule ReachabilityRule] !ReachabilityRule
     deriving (Show)
@@ -55,8 +55,8 @@ prettyInfoReachabilityGoalAndRules transition goal rules fromRule =
 instance Pretty.Pretty InfoReachability where
     pretty (InfoSimplify goal) =
         prettyInfoReachabilityGoal "Simplify" goal
-    pretty (InfoRemoveDestination goal) =
-        prettyInfoReachabilityGoal "RemoveDestination" goal
+    pretty (InfoCheckImplication goal) =
+        prettyInfoReachabilityGoal "CheckImplication" goal
     pretty (InfoDeriveSeq rules goal) =
         prettyInfoReachabilityGoalAndRules
             "DeriveSeq"
@@ -74,7 +74,7 @@ instance Entry InfoReachability where
     entrySeverity _ = Info
     shortDoc (InfoSimplify _) =
         Just "While simplifying the configuration"
-    shortDoc (InfoRemoveDestination _) =
+    shortDoc (InfoCheckImplication _) =
         Just "While checking implication of the proof goal"
     shortDoc (InfoDeriveSeq _ _) =
         Just "While applying axioms in sequence"
@@ -89,12 +89,12 @@ whileSimplify
     -> log a
 whileSimplify goal = logWhile (InfoSimplify goal)
 
-whileRemoveDestination
+whileCheckImplication
     :: MonadLog log
     => ReachabilityRule
     -> log a
     -> log a
-whileRemoveDestination goal = logWhile (InfoRemoveDestination goal)
+whileCheckImplication goal = logWhile (InfoCheckImplication goal)
 
 whileDeriveSeq
     :: MonadLog log