From e1f0569f88fd367f321f571c341ec9a1c10d0857 Mon Sep 17 00:00:00 2001 From: n33levo Date: Tue, 11 Aug 2026 01:26:46 -0400 Subject: [PATCH 1/3] fix: avoid recursion in invariant side conditions --- Iris/Iris/Std/Namespaces.lean | 4 ++++ Iris/Iris/Tests/Tactics.lean | 15 +++++++++++++++ 2 files changed, 19 insertions(+) diff --git a/Iris/Iris/Std/Namespaces.lean b/Iris/Iris/Std/Namespaces.lean index fa9ddbb8e..d38cea407 100644 --- a/Iris/Iris/Std/Namespaces.lean +++ b/Iris/Iris/Std/Namespaces.lean @@ -44,6 +44,10 @@ instance ndisjoint : Iris.Std.Disjoint Namespace where theorem nclose_root : ↑nroot = CoPset.full := by rfl +-- `trivial` tries `apply_rfl`; keep its definitional equality check from evaluating concrete +-- namespace encodings through `CoPset.suffixesRaw`. +attribute [irreducible] nclose + theorem nclose_subseteq [Pos.Countable A] N (x : A) : (↑N.@x : CoPset) ⊆ (↑N : CoPset) := by intros p simp only [nclose, CoPset.elem_suffixes] diff --git a/Iris/Iris/Tests/Tactics.lean b/Iris/Iris/Tests/Tactics.lean index b234f7ab8..c2d104d58 100644 --- a/Iris/Iris/Tests/Tactics.lean +++ b/Iris/Iris/Tests/Tactics.lean @@ -3684,6 +3684,10 @@ section iinv variable {hlc : HasLC} {GF : BundledGFunctors} [InvGS_gen hlc GF] {N : Namespace} +/-- Tests fallback after `apply_rfl` inspects a concrete namespace side condition. -/ +example : nclose (ofName `rnd) ⊆ ⊤ := by + first | apply_rfl | exact CoPset.subseteq_top + /-- Tests `iinv` with `elimInv_acc_without_close`, `elimAcc_fupd` and `intoAcc_inv` where the side condition is trivial. @@ -3698,6 +3702,17 @@ example {P : IProp GF} : inv N iprop( P) ={⊤}=∗ ▷ P := by inext iexact H +/-- Tests `iinv` with a concrete namespace whose closure is expensive to unfold. -/ +example {P : IProp GF} : inv (ofName `rnd) iprop( P) ={⊤}=∗ ▷ P := by + iintro #Hinv + iinv Hinv with #H + imodintro + isplit + · iexact H + · imodintro + inext + iexact H + /-- Tests `iinv` with `elimInv_acc_with_close`, `elimModal_fupd_fupd` and `intoAcc_inv` where the side condition is trivial. From 2c1cf06d626e6b71106a0eed9d54cfba1da8bb4d Mon Sep 17 00:00:00 2001 From: Michael Sammler Date: Wed, 12 Aug 2026 14:54:35 +0200 Subject: [PATCH 2/3] cleanup and use iinv more --- Iris/Iris/HeapLang/Lib/LandinsKnot.lean | 11 ++--- Iris/Iris/HeapLang/Lib/NondetBool.lean | 2 +- Iris/Iris/HeapLang/Lib/Spawn.lean | 37 +++++----------- Iris/Iris/HeapLang/Lib/SpinLock.lean | 57 +++++++++---------------- Iris/Iris/Std/CoPset.lean | 7 ++- Iris/Iris/Std/Namespaces.lean | 10 ++--- 6 files changed, 47 insertions(+), 77 deletions(-) diff --git a/Iris/Iris/HeapLang/Lib/LandinsKnot.lean b/Iris/Iris/HeapLang/Lib/LandinsKnot.lean index 5ee59704c..35d2d157c 100644 --- a/Iris/Iris/HeapLang/Lib/LandinsKnot.lean +++ b/Iris/Iris/HeapLang/Lib/LandinsKnot.lean @@ -51,14 +51,11 @@ theorem wp_landinsKnot (P : Val → IProp GF) (Q : Val → Val → IProp GF) (F iloeb as IH generalizing %v1 %Φ wp_rec wp_bind !_ - iapply wp_atomic - imod inv_acc $$ Hinv with ⟨Hr, Hcl⟩ - simp only [CoPset.subseteq_top] - imodintro + iinv Hinv with >Hr + · simp; infer_instance -- TODO: iinv should solve this wp_load - imod Hcl $$ Hr - iapply H $$ [HP] [$] - iframe HP + imodintro; iframe + iapply H $$ [$HP] [$] iintro %v3 !> %Φ HP HQ iapply IH $$ HP HQ diff --git a/Iris/Iris/HeapLang/Lib/NondetBool.lean b/Iris/Iris/HeapLang/Lib/NondetBool.lean index f1de62986..cc8b79f15 100644 --- a/Iris/Iris/HeapLang/Lib/NondetBool.lean +++ b/Iris/Iris/HeapLang/Lib/NondetBool.lean @@ -26,7 +26,7 @@ theorem nondetBool.spec : unfold nondetBool wp_alloc l with Hl wp_pures - imod inv_alloc `n ⊤ iprop(∃ (b : Bool), l ↦ hl_val(#b)) $$ [$Hl] with #Hinv + imod inv_alloc `rnd ⊤ iprop(∃ (b : Bool), l ↦ hl_val(#b)) $$ [$Hl] with #Hinv wp_bind fork(_) iapply wp_fork $$ [K] [] · inext diff --git a/Iris/Iris/HeapLang/Lib/Spawn.lean b/Iris/Iris/HeapLang/Lib/Spawn.lean index 358463e0a..2010dbd65 100644 --- a/Iris/Iris/HeapLang/Lib/Spawn.lean +++ b/Iris/Iris/HeapLang/Lib/Spawn.lean @@ -109,15 +109,12 @@ theorem spawn_spec (Ψ : Val → IProp GF) (f : Val) : iapply wp_wand $$ Hf iintro %v HΨ wp_pures - iapply wp_atomic - imod inv_acc (fun _ _ => CoPset.mem_full) $$ Hinv with ⟨Hpt, Hclose⟩ + iinv Hinv with Hpt + · simp; infer_instance -- TODO: iinv should solve this unfold spawnInv icases Hpt with ⟨%_, Hl, _⟩ - imodintro wp_store - iapply Hclose - inext - iexists _; iframe Hl + imodintro; iframe Hl; imodintro iright; iexists v; isplit · itrivial · iframe @@ -134,33 +131,21 @@ theorem join_spec (Ψ : Val → IProp GF) (l : Loc) : iloeb as IH wp_rec wp_bind !_ - iapply wp_atomic - imod inv_acc (fun _ _ => CoPset.mem_full) $$ Hinv with ⟨Hpt, Hclose⟩ + iinv Hinv with Hpt + · simp; infer_instance -- TODO: iinv should solve this unfold spawnInv icases Hpt with ⟨%lv, Hl, Hcond⟩ - imodintro - wp_load + wp_load; imodintro; iframe Hl icases Hcond with (%Heq | ⟨%w, %Heq, (HΨw | Hγ')⟩) <;> subst Heq - · imod Hclose $$ [Hl] - · inext - iexists _ - iframe Hl - ileft; itrivial - imodintro + · isplitr + · ileft; itrivial wp_pures iapply IH $$ HΦ Hγ - · imod Hclose $$ [Hl Hγ] - · inext - iexists _; iframe Hl - iright; iexists w; isplit - · itrivial - · iframe - imodintro + · isplitl [Hγ] + · iright; iframe Hγ; itrivial wp_pures iapply HΦ $$ HΨw - · iexfalso - iapply token_exclusive - iframe + · icombine Hγ Hγ' gives %⟨⟩ end Specs diff --git a/Iris/Iris/HeapLang/Lib/SpinLock.lean b/Iris/Iris/HeapLang/Lib/SpinLock.lean index d22cdc944..c19135f57 100644 --- a/Iris/Iris/HeapLang/Lib/SpinLock.lean +++ b/Iris/Iris/HeapLang/Lib/SpinLock.lean @@ -130,37 +130,29 @@ theorem try_acquire_spec (γ : GName) (lk : Val) (R : IProp GF) : icases Hlock with ⟨%l, %Heq, #Hinv⟩ subst Heq wp_bind cmpXchg(_,_,_) - iapply wp_atomic - imod inv_acc $$ Hinv with ⟨G1, G2⟩ - · simp + iinv Hinv with G1 + · simp; infer_instance -- TODO: iinv should solve this unfold lockInv - imodintro icases G1 with ⟨%b, Hpt, Hcond⟩ cases b · simp only [Bool.false_eq_true, ↓reduceIte] wp_cmpxchg_suc - imod G2 $$ [Hpt] - · iexists true - simp only [↓reduceIte] - iframe - · imodintro - wp_pure - imodintro - iapply Hcont $$ [Hcond] - simp only [↓reduceIte] - iframe + imodintro + isplitl [Hpt] + · iframe; simp; itrivial + wp_pures + imodintro + iapply Hcont $$ [Hcond] + simp only [↓reduceIte]; iframe · simp only [↓reduceIte] wp_cmpxchg_fail - imod G2 $$ [Hpt] - · iexists true - simp only [↓reduceIte] - iframe - · imodintro - wp_pure - imodintro - iapply Hcont - simp only [Bool.false_eq_true, ↓reduceIte] - itrivial + imodintro + isplitl [Hpt] + · iframe; simp; itrivial + wp_pures + imodintro + iapply Hcont $$ [Hcond] + simp only [Bool.false_eq_true, ↓reduceIte]; itrivial @[rocq_alias heap_lang.spin_lock.acquire_spec] theorem acquire_spec (γ : GName) (lk : Val) (R : IProp GF) : @@ -195,21 +187,14 @@ theorem release_spec (γ : GName) (lk : Val) (R : IProp GF) : unfold isLock icases Hlock with ⟨%l, %Heq, #Hinv⟩ subst Heq - iapply wp_atomic - imod inv_acc $$ Hinv with ⟨G1, G2⟩ - · simp + iinv Hinv with G1 + · simp; infer_instance -- TODO: iinv should solve this unfold lockInv - imodintro icases G1 with ⟨%b, Hpt, Hcond⟩ wp_store - imod G2 $$ [- Hcont] - · inext - iexists false - simp only [Bool.false_eq_true, ↓reduceIte] - iframe - · imodintro - iapply Hcont - itrivial + imodintro; iframe Hpt + simp only [Bool.false_eq_true, ↓reduceIte]; iframe + iapply Hcont; itrivial end Specs diff --git a/Iris/Iris/Std/CoPset.lean b/Iris/Iris/Std/CoPset.lean index e7d78cf5b..dc6112d05 100644 --- a/Iris/Iris/Std/CoPset.lean +++ b/Iris/Iris/Std/CoPset.lean @@ -492,6 +492,9 @@ theorem coPsetSuffixes_wf p : coPsetWf (CoPsetRaw.suffixesRaw p) := by induction p <;> simp [CoPsetRaw.suffixesRaw, coPsetWf] <;> apply node'_wf <;> simp_all [coPsetWf] +-- `suffixes` is irreducible since computing `CoPsetRaw.suffixesRaw easily +-- hits the recursion limit, see https://github.com/leanprover-community/iris-lean/issues/557 +@[irreducible] def suffixes (p : Pos) : CoPset := ⟨CoPsetRaw.suffixesRaw p, coPsetSuffixes_wf p⟩ @@ -499,13 +502,13 @@ theorem elem_suffixes {p q} : p ∈ suffixes q <-> ∃ q', p = q' ++ q := by constructor · induction q generalizing p with | xI q IH => - simp only [suffixes, CoPsetRaw.suffixesRaw, Membership.mem, elem_of_node] + simp only [suffixes, CoPsetRaw.suffixesRaw, Membership.mem, elem_of_node] at IH |- intros Hin cases p <;> simp [CoPsetRaw.ElemOf] at Hin obtain ⟨q', rfl⟩ := IH Hin exact ⟨q', rfl⟩ | xO q IH => - simp only [suffixes, CoPsetRaw.suffixesRaw, Membership.mem, elem_of_node] + simp only [suffixes, CoPsetRaw.suffixesRaw, Membership.mem, elem_of_node] at IH |- intros Hin cases p <;> simp [CoPsetRaw.ElemOf] at Hin obtain ⟨q', rfl⟩ := IH Hin diff --git a/Iris/Iris/Std/Namespaces.lean b/Iris/Iris/Std/Namespaces.lean index d38cea407..4a9b1d5d0 100644 --- a/Iris/Iris/Std/Namespaces.lean +++ b/Iris/Iris/Std/Namespaces.lean @@ -42,11 +42,11 @@ infix:80 ".@" => ndot instance ndisjoint : Iris.Std.Disjoint Namespace where disjoint N1 N2 := nclose N1 ## nclose N2 -theorem nclose_root : ↑nroot = CoPset.full := by rfl - --- `trivial` tries `apply_rfl`; keep its definitional equality check from evaluating concrete --- namespace encodings through `CoPset.suffixesRaw`. -attribute [irreducible] nclose +theorem nclose_root : ↑nroot = CoPset.full := by + ext p + simp only [nclose, Pos.flatten, nroot, Pos.flattenGo, CoPset.elem_suffixes, + CoPset.mem_full, iff_true, HAppend.hAppend, Pos.app] + exists p theorem nclose_subseteq [Pos.Countable A] N (x : A) : (↑N.@x : CoPset) ⊆ (↑N : CoPset) := by intros p From b4982bdb330f6ff0c690c0cb6be675bbb6b9bf66 Mon Sep 17 00:00:00 2001 From: Michael Sammler Date: Wed, 12 Aug 2026 14:55:24 +0200 Subject: [PATCH 3/3] tweak tests --- Iris/Iris/Tests/Tactics.lean | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) diff --git a/Iris/Iris/Tests/Tactics.lean b/Iris/Iris/Tests/Tactics.lean index c2d104d58..4b4adebc9 100644 --- a/Iris/Iris/Tests/Tactics.lean +++ b/Iris/Iris/Tests/Tactics.lean @@ -3684,10 +3684,6 @@ section iinv variable {hlc : HasLC} {GF : BundledGFunctors} [InvGS_gen hlc GF] {N : Namespace} -/-- Tests fallback after `apply_rfl` inspects a concrete namespace side condition. -/ -example : nclose (ofName `rnd) ⊆ ⊤ := by - first | apply_rfl | exact CoPset.subseteq_top - /-- Tests `iinv` with `elimInv_acc_without_close`, `elimAcc_fupd` and `intoAcc_inv` where the side condition is trivial. @@ -3702,8 +3698,9 @@ example {P : IProp GF} : inv N iprop( P) ={⊤}=∗ ▷ P := by inext iexact H -/-- Tests `iinv` with a concrete namespace whose closure is expensive to unfold. -/ -example {P : IProp GF} : inv (ofName `rnd) iprop( P) ={⊤}=∗ ▷ P := by +/-- Tests `iinv` with a concrete namespace whose closure is expensive to unfold. +Regression test for https://github.com/leanprover-community/iris-lean/issues/557 -/ +example {P : IProp GF} : inv `long_name iprop( P) ={⊤}=∗ ▷ P := by iintro #Hinv iinv Hinv with #H imodintro