4059 ensures substitution #4060

geo2a · 2024-10-15T16:27:34Z

This PR improves Booster's handling of substitutions.

Summary

Substitutions are special predicates: equations where the LHS is a variable, for example VAR ==Int TERM. See Booster.Syntax.Json.Internalise.mbSubstitution for the exact specification of what is considered to be a substitution.

This PR changes the Pattern type to explicitly carry these special substitution predicates:

+type Substitution = Map Variable Term
+
 -- | A term (configuration) constrained by a number of predicates.
 data Pattern = Pattern
     { term :: Term
     , constraints :: !(Set Predicate)
+    , substitution :: Substitution
     , ceilConditions :: ![Ceil]
     }
     deriving stock (Eq, Ord, Show, Generic, Data)

Substitution may appear out of three places:

sent in the request body
ensured as a post condition of a rewrite rule
NOT IMPLEMENTED learned from the branching condition --- this is something that will be added as part of 3956 branching on complete conditions in Booster #4058

The first source is handled by the pattern internalisation code. The second and third sources are different, as the pattern has already been internalised. All this sources can also produce generic (i.e. non-substitution) constrains that should be added into the constrains set of a Pattern. Substitutions, when produces, should be applied to the term of the Pattern and added to the substitution field. This PR makes sure we use the same code path for separating substitutions from generic predicates everywhere. We use Booster.Syntax.Json.Internalise.mbSubstitution.mkSubstitution to take care of cyclic, which are broken up, and duplicate bindings, which are treated as constraints.

With these changes, we can harmonize many (but not all) specialisations of the integrations test responses, i.e. we do not need many of the *.booster-dev and *.kore-rpc-dev response files.

Changes to pattern simplification code

As the Pattern type has changed, we must adapt the ApplyEquations.evaluatePattern and ApplyEquations.evaluatePattern' functions to:

consider substitutions as known truth together with all other constraints (that's what we did before)
simplify the substitution

We achieve that by doing the following:

convert the substitution into equalities and assume it as know truth
when constructing the new, simplified pattern, use the same code as when internalising a pattern to partition predicates into the substitution and non-substitution ones

Changes to rewrite rule application code

The Pattern.Rewrite.applyRule function has been changed to:

consider substiontion as known truth together with all other constraints (that's what we did before) when checking requires/ensures
extract the substitution from the ensured conditions and add it to the rewritten pattern

booster/library/Booster/Pattern/Bool.hs

booster/library/Booster/Syntax/ParsedKore/Internalise.hs

booster/library/Booster/Pattern/Bool.hs

booster/library/Booster/Pattern/Rewrite.hs

geo2a · 2024-10-17T14:25:46Z

Failed KEVM tests as of 52d3ad4

FAILED src/tests/integration/test_prove.py::test_prove_rules[mcd/flopper-dent-guy-diff-tic-not-0-pass-rough-spec.k]
FAILED src/tests/integration/test_prove.py::test_prove_rules[mcd/flopper-dent-guy-same-pass-rough-spec.k]
FAILED src/tests/integration/test_prove.py::test_prove_rules[mcd/flopper-kick-pass-rough-spec.k]
FAILED src/tests/integration/test_prove.py::test_prove_rules[mcd/cat-file-addr-pass-rough-spec.k]
FAILED src/tests/integration/test_prove.py::test_prove_rules[mcd/pot-join-pass-rough-spec.k]
FAILED src/tests/integration/test_prove.py::test_prove_rules[mcd/end-pack-pass-rough-spec.k]
FAILED src/tests/integration/test_prove.py::test_prove_rules[mcd/flapper-yank-pass-rough-spec.k]
FAILED src/tests/integration/test_prove.py::test_prove_rules[mcd/flopper-cage-pass-spec.k]

geo2a · 2024-10-22T11:35:54Z

No failed KEVM tests at commit fdf62fc and not much difference in performance:

| Test                                          | 4059-ensures-substitution time | master-434710529 time | (4059-ensures-substitution/master-434710529) time
|-----------------------------------------------|--------------------------------|-----------------------|---------------------------------------------------
| mcd/vow-fess-fail-rough-spec.k                | 108.68                         | 115.11                | 0.9441403874554775
| mcd-structured/flopper-file-pass-rough-spec.k | 18.23                          | 19.14                 | 0.9524555903866249
| erc20/ds/allowance-spec.k                     | 52.94                          | 55.03                 | 0.9620207159731056
| benchmarks/storagevar01-spec.k                | 49.16                          | 47.2                  | 1.0415254237288134
| mcd/flopper-file-pass-rough-spec.k            | 19.46                          | 18.58                 | 1.047362755651238
| mcd-structured/cat-exhaustiveness-spec.k      | 118.05                         | 111.06                | 1.0629389519178822
| TOTAL                                         | 366.52000000000004             | 366.12                | 1.0010925379656943

Include substitution in known truth when simplifying

Fix unit tests add test

Format with fourmolu

Handle with care

jberthold

Big job, well done! I like that we can ditch many of the response*.booster-dev files.

One open question is the removal of purging the simplifier cache when we have new constraints, I think that should still be done. Please put this back or explain why we don't.

The other things are minor and stylistic. Maybe we should think about the pattern constructor, as mentioned.

jberthold · 2024-10-22T23:19:08Z

booster/library/Booster/JsonRpc.hs

                        let substPat =
                                Pattern
-                                    { term = substituteInTerm substitution pat.term
-                                    , constraints = Set.map (substituteInPredicate substitution) pat.constraints
+                                    { term = Substitution.substituteInTerm pat.substitution pat.term
+                                    , constraints = Set.map (Substitution.substituteInPredicate pat.substitution) pat.constraints
                                    , ceilConditions = pat.ceilConditions
+                                    , substitution = pat.substitution
                                    }


While reading through here, I thought that internaliseTermOrPredicates, and any internalisation that may return a Pattern as a whole, should maybe already apply the substitution before returning the result (somewhat "normalising" the pattern before it is returned).
The internalisePattern, in contrast, returns the parts separately and leaves it to the caller to piece them back together. This is because we use it a lot in the definition internalisation where we need the parts separately.
This is more of a stylistic preference, and IDK how much fall-out it will have, so it is not necessary.

This is a very good point. I'll try putting this change in.

jberthold · 2024-10-22T23:31:43Z

booster/library/Booster/Log.hs

-withPatternContext Pattern{term, constraints} m =
-    let t' = foldl' AndTerm term $ Set.toList $ Set.map coerce constraints -- FIXME
+withPatternContext Pattern{term, constraints, substitution} m =
+    let t' = foldl' AndTerm term . map coerce $ Set.toList constraints <> asEquations substitution


That FIXME was referring to the fact that the t' :: Term is not well-sorted. Probably good enough for logging, though... just that nobody should use the json version of it as input directly.

How do we make it well-sorted? Replace AndTerm with _andBool_?

Ah no, there's a term there...

jberthold · 2024-10-22T23:41:45Z

booster/library/Booster/Pattern/Implies.hs

                                    Pattern
-                                        { term = substituteInTerm substitutionL patL.term
-                                        , constraints = Set.map (substituteInPredicate substitutionL) patL.constraints
+                                        { term = Substitution.substituteInTerm substitutionL patL.term
+                                        , constraints = Set.map (Substitution.substituteInPredicate substitutionL) patL.constraints
                                        , ceilConditions = patL.ceilConditions
+                                        , substitution = substitutionL
                                        }
                                substPatR =
                                    Pattern
-                                        { term = substituteInTerm substitutionR patR.term
-                                        , constraints = Set.map (substituteInPredicate substitutionR) patR.constraints
+                                        { term = Substitution.substituteInTerm substitutionR patR.term
+                                        , constraints = Set.map (Substitution.substituteInPredicate substitutionR) patR.constraints
                                        , ceilConditions = patR.ceilConditions
+                                        , substitution = substitutionR
                                        }


Same comment as above, maybe the Pattern returned from internalisePatternOrTopOrBottom should already have the substitution applied...
I wonder whether we could just enforce that by a smart constructor for Pattern.

We very often construct a pattern directly, bypassing the Pattern_ smart-constructor. I'd love to have a smart constructor that is used consistently, but I think it may be out-of-scope for this PR. I do agree that it's best to apply the substitution in the internalisation function that return a Pattern.

jberthold · 2024-10-22T23:57:39Z

booster/library/Booster/Pattern/Rewrite.hs

+        toCheck <-
+            lift $
+                filterOutKnownConstraints
+                    (pat.constraints <> (Set.fromList . asEquations $ pat.substitution))
+                    ruleRequires


(nit) maybe worth giving this expression a name:

Suggested change

toCheck <-

lift $

filterOutKnownConstraints

(pat.constraints <> (Set.fromList . asEquations $ pat.substitution))

ruleRequires

let knownConstraints = pat.constraints <> Set.fromList (asEquations pat.substitution)

toCheck <- lift $ filterOutKnownConstraints knownConstraints ruleRequires

and onwards below just inserting knownConstraints for pat.constraints in the old code?

jberthold · 2024-10-23T00:00:22Z

booster/library/Booster/Pattern/Rewrite.hs

-        -- if a new constraint is going to be added, the equation cache is invalid
-        unless (null newConstraints) $ do
-            withContextFor Equations . logMessage $
-                ("New path condition ensured, invalidating cache" :: Text)
-
-            lift . RewriteT . lift . modify $ \s -> s{equations = mempty}


(Why) Is this not true any more?

We have a similar piece of code in applyRule, just after the call to checkEnsures. On master we are invalidating the cache twice: at the end of checkEnsures (removed here) and right after the call to checkEnsures in applyRule.

jberthold · 2024-10-23T00:03:18Z

booster/library/Booster/Pattern/Util.hs

 modifyVariables :: (Variable -> Variable) -> Pattern -> Pattern
 modifyVariables f p =
    Pattern
        { term = modifyVariablesInT f p.term
        , constraints = Set.map (modifyVariablesInP f) p.constraints
+        , substitution = Map.map (coerce $ modifyVariablesInT f) p.substitution


This function is currently unused but we should either delete it or also modify the Map keys (variables).

Removed, thanks!

jberthold · 2024-10-23T00:14:44Z

booster/library/Booster/Syntax/Json/Internalise.hs

+    -- substitution mining
+    extractSubsitution,


Suggested change

-- substitution mining

extractSubsitution,

-- substitution mining

extractSubstitution,

😁

jberthold · 2024-10-23T00:23:54Z

booster/library/Booster/Syntax/Json/Internalise.hs

+extractSubsitution ::
+    [Internal.Predicate] -> (Map Internal.Variable Internal.Term, Set Internal.Predicate)
+extractSubsitution ps =
+    let (potentialSubstituion, otherPreds) = partitionSubstitutionPreds . map mbSubstitution . coerce $ ps
+        (newSubstitution, leftoverPreds) = mkSubstitution potentialSubstituion
+     in (newSubstitution, Set.fromList $ leftoverPreds <> map unsafeFromBoolPred otherPreds)
+  where
+    partitionSubstitutionPreds = foldl' accumulate ([], [])
+      where
+        accumulate (accSubst, accOther) = \case
+            pSubst@SubstitutionPred{} -> (pSubst : accSubst, accOther)
+            pOther -> (accSubst, pOther : accOther)


Maybe simpler to just use partition and a helper that extracts the Terms from BoolPred immediately (avoids unsafeFromBoolPred below)

Suggested change

extractSubsitution ::

[Internal.Predicate] -> (Map Internal.Variable Internal.Term, Set Internal.Predicate)

extractSubsitution ps =

let (potentialSubstituion, otherPreds) = partitionSubstitutionPreds . map mbSubstitution . coerce $ ps

(newSubstitution, leftoverPreds) = mkSubstitution potentialSubstituion

in (newSubstitution, Set.fromList $ leftoverPreds <> map unsafeFromBoolPred otherPreds)

where

partitionSubstitutionPreds = foldl' accumulate ([], [])

where

accumulate (accSubst, accOther) = \case

pSubst@SubstitutionPred{} -> (pSubst : accSubst, accOther)

pOther -> (accSubst, pOther : accOther)

extractSubstitution ::

[Internal.Predicate] -> (Map Internal.Variable Internal.Term, Set Internal.Predicate)

extractSubstitution ps =

let (potentialSubstitution, otherPreds) = partitionSubstitutionPreds . map mbSubstitution . coerce $ ps

(newSubstitution, leftoverPreds) = mkSubstitution potentialSubstitution

in (newSubstitution, Set.fromList $ leftoverPreds <> otherPreds)

where

partitionSubstitutionPreds = partitionEithers . unpackBoolPred

where

unpackBoolPred = \case

pSubst@SubstitutionPred{} -> Left pSubst

BoolPred p -> Right p

other -> error $ "extractSubstitution: unsupported predicate " <> show other

Great idea, done!

geo2a · 2024-10-23T06:40:39Z

booster/library/Booster/Pattern/Rewrite.hs


                    -- if a new constraint is going to be added, the equation cache is invalid
-                    unless (null newConstraints) $ do
+                    unless (null ensuredConditions) $ do


We invalidate the cache here if a new constraint has been ensured.

Fixes #4059 This PR improves Booster's handling of substitutions. ## Summary Substitutions are special predicates: equations where the LHS is a variable, for example `VAR ==Int TERM`. See `Booster.Syntax.Json.Internalise.mbSubstitution` for the exact specification of what is considered to be a substitution. This PR changes the `Pattern` type to explicitly carry these special substitution predicates: ```diff +type Substitution = Map Variable Term + -- | A term (configuration) constrained by a number of predicates. data Pattern = Pattern { term :: Term , constraints :: !(Set Predicate) + , substitution :: Substitution , ceilConditions :: ![Ceil] } deriving stock (Eq, Ord, Show, Generic, Data) ``` Substitution may appear out of three places: - sent in the request body - ensured as a post condition of a rewrite rule - **NOT IMPLEMENTED** learned from the branching condition --- this is something that will be added as part of #4058 The first source is handled by the pattern internalisation code. The second and third sources are different, as the pattern has already been internalised. All this sources can also produce generic (i.e. non-substitution) constrains that should be added into the `constrains` set of a `Pattern`. Substitutions, when produces, should be applied to the `term` of the `Pattern` and added to the `substitution` field. This PR makes sure we use the same code path for separating substitutions from generic predicates everywhere. We use `Booster.Syntax.Json.Internalise.mbSubstitution.mkSubstitution` to take care of cyclic, which are broken up, and duplicate bindings, which are treated as constraints. With these changes, we can harmonize many (but not all) specialisations of the integrations test responses, i.e. we do not need many of the `*.booster-dev` and `*.kore-rpc-dev` response files. ## Changes to pattern simplification code As the `Pattern` type has changed, we must adapt the `ApplyEquations.evaluatePattern` and `ApplyEquations.evaluatePattern'` functions to: - consider `substitutions` as known truth together with all other constraints (that's what we did before) - simplify the substitution We achieve that by doing the following: - convert the substitution into equalities and assume it as know truth - when constructing the new, simplified pattern, use the same code as when internalising a pattern to partition predicates into the substitution and non-substitution ones ## Changes to rewrite rule application code The `Pattern.Rewrite.applyRule` function has been changed to: - consider `substiontion` as known truth together with all other constraints (that's what we did before) when checking requires/ensures - extract the substitution from the ensured conditions and add it to the rewritten pattern --------- Co-authored-by: github-actions <[email protected]>

geo2a force-pushed the 4059-ensures-substitution branch 3 times, most recently from 9b4f310 to bc44927 Compare October 17, 2024 09:46

jberthold reviewed Oct 17, 2024

View reviewed changes

geo2a force-pushed the 4059-ensures-substitution branch 2 times, most recently from 2e7f126 to 52d3ad4 Compare October 17, 2024 13:55

geo2a force-pushed the 4059-ensures-substitution branch 5 times, most recently from 4e34924 to fdf62fc Compare October 22, 2024 09:05

geo2a added 17 commits October 22, 2024 14:28

Make substitution part of Pattern

5481f26

Do not invalidate cache twice when ensuring conditions

1e7ce61

Extract substitution items from ensured conditions

b491b85

Include ensured substitution when externalising pattern

f98f4b5

Update integration test output

b4502f9

Add substitution conversion helpers

aee79b7

Build existential substitution together with the matching one

0f6ccf5

Fix imports

7c7a4ba

Move partitionPredicates to Booster.Pattern.Bool

82f0955

Consider substitution as constraints in evaluatePattern

20c10ef

Include substitution in known truth when simplifying

Delete obsolete booster-dev responses

8b6fbfd

Include input substitution into the pattern

ac825e6

Extend Unknown type, abort on unsafe unknown ensures

a6c7808

Include substitution when pretty-printing Pattern

ffc4035

Fix substitution externalisation

32a8418

Do not simplify substitution when normalising it

7da0911

Kill redundant patterns

9f11343

geo2a and others added 10 commits October 22, 2024 14:29

Move substitution-related stuff into a separate module

9e47e06

Fix unit tests add test

Tweak substitution naming in applyRule

ef7ea92

Rename rule pattern internalisation function

2f3017f

Format with fourmolu

b72baf9

Float mbSubstitution out, make pure

a6f2dd9

Format with fourmolu

Reuse substitution internalisation code

a08f937

Handle with care

Do not override with old substitution when externalising

900e13d

Update test-substitution

b4a3599

Update test-questionmark-vars

3b2b7d5

Update test-a-to-f

598c8a4

geo2a force-pushed the 4059-ensures-substitution branch from 8e622f9 to 598c8a4 Compare October 22, 2024 12:29

geo2a added 2 commits October 22, 2024 14:59

Remove dead code

bc72188

Use substitution in Implies

b2ea0f8

geo2a force-pushed the 4059-ensures-substitution branch from 0c612f3 to b2ea0f8 Compare October 22, 2024 13:46

geo2a added 2 commits October 22, 2024 17:21

Handle input substitution as part of Pattern

f8f956f

Handle substitution better when simplifying standalone predicates

c73a2c9

geo2a requested a review from jberthold October 22, 2024 15:48

geo2a marked this pull request as ready for review October 22, 2024 15:48

jberthold approved these changes Oct 23, 2024

View reviewed changes

geo2a commented Oct 23, 2024

View reviewed changes

geo2a added 5 commits October 23, 2024 08:45

Remove unused function modifyVariables

cc808a2

Fix typo

f9f0d51

Refactor extractSubstitution

c974346

Bind the known constraints expressin

9bcdc52

Substitute in the internalisation functions directly

58f6402

geo2a merged commit aaf0ef5 into master Oct 23, 2024
6 checks passed

geo2a deleted the 4059-ensures-substitution branch October 23, 2024 10:25

jberthold mentioned this pull request Oct 23, 2024

Use smart Pattern constructor throughout the code #4065

Open

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

4059 ensures substitution #4060

4059 ensures substitution #4060

geo2a commented Oct 15, 2024 •

edited

Loading

geo2a commented Oct 17, 2024

geo2a commented Oct 22, 2024

jberthold left a comment

jberthold Oct 22, 2024

geo2a Oct 23, 2024

jberthold Oct 22, 2024

geo2a Oct 23, 2024

geo2a Oct 23, 2024

jberthold Oct 22, 2024

geo2a Oct 23, 2024

jberthold Oct 22, 2024

geo2a Oct 23, 2024

jberthold Oct 23, 2024

geo2a Oct 23, 2024

jberthold Oct 23, 2024

geo2a Oct 23, 2024

jberthold Oct 23, 2024

geo2a Oct 23, 2024

jberthold Oct 23, 2024

geo2a Oct 23, 2024

geo2a Oct 23, 2024

4059 ensures substitution #4060

4059 ensures substitution #4060

Conversation

geo2a commented Oct 15, 2024 • edited Loading

Summary

Changes to pattern simplification code

Changes to rewrite rule application code

geo2a commented Oct 17, 2024

geo2a commented Oct 22, 2024

jberthold left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

geo2a commented Oct 15, 2024 •

edited

Loading