Prove infeasible states (#1950)

* test/issue-1665

* Add InferDefined step to reachability strategy

For now, this step applies only to patterns that cannot be rewritten further, to
avoid getting stuck. Later, this will also be used to avoid repeated generation
of the same \ceil patterns.

Co-authored-by: rv-jenkins <[email protected]>

Author: ttuegel

kore/src/Kore/Strategies/Goal.hs

@@ -85,6 +85,9 @@ import Kore.Internal.Pattern
     ( Pattern
     )
 import qualified Kore.Internal.Pattern as Pattern
+import Kore.Internal.Predicate
+    ( makeCeilPredicate_
+    )
 import qualified Kore.Internal.SideCondition as SideCondition
 import Kore.Internal.Symbol
     ( Symbol
@@ -199,6 +202,11 @@ class Goal goal where
     -- checkImplication.
     isTriviallyValid :: goal -> Bool
 
+    inferDefined
+        :: MonadSimplify m
+        => goal
+        -> Strategy.TransitionT (Rule goal) m goal
+
     checkImplication
         :: MonadSimplify m
         => goal -> m (CheckImplicationResult goal)
@@ -277,8 +285,9 @@ simplifies the implementation. However, this assumption is not an essential
 feature of the algorithm. You should not rely on this assumption elsewhere. This
 decision is subject to change without notice.
 
-This instance contains the default implementation for a one-path strategy. You can apply it to the
-first two arguments and pass the resulting function to 'Kore.Strategies.Verification.verify'.
+This instance contains the default implementation for a one-path strategy. You
+can apply it to the first two arguments and pass the resulting function to
+'Kore.Strategies.Verification.verify'.
 
 Things to note when implementing your own:
 
@@ -304,6 +313,8 @@ instance Goal OnePathRule where
 
     isTriviallyValid = isTriviallyValid' _Unwrapped
 
+    inferDefined = inferDefined' _Unwrapped
+
 deriveSeqOnePath
     ::  MonadSimplify simplifier
     =>  [Rule OnePathRule]
@@ -331,6 +342,7 @@ instance Goal AllPathRule where
     simplify = simplify' _Unwrapped
     checkImplication = checkImplication' _Unwrapped
     isTriviallyValid = isTriviallyValid' _Unwrapped
+    inferDefined = inferDefined' _Unwrapped
     applyClaims claims = deriveSeqAllPath (map goalToRule claims)
 
     applyAxioms axiomss = \goal ->
@@ -406,6 +418,15 @@ instance Goal ReachabilityRule where
     isTriviallyValid (AllPath goal) = isTriviallyValid goal
     isTriviallyValid (OnePath goal) = isTriviallyValid goal
 
+    inferDefined (AllPath goal) =
+        inferDefined goal
+        & fmap AllPath
+        & allPathTransition
+    inferDefined (OnePath goal) =
+        inferDefined goal
+        & fmap OnePath
+        & onePathTransition
+
     applyClaims claims (AllPath goal) =
         applyClaims (mapMaybe maybeAllPath claims) goal
         & fmap (fmap AllPath)
@@ -498,6 +519,13 @@ transitionRule claims axiomGroups = transitionRuleWorker
         Profile.timeStrategy "Goal.SimplifyRemainder"
         $ GoalRemainder <$> simplify goal
 
+    transitionRuleWorker InferDefined (GoalRemainder goal) =
+        Profile.timeStrategy "inferDefined" $ do
+            results <- tryTransitionT (inferDefined goal)
+            case results of
+                [] -> return Proven
+                _ -> GoalRemainder <$> Transition.scatter results
+
     transitionRuleWorker CheckImplication (Goal goal) =
         Profile.timeStrategy "Goal.CheckImplication" $ do
             result <- checkImplication goal
@@ -559,6 +587,7 @@ reachabilityFirstStep =
         , CheckGoalStuck
         , CheckGoalRemainder
         , Simplify
+        , InferDefined
         , TriviallyValid
         , CheckImplication
         , ApplyAxioms
@@ -574,6 +603,7 @@ reachabilityNextStep =
         , CheckGoalStuck
         , CheckGoalRemainder
         , Simplify
+        , InferDefined
         , TriviallyValid
         , CheckImplication
         , ApplyClaims
@@ -623,7 +653,10 @@ checkImplication' lensRulePattern goal =
         do
             removal <- removalPatterns destination configuration existentials
             when (isTop removal) (succeed . NotImplied $ rulePattern)
-            let configAndRemoval = fmap (configuration <*) removal
+            let definedConfig =
+                    Pattern.andCondition configuration
+                    $ from $ makeCeilPredicate_ (Conditional.term configuration)
+            let configAndRemoval = fmap (definedConfig <*) removal
                 sideCondition =
                     Pattern.withoutTerm configuration
                     & SideCondition.fromCondition
@@ -669,6 +702,22 @@ simplify' lensRulePattern =
             then pure Pattern.bottom
             else Foldable.asum (pure <$> configs)
 
+inferDefined'
+    :: MonadSimplify m
+    => Lens' goal (RulePattern VariableName)
+    -> goal
+    -> Strategy.TransitionT (Rule goal) m goal
+inferDefined' lensRulePattern =
+    Lens.traverseOf (lensRulePattern . RulePattern.leftPattern) $ \config -> do
+        let definedConfig =
+                Pattern.andCondition config
+                $ from $ makeCeilPredicate_ (Conditional.term config)
+        configs <-
+            simplifyTopConfiguration definedConfig
+            >>= SMT.Evaluator.filterMultiOr
+            & lift
+        Foldable.asum (pure <$> configs)
+
 isTriviallyValid' :: Lens' goal (RulePattern variable) -> goal -> Bool
 isTriviallyValid' lensRulePattern =
     isBottom . RulePattern.left . Lens.view lensRulePattern

kore/src/Kore/Strategies/ProofState.hs

@@ -38,6 +38,10 @@ data Prim
     -- ^ Mark all goals rewritten previously as new goals.
     | Simplify
     | CheckImplication
+    -- ^ Check if the claim's implication is valid.
+    | InferDefined
+    -- ^ Infer that the left-hand side of the claim is defined. This is related
+    -- to 'CheckImplication', but separated as an optimization.
     | TriviallyValid
     | ApplyClaims
     | ApplyAxioms
@@ -50,6 +54,7 @@ instance Pretty Prim where
     pretty ResetGoal = "Transition ResetGoal."
     pretty Simplify = "Transition Simplify."
     pretty CheckImplication = "Transition CheckImplication."
+    pretty InferDefined = "infer left-hand side is defined"
     pretty TriviallyValid = "Transition TriviallyValid."
     pretty ApplyClaims = "apply claims"
     pretty ApplyAxioms = "apply axioms"

kore/test/Test/Kore/Strategies/AllPath/AllPath.hs

@@ -3,6 +3,7 @@ module Test.Kore.Strategies.AllPath.AllPath
     , test_transitionRule_CheckProven
     , test_transitionRule_CheckGoalRem
     , test_transitionRule_CheckImplication
+    , test_transitionRule_InferDefined
     , test_transitionRule_TriviallyValid
     , test_transitionRule_ApplyClaims
     , test_transitionRule_ApplyAxioms
@@ -226,6 +227,19 @@ test_transitionRule_ApplyAxioms =
         -> TestTree
     derives rules = equals_ (run rules $ ProofState.GoalRemainder (A, C))
 
+test_transitionRule_InferDefined :: [TestTree]
+test_transitionRule_InferDefined =
+    [ unmodified ProofState.Proven
+    , unmodified (ProofState.Goal (A, B))
+    , unmodified (ProofState.GoalStuck (A, B))
+    , ProofState.GoalRemainder (NotDef, B) `becomes` (ProofState.Proven, mempty)
+    ]
+  where
+    run = runTransitionRule [] [] ProofState.InferDefined
+    unmodified :: HasCallStack => ProofState -> TestTree
+    unmodified state = run state `equals_` [(state, mempty)]
+    becomes initial final = run initial `equals_` [final]
+
 test_runStrategy :: [TestTree]
 test_runStrategy =
     [ [] `proves`    (A, A)
@@ -240,7 +254,8 @@ test_runStrategy =
 
     , [Rule (A, A)] `proves` (A, B)
     , [Rule (A, A)] `proves` (A, C)
-    , [Rule (A, A)] `disproves` (A, C) $ []
+
+    , [Rule (A, NotDef)] `disproves` (A, C) $ []
 
     , fmap Rule [(A, B), (A, C)] `proves`    (A, BorC)
     , fmap Rule [(A, B), (A, C)] `disproves` (A, B   ) $ [(C, B)]
@@ -307,7 +322,7 @@ insEdge
 insEdge = Strategy.insEdge
 
 -- | Simple program configurations for unit testing.
-data K = BorC | A | B | C | D | E | F | Bot
+data K = BorC | A | B | C | D | E | F | NotDef | Bot
     deriving (Eq, GHC.Generic, Ord, Show)
 
 instance SOP.Generic K
@@ -346,6 +361,7 @@ newtype instance Goal.Rule Goal =
 instance Goal.Goal Goal where
     checkImplication (src, dst)
       | src' == Bot = return Goal.Implied
+      | src == NotDef = return Goal.Implied
       | otherwise = return $ Goal.NotImplied (src', dst)
       where
         src' = difference src dst
@@ -356,6 +372,10 @@ instance Goal.Goal Goal where
 
     simplify = return
 
+    inferDefined goal@(src, _)
+      | src == NotDef = empty
+      | otherwise = pure goal
+
     applyClaims claims = derivePar (map Rule claims)
 
     applyAxioms axiomGroups = derivePar (concat axiomGroups)

test/issue-1665/Makefile

@@ -0,0 +1 @@
+include $(CURDIR)/../include.mk

test/issue-1665/issue-1665-spec.k

@@ -0,0 +1,12 @@
+module VERIFICATION
+  import TEST
+endmodule
+
+module ISSUE-1665-SPEC
+  import VERIFICATION
+
+  // Proving this claim requires inferring that the left-hand side of an
+  // intermediate proof goal is defined.
+  //
+  rule <k> begin _ => end ?_ </k>
+endmodule

test/issue-1665/issue-1665-spec.k.out.golden

@@ -0,0 +1 @@
+#True

test/issue-1665/test.k

@@ -0,0 +1,19 @@
+module TEST-SYNTAX
+  import INT
+
+  syntax Pgm ::= "begin" Int | "end" Int
+  syntax Int ::= fun(Int) [function, no-evaluators]
+  syntax Bool ::= isFun(Int) [function, functional, no-evaluators]
+
+endmodule
+
+module TEST
+  import TEST-SYNTAX
+
+  configuration <k> $PGM:Pgm </k>
+
+  rule begin X => end fun(X)
+
+  rule [ceil-fun]: #Ceil(fun(X:Int)) => #True requires isFun(X) [anywhere, simplification]
+
+endmodule