Refresh existential claim variables (#1910)

* Add test/issue-1909

*  deriveWith: Refresh existential variables

* removeDestination: refresh claim at beginning

Modifying the right-hand side of the claim at the end of deriveWith does not
have the intended effect because the right-hand side of the claim is eventually
replaced by the transition rule, which assumes that the right-hand side never
changes.

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

kore/src/Kore/Step/RulePattern.hs

@@ -407,6 +407,30 @@ rhsSubstitute subst RHS { existentials, right, ensures } =
   where
     subst' = foldr (Map.delete . inject . variableName) subst existentials
 
+renameExistentials
+    :: forall variable
+    .  HasCallStack
+    => InternalVariable variable
+    => Map (SomeVariableName variable) (SomeVariable variable)
+    -> RHS variable
+    -> RHS variable
+renameExistentials rename RHS { existentials, right, ensures } =
+    RHS
+        { existentials =
+            renameVariable <$> existentials
+        , right = TermLike.substitute subst right
+        , ensures = Predicate.substitute subst ensures
+        }
+  where
+    renameVariable
+        :: ElementVariable variable
+        -> ElementVariable variable
+    renameVariable var =
+        let name = SomeVariableNameElement . variableName $ var
+         in maybe var expectElementVariable
+            $ Map.lookup name rename
+    subst = TermLike.mkVar <$> rename
+
 rhsForgetSimplified :: InternalVariable variable => RHS variable -> RHS variable
 rhsForgetSimplified RHS { existentials, right, ensures } =
     RHS
@@ -871,26 +895,36 @@ instance UnifyingRule RulePattern where
 
     precondition = requires
 
-    refreshRule avoid' rule1@(RulePattern _ _ _ _ _) =
-        let avoid = FreeVariables.toNames avoid'
-            rename = refreshVariables (avoid <> exVars) originalFreeVariables
-            subst = TermLike.mkVar <$> rename
-            left' = TermLike.substitute subst left
-            antiLeft' = TermLike.substitute subst <$> antiLeft
-            requires' = Predicate.substitute subst requires
-            rhs' = rhsSubstitute subst rhs
-            rule2 =
-                rule1
-                    { left = left'
-                    , antiLeft = antiLeft'
-                    , requires = requires'
-                    , rhs = rhs'
-                    }
-        in (rename, rule2)
+    refreshRule stale0' rule0@(RulePattern _ _ _ _ _) =
+        let stale0 = FreeVariables.toNames stale0'
+            freeVariables0 = freeVariables rule0
+            renaming1 =
+                refreshVariables stale0
+                $ FreeVariables.toSet freeVariables0
+            freeVariables1 =
+                FreeVariables.toSet freeVariables0
+                & Set.map (renameVariable renaming1)
+                & foldMap FreeVariables.freeVariable
+            existentials0 = Set.fromList . map inject $ existentials $ rhs rule0
+            stale1 = FreeVariables.toNames freeVariables1 <> stale0
+            renamingExists = refreshVariables stale1 existentials0
+            subst = TermLike.mkVar <$> renaming1
+            rule1 =
+                RulePattern
+                { left = left rule0 & TermLike.substitute subst
+                , antiLeft = antiLeft rule0 & fmap (TermLike.substitute subst)
+                , requires = requires rule0 & Predicate.substitute subst
+                , rhs =
+                    rhs rule0
+                    & renameExistentials renamingExists
+                    & rhsSubstitute subst
+                , attributes = attributes rule0
+                }
+        in (renaming1, rule1)
       where
-        RulePattern { left, antiLeft, requires, rhs } = rule1
-        exVars = Set.fromList $ inject . variableName <$> existentials rhs
-        originalFreeVariables = freeVariables rule1 & FreeVariables.toSet
+        renameVariable map' var =
+            Map.lookup (variableName var) map'
+            & fromMaybe var
 
     mapRuleVariables adj rule1@(RulePattern _ _ _ _ _) =
         rule1

kore/src/Kore/Strategies/Goal.hs

@@ -808,7 +808,7 @@ removeDestination lensRulePattern mkState goal =
     removeDestinationWorker
         :: RulePattern VariableName
         -> m (ProofState goal (RulePattern VariableName))
-    removeDestinationWorker rulePattern =
+    removeDestinationWorker (snd . Step.refreshRule mempty -> rulePattern) =
         do
             removal <- removalPatterns destination configuration existentials
             when (isTop removal) (succeed . mkState $ rulePattern)
@@ -902,11 +902,14 @@ deriveWith
     -> goal
     -> Strategy.TransitionT (Rule goal) m (ProofState goal goal)
 deriveWith lensRulePattern mkRule takeStep rewrites goal =
-    (\x -> getCompose $ x goal)
-    $ Lens.traverseOf (lensRulePattern . RulePattern.leftPattern)
-    $ \config -> Compose $ withConfiguration config $ do
-        results <- takeStep rewrites config & lift
-        deriveResults mkRule results
+    getCompose
+    $ Lens.forOf lensRulePattern goal
+    $ \rulePattern ->
+        fmap (snd . Step.refreshRule mempty)
+        $ Lens.forOf RulePattern.leftPattern rulePattern
+        $ \config -> Compose $ withConfiguration config $ do
+            results <- takeStep rewrites config & lift
+            deriveResults mkRule results
 
 -- | Apply 'Rule's to the goal in sequence.
 deriveSeq

kore/test/Test/Kore/Step/RulePattern.hs

@@ -1,6 +1,6 @@
 module Test.Kore.Step.RulePattern
     ( test_freeVariables
-    , test_refreshRulePattern
+    , test_refreshRule
     ) where
 
 import Prelude.Kore
@@ -32,9 +32,9 @@ test_freeVariables =
             actual = freeVariables testRulePattern
         assertEqual "Expected free variables" expect actual
 
-test_refreshRulePattern :: TestTree
-test_refreshRulePattern =
-    testCase "Rename target variables" $ do
+test_refreshRule :: [TestTree]
+test_refreshRule =
+    [ testCase "Rename target variables" $ do
         let avoiding :: FreeVariables VariableName
             avoiding = freeVariables testRulePattern
             (renaming, rulePattern') =
@@ -54,6 +54,26 @@ test_refreshRulePattern =
         assertBool
             "Expected no free variables in common with original RulePattern"
             (all notAvoided (FreeVariables.toList free'))
+    , testCase "no stale variables" $ do
+        let (renaming, _) = refreshRule mempty testRulePattern
+        assertBool "expected not to rename variables" (null renaming)
+    , testGroup "stale existentials" $
+        let assertions (renaming, RulePattern { rhs }) = do
+                assertBool "expected to refresh existentials"
+                    (notElem Mock.y $ existentials rhs)
+                assertBool "expected to substitute fresh variables"
+                    ((/=) (mkElemVar Mock.y) $ right rhs)
+                assertBool "expected not to rename free variables"
+                    (null renaming)
+        in
+        [ testCase "from outside" $ do
+            let stale = freeVariable (inject Mock.y)
+            assertions $ refreshRule stale testRulePattern
+        , testCase "from left-hand side" $ do
+            let input = testRulePattern { left = mkElemVar Mock.y }
+            assertions $ refreshRule mempty input
+        ]
+    ]
 
 testRulePattern :: RulePattern VariableName
 testRulePattern =

test/issue-1909/Makefile

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

test/issue-1909/sum-spec.k

@@ -0,0 +1,15 @@
+module VERIFICATION
+  imports TEST
+endmodule
+
+module SUM-SPEC
+  import VERIFICATION
+
+  rule  <k> loop(N:Int) => . ...</k>
+        <counter> C:Int => ?_ </counter>
+        <sum> S:Int => ?S:Int </sum>
+    requires
+      N >=Int 0
+    ensures
+      ?S ==Int S +Int N *Int C +Int (N -Int 1) *Int N /Int 2
+endmodule

test/issue-1909/sum-spec.k.out.golden

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

test/issue-1909/test.k

@@ -0,0 +1,24 @@
+// Copyright (c) 2020 K Team. All Rights Reserved.
+
+module TEST-SYNTAX
+    imports INT
+
+    syntax Pgm ::= loop ( Int )
+endmodule
+
+module TEST
+    imports TEST-SYNTAX
+
+    configuration
+      <k> $PGM:Pgm </k>
+      <counter> 1 </counter>
+      <sum> 0 </sum>
+
+    rule
+      <k> loop(0) => . ... </k>
+    rule
+      <k> loop(Times:Int => Times -Int 1) ...</k>
+      <counter> C:Int => C +Int 1 </counter>
+      <sum> S:Int => S +Int C </sum>
+      requires Times >Int 0
+endmodule