Skip to content

Fixed iFrame under ∧ and ∨ taking forever to fail in the presence of evars, alternative

Ike Mulder requested to merge snyke7/iris:ike/frame_evar∨∧_2 into master

See also !989 (merged). This MR is an alternative to !989 (merged) that keeps iFrame as strong as it currently is, while still speeding it up significantly when framing under ∧ or ∨ when evars are present.

Specifically, this MR changes some frame instances to minimize the number of different ways to derive a MaybeFrame instance. This limits the amount of backtracking Coq does on failing instances. To do so, it e.g. inserts TCNoBackTrack at some strange places (around MakeSeps in the frame instance for ∗, for example), and merges the two frame_here instances into a single one.

The frame instance for ∨ remains somewhat problematic: when deriving a Frame false R (P1 ∨ P2) for which R cán be framed in P1, but cannot be framed in P2, typeclass inference will still try to see if not framing R in P1 makes a difference. This means Coq will attempt (and fail) to frame R in P2 twice in this case.
Concretely, this causes iFrame's running time to scale quadratically with n, the number of disjuncts, in the following example:

Lemma test_iFrame_disjunction_3_evars `(Φ : nat → PROP) P1 P2 P3 P4 :
  BiAffine PROP →
  let n := 8 in
  let R := fun a => Nat.iter n (fun P => (P1 ∗ P2 ∗ P3 ∗ P4 ∗ Φ a) ∨ P)%I (Φ a) in
  P1 ⊢ ∃ a, R a.
Proof.
  intros ?. cbn. iIntros "HP1". iExists _.
  time iFrame.
Abort.

Merge request reports