Skip to content
GitLab
Projects Groups Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in / Register
  • Iris Iris
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 170
    • Issues 170
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 25
    • Merge requests 25
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
  • Deployments
    • Deployments
    • Releases
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Iris
  • IrisIris
  • Issues
  • #406
Closed
Open
Issue created Mar 03, 2021 by Armaël Guéneau@ArmaelContributor

Slow typechecking / nonterminating Qed when using auxiliary definitions in RAs

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.

Assignee
Assign to
Time tracking