Prove infeasible states

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