Skip to content

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

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

If evars are present, Coq sometimes does extra backtracking when constructing typeclass instances. This is problematic for the Frame instances for ∨ and ∧: if evars are present, Coq may backtrack excessively on the premises of these instances. In practice, this causes some failing iFrames to take a very long time.

Consider the instance for ∨:

Instance frame_or_spatial progress1 progress2 R P1 P2 Q1 Q2 Q :
  MaybeFrame false R P1 Q1 progress1 →
  MaybeFrame false R P2 Q2 progress2 →
  TCOr (TCEq (progress1 && progress2) true) (TCOr
    (TCAnd (TCEq progress1 true) (TCEq Q1 True%I))
    (TCAnd (TCEq progress2 true) (TCEq Q2 True%I))) →
  MakeOr Q1 Q2 Q →
  Frame false R (P1 ∨ P2) Q | 9.

Suppose the R we are framing does not occur in P1 and P2. The two MaybeFrame instances will thus have false for progress, causing the TCOr instance to not be found.
If P1 and/or P2 contain evars, Coq does not yet give up: it (wrongfully) surmises that the TCOr might succeed for different MaybeFrame instances, since the evars might get instantiated differently.

This MR wraps the MaybeFrame premise in a TCNoBackTrack to prevent this behavior. It also adds some tests for iFrameing under ∧ and ∨ in the presence of evars, which previously took a very long time to terminate.

Edited by Ike Mulder

Merge request reports