Rename free rule variables at initialization (#1794)

* Kore.Exec: Remove ToRulePattern

* Kore.HasPriority

* Kore.Step: Remove ToRulePattern

* HasAttributes

* Kore.Repl: Remove type parameters

* Kore.Repl: Remove ReplState type parameter

* Kore.Repl: Remove Config type parameter

* instance From _ SourceLocation

* instance From _ Label, instance From _ RuleIndex

* ReachabilityRule: Remove type parameter

* OnePathRule: Remove type parameter

* AllPathRule: Remove type parameter

* Kore.Strategies.Goal: Formatting

* Kore.Strategies.Goal.ProofState: Require fewer type parameters

* Generalize signature of getPriorityOfAxiom

* Kore.Strategies.Goal.removeDestination: Specify signature

* Kore.Strategies.Goal.removeDestination: Remove ToRulePattern

* leftPattern: Obey Lens laws

* Kore.Step.RulePattern: Initialize predicate sorts correctly

* Test.Kore.Strategies.OnePath.Step: Initialize rule sorts correctly

* Kore.Strategies.Goal: Preserve proof goal sorts

* Test.Kore.Step.Rule.Simplify: Preserve sorts

* simplifyClaimRule: Apply simplification substitution

* instance From (Conditional _ _) (Predicate _): Preserve predicate sort

* removeDestination: Remove nested if statements

* Kore.Strategies.Goal.simplify: Remove ToRulePattern

* Refactor Kore.Strategies.Goal.simplify

* Kore.Strategies.Goal.isTriviallyValid: Remove ToRulePattern

* Kore.Strategies.Goal.isTrusted: Remove ToRulePattern

* Kore.Strategies.Goal.deriveWith: Remove constraint ToRulePattern

* Kore.Strategies.Goal.deriveResults: Remove constraint FromRulePattern

* Kore.Strategies.Goal: Remove constraints ToRulePattern, FromRulePattern

* Kore.Strategies.Verification: Specialize to ReachabilityRule

* Kore.Strategies.Verification.verifyHelper: Specialize to ReachabilityRule

* Kore.Strategies.Verification.Stuck: Specialize type

* Kore.Strategies.Verification.verifyClaim: Specialize type to ReachabilityRule

* Kore.Strategies.Verification.verifyClaimStep: Specialize type to ReachabilityRule

* Kore.Strategies.Verification.transitionRule': Specialize type to ReachabilityRule

* Kore.Strategies.Verification: Clean up

* Remove type Kore.Strategies.Verification.Claim

* Kore.Strategies.Verification: TODO

* Kore.Strategies.Goal: Remove ToRulePattern

* Remove function Kore.Strategies.Goal.configurationDestinationToRule

* Kore.Strategies.Rule: Remove instances of ToRulePattern and FromRulePattern

* Revert "Kore.Strategies.Rule: Remove instances of ToRulePattern and FromRulePattern"

This reverts commit 4260645.

* Kore.Repl: Remove constraint ToRulePattern

* Kore.Strategies.Rule: Remove instances of FromRulePattern

* Kore.Repl: Remove use of function ruleToGoal

* Remove member ruleToGoal of class Goal

* Rename free rule variables at initialization

Instead of renaming the variables of each semantic rule as it is attempted, the
free variables of each rule are renamed at initialization. The former behavior
exhibits poor performance: the work of renaming is substantially duplicated
because every semantic rule is attempted at every step. There is a small amount
of work to rename the free variables of each _applied_ semantic rule, but the
number of applied rules is small, and this work is not really duplicated.

* Kore.Exec: Undo CPS transformations

* Kore.Exec: Use Compose

* extractClaim: Do not return attributes used to construct claim

The attributes can be accessed from the claim itself, there is no need to
return a tuple of attributes and claim.

* PROF OPTIONS_GHC -fno-prof-auto

* ruleAllPathToRuleReachability: Use coerce

* fixup! PROF OPTIONS_GHC -fno-prof-auto

* Kore.Exec: Lint

* Kore.Exec: Lint

* Kore.Strategies.Goal: Remove duplicate withConfiguration'

Author: ttuegel

kore/src/Branch.hs

@@ -6,6 +6,8 @@ License     : NCSA
 
 {-# LANGUAGE UndecidableInstances #-}
 
+{-# OPTIONS_GHC -fno-prof-auto #-}
+
 module Branch
     ( BranchT (..)
     , mapBranchT

kore/src/Kore/Debug.hs

@@ -1,4 +1,5 @@
 {-# OPTIONS_GHC -Wno-unused-top-binds    #-}
+{-# OPTIONS_GHC -fno-prof-auto #-}
 
 {- |
 Copyright   : (c) Runtime Verification, 2018

kore/src/Kore/Exec.hs

@@ -34,9 +34,6 @@ import Control.Monad.Catch
 import Control.Monad.Trans.Except
     ( runExceptT
     )
-import qualified Data.Bifunctor as Bifunctor
-    ( second
-    )
 import Data.Coerce
     ( coerce
     )
@@ -110,6 +107,7 @@ import qualified Kore.Profiler.Profile as Profiler
     )
 import qualified Kore.Repl as Repl
 import qualified Kore.Repl.Data as Repl.Data
+import Kore.Rewriting.RewritingVariable
 import Kore.Step
 import Kore.Step.Rule
     ( extractImplicationClaims
@@ -126,9 +124,7 @@ import Kore.Step.Rule.Simplify
     ( SimplifyRuleLHS (..)
     )
 import Kore.Step.RulePattern
-    ( AllPathRule (..)
-    , ImplicationRule (..)
-    , OnePathRule (..)
+    ( ImplicationRule (..)
     , ReachabilityRule (..)
     , RewriteRule (RewriteRule)
     , RulePattern (RulePattern)
@@ -329,10 +325,14 @@ prove
     depthLimit
     definitionModule
     specModule
-    maybeAlreadyProvenModule
+    trustedModule
   =
-    evalProver definitionModule specModule maybeAlreadyProvenModule
-    $ \initialized -> do
+    evalSimplifier definitionModule $ do
+        initialized <-
+            initializeProver
+                definitionModule
+                specModule
+                trustedModule
         let InitializedProver { axioms, claims, alreadyProven } = initialized
         verify
             breadthLimit
@@ -373,16 +373,20 @@ proveWithRepl
 proveWithRepl
     definitionModule
     specModule
-    maybeAlreadyProvenModule
+    trustedModule
     mvar
     replScript
     replMode
     scriptModeOutput
     outputFile
     mainModuleName
   =
-    evalProver definitionModule specModule maybeAlreadyProvenModule
-    $ \initialized -> do
+    evalSimplifier definitionModule $ do
+        initialized <-
+            initializeProver
+                definitionModule
+                specModule
+                trustedModule
         let InitializedProver { axioms, claims } = initialized
         Repl.runRepl
             axioms
@@ -410,8 +414,8 @@ boundedModelCheck
     -> Strategy.GraphSearchOrder
     -> smt (Bounded.CheckResult (TermLike Variable))
 boundedModelCheck breadthLimit depthLimit definitionModule specModule searchOrder =
-    evalSimplifier definitionModule $ initialize definitionModule
-    $ \initialized -> do
+    evalSimplifier definitionModule $ do
+        initialized <- initialize definitionModule
         let Initialized { rewriteRules } = initialized
             specClaims = extractImplicationClaims specModule
         assertSomeClaims specClaims
@@ -473,9 +477,8 @@ mergeRules
     -- ^ The list of rules to merge
     -> smt (Either Text [RewriteRule Variable])
 mergeRules ruleMerger verifiedModule ruleNames =
-    evalSimplifier verifiedModule
-    $ initialize verifiedModule
-    $ \initialized -> do
+    evalSimplifier verifiedModule $ do
+        initialized <- initialize verifiedModule
         let Initialized { rewriteRules } = initialized
 
         let nonEmptyRules :: Either Text (NonEmpty (RewriteRule Variable))
@@ -565,29 +568,19 @@ assertSomeClaims claims =
         ++  "Possible explanation: the frontend and the backend don't agree "
         ++  "on the representation of claims."
 
-makeReachabilityRule
-    :: (Attribute.Axiom Symbol Variable, ReachabilityRule)
-    -> ReachabilityRule
-makeReachabilityRule (attributes, reachabilityRule) =
-    case reachabilityRule of
-        OnePath (OnePathRule rulePattern) ->
-            OnePath (OnePathRule rulePattern { attributes })
-        AllPath (AllPathRule rulePattern) ->
-            AllPath (AllPathRule rulePattern { attributes })
-
 makeImplicationRule
     :: (Attribute.Axiom Symbol Variable, ImplicationRule Variable)
     -> ImplicationRule Variable
 makeImplicationRule (attributes, ImplicationRule rulePattern) =
     ImplicationRule rulePattern { attributes }
 
-simplifyRuleOnSecond
+simplifyReachabilityRule
     :: MonadSimplify simplifier
-    => (Attribute.Axiom Symbol variable, ReachabilityRule)
-    -> simplifier (Attribute.Axiom Symbol variable, ReachabilityRule)
-simplifyRuleOnSecond (atts, rule) = do
+    => ReachabilityRule
+    -> simplifier ReachabilityRule
+simplifyReachabilityRule rule = do
     rule' <- Rule.simplifyRewriteRule (RewriteRule . toRulePattern $ rule)
-    return (atts, Goal.fromRulePattern rule . getRewriteRule $ rule')
+    return (Goal.fromRulePattern rule . getRewriteRule $ rule')
 
 -- | Construct an execution graph for the given input pattern.
 execute
@@ -600,39 +593,37 @@ execute
     -> TermLike Variable
     -- ^ The input pattern
     -> simplifier Execution
-execute breadthLimit verifiedModule strategy inputPattern =
-    initialize verifiedModule $ \initialized -> do
-        let Initialized { rewriteRules } = initialized
-        simplifier <- Simplifier.askSimplifierTermLike
-        axiomIdToSimplifier <- Simplifier.askSimplifierAxioms
-        simplifiedPatterns <-
-            Pattern.simplify
-                SideCondition.top
-                (Pattern.fromTermLike inputPattern)
-        let
-            initialPattern =
-                case MultiOr.extractPatterns simplifiedPatterns of
-                    [] -> Pattern.bottomOf patternSort
-                    (config : _) -> config
-              where
-                patternSort = termLikeSort inputPattern
-            runStrategy' =
-                runStrategy breadthLimit transitionRule (strategy rewriteRules)
-        executionGraph <- runStrategy' initialPattern
-        return Execution
-            { simplifier
-            , axiomIdToSimplifier
-            , executionGraph
-            }
+execute breadthLimit verifiedModule strategy inputPattern = do
+    initialized <- initialize verifiedModule
+    let Initialized { rewriteRules } = initialized
+    simplifier <- Simplifier.askSimplifierTermLike
+    axiomIdToSimplifier <- Simplifier.askSimplifierAxioms
+    simplifiedPatterns <-
+        Pattern.simplify SideCondition.top
+        $ Pattern.fromTermLike inputPattern
+    let
+        initialPattern =
+            case MultiOr.extractPatterns simplifiedPatterns of
+                [] -> Pattern.bottomOf patternSort
+                (config : _) -> config
+          where
+            patternSort = termLikeSort inputPattern
+        runStrategy' =
+            runStrategy breadthLimit transitionRule (strategy rewriteRules)
+    executionGraph <- runStrategy' initialPattern
+    return Execution
+        { simplifier
+        , axiomIdToSimplifier
+        , executionGraph
+        }
 
 -- | Collect various rules and simplifiers in preparation to execute.
 initialize
-    :: forall a simplifier
+    :: forall simplifier
     .  MonadSimplify simplifier
     => VerifiedModule StepperAttributes
-    -> (Initialized -> simplifier a)
-    -> simplifier a
-initialize verifiedModule within = do
+    -> simplifier Initialized
+initialize verifiedModule = do
     let rewriteRules = extractRewriteAxioms verifiedModule
         simplifyToList
             :: SimplifyRuleLHS rule
@@ -646,9 +637,7 @@ initialize verifiedModule within = do
         $ find (lhsEqualsRhs . getRewriteRule) rewriteRules
     rewriteAxioms <- Profiler.initialization "simplifyRewriteRule" $
         mapM simplifyToList rewriteRules
-    --let axioms = coerce (concat simplifiedRewrite)
-    let initialized = Initialized { rewriteRules = concat rewriteAxioms }
-    within initialized
+    pure Initialized { rewriteRules = concat rewriteAxioms }
 
 data InitializedProver =
     InitializedProver
@@ -665,79 +654,44 @@ fromMaybeChanged (Unchanged a) = a
 
 -- | Collect various rules and simplifiers in preparation to execute.
 initializeProver
-    :: forall simplifier a
+    :: forall simplifier
     .  MonadSimplify simplifier
     => VerifiedModule StepperAttributes
     -> VerifiedModule StepperAttributes
     -> Maybe (VerifiedModule StepperAttributes)
-    -> (InitializedProver -> simplifier a)
-    -> simplifier a
-initializeProver definitionModule specModule maybeAlreadyProvenModule within =
-    initialize definitionModule
-    $ \initialized -> do
-        tools <- Simplifier.askMetadataTools
-        let Initialized { rewriteRules } = initialized
-            changedSpecClaims
-                ::  [   ( Attribute.Axiom Symbol Variable
-                        , MaybeChanged ReachabilityRule
-                        )
-                    ]
-            changedSpecClaims =
-                map
-                    (Bifunctor.second $ expandClaim tools)
-                    (Goal.extractClaims specModule)
-            mapMSecond
-                :: Monad m
-                => (rule -> m [rule'])
-                -> (attributes, rule) -> m [(attributes, rule')]
-            mapMSecond f (attribute, rule) = do
-                simplified <- f rule
-                return (map ((,) attribute) simplified)
-            simplifyToList
-                :: SimplifyRuleLHS rule
-                => rule
-                -> simplifier [rule]
-            simplifyToList rule = do
-                simplified <- simplifyRuleLhs rule
-                return (MultiAnd.extractPatterns simplified)
-
-            maybeClaimsAlreadyProven
-                :: Maybe
-                    [   ( Attribute.Axiom Symbol Variable
-                        , ReachabilityRule
-                        )
-                    ]
-            maybeClaimsAlreadyProven =
-                Goal.extractClaims <$> maybeAlreadyProvenModule
-            claimsAlreadyProven
-                ::  [   (Attribute.Axiom Symbol Variable
-                        , ReachabilityRule
-                        )
-                    ]
-            claimsAlreadyProven = fromMaybe [] maybeClaimsAlreadyProven
-
-        mapM_ (logChangedClaim . snd) changedSpecClaims
-
-        let specClaims
-                ::  [   ( Attribute.Axiom Symbol Variable
-                        , ReachabilityRule
-                        )
-                    ]
-            specClaims =
-                map (Bifunctor.second fromMaybeChanged) changedSpecClaims
-        -- This assertion should come before simplifying the claims,
-        -- since simplification should remove all trivial claims.
-        assertSomeClaims specClaims
-        simplifiedSpecClaims <-
-            mapM (mapMSecond simplifyToList) specClaims
-        specAxioms <- Profiler.initialization "simplifyRuleOnSecond"
-            $ traverse simplifyRuleOnSecond (concat simplifiedSpecClaims)
-        let claims = fmap makeReachabilityRule specAxioms
-            axioms = coerce rewriteRules
-            alreadyProven = fmap makeReachabilityRule claimsAlreadyProven
-            initializedProver =
-                InitializedProver {axioms, claims, alreadyProven}
-        within initializedProver
+    -> simplifier InitializedProver
+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
+            :: SimplifyRuleLHS rule
+            => rule
+            -> simplifier [rule]
+        simplifyToList rule = do
+            simplified <- simplifyRuleLhs rule
+            return (MultiAnd.extractPatterns simplified)
+
+        trustedClaims :: [ReachabilityRule]
+        trustedClaims =
+            fmap Goal.extractClaims maybeTrustedModule & fromMaybe []
+
+    mapM_ logChangedClaim changedSpecClaims
+
+    let specClaims :: [ReachabilityRule]
+        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 <- Profiler.initialization "simplifyRuleOnSecond"
+        $ traverse simplifyReachabilityRule (concat simplifiedSpecClaims)
+    let axioms = coerce . mkRewritingRule <$> rewriteRules
+        alreadyProven = trustedClaims
+    pure InitializedProver { axioms, claims, alreadyProven }
   where
     expandClaim
         :: SmtMetadataTools attributes
@@ -756,27 +710,3 @@ initializeProver definitionModule specModule maybeAlreadyProvenModule within =
     logChangedClaim (Changed claim) =
         Log.logInfo ("Claim variables were expanded:\n" <> unparseToText claim)
     logChangedClaim (Unchanged _) = return ()
-
-evalProver
-    ::  forall smt a
-      . ( Log.WithLog Log.LogMessage smt
-        , MonadProfiler smt
-        , MonadIO smt
-        , MonadSMT smt
-        )
-    => VerifiedModule StepperAttributes
-    -- ^ The main module
-    -> VerifiedModule StepperAttributes
-    -- ^ The spec module
-    -> Maybe (VerifiedModule StepperAttributes)
-    -- ^ The module containing the claims that were proven in a previous run.
-    -> (InitializedProver -> Simplifier.SimplifierT smt a)
-    -- The prover
-    -> smt a
-evalProver definitionModule specModule maybeAlreadyProvenModule prover =
-    evalSimplifier definitionModule
-    $ initializeProver
-        definitionModule
-        specModule
-        maybeAlreadyProvenModule
-        prover

kore/src/Kore/Internal/Conditional.hs

@@ -6,6 +6,8 @@ Representation of conditional terms.
 
 -}
 
+{-# OPTIONS_GHC -fno-prof-auto #-}
+
 module Kore.Internal.Conditional
     ( Conditional (..)
     , withoutTerm

kore/src/Kore/Log/DebugProofState.hs

@@ -14,9 +14,7 @@ import Data.Text.Prettyprint.Doc
     )
 import qualified Data.Text.Prettyprint.Doc as Pretty
 
-import Kore.Internal.TermLike
-    ( Variable
-    )
+import Kore.Rewriting.RewritingVariable
 import Kore.Step.RulePattern
     ( ReachabilityRule (..)
     , RewriteRule (..)
@@ -30,7 +28,7 @@ import Log
 data DebugProofState =
     DebugProofState
         { proofState :: ProofState ReachabilityRule
-        , transition :: Prim (RewriteRule Variable)
+        , transition :: Prim (RewriteRule RewritingVariable)
         , result :: Maybe (ProofState ReachabilityRule)
         }
 

kore/src/Kore/Profiler/Data.hs

@@ -2,6 +2,7 @@
 Copyright   : (c) Runtime Verification, 2019
 License     : NCSA
 -}
+{-# OPTIONS_GHC -fno-prof-auto #-}
 module Kore.Profiler.Data
     ( MonadProfiler (..)
     , profileEvent