Unsound instantiation of existentials by `iFrame` on persistent facts

@janno and I found that the new support for existential instantiation in iFrame (from !1017 (merged)) can sometimes instantiate existential quantifiers too eagerly for persistent facts.

Reproducing example:

Require Import iris.bi.interface.
Require Import iris.proofmode.proofmode.

Goal ∀ (PROP : bi) (P : nat -> PROP),
  □ P 0 ⊢ P 0 ∗ (∀ n : nat, P n -∗ ∃ n, P n ∗ ⌜n = 1⌝).
Proof.
  iIntros (??) "#$".
  (*
  PROP : bi
  P : nat → PROP
  ============================
  _ : P 0
  --------------------------------------□
  ∀ x : nat, P x -∗ ⌜0 = 1⌝
  *)
Abort.

So on the one hand this is easy to fix, we can just use the 'old' instance when framing persistent hypotheses under existential quantifiers.

On the other hand, we could leave it as it is. iFrame does not always do what you want, and this is a new instance where that happens.

I don't know what would be best here.

Did you encounter this pattern a lot? What are the kind of Ps for which you encountered this in proofs?

We are still porting code. We have covered about 250 out of 2000 iFrame calls and only encountered this problem once, so far.

I think the general pattern is very common in atomic updates and related concepts. You give away resources, get them back, and then show that you still have them but with possibly changed parameters. Sometimes there are view shifts in the way when ghost state is changed in this way.

This pattern definitely appears in our specifications but not many of those ever have iFrame called on them. Our own automation's support for instantiating existentials stops at ∀ and -∗ exactly because it made goals unprovable.

IIRC iFrame lacks support for limiting how often something is framed (and where exactly), especially for pure hypotheses. For that reason I would argue for it being more careful under magic wands and ∀ instead of just leaving it.

We actually encountered this in a public proof in case you'd like to have a look:

https://github.com/bedrocksystems/BRiCk/blob/master/theories/lang/cpp/logic/heap_pred/tptsto.v#L222

The problem occurs when running iFrame (HVal) ...

For that reason I would argue for it being more careful under magic wands and ∀ instead of just leaving it.

That makes a lot of sense to me. I also ran into a couple of cases where iFrame did the wrong thing for the accessor pattern.

I also like that proposal.

So concretely the proposal is not stop framing under ∀ and wand? That makes sense to me. We probably should also stop at implication then?

Or is the idea that only specifically the ∃ instantiation support stops at ∀ etc, but other framing still happens below those connectives?

Or is the idea that only specifically the ∃ instantiation support stops at ∀ etc, but other framing still happens below those connectives?

That was what I had in mind. And I think it would be objectively the best solution.

I agree, only the existential introduction should stop under forall/etc.

Okay... so then it sounds like the Frame typeclass needs a new parameter to indicate whether it is below an ∃ ?

Okay... so then it sounds like the Frame typeclass needs a new parameter to indicate whether it is below an ∃ ?

below a ∀* but that seems to be the easiest solution. It's a somewhat invasive change though.

I guess we could also do something like

Class FrameCanInstantiateEx : Prop := frame_can_instantiate_ex : True.

Class FrameNoInstantiateEx : Prop := frame_no_instantiate_ex : True.

Hint Extern 4 FrameCanInstantiateEx =>
   lazymatch goal with
   | _ : FrameNoInstantiateEx |- _ => fail
   | |- _ => exact I
   end : typeclass_instances.

(* The frame instance for ∃ should also require a [FrameCanInstantiateEx] instance *)
Global Instance frame_exist ... :
  FrameCanInstantiateEx →
  ... →
  Frame p P (∃ a, Φ a) ... .

(* The frame instance for ∀, -∗ and → should introduce a [FrameNoInstantiateEx] into the context *)
Global Instance frame_wand p P L R Q :
  (FrameNoInstantiateEx → Frame p P R Q) →
  Frame p P (L -∗ R) (L -∗ Q).

which is less invasive but more convoluted.

I think Ike's solution is worth trying. It also seems more scalable instead of adding a new boolean flag for each future option.

I threw something together in !1035 (merged)

I think we are also hitting this in simuliris, where

  l_t ↦t v_t ∗ l_s ↦s v_s ∗ val_rel v_t v_s ∗
  (∀ (v_t' : V_t) (v_s' : V_s), l_t ↦t v_t' -∗ l_s ↦s v_s' -∗ val_rel v_t' v_s' -∗ gen_heap_bij_inv val_rel)

turns into

  ∀ (x : V_t) (x0 : V_s), l_t ↦t x -∗ l_s ↦s x0 -∗ val_rel x x0 -∗ gen_heap_bij_auth (L ∖ {[(l_t, l_s)]})

This is instantiating some ∃ inside gen_heap_bij_inv, which I don't think we want to happen.

mentioned in merge request !1035 (merged)

mentioned in commit d71f4877

closed with merge request !1035 (merged)

mentioned in merge request !1041