PLE produces incorrect equalities

[facundominguez]

Verification of the following example succeeds when constraints 1 and 3 are actually unsafe.

// test.fq
define f(lq1:a) : a = { lq1 }

expand [1 : True; 2 : True; 3 : True; 4 : True]

bind 0 f : {v : func(1,[@(0);@(0)]) | []}
bind 1 x : {v : int | []}
bind 2 y : {v : int | x = 0}
bind 3 z : {v : int | x = 1}
bind 4 w : {v : int | f(x) = 0}
      
constraint:
  env [0;1;2;4]
  lhs {v : int | true}
  rhs {v : int | false }
  id 1 tag []

constraint:
  env [0;1;3;4]
  lhs {v : int | true}
  rhs {v : int | false}
  id 2 tag []

constraint:
  env [0;1;2;4]
  lhs {v : int | true}
  rhs {v : int | false }
  id 3 tag []

constraint:
  env [0;1;3;4]
  lhs {v : int | true}
  rhs {v : int | false }
  id 4 tag []

Verify with

$ fixpoint --eliminate=some --rewriteaxioms test.fq

Liquid-Fixpoint Copyright 2013-21 Regents of the University of California.
All Rights Reserved.

Working  80% [====================================================.............]
Working 180% [=====================================================================================================================]

fromList
  [ (1,PAnd [])
  , (4,PAtom Eq (EApp (EVar "f") (EVar "x")) (ECon (I 1)))
  , (5,PAtom Eq (EApp (EVar "f") (EVar "x")) (ECon (I 0)))
  , (6,PAtom Eq (EApp (EVar "f") (EVar "x")) (ECon (I 1)))
  , (7,PAtom Eq (EApp (EVar "f") (EVar "x")) (ECon (I 0)))
  , (8,PAtom Eq (EApp (EVar "f") (EVar "x")) (ECon (I 1)))
  ]

Safe ( 4  constraints checked)

I modified liquid-fixpoint to print the assignments of discovered equations to bindings as shown above.

I think the problem is that different constraints produce different equations for binding 4, and they all compete to assign their equations to the same binding in the output of PLE.

Fixing this will probably require to add new bindings to each constraint, rather than attempting to modify the existing bindings.

[ranjitjhala]

I was first alarmed but then recalled this violates the “tree-like” precondition on the binders. I *think* I wrote the property down somewhere let me look for it. In essence the binder numbers are important: If two constraints both have binders i and j they have the same set of binders between i and j. This invariant let’s us build a “trie” from the constraints where the binders are in increasing order. Otherwise, as here, you have a DAG where 1 splits to 2 and 3 which join at 4 — which I suspect is causing the problem…

…

On Wed, Oct 6, 2021 at 6:34 PM Facundo Domínguez ***@***.***> wrote: Verification of the following example succeeds when constraints 1 and 3 are actually unsafe. // test.fq define f(lq1:a) : a = { lq1 } expand [1 : True; 2 : True; 3 : True; 4 : True] bind 0 f : {v : func(1,[@(0);@(0)]) | []} bind 1 x : {v : int | []} bind 2 y : {v : int | x = 0} bind 3 z : {v : int | x = 1} bind 4 w : {v : int | f(x) = 0} constraint: env [0;1;2;4] lhs {v : int | true} rhs {v : int | false } id 1 tag [] constraint: env [0;1;3;4] lhs {v : int | true} rhs {v : int | false} id 2 tag [] constraint: env [0;1;2;4] lhs {v : int | true} rhs {v : int | false } id 3 tag [] constraint: env [0;1;3;4] lhs {v : int | true} rhs {v : int | false } id 4 tag [] Verify with $ fixpoint --eliminate=some --rewriteaxioms test.fq Liquid-Fixpoint Copyright 2013-21 Regents of the University of California. All Rights Reserved. Working 80% [====================================================.............] Working 180% [=====================================================================================================================] fromList [ (1,PAnd []) , (4,PAtom Eq (EApp (EVar "f") (EVar "x")) (ECon (I 1))) , (5,PAtom Eq (EApp (EVar "f") (EVar "x")) (ECon (I 0))) , (6,PAtom Eq (EApp (EVar "f") (EVar "x")) (ECon (I 1))) , (7,PAtom Eq (EApp (EVar "f") (EVar "x")) (ECon (I 0))) , (8,PAtom Eq (EApp (EVar "f") (EVar "x")) (ECon (I 1))) ] Safe ( 4 constraints checked) I modified liquid-fixpoint to print the assignments of discovered equations to bindings as shown above. I think the problem is that different constraints produce different equations for binding 4, and they all compete to assign their equations to the same binding in the output of PLE. Fixing this will probably require to add new bindings to each constraint, rather than attempting to modify the existing bindings. — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_ucsd-2Dprogsys_liquid-2Dfixpoint_issues_496&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=9VjL3buQccQEkuvbwNxm9sPPhIb0X_mP_MA6nuMOB3w&s=kz3613SfeIMHZ5rcaw-KaX2-PkEGoGik-et8ePs6Et4&e=>, or unsubscribe <https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_notifications_unsubscribe-2Dauth_AAMS4OB4DGDSR7I7NKFR2ITUFT2JJANCNFSM5FQEMCWA&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=9VjL3buQccQEkuvbwNxm9sPPhIb0X_mP_MA6nuMOB3w&s=Afy7bNUVw0TSbgrltFQQufvvbVKdbHgvrlt-9rDqc-0&e=> . Triage notifications on the go with GitHub Mobile for iOS <https://urldefense.proofpoint.com/v2/url?u=https-3A__apps.apple.com_app_apple-2Dstore_id1477376905-3Fct-3Dnotification-2Demail-26mt-3D8-26pt-3D524675&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=9VjL3buQccQEkuvbwNxm9sPPhIb0X_mP_MA6nuMOB3w&s=SMkF35OmG3PdWm0LVYFRIPp8rJ3tBf7QXL3hAOu1Usk&e=> or Android <https://urldefense.proofpoint.com/v2/url?u=https-3A__play.google.com_store_apps_details-3Fid-3Dcom.github.android-26referrer-3Dutm-5Fcampaign-253Dnotification-2Demail-2526utm-5Fmedium-253Demail-2526utm-5Fsource-253Dgithub&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=9VjL3buQccQEkuvbwNxm9sPPhIb0X_mP_MA6nuMOB3w&s=Beg4GHQiFdHwcArfRiPHfm6Bu4cu3pxJVB9SbErm6kw&e=>.

[facundominguez]

If two constraints both have binders i and j they have the same set of binders between i and j.

Ah, in that case, the current situation is still problematic.

1. The software or human interacting with liquid-fixpoint gets no feedback that the invariant is broken
2. I don't think liquid-fixpoint is maintaining this invariant internally. At least environment reduction would eliminate redundant bindings without considering it.
3. It doesn't look like an algorithm to establish the invariant exists without duplicating bindings. Say we have constraints with bindings [1;2;3;4], [1;2;4], [1;3;4]. These can't be organized tree-like without duplicating and reordering constraints. Maybe: [1;4;old_2;old_3], [1;4;old_2], [1;4;copy_of_3]. Perhaps we can reduce the damage by choosing wisely what bindings to duplicate, and maybe the Trie deserves this complexity, but it looks a bit too much to push to the users.

[facundominguez]

If two constraints both have binders i and j they have the same set of binders between i and j.

Also, it is worth noting that this invariant doesn't affect correctness of the core of PLE itself. If the invariant doesn't hold, PLE will just duplicate some effort analyzing some bindings more than once.

The thing that breaks is the way in which equalities are collected. Whether a Trie or some other data structure is used, is of little consequence if the algorithm is forced to deliver new equalities per binding instead of per constraint.

[ranjitjhala]

Hi @facundominguez -- sorry I was putting out some other fires :-)

First, in this case, here's the duplicated variant which respects the "trie invariant" by cloning 4 as 40:

// test.fq
define f(lq1:a) : a = { lq1 }

expand [1 : True; 2 : True; 3 : True; 4 : True]

bind 0 f : {v : func(1,[@(0);@(0)]) | []}
bind 1 x : {v : int | []}
bind 2 y : {v : int | x = 0}
bind 3 z : {v : int | x = 1}
bind 4 w : {v : int | f(x) = 0}
bind 40 w : {v : int | f(x) = 0}

constraint:
  env [0;1;2;4]
  lhs {v : int | true}
  rhs {v : int | false }
  id 1 tag []

constraint:
  env [0;1;3;40]
  lhs {v : int | true}
  rhs {v : int | false}
  id 2 tag []

constraint:
  env [0;1;2;4]
  lhs {v : int | true}
  rhs {v : int | false }
  id 3 tag []

constraint:
  env [0;1;3;40]
  lhs {v : int | true}
  rhs {v : int | false }
  id 4 tag []

Now I get:

$ fixpoint --eliminate=some --rewriteaxioms T496.fq
...
Unsafe:
WARNING: 1
WARNING: 3

Second, the goal of the trie is precisely to

1. Represent all the constraints with shared binders,
2. Compute (PLE) equalities per binder, which allows
3. Sharing the equalities across all constraints that use those binders.

It is better to do it per binder than constraint because (2) ensures the binders
are shared across constraints. For example, consider two constraints:

Env |- f(x) = 0
Env |- f(y) = 10

Now if the Env is shared we want to just compute the PLE equalities once, and not duplicate work across the two constraints, which is what the trie is doing.

Does that make sense?

[The pre-trie version computed equalities per-constraint and was way slower]

[facundominguez]

Does that make sense?

I think I follow this far. Though I'm not proposing to eliminate the trie, I'm just saying that the discovered equalities shouldn't be collapsed into a single map of bindings to equalities (i.e. the InstRes type in the implementation).

When the constraints are tree like, bindings are shared and no work is duplicated. And when the constraints aren't tree like, it is just slower, but still yields correct equalities for each constraint. After all, your own fixup is cloning the bindings which creates more work for PLE anyway.

sorry I was putting out some other fires :-)

That's alright. We can get back to this when you have the availability. Could have a call as well about it.

[facundominguez]

Here goes an attempt at explaining a fix. I'm proposing to eliminate the tree-like invariant. PLE will continue to be as fast as today if the invariant holds. And when the invariant doesn't hold, PLE will become as slow as the fixup that duplicates bindings as necessary to establish the invariant again.

Simplifying many details, the current PLE works schematically as follows:

type Trie = [Branch]
data Branch = Branch BindId Trie | Val ConstraintId

ple :: (Bindings, Constraints) -> Bindings
ple (bs, cs) = updateBindings bs $ equalitiesFromTrie $ buildTrie cs

updateBindings :: Bindings -> HashMap BindId EqualitySet -> Bindings
updateBindings bs eqs = [ (b, rhs && (eqs ! b)) | (b, rhs) <- bs]

equalitiesFromTrie :: Trie -> HashMap BindId EqualitySet
equalitiesFromTrie = mconcat . map pleBranch

-- | This goes into the details of producing the actual equalities and may
-- call in mutual recursion to 'equalitiesFromTrie'.
pleBranch :: Trie -> HashMap BindId EqualitySet

buildTrie :: Constraints -> Trie

As the multiple HashMaps are merged, there is no check that the entries on one HashMap don't overwrite the entries in another. We could change this algorithm to give it a richer output so when the HashMaps do have colliding keys, all the values are preserved.

- equalitiesFromTrie :: Trie -> HashMap BindId EqualitySet
+ equalitiesFromTrie :: Trie -> HashMap BindId [(EqualitySet, HashSet ConstraintId)]

Now, whenever a binding is assigned equalities on different branches of the trie, each branch originates a new item in the list.

- equalitiesFromTries = mconcat . map pleBranch
+ equalitiesFromTries = unionsWith (++) . map pleBranch

Rather than overwriting one with another, the discovered equalities are kept together. The set of constraints (i.e. the second component of (EqualitySet, HashSet ConstraintId)) explains for which constraints the equalities apply. An invariant of the enriched output is that the constraints sets for a given binding are disjoint. More formally:

forall (b :: BindId) (cs :: Constraints).
  allDisjoint (map snd (equalitiesFromTrie (buildTrie cs) ! b))

allDisjoint [] = True
allDisjoint (x : xs) = all (null . intersection x) xs && allDisjoint xs

When we update the bindings, we duplicate the bindings for each equality set that has been produced.

updateBindings
  :: Bindings
  -> HashMap BindId [(EqualitySet, HashSet ConstraintId)]
  -> (Bindings, [(BindId, HashSet ConstraintId)]) -- updated bindings + new bindids to insert in some constraints

[facundominguez]

Some tests in LiquidHaskell fail if we check that joint points in the trie do not occur on separate branches (here's the patch: a0f2dc9). All the tests I tried pass if I disable environment reduction.

[facundominguez]

Interesting. Github doesn't let me reopen this issue.

[ranjitjhala]

Oops! Just reopened