New matching: no backtracking on SMT results

[mtzguido]

This changes the slprop matching procedure in the checker to never backtrack on the result of SMT queries, and instead decide "which path" to take only through syntactic and unification checks. We still allow using the SMT explicitly via rewrites, and also this introduces a notion of matching key to automatically allow the checker to generate SMT guards. As an example

val pts_to ([@@@mkey] r : ref int) (x : int) : slprop

marks the reference as a matching key, and if we ever have pts_to r foo in the context and need to prove pts_to r bar, the matcher will succeed generating a (delayed) guard for pts_to r foo == pts_to r bar, which we will later try to discharge. We also still perform ambiguity checks, so if we also had pts_to r baz in the context, both matches would be "guarded" successes, and we would provide an error explaining the ambiguity:

fn test (r : ref int) (foo bar baz : int)
  requires pts_to r foo ** pts_to r bar
  ensures  pts_to r baz
{
  ();
}

- Cannot prove:
    pts_to r baz
- In the context:
    pts_to r foo ** pts_to r bar
- Some hints:
- Ambiguous match for resource:
    pts_to r baz
- It can be matched by both:
    pts_to r foo
  and:
    pts_to r bar
  in the context.

This impacts heavily on all existing Pulse code. All code in this repo is updated to work, but we should look at external repos.

[mtzguido]

I should add this means we can safely admit queries when checking pulse code, since they don't affect the behavior of the checker. Lax-checking is therefore reenabled.

[gebner]

I have run into this issue many times where you need to add an extra dummy statement to trigger the matcher. (Sometimes even let x = foo (); x...)

Could we fix this more generally?

[mtzguido]

It's not needed here. I probably added it since when there's a failure in the last statement of a function there's no clear indication of whether it's the precondition that failed, or proving the function's postcondition. I want to fix that soon too, it's very annoying.

I'm not sure if I've seen an instance of what you mention on this branch, if you see it could you post an example?

[gebner]

#347

[gebner]

Leftover comment.

[gebner]

You forgot an admit here.

[gebner]

You forgot an admit here.

[gebner]

This is a common pattern in matches now. Can you do a rewrite each tree to None instead?

[mtzguido]

That rewrite is actually implicitly injected by the checker on a match, and now without the SMT it's kind of working against us. The state at the beginning of the branch is is_tree None ', so we lost the mention of tree, but we anyway need to prove a postcondition mentioning it.

I'm gonna try removing this automatic rewrite and see if things are better. We added it for compactness, but seems to be counterproductive now.

I suppose another possibly much nicer solution would be having the rewrite operate on the postcondition, but so far we don't do much to the postcondition at all.

[gebner]

Stray debugging option.

[gebner]

Stray debugging option.

[gebner]

Why does this no longer work?

[gebner]

To answer my own question, it's because maybe_holds is a match. And so you need to tell the matcher which branch is true.

[gebner]

You forgot an admit here.

[gebner]

Yes indeed. Are you saying that (x, y)._1 doesn't unify with x? @nikswamy ?

[mtzguido]

Not without unfolding, and we disable all unfolding during the unification checks performed by the matcher since we found them to go haywire previously. Probably something to revisit now.

I did add special support in Pulse to simplify (x,y)._1 ~> x for tuple2, I think I can extend this for all tuples and make this work, trying.

[mtzguido]

I allowed some unfolding and now this is just let p31, p32, pivot = partition_wrapper a lo hi lb rb;