GitLab

From iris.base_logic Require Export invariants gen_heap.
From iris.program_logic Require Export weakestpre ectx_lifting.
From iris.proofmode Require Import tactics.
From iris.algebra Require Import frac auth gmap excl list.

Definition memspecUR : ucmraT :=
  gmapUR nat (prodR fracR (agreeR (leibnizO nat))).
Definition regspecUR : ucmraT :=
  gmapUR nat (prodR fracR (agreeR (leibnizO nat))).
Definition memreg_specUR := prodUR regspecUR memspecUR.

Definition exprUR : cmraT := (exclR (leibnizO nat)).
Definition cfgUR : ucmraT := prodUR (optionUR exprUR) memreg_specUR.

Class cfgSG Σ := CFGSG {
  cfg_invG :> inG Σ (authR cfgUR);
  cfg_name : gname }.

Section S.
  Context `{cfgSG Σ}.

Lemma spec_heap_valid (e:option (excl (leibnizO nat))) a q w
  (rm: gmapUR nat (prodR fracR (agreeR (leibnizO nat))))
  (mm: gmapUR nat (prodR fracR (agreeR (leibnizO nat)))) :
  False →
  own cfg_name (● (e,(rm,mm))) ∗
  own cfg_name (◯ (ε, (∅,{[ a := (q, to_agree w) ]})))
  -∗ False.
Proof. intro.
  iIntros "(Hown & Ha)".
  iDestruct (own_valid_2 with "Hown Ha") as "HH". exfalso. assumption.
Qed.

End S.

The snippet above:

• works fine with Iris 3.3
• takes a very long time at Qed with Iris 3.4 (modulo replacing cmraT with cmra in the script)

The issue seems to be with the use of auxiliary definitions to define the resource algebra cfgUR. Manually inlining cfgUR and the other auxiliary definitions in the definition of cfgSG makes it work again with Iris 3.4.

Since the fix is relatively simple, this issue doesn't seem to be too big of a deal, but I thought that I'd report it just in case. Coq version used: 8.12.1 in both cases.