This is now substantially improved using the with ... assert construct. See https://github.com/FStarLang/steel/blob/main/share/steel/examples/pulse/bug-reports/ExistsWitness.fst

A short description:

Assert with binders

fn sample6 (x0:R.ref int) (x1:R.ref bool)

requires exists p0 p1 v0 v1. R.pts_to x0 p0 v0 ** R.pts_to x1 p1 v1

ensures emp

{

   

    with p0 p1 v0 v1.

    assert R.pts_to x0 p0 v0 ** R.pts_to x1 p1 v1;

    drop (R.pts_to x0 p0 v0);

    drop (R.pts_to x1 p1 v1);

    ()

}

with bs. assert p allows you to write an assertion while binding the variables in the continuation. The checker finds instantiations in the context for these binders. It gives you a way to "get your hands" on existentially bound variables.

from steel.

I'm keeping the issue open since there is still an example that fails related to the handling of reveal/hide and the perm type.

from steel.

This is now fixed with f888fc8

The problem was the Pulse was now respecting the smt_fallback attribute. So, it would refuse to equate R.pts_to x p v and R.pts_to x q v even if p and q are provably equal.

From the code comment:

When comparing t0 =?= t1, if they are not syntactically equal, we
have to decide whether or not we should fire an SMT query to compare
them for provable equality.
The criterion is as follows:

1. We allow an SMT query if either t0 or t1 is "equational". For now, that means
   that either is a match expression.
2. Otherwise, if they are both applications of f v0...vn and f u0...un
   of the same head symbol f, a top-level constant, then we check if the
   type of f decorates any of its binders with the smt_fallback attribute.
   • If none of them are marked as such,
     then we check if f v0... is syntactically equal to f u0...
     and allow an SMT query to check if vn = vm. That is, the default behavior
     for predicates is that they last argument is eligible for SMT equality.
   • Otherwise, for each binder that is NOT marked as smt_fallback, we check
     if the corresponding argument is syntactically equal. If so, we allow
     t0 and t1 to be compared for SMT equality.
     For example, Steel.ST.Reference.pts_to is defined like so:
     /// For instance, [pts_to r (sum_perm (half_perm p) (half_perm p)) (v + 1)]
     /// is unifiable with [pts_to r p (1 + v)]
     val pts_to (#a:Type0)
     (r:ref a)
     ([@@@smt_fallback] p:perm)
     ([@@@smt_fallback] v:a)
     : vprop

from steel.