Georgy/fix rule unification (#408)

Closes #406 * Make result indeterminate when trying to bind an already bound variable with a different expression. This was returning a failing result before, causing a soundness bug, because in some cases rules with duplicate variables in LHS would not be applied. * Make result indeterminate when unifying an injection with a variable. This allows us to get a clear remainder instead of a weird swapped substitution item * Only report violating substitution items
runtimeverification · Apr 10, 2024 · 6e358d8 · 6e358d8
1 parent 57cd6f6
commit 6e358d8
Show file tree

Hide file tree

Showing 4 changed files with 11 additions and 8 deletions.
diff --git a/booster/library/Booster/Pattern/Rewrite.hs b/booster/library/Booster/Pattern/Rewrite.hs
@@ -257,9 +257,10 @@ applyRule pat@Pattern{ceilConditions} rule = runRewriteRuleAppT $ do
 
     -- check it is a "matching" substitution (substitutes variables
     -- from the subject term only). Fail the entire rewrite if not.
-    unless (Map.keysSet subst == freeVariables rule.lhs) $
+    unless (Map.keysSet subst == freeVariables rule.lhs) $ do
+        let violatingItems = Map.restrictKeys subst (Map.keysSet subst `Set.difference` freeVariables rule.lhs)
         failRewrite $
-            UnificationIsNotMatch rule pat.term subst
+            UnificationIsNotMatch rule pat.term violatingItems
 
     -- Also fail the whole rewrite if a rule applies but may introduce
     -- an undefined term.

diff --git a/booster/library/Booster/Pattern/Unify.hs b/booster/library/Booster/Pattern/Unify.hs
@@ -261,6 +261,11 @@ unify1
             if isSubsort
                 then bindVariable var term2
                 else failWith $ DifferentSorts term1 term2
+-- term1 is an injection. We could unify, but it would not be a matching substitution: indeterminate
+unify1
+    inj@Injection{}
+    v@Var{} =
+        addIndeterminate inj v
 -- term2 variable (not target), term1 not a variable: swap arguments (won't recurse)
 unify1
     term1
@@ -575,7 +580,7 @@ bindVariable var term = do
                     | otherwise ->
                         -- the term in the binding could be _equivalent_
                         -- (not necessarily syntactically equal) to term'
-                        failWith $ VariableConflict var oldTerm term
+                        addIndeterminate oldTerm term
                 Nothing -> do
                     let
                         -- apply existing substitutions to term

diff --git a/booster/unit-tests/Test/Booster/Pattern/Rewrite.hs b/booster/unit-tests/Test/Booster/Pattern/Rewrite.hs
@@ -215,8 +215,6 @@ unifyNotMatch =
             subst =
                 Map.fromList
                     [ (Variable someSort "X", dv someSort "otherThing")
-                    , (Variable someSort "Y", d)
-                    , (Variable kSort "RuleVar", var "ConfigVar" kSort)
                     ]
         [trm| kCell{}( kseq{}( inj{SomeSort{}, SortKItem{}}( con3{}( X:SomeSort{}, \dv{SomeSort{}}("thing") ) ), ConfigVar:SortK{}) ) |]
             `failsWith` UnificationIsNotMatch rule3 t subst

diff --git a/booster/unit-tests/Test/Booster/Pattern/Unify.hs b/booster/unit-tests/Test/Booster/Pattern/Unify.hs
@@ -125,9 +125,8 @@ constructors =
               z = var "Z" someSort
               t1 = app con3 [var "X" someSort, var "X" someSort]
               t2 = app con3 [y, z]
-           in test "Matching the same variable in a constructor (failing)" t1 t2 $
-                failed $
-                    VariableConflict (Variable someSort "X") y z
+           in test "Matching the same variable in a constructor (indeterminate)" t1 t2 $
+                remainder [(y, z)]
         ]
 
 functions :: TestTree