diff --git a/booster/library/Booster/Pattern/Match.hs b/booster/library/Booster/Pattern/Match.hs index 64d56776a2..11f0d64438 100644 --- a/booster/library/Booster/Pattern/Match.hs +++ b/booster/library/Booster/Pattern/Match.hs @@ -196,122 +196,73 @@ match1 :: Term -> StateT MatchState (Except MatchResult) () {- FOURMOLU_DISABLE -} +-- The matcher defers by default: the final generic rule resolves every pair +-- not handled earlier to addIndeterminate, which is always sound (the caller +-- decides what to do with an indeterminate verdict). Every row above it must +-- justify a stronger outcome: decomposition (\and, same-category descent), +-- variable binding, or decisive failure. Decisive failure is only sound for +-- two terms whose top-level categories are rigid (cannot change under +-- evaluation or instantiation, see isRigidCategory) and distinct. The few +-- explicit addIndeterminate rows below exist only to shadow a more generic +-- stronger row that would otherwise capture their cells. match1 Implies t1 t2 | t1 == t2 = pure () -match1 Eval t1@AndTerm{} t2@AndTerm{} = addIndeterminate t1 t2 -match1 _ (AndTerm t1a t1b) t2@AndTerm{} = enqueueRegularProblem t1a t2 >> enqueueRegularProblem t1b t2 -match1 _ (AndTerm t1a t1b) t2@DomainValue{} = enqueueRegularProblem t1a t2 >> enqueueRegularProblem t1b t2 -match1 _ (AndTerm t1a t1b) t2@Injection{} = enqueueRegularProblem t1a t2 >> enqueueRegularProblem t1b t2 -match1 _ (AndTerm t1a t1b) t2@KMap{} = enqueueRegularProblem t1a t2 >> enqueueRegularProblem t1b t2 -match1 _ (AndTerm t1a t1b) t2@KList{} = enqueueRegularProblem t1a t2 >> enqueueRegularProblem t1b t2 -match1 _ (AndTerm t1a t1b) t2@KSet{} = enqueueRegularProblem t1a t2 >> enqueueRegularProblem t1b t2 -match1 _ (AndTerm t1a t1b) t2@ConsApplication{} = enqueueRegularProblem t1a t2 >> enqueueRegularProblem t1b t2 -match1 _ (AndTerm t1a t1b) t2@FunctionApplication{} = enqueueRegularProblem t1a t2 >> enqueueRegularProblem t1b t2 +-- \and: Eval mode defers on a subject \and and on a pattern \and facing a +-- variable (shadowing the decomposition rules below); all other \and cells +-- decompose, pattern side first +match1 Eval t1 t2@AndTerm{} = addIndeterminate t1 t2 match1 Eval t1@AndTerm{} t2@Var{} = addIndeterminate t1 t2 -match1 _ (AndTerm t1a t1b) t2@Var{} = enqueueRegularProblem t1a t2 >> enqueueRegularProblem t1b t2 -match1 Eval t1@DomainValue{} t2@AndTerm{} = addIndeterminate t1 t2 -match1 _ t1@DomainValue{} (AndTerm t2a t2b) = enqueueRegularProblem t1 t2a >> enqueueRegularProblem t1 t2b -match1 _ (DomainValue s1 t1) (DomainValue s2 t2) = matchDV s1 t1 s2 t2 -match1 _ t1@DomainValue{} t2@Injection{} = failWith $ DifferentSymbols t1 t2 -match1 _ t1@DomainValue{} t2@KMap{} = failWith $ DifferentSymbols t1 t2 -match1 _ t1@DomainValue{} t2@KList{} = failWith $ DifferentSymbols t1 t2 -match1 _ t1@DomainValue{} t2@KSet{} = failWith $ DifferentSymbols t1 t2 -match1 _ t1@DomainValue{} t2@ConsApplication{} = failWith $ DifferentSymbols t1 t2 -match1 _ t1@DomainValue{} t2@FunctionApplication{} = addIndeterminate t1 t2 --- match with var on the RHS must be indeterminate when evaluating functions. see: https://github.com/runtimeverification/hs-backend-booster/issues/231 -match1 Eval t1@DomainValue{} t2@Var{} = addIndeterminate t1 t2 +match1 _ (AndTerm t1a t1b) t2 = enqueueRegularProblem t1a t2 >> enqueueRegularProblem t1b t2 +match1 _ t1 (AndTerm t2a t2b) = enqueueRegularProblem t1 t2a >> enqueueRegularProblem t1 t2b +-- variable patterns: bind (or defer/fail on sort grounds, inside matchVar) +match1 matchTy (Var var1) t2 = matchVar matchTy var1 t2 +-- variable subjects: indeterminate. see https://github.com/runtimeverification/hs-backend-booster/issues/231 (Eval) +match1 Eval t1 t2@Var{} = addIndeterminate t1 t2 -- match with var on RHS may lead to branching during rewriting, see https://github.com/runtimeverification/haskell-backend/issues/4100 --- Related cases are currently marked with a special function so they can be identified and changed together later (extending branching functionality) -match1 Rewrite t1@DomainValue{} (Var v2) = subjectVariableMatch t1 v2 -match1 Implies t1@DomainValue{} (Var v2) = subjectVariableMatch t1 v2 -match1 Eval t1@Injection{} t2@AndTerm{} = addIndeterminate t1 t2 -match1 _ t1@Injection{} (AndTerm t2a t2b) = enqueueRegularProblem t1 t2a >> enqueueRegularProblem t1 t2b -match1 _ t1@Injection{} t2@DomainValue{} = failWith $ DifferentSymbols t1 t2 -match1 matchTy (Injection source1 target1 trm1) (Injection source2 target2 trm2) = matchInj matchTy source1 target1 trm1 source2 target2 trm2 -match1 _ t1@Injection{} t2@KMap{} = failWith $ DifferentSymbols t1 t2 -match1 _ t1@Injection{} t2@KList{} = failWith $ DifferentSymbols t1 t2 -match1 _ t1@Injection{} t2@KSet{} = failWith $ DifferentSymbols t1 t2 -match1 _ t1@Injection{} t2@ConsApplication{} = failWith $ DifferentSymbols t1 t2 -match1 _ t1@Injection{} t2@FunctionApplication{} = addIndeterminate t1 t2 -match1 Rewrite t1@Injection{} (Var v2) = subjectVariableMatch t1 v2 -match1 _ t1@Injection{} t2@Var{} = addIndeterminate t1 t2 -match1 Eval t1@KMap{} t2@AndTerm{} = addIndeterminate t1 t2 -match1 _ t1@KMap{} (AndTerm t2a t2b) = enqueueRegularProblem t1 t2a >> enqueueRegularProblem t1 t2b -match1 _ t1@KMap{} t2@DomainValue{} = failWith $ DifferentSymbols t1 t2 -match1 Eval t1@KMap{} t2@Injection{} = addIndeterminate t1 t2 -match1 _ t1@KMap{} t2@Injection{} = failWith $ DifferentSymbols t1 t2 +-- Related cases are marked with a special function so they can be identified and changed together later (extending branching functionality) +match1 _ t1 (Var v2) = subjectVariableMatch t1 v2 +-- same-category pairs descend into their contents +match1 _ (DomainValue s1 t1) (DomainValue s2 t2) = matchDV s1 t1 s2 t2 +match1 _ (Injection source1 target1 trm1) (Injection source2 target2 trm2) = matchInj source1 target1 trm1 source2 target2 trm2 match1 _ t1@(KMap def1 patKeyVals patRest) t2@(KMap def2 subjKeyVals subjRest) = if def1 == def2 then matchMaps def1 patKeyVals patRest subjKeyVals subjRest else failWith $ DifferentSorts t1 t2 -match1 _ t1@KMap{} t2@KList{} = failWith $ DifferentSymbols t1 t2 -match1 _ t1@KMap{} t2@KSet{} = failWith $ DifferentSymbols t1 t2 -match1 _ t1@KMap{} t2@ConsApplication{} = failWith $ DifferentSymbols t1 t2 -match1 _ t1@KMap{} t2@FunctionApplication{} = addIndeterminate t1 t2 -match1 Rewrite t1@KMap{} (Var v2) = subjectVariableMatch t1 v2 -match1 _ t1@KMap{} t2@Var{} = addIndeterminate t1 t2 -match1 Eval t1@KList{} t2@AndTerm{} = addIndeterminate t1 t2 -match1 _ t1@KList{} (AndTerm t2a t2b) = enqueueRegularProblem t1 t2a >> enqueueRegularProblem t1 t2b -match1 _ t1@KList{} t2@DomainValue{} = failWith $ DifferentSymbols t1 t2 -match1 Eval t1@KList{} t2@Injection{} = addIndeterminate t1 t2 -match1 _ t1@KList{} t2@Injection{} = failWith $ DifferentSymbols t1 t2 -match1 _ t1@KList{} t2@KMap{} = failWith $ DifferentSymbols t1 t2 match1 _ t1@(KList def1 heads1 rest1) t2@(KList def2 heads2 rest2) = if def1 == def2 then matchLists def1 heads1 rest1 heads2 rest2 else failWith $ DifferentSorts t1 t2 -match1 _ t1@KList{} t2@KSet{} = failWith $ DifferentSymbols t1 t2 -match1 _ t1@KList{} t2@ConsApplication{} = failWith $ DifferentSymbols t1 t2 -match1 _ t1@KList{} t2@FunctionApplication{} = addIndeterminate t1 t2 -match1 Rewrite t1@KList{} (Var t2) = subjectVariableMatch t1 t2 -match1 _ t1@KList{} t2@Var{} = addIndeterminate t1 t2 -match1 Eval t1@KSet{} t2@AndTerm{} = addIndeterminate t1 t2 -match1 _ t1@KSet{} (AndTerm t2a t2b) = enqueueRegularProblem t1 t2a >> enqueueRegularProblem t1 t2b -match1 _ t1@KSet{} t2@DomainValue{} = failWith $ DifferentSymbols t1 t2 -match1 Eval t1@KSet{} t2@Injection{} = addIndeterminate t1 t2 -match1 _ t1@KSet{} t2@Injection{} = failWith $ DifferentSymbols t1 t2 -match1 _ t1@KSet{} t2@KMap{} = failWith $ DifferentSymbols t1 t2 -match1 _ t1@KSet{} t2@KList{} = failWith $ DifferentSymbols t1 t2 match1 _ t1@(KSet def1 patElements patRest) t2@(KSet def2 subjElements subjRest) = if def1 == def2 then matchSets def1 patElements patRest subjElements subjRest else failWith $ DifferentSorts t1 t2 -match1 _ t1@KSet{} t2@ConsApplication{} = failWith $ DifferentSymbols t1 t2 -match1 _ t1@KSet{} t2@FunctionApplication{} = addIndeterminate t1 t2 -match1 Rewrite t1@KSet{} (Var t2) = subjectVariableMatch t1 t2 -match1 _ t1@KSet{} t2@Var{} = addIndeterminate t1 t2 -match1 Eval t1@ConsApplication{} t2@AndTerm{} = addIndeterminate t1 t2 -match1 _ t1@ConsApplication{} (AndTerm t2a t2b) = enqueueRegularProblem t1 t2a >> enqueueRegularProblem t1 t2b -match1 _ t1@ConsApplication{} t2@DomainValue{} = failWith $ DifferentSymbols t1 t2 -match1 _ t1@ConsApplication{} t2@Injection{} = failWith $ DifferentSymbols t1 t2 -match1 _ t1@ConsApplication{} t2@KMap{} = failWith $ DifferentSymbols t1 t2 -match1 _ t1@ConsApplication{} t2@KList{} = failWith $ DifferentSymbols t1 t2 -match1 _ t1@ConsApplication{} t2@KSet{} = failWith $ DifferentSymbols t1 t2 match1 matchTy (ConsApplication symbol1 sorts1 args1) (ConsApplication symbol2 sorts2 args2) = matchSymbolAplications matchTy symbol1 sorts1 args1 symbol2 sorts2 args2 -match1 Eval (ConsApplication symbol1 sorts1 args1) (FunctionApplication symbol2 sorts2 args2) = matchSymbolAplications Eval symbol1 sorts1 args1 symbol2 sorts2 args2 -match1 _ t1@ConsApplication{} t2@FunctionApplication{} = addIndeterminate t1 t2 -match1 Rewrite t1@ConsApplication{} (Var t2) = subjectVariableMatch t1 t2 -match1 _ t1@ConsApplication{} t2@Var{} = addIndeterminate t1 t2 -match1 Eval t1@FunctionApplication{} t2@AndTerm{} = addIndeterminate t1 t2 -match1 _ t1@FunctionApplication{} (AndTerm t2a t2b) = enqueueRegularProblem t1 t2a >> enqueueRegularProblem t1 t2b -match1 Eval t1@FunctionApplication{} t2@DomainValue{} = failWith $ DifferentSymbols t1 t2 -match1 _ t1@FunctionApplication{} t2@DomainValue{} = addIndeterminate t1 t2 -match1 Eval t1@FunctionApplication{} t2@Injection{} = failWith $ DifferentSymbols t1 t2 -match1 _ t1@FunctionApplication{} t2@Injection{} = addIndeterminate t1 t2 -match1 Eval t1@FunctionApplication{} t2@KMap{} = failWith $ DifferentSymbols t1 t2 -match1 _ t1@FunctionApplication{} t2@KMap{} = addIndeterminate t1 t2 -match1 Eval t1@FunctionApplication{} t2@KList{} = failWith $ DifferentSymbols t1 t2 -match1 _ t1@FunctionApplication{} t2@KList{} = addIndeterminate t1 t2 -match1 Eval t1@FunctionApplication{} t2@KSet{} = failWith $ DifferentSymbols t1 t2 -match1 _ t1@FunctionApplication{} t2@KSet{} = addIndeterminate t1 t2 -match1 Eval (FunctionApplication symbol1 sorts1 args1) (ConsApplication symbol2 sorts2 args2) = matchSymbolAplications Eval symbol1 sorts1 args1 symbol2 sorts2 args2 -match1 _ t1@FunctionApplication{} t2@ConsApplication{} = addIndeterminate t1 t2 match1 Eval (FunctionApplication symbol1 sorts1 args1) (FunctionApplication symbol2 sorts2 args2) = matchSymbolAplications Eval symbol1 sorts1 args1 symbol2 sorts2 args2 -match1 _ t1@FunctionApplication{} t2@FunctionApplication{} = addIndeterminate t1 t2 -match1 Rewrite t1@FunctionApplication{} (Var t2) = subjectVariableMatch t1 t2 -match1 _ t1@FunctionApplication{} t2@Var{} = addIndeterminate t1 t2 -match1 Eval t1@Var{} t2@AndTerm{} = addIndeterminate t1 t2 -match1 _ t1@Var{} (AndTerm t2a t2b) = enqueueRegularProblem t1 t2a >> enqueueRegularProblem t1 t2b -match1 matchTy (Var var1) t2@DomainValue{} = matchVar matchTy var1 t2 -match1 matchTy (Var var1) t2@Injection{} = matchVar matchTy var1 t2 -match1 matchTy (Var var1) t2@KMap{} = matchVar matchTy var1 t2 -match1 matchTy (Var var1) t2@KList{} = matchVar matchTy var1 t2 -match1 matchTy (Var var1) t2@KSet{} = matchVar matchTy var1 t2 -match1 matchTy (Var var1) t2@ConsApplication{} = matchVar matchTy var1 t2 -match1 matchTy (Var var1) t2@FunctionApplication{} = matchVar matchTy var1 t2 -match1 matchTy (Var var1) t2@Var{} = matchVar matchTy var1 t2 +-- injection-vs-builtin-collection is indeterminate in both directions under +-- Eval (the injected term may simplify, and equation LHS sorts may be +-- misaligned with the subject); these rows shadow the decisive rule below +match1 Eval t1@Injection{} t2 | isCollection t2 = addIndeterminate t1 t2 +match1 Eval t1 t2@Injection{} | isCollection t1 = addIndeterminate t1 t2 +-- the remaining rigid pairs are cross-category and can never become equal +match1 _ t1 t2 | isRigidCategory t1, isRigidCategory t2 = failWith $ DifferentSymbols t1 t2 +-- everything else (a function application somewhere, or a future Term +-- constructor): cannot be decided here, defer +match1 _ t1 t2 = addIndeterminate t1 t2 {- FOURMOLU_ENABLE -} +{- | Whether the term's top-level category is rigid: it cannot change under + evaluation or instantiation. Domain values, injections, internalised + collections, and constructor applications are rigid: two such terms of + different categories can never become equal, so a decisive mismatch is + sound. Function applications, variables, and \and terms are not rigid. +-} +isRigidCategory :: Term -> Bool +isRigidCategory = \case + DomainValue{} -> True + Injection{} -> True + KMap{} -> True + KList{} -> True + KSet{} -> True + ConsApplication{} -> True + _ -> False + +isCollection :: Term -> Bool +isCollection = \case + KMap{} -> True + KList{} -> True + KSet{} -> True + _ -> False + matchDV :: Sort -> ByteString -> Sort -> ByteString -> StateT s (Except MatchResult) () matchDV s1 t1 s2 t2 = do @@ -327,7 +278,6 @@ matchDV s1 t1 s2 t2 = -- the contained pattern term is just a variable, otherwise they need -- to be identical. matchInj :: - MatchType -> Sort -> Sort -> Term -> @@ -336,7 +286,6 @@ matchInj :: Term -> StateT MatchState (Except MatchResult) () matchInj - _matchType source1 target1 trm1 @@ -348,7 +297,6 @@ matchInj | source1 == source2 = do enqueueRegularProblem trm1 trm2 matchInj - matchType source1 target1 trm1 @@ -367,24 +315,41 @@ matchInj -- source2 is already handled) unless (s1IsSubsort || s2IsSubsort) $ failWith (DifferentSorts trm1 trm2) - -- Functions may have a more general sort than the actual result. - -- This means we cannot simply fail the rewrite: the match is - -- indeterminate if the function result is. - case (s1IsSubsort, trm2) of - (True, FunctionApplication{}) -> - addIndeterminate trm1 trm2 - _ -> do - -- If the rule has a variable with a supersort of the - -- subject, trm2 can be bound with a suitable injection - case (s2IsSubsort, trm1) of - (True, Var v) -> - bindVariable matchType v (Injection source2 source1 trm2) - _ -> - -- truly different sorts, safe to just fail - failWith $ - DifferentSorts - (Injection source1 target1 trm1) - (Injection source2 target2 trm2) + -- A decisive failure is only sound when neither child can + -- change sort: a function application may have a more general + -- sort than the actual result, and a variable may be + -- instantiated at any subsort of its declared sort. Exactly + -- one of the subsort relations holds here (sources differ, + -- and the subsort order is antisymmetric). + case (trm1, trm2) of + (_, FunctionApplication{}) + | s1IsSubsort -> + -- the subject child may evaluate into source1 + addIndeterminate trm1 trm2 + (_, Var{}) + | s1IsSubsort -> + -- the subject child may be instantiated in source1 + addIndeterminate trm1 trm2 + (Var v, _) + | s2IsSubsort -> + -- pattern variable with a supersort of the subject: + -- bind with a suitable injection + bindVariable v (Injection source2 source1 trm2) + (FunctionApplication{}, _) + | s2IsSubsort -> + -- the pattern child may evaluate into source2 + addIndeterminate trm1 trm2 + _ -> + -- The remaining children are rigid (their sorts are exact), + -- or a function/variable at a sort that cannot narrow into + -- the other side (the narrowable directions are deferred by + -- the cases above): a decisive failure is sound. An \and + -- child never reaches matchInj (match1 decomposes a subject + -- \and before dispatching an injection pattern). + failWith $ + DifferentSorts + (Injection source1 target1 trm1) + (Injection source2 target2 trm2) {-# INLINE matchInj #-} ----- Symbol Applications @@ -462,7 +427,7 @@ matchVar failWith $ VariableConflict var1 (Var var1) (Var var2) matchVar -- term1 variable (target): introduce a new binding - matchType + _matchType var@Variable{variableSort} term2 = do @@ -473,11 +438,31 @@ matchVar checkSubsort subsorts termSort variableSort if isSubsort then - bindVariable matchType var $ + bindVariable var $ if termSort == variableSort then term2 else Injection termSort variableSort term2 - else failWith $ DifferentSorts (Var var) term2 + else case term2 of + -- The subject's static sort is only an upper bound when + -- the subject can still change shape: a function + -- application may evaluate to a term of a narrower sort, + -- and a variable may be instantiated with one. If the two + -- sorts share a subsort, a match may yet be possible, so + -- defer instead of failing decisively. + FunctionApplication{} + | sortsOverlap subsorts termSort variableSort -> + addIndeterminate (Var var) term2 + Var{} + | sortsOverlap subsorts termSort variableSort -> + addIndeterminate (Var var) term2 + -- term2 here is either rigid (its sort is exact) or a + -- function/variable whose sort is disjoint from the + -- variable's (sortsOverlap already deferred the overlapping + -- case): in neither case can evaluation or instantiation + -- bridge the sorts, so a decisive failure is sound. An \and + -- never reaches matchVar (match1 decomposes a subject \and + -- before dispatching a variable pattern). + _ -> failWith $ DifferentSorts (Var var) term2 -- Subject variable matches are currently marked as indeterminate. -- The code may be extended to collect these as separate conditional @@ -801,8 +786,8 @@ enqueueRegularProblems ts = binding to a term is added. This avoids repeated traversals while guarding against substitution loops. -} -bindVariable :: MatchType -> Variable -> Term -> StateT MatchState (Except MatchResult) () -bindVariable matchType var term@(Term termAttrs _) = do +bindVariable :: Variable -> Term -> StateT MatchState (Except MatchResult) () +bindVariable var term@(Term termAttrs _) = do State{mSubstitution = currentSubst} <- get case Map.lookup var currentSubst of Just oldTerm@(Term oldTermAttrs _) @@ -811,11 +796,18 @@ bindVariable matchType var term@(Term termAttrs _) = do , oldTermAttrs.isConstructorLike -> failWith $ VariableConflict var oldTerm term | otherwise -> - -- the term in the binding could be _equivalent_ - -- (not necessarily syntactically equal) to term' - case matchType of - Rewrite -> addIndeterminate oldTerm term - _ -> failWith $ VariableConflict var oldTerm term + -- A variable already bound to oldTerm is now matched against + -- term, and the two are not both constructor-like: they may + -- still be _equivalent_ (not syntactically equal), so the match + -- cannot be decided here and we defer in every mode. The + -- soundness concern is function evaluation: handleFunctionEquation + -- treats a MatchFailed as "skip this equation, try the next + -- priority" and an indeterminate match as "abort". A spurious + -- decisive failure here would let evaluation fall through to a + -- lower-priority equation (a higher priority number; priorities + -- count up from 1) that should not have been reached. See + -- hs-backend-booster issue #231. + addIndeterminate oldTerm term Nothing -> do let -- apply existing substitutions to term @@ -856,6 +848,20 @@ checkSubsort subsorts sub sup argsCheck <- zipWithM (checkSubsort subsorts) subArgs supArgs pure $ and argsCheck +{- | Whether two sorts can have a common inhabitant, i.e., share a + subsort. The subsort sets in the 'SortTable' are reflexive-transitive + closures (each sort is a member of its own set), so a non-empty + intersection is exactly sort overlap. Sort variables, parametric + sorts, and sorts missing from the table cannot be decided here and + are conservatively reported as overlapping. +-} +sortsOverlap :: SortTable -> Sort -> Sort -> Bool +sortsOverlap subsorts (SortApp name1 []) (SortApp name2 []) + | Just subs1 <- Map.lookup name1 subsorts + , Just subs2 <- Map.lookup name2 subsorts = + not $ subs1 `Set.disjoint` subs2 +sortsOverlap _ _ _ = True + data SortError = FoundSortVariable VarName | FoundUnknownSort Sort diff --git a/booster/unit-tests/Test/Booster/Pattern/ApplyEquations.hs b/booster/unit-tests/Test/Booster/Pattern/ApplyEquations.hs index d8cb3ed9b2..0839726ccf 100644 --- a/booster/unit-tests/Test/Booster/Pattern/ApplyEquations.hs +++ b/booster/unit-tests/Test/Booster/Pattern/ApplyEquations.hs @@ -14,6 +14,7 @@ module Test.Booster.Pattern.ApplyEquations ( test_simplifyConstraint, test_localFixpoint, test_errors, + test_soundnessGap, ) where import Control.Exception (finally) @@ -320,6 +321,43 @@ test_errors = isLoop _ (Left err) = assertFailure $ "Unexpected error " <> show err isLoop _ (Right r) = assertFailure $ "Unexpected result " <> show r +{- | Soundness regression test for 'Eval' mode of 'matchTerms': when a +pattern variable rebinds to two terms that are not both constructor-like +(e.g. a domain value and a function application), the matcher must +return @MatchIndeterminate@, which routes through +@IndeterminateMatch{} -> abort@ in 'handleFunctionEquation' and leaves +the term unchanged so the caller can decide what to do. + +Before this was fixed, the matcher returned a decisive +@MatchFailed VariableConflict@, which 'handleFunctionEquation' routes to +@continue@ — silently skipping a higher-priority equation and committing +to a lower-priority catch-all. Because function-equation priorities are +semantically binding, that violated the priority contract. + +The simplification companion is the dual: simplification priorities are +advisory, so both @FailedMatch@ and @IndeterminateMatch@ route to +@continue@ and the behaviour is unchanged. The companion is included to +pin that simplifications are unaffected by the fix. +-} +test_soundnessGap :: TestTree +test_soundnessGap = + testGroup + "Eval matcher soundness: mixed-determinacy rebind" + [ testCase + "Function equations: high-priority indeterminate match aborts, lower-priority rule NOT tried" + $ do + let subj = [trm| f1{}(con3{}(\dv{SomeSort{}}("a"), f2{}(\dv{SomeSort{}}("x")))) |] + ns <- noSolver + runNoLoggingT (fst <$> evaluateTerm TopDown soundnessGapFunDef Nothing ns mempty mempty subj) + @?>>= Right subj + , testCase "Simplifications: high-priority indeterminate match continues, lower-priority rule fires" $ do + let subj = [trm| f1{}(con3{}(\dv{SomeSort{}}("a"), f2{}(\dv{SomeSort{}}("x")))) |] + result = [trm| con2{}(con3{}(\dv{SomeSort{}}("a"), f2{}(\dv{SomeSort{}}("x")))) |] + ns <- noSolver + runNoLoggingT (fst <$> evaluateTerm TopDown soundnessGapSimplDef Nothing ns mempty mempty subj) + @?>>= Right result + ] + ---------------------------------------- index :: (ByteString -> CellIndex) -> SymbolName -> TermIndex @@ -399,6 +437,47 @@ loopDef = ] } +{- | Rules used by 'test_soundnessGap'. Both definitions hold the same +two equations on @f1@: + +* Priority 40: @f1(con3(X, X)) = con1(X)@ — narrow pattern that requires + the two arguments of @con3@ to be the same. +* Priority 50: @f1(X) = con2(X)@ — catch-all. + +The test subject is @f1(con3(\\dv "a", f2(\\dv "x")))@: when matching +the priority-40 rule's LHS, the variable @X@ is bound first to +@\\dv "a"@ (constructor-like) and then to @f2(\\dv "x")@ (a +'FunctionApplication', not constructor-like). 'Match.bindVariable' +returns @MatchIndeterminate@ for this mixed-determinacy rebind (it +returned a decisive @MatchFailed VariableConflict@ in 'Eval' mode +before this was fixed). +-} +soundnessGapRules :: [RewriteRule t] +soundnessGapRules = + [ equation + (Just "soundness-gap-pri40") + [trm| f1{}(con3{}(X:SomeSort{}, X:SomeSort{})) |] + [trm| con1{}(X:SomeSort{}) |] + 40 + , equation + (Just "soundness-gap-pri50") + [trm| f1{}(X:SomeSort{}) |] + [trm| con2{}(X:SomeSort{}) |] + 50 + ] + +soundnessGapFunDef, soundnessGapSimplDef :: KoreDefinition +soundnessGapFunDef = + testDefinition + { functionEquations = + mkTheory [(index IdxFun "f1", soundnessGapRules)] + } +soundnessGapSimplDef = + testDefinition + { simplifications = + mkTheory [(index IdxFun "f1", soundnessGapRules)] + } + f1Equations, f2Equations :: [RewriteRule t] f1Equations = [ equation -- f1(con1(X)) == con2(f1(X)) diff --git a/booster/unit-tests/Test/Booster/Pattern/MatchDispatch.hs b/booster/unit-tests/Test/Booster/Pattern/MatchDispatch.hs index 84d6617f02..ceeb042484 100644 --- a/booster/unit-tests/Test/Booster/Pattern/MatchDispatch.hs +++ b/booster/unit-tests/Test/Booster/Pattern/MatchDispatch.hs @@ -108,12 +108,12 @@ grid Eval = -- And DV Inj Map List Set Cons Fun Var [ [I, S, S, F, F, F, S, S, I] -- AndTerm , [I, S, F, F, F, F, F, I, I] -- DomainValue - , [I, F, S, F, F, F, F, I, I] -- Injection + , [I, F, S, I, I, I, F, I, I] -- Injection , [I, F, I, S, F, F, F, I, I] -- KMap , [I, F, I, F, S, F, F, I, I] -- KList , [I, F, I, F, F, S, F, I, I] -- KSet , [I, F, F, F, F, F, S, I, I] -- ConsApplication - , [I, F, F, F, F, F, I, S, I] -- FunctionApplication + , [I, I, I, I, I, I, I, S, I] -- FunctionApplication , [I, S, S, F, F, F, S, S, S] -- Var ] grid Implies = diff --git a/booster/unit-tests/Test/Booster/Pattern/MatchEval.hs b/booster/unit-tests/Test/Booster/Pattern/MatchEval.hs index 18f9c8533d..631946a315 100644 --- a/booster/unit-tests/Test/Booster/Pattern/MatchEval.hs +++ b/booster/unit-tests/Test/Booster/Pattern/MatchEval.hs @@ -30,6 +30,8 @@ test_match_eval = , composite , kmapTerms , internalSets + , variableRebindMixedDeterminacy + , injectionChildNarrowing ] symbols :: TestTree @@ -66,10 +68,6 @@ symbols = subj = app con1 [d] in test "same constructor, different argument sorts" pat subj $ failed (DifferentSorts x d) - , let pat = app f1 [var "X" someSort] - subj = dv someSort "something" - in test "function and something else" pat subj $ - failed (DifferentSymbols pat subj) ] composite :: TestTree @@ -97,8 +95,8 @@ composite = b = var "B" someSort pat = app con3 [var "X" someSort, var "X" someSort] -- same! subj = app con3 [a, b] - in test "Matching two constructor argument to be the same (failing)" pat subj $ - failed (VariableConflict (Variable someSort "X") a b) + in test "Matching two constructor argument to be the same (indeterminate)" pat subj $ + remainderWith [("X", someSort, a)] [(a, b)] ] varsAndValues :: TestTree @@ -115,8 +113,20 @@ varsAndValues = success [("X", someSort, inj aSubsort someSort v2)] , let v1 = var "X" aSubsort v2 = var "Y" someSort - in test "two variables (v1 subsort v2)" v1 v2 $ + in test "two variables (v1 subsort v2): indeterminate, Y may narrow" v1 v2 $ + remainder [(v1, v2)] + , let v1 = var "X" aSubsort + v2 = var "Y" differentSort + in test "two variables (disjoint sorts): fail" v1 v2 $ failed (DifferentSorts v1 v2) + , let v1 = var "X" aSubsort + f = app f1 [dv someSort "y"] + in test "var against function call of wider sort: indeterminate, result may narrow" v1 f $ + remainder [(v1, f)] + , let v1 = var "X" differentSort + f = app f1 [dv someSort "y"] + in test "var against function call of disjoint sort: fail" v1 f $ + failed (DifferentSorts v1 f) , let v1 = var "X" someSort v2 = var "X" differentSort in test "same variable name, different sort" v1 v2 $ @@ -306,6 +316,109 @@ internalSets = (success []) ] +{- | When a pattern variable is bound first to one term and then to +another where the two terms are not both constructor-like (e.g. a +domain value and a function application), the verdict must be +'MatchIndeterminate', because the function application could simplify +into the constructor-like term. + +A decisive 'MatchFailed VariableConflict' here would be a soundness gap +for function-equation priorities: 'handleFunctionEquation' +(Pattern.ApplyEquations) routes @FailedMatch _@ to @continue@ but +@IndeterminateMatch{}@ to @abort@, so a spurious failure silently skips +a higher-priority equation and commits to a lower-priority one. The +tests below pin both orderings of the rebind. + +The companion soundness regression test lives in +"Test.Booster.Pattern.ApplyEquations.test_soundnessGap". +-} +variableRebindMixedDeterminacy :: TestTree +variableRebindMixedDeterminacy = + testGroup + "Variable rebinding with mixed-determinacy subject" + [ let d = dv someSort "1" + fnApp = app f1 [dv someSort "x"] + t1 = app con3 [var "X" someSort, var "X" someSort] + t2 = app con3 [d, fnApp] + in test + "Rebind X to a domain value then to a function application is indeterminate" + t1 + t2 + (remainderWith [("X", someSort, d)] [(d, fnApp)]) + , let d = dv someSort "1" + fnApp = app f1 [dv someSort "x"] + t1 = app con3 [var "X" someSort, var "X" someSort] + t2 = app con3 [fnApp, d] + in test + "Rebind X to a function application then to a domain value is indeterminate" + t1 + t2 + (remainderWith [("X", someSort, fnApp)] [(fnApp, d)]) + ] + +{- | Two injections with the same target but different source sorts can +only be decisively distinguished when neither child can change sort: a +function-application child may evaluate to a term of a narrower sort, +and a variable child may be instantiated with one. Whenever the +narrowable child sits on the wider-sorted side, the verdict is +'MatchIndeterminate'; only rigid children at incompatible sorts fail +decisively. +-} +injectionChildNarrowing :: TestTree +injectionChildNarrowing = + let dSub = dv aSubsort "x" + dSome = dv someSort "y" + varSome = var "Y" someSort + varSub = var "Z" aSubsort + fnSome = app f1 [dSome] + in testGroup + "Injection children that may narrow" + [ test + "subject variable child of wider sort is indeterminate" + (Injection aSubsort kItemSort dSub) + (Injection someSort kItemSort varSome) + (remainder [(dSub, varSome)]) + , test + "subject function child of wider sort is indeterminate" + (Injection aSubsort kItemSort dSub) + (Injection someSort kItemSort fnSome) + (remainder [(dSub, fnSome)]) + , test + "pattern function child of wider sort is indeterminate" + (Injection someSort kItemSort fnSome) + (Injection aSubsort kItemSort dSub) + (remainder [(fnSome, dSub)]) + , test + "rigid children at incompatible sorts fail" + (Injection aSubsort kItemSort dSub) + (Injection someSort kItemSort dSome) + ( failed $ + DifferentSorts + (Injection aSubsort kItemSort dSub) + (Injection someSort kItemSort dSome) + ) + , -- Mirror of the wider-sort cases above, but with the non-rigid + -- child on the *narrower-sorted* side. Here no evaluation or + -- instantiation can bridge the sorts: normalising the narrower + -- injection wraps the child in an inj{aSubsort -> someSort}(...), + -- which the rigid wider-sorted pattern child (a domain value) can + -- never equal, whatever the variable resolves to. So the decisive + -- failure is kept rather than deferred. This pins the regression + -- behind keeping matchInj's catch-all decisive: broadening it to + -- addIndeterminate on any non-rigid child made a KEVM execution + -- abort instead of branch (rpc-integration test-3934-smt, where a + -- subject function child of a narrower sort took this same path). + test + "subject variable child of narrower sort fails" + (Injection someSort kItemSort dSome) + (Injection aSubsort kItemSort varSub) + ( failed $ + DifferentSorts + (Injection someSort kItemSort dSome) + (Injection aSubsort kItemSort varSub) + ) + ] + ---------------------------------------- test :: String -> Term -> Term -> MatchResult -> TestTree @@ -323,6 +436,23 @@ success assocs = failed :: FailReason -> MatchResult failed = MatchFailed +remainder :: [(Term, Term)] -> MatchResult +remainder = MatchIndeterminate mempty . NE.fromList + +{- | Like 'remainder' but also asserts a non-empty partial substitution +from pairs that the matcher resolved before reaching the indeterminate +pairs. +-} +remainderWith :: [(VarName, Sort, Term)] -> [(Term, Term)] -> MatchResult +remainderWith assocs pairs = + MatchIndeterminate + ( Map.fromList + [ (Variable{variableSort, variableName}, term) + | (variableName, variableSort, term) <- assocs + ] + ) + (NE.fromList pairs) + errors :: String -> Term -> Term -> TestTree errors name pat subj = testCase name $ diff --git a/booster/unit-tests/Test/Booster/Pattern/MatchImplies.hs b/booster/unit-tests/Test/Booster/Pattern/MatchImplies.hs index 7d50efb673..c46e77a458 100644 --- a/booster/unit-tests/Test/Booster/Pattern/MatchImplies.hs +++ b/booster/unit-tests/Test/Booster/Pattern/MatchImplies.hs @@ -28,6 +28,7 @@ test_match_implies = [ constructors , functions , varsAndValues + , variableRebindMixedDeterminacy , andTerms , sorts , injections @@ -126,9 +127,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 (fail)" t1 t2 $ - failed $ - VariableConflict (Variable someSort "X") y z + in test "Matching the same variable in a constructor (indeterminate)" t1 t2 $ + remainderWith [("X", someSort, y)] [(y, z)] ] functions :: TestTree @@ -181,7 +181,11 @@ varsAndValues = success [("X", someSort, inj aSubsort someSort v2)] , let v1 = var "X" aSubsort v2 = var "Y" someSort - in test "two variables (v1 subsort v2)" v1 v2 $ + in test "two variables (v1 subsort v2): indeterminate, Y may narrow" v1 v2 $ + remainder [(v1, v2)] + , let v1 = var "X" aSubsort + v2 = var "Y" differentSort + in test "two variables (disjoint sorts): fail" v1 v2 $ failed (DifferentSorts v1 v2) , let v1 = var "X" someSort v2 = var "X" differentSort @@ -213,6 +217,44 @@ varsAndValues = failed (DifferentSorts v d) ] +{- | A pattern variable that gets matched against two different subject +positions — one a domain value (constructor-like), one a function +application (not constructor-like) — must be reported as +'MatchIndeterminate', because the second term might simplify into +something equivalent to the first (the comment on 'bindVariable' says +exactly this). + +A decisive 'MatchFailed VariableConflict' here (as 'Implies' mode +returned before this was fixed) would be a soundness gap: the implies +handler trusts the matcher's decisive verdict and returns a +non-'indeterminate' @valid:false@, even though simplifying the function +application could reveal the subsumption. The tests below pin both +orderings of the rebind. +-} +variableRebindMixedDeterminacy :: TestTree +variableRebindMixedDeterminacy = + testGroup + "Variable rebinding with mixed-determinacy subject" + [ let d = dv someSort "1" + fnApp = app f1 [dv someSort "x"] + t1 = app con3 [var "X" someSort, var "X" someSort] + t2 = app con3 [d, fnApp] + in test + "Rebind X to a domain value then to a function application is indeterminate" + t1 + t2 + (remainderWith [("X", someSort, d)] [(d, fnApp)]) + , let d = dv someSort "1" + fnApp = app f1 [dv someSort "x"] + t1 = app con3 [var "X" someSort, var "X" someSort] + t2 = app con3 [fnApp, d] + in test + "Rebind X to a function application then to a domain value is indeterminate" + t1 + t2 + (remainderWith [("X", someSort, fnApp)] [(fnApp, d)]) + ] + andTerms :: TestTree andTerms = testGroup @@ -517,6 +559,19 @@ failed = MatchFailed remainder :: [(Term, Term)] -> MatchResult remainder = MatchIndeterminate mempty . NE.fromList +{- | Like 'remainder' but also asserts a non-empty partial substitution from +pairs that the matcher resolved before reaching the indeterminate pairs. +-} +remainderWith :: [(VarName, Sort, Term)] -> [(Term, Term)] -> MatchResult +remainderWith assocs pairs = + MatchIndeterminate + ( Map.fromList + [ (Variable{variableSort, variableName}, term) + | (variableName, variableSort, term) <- assocs + ] + ) + (NE.fromList pairs) + sortErr :: SortError -> MatchResult sortErr = MatchFailed . SubsortingError diff --git a/booster/unit-tests/Test/Booster/Pattern/MatchRewrite.hs b/booster/unit-tests/Test/Booster/Pattern/MatchRewrite.hs index d478861741..ce93b6b78d 100644 --- a/booster/unit-tests/Test/Booster/Pattern/MatchRewrite.hs +++ b/booster/unit-tests/Test/Booster/Pattern/MatchRewrite.hs @@ -205,7 +205,11 @@ varsAndValues = success [("X", someSort, inj aSubsort someSort v2)] , let v1 = var "X" aSubsort v2 = var "Y" someSort - in test "two variables (v1 subsort v2)" v1 v2 $ + in test "two variables (v1 subsort v2): indeterminate, Y may narrow" v1 v2 $ + remainder [(v1, v2)] + , let v1 = var "X" aSubsort + v2 = var "Y" differentSort + in test "two variables (disjoint sorts): fail" v1 v2 $ failed (DifferentSorts v1 v2) , let v1 = var "X" someSort v2 = var "X" differentSort