From d8807b71bce49c262a3b30af4f4a4efd8f0b04f4 Mon Sep 17 00:00:00 2001 From: Markus de Medeiros Date: Mon, 10 Aug 2026 19:04:46 -0400 Subject: [PATCH 1/8] generate --- Iris/Iris/Algebra.lean | 1 + Iris/Iris/Algebra/Frac.lean | 12 +- Iris/Iris/Algebra/LeibnizMultiSet.lean | 140 +++++++ Iris/Iris/BI/Lib/Fractional.lean | 52 +++ Iris/Iris/HeapLang/Lib.lean | 2 + Iris/Iris/HeapLang/Lib/RwLock.lean | 110 +++++ Iris/Iris/HeapLang/Lib/RwSpinLock.lean | 549 +++++++++++++++++++++++++ Iris/Iris/Std/GenMultiSets.lean | 89 +++- 8 files changed, 953 insertions(+), 2 deletions(-) create mode 100644 Iris/Iris/Algebra/LeibnizMultiSet.lean create mode 100644 Iris/Iris/HeapLang/Lib/RwLock.lean create mode 100644 Iris/Iris/HeapLang/Lib/RwSpinLock.lean diff --git a/Iris/Iris/Algebra.lean b/Iris/Iris/Algebra.lean index 0ce0a7bd5..4beadf358 100644 --- a/Iris/Iris/Algebra.lean +++ b/Iris/Iris/Algebra.lean @@ -16,6 +16,7 @@ public import Iris.Algebra.Heap public import Iris.Algebra.HeapView public import Iris.Algebra.IProp public import Iris.Algebra.IsOp +public import Iris.Algebra.LeibnizMultiSet public import Iris.Algebra.LeibnizSet public import Iris.Algebra.List public import Iris.Algebra.LocalUpdates diff --git a/Iris/Iris/Algebra/Frac.lean b/Iris/Iris/Algebra/Frac.lean index 1910dc332..20f1e405d 100644 --- a/Iris/Iris/Algebra/Frac.lean +++ b/Iris/Iris/Algebra/Frac.lean @@ -59,6 +59,12 @@ def Qp.div (x y : Qp) : Qp := ⟨x.val / y.val, Rat.div_pos x.2 y.2⟩ instance instHDivQpQpQp : HDiv Qp Qp Qp where hDiv := Qp.div +/-- The fraction `1/4`. -/ +def Qp.quarter : Qp := ⟨1 / 4, by grind⟩ + +/-- The fraction `3/4`. -/ +def Qp.threeQuarters : Qp := ⟨3 / 4, by grind⟩ + def Qp.divide_even (q : Qp) (n : Nat) (hn : 0 < n) : Qp := ⟨q.val / n, Rat.div_pos q.2 (by exact_mod_cast hn)⟩ @@ -86,7 +92,6 @@ instance instCMRAQp : CMRA Qp where extend {_ x y z} := by rintro H He; exact ⟨y, z, He, .rfl, .rfl⟩ - -- TODO: A different solution to having these bridge lemmas might be to internalize -- positivity into the CMRA's validity predicate, removing the sybtype, and having Qp -- become just a Leibniz CMRA over Rat. This admits two-way coercions to Rat for the automation. @@ -94,6 +99,8 @@ instance instCMRAQp : CMRA Qp where @[simp, grind =] theorem Qp.val_add (x y : Qp) : (x + y).val = x.val + y.val := rfl @[simp, grind =] theorem Qp.val_one : (1 : Qp).val = 1 := rfl @[simp, grind =] theorem Qp.val_half (q : Qp) : q.half.val = q.val / 2 := rfl +@[simp, grind =] theorem Qp.val_quarter : Qp.quarter.val = 1 / 4 := rfl +@[simp, grind =] theorem Qp.val_threeQuarters : Qp.threeQuarters.val = 3 / 4 := rfl @[simp, grind =] theorem Qp.val_div (x y : Qp) : (x / y).val = x.val / y.val := rfl @[simp, grind =] theorem Qp.val_divide_even (q : Qp) (n : Nat) (hn : 0 < n) : (q.divide_even n hn).val = q.val / n := rfl @@ -106,6 +113,9 @@ instance instCMRAQp : CMRA Qp where @[simp] theorem Qp.dist_iff {n} {x y : Qp} : x ≡{n}≡ y ↔ x.val = y.val := Subtype.ext_iff @[simp, rocq_alias frac_valid_1] theorem Qp.valid_one : ✓ (1 : Qp) := by grind @[simp, grind =] theorem Qp.half_add_half (q : Qp) : q.half + q.half = q := Subtype.ext (by grind) +@[grind =] theorem Qp.add_left_comm (x y z : Qp) : x + (y + z) = y + (x + z) := by grind +@[simp, grind =] theorem Qp.quarter_add_threeQuarters : Qp.quarter + Qp.threeQuarters = 1 := by + grind theorem Qp.lt_iff_exists_add {a b : Qp} : a < b ↔ ∃ c : Qp, a + c = b := by refine ⟨fun h => ⟨⟨b.val - a.val, by have := Qp.lt_iff.mp h; grind⟩, Subtype.ext (by grind)⟩, ?_⟩ diff --git a/Iris/Iris/Algebra/LeibnizMultiSet.lean b/Iris/Iris/Algebra/LeibnizMultiSet.lean new file mode 100644 index 000000000..a931e9f7f --- /dev/null +++ b/Iris/Iris/Algebra/LeibnizMultiSet.lean @@ -0,0 +1,140 @@ +/- +Copyright (c) 2026. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: +-/ +module + +public import Iris.Algebra.BigOp +public import Iris.Algebra.CMRA +public import Iris.Algebra.LocalUpdates +public import Iris.Algebra.Updates +public import Iris.Std.GenMultiSets +meta import Iris.Std.RocqPorting + +@[expose] public section + +/-! ## The multiset union CMRA +Every multiset is valid, composition is disjoint union, and the core is the empty multiset. +Multisets are given the discrete Leibniz OFE, and as a consequence are unrelated to any +OFE/CMRA on the element type. -/ + +open Iris Std CMRA OFE + +@[rocq_alias gmultisetO, rocq_alias gmultisetR, rocq_alias gmultisetUR] +inductive LeibnizMultiSet (MS : Type _) where + | valid (X : MS) + +#rocq_ignore gmultiset_valid_instance "Provided by the `CMRA (LeibnizMultiSet MS)` instance." +#rocq_ignore gmultiset_validN_instance "Provided by the `CMRA (LeibnizMultiSet MS)` instance." +#rocq_ignore gmultiset_unit_instance "Provided by the `UCMRA (LeibnizMultiSet MS)` instance." +#rocq_ignore gmultiset_op_instance "Provided by the `CMRA (LeibnizMultiSet MS)` instance." +#rocq_ignore gmultiset_pcore_instance "Provided by the `CMRA (LeibnizMultiSet MS)` instance." +#rocq_ignore gmultiset_ra_mixin "Provided by the `CMRA (LeibnizMultiSet MS)` instance." +#rocq_ignore gmultiset_ucmra_mixin "Provided by the `UCMRA (LeibnizMultiSet MS)` instance." + +instance : COFE (LeibnizMultiSet MS) := COFE.ofDiscrete _ + +namespace LeibnizMultiSet + +variable {MS : Type _} [LawfulMultiSet MS A] + +instance : CMRA (LeibnizMultiSet MS) where + pcore _ := some (valid ∅) + op | valid X, valid Y => valid (X ⊎ Y) + ValidN _ _ := True + Valid _ := True + op_ne.ne _ _ _ H := by rw [(H : _ = _)] + pcore_ne {_ _ _ cx} _ H := ⟨cx, H, .rfl⟩ + validN_ne _ _ := trivial + valid_iff_validN := by simp + validN_succ _ := trivial + validN_op_left _ := trivial + assoc {X Y Z} := by cases X; cases Y; cases Z; exact congrArg valid disjUnion_assoc.symm + comm {X Y} := by cases X; cases Y; exact congrArg valid disjUnion_comm + pcore_op_left {_ X} := by cases X; rintro ⟨rfl⟩; exact congrArg valid disjUnion_empty_left + pcore_idem := id + pcore_op_mono {_ X} := by + cases X; rintro ⟨rfl⟩ _ + exact ⟨valid ∅, congrArg (some ∘ valid) disjUnion_empty_left.symm⟩ + extend {_ _ _ _} _ h := ⟨_, _, h, .rfl, .rfl⟩ + +instance : UCMRA (LeibnizMultiSet MS) where + unit := valid ∅ + unit_valid := trivial + unit_left_id {X} := by cases X; exact congrArg valid disjUnion_empty_left + pcore_unit := rfl + +@[rocq_alias gmultiset_cmra_discrete] +instance : CMRA.Discrete (LeibnizMultiSet MS) where + discrete_0 h := h + discrete_valid := id + +instance : CMRA.IsTotal (LeibnizMultiSet MS) where + total _ := ⟨valid ∅, rfl⟩ + +@[rocq_alias gmultiset_op] +theorem op_disjUnion (X Y : MS) : (valid X) • (valid Y) = valid (X ⊎ Y) := rfl + +@[rocq_alias gmultiset_core] +theorem core_eq_empty (X : LeibnizMultiSet MS) : core X = valid ∅ := rfl + +@[rocq_alias gmultiset_opM] +theorem opM_disjUnion (X : LeibnizMultiSet MS) (mY : Option (LeibnizMultiSet MS)) : + X •? mY = X • mY.getD (valid ∅) := by + cases X; cases mY <;> simp [op?, op, disjUnion_empty_right] + +@[rocq_alias gmultiset_included] +theorem included_iff_subset {X Y : MS} : valid X ≼ valid Y ↔ X ⊆ Y where + mp | ⟨.valid _, h⟩ => valid.inj h ▸ disjUnion_subset_left + mpr h := ⟨valid (Y \ X), congrArg valid (disjUnion_difference_of_subseteq h)⟩ + +@[rocq_alias gmultiset_cancelable] +instance (X : LeibnizMultiSet MS) : CMRA.Cancelable X := + discrete_cancelable fun {Y Z} _ h => by + cases X; cases Y; cases Z + exact congrArg valid (disjUnion_left_inj (valid.inj h)) + +@[rocq_alias gmultiset_update] +theorem update (X Y : MS) : valid X ~~> valid Y := fun _ _ _ => trivial + +@[rocq_alias gmultiset_local_update] +theorem localUpdate {X Y X' Y' : MS} (h : X ⊎ Y' = X' ⊎ Y) : + (valid X, valid Y) ~l~> (valid X', valid Y') := by + refine (local_update_unital_discrete ..).mpr fun ⟨Z⟩ _ e => ⟨trivial, ?_⟩ + have hX : X = Y ⊎ Z := valid.inj e + refine congrArg valid (LawfulMultiSet.ext fun a => ?_) + have h1 := congrArg (MultiSet.multiplicity a) h + have h2 := congrArg (MultiSet.multiplicity a) hX + simp only [multiplicity_disjUnion] at h1 h2 ⊢ + omega + +@[rocq_alias gmultiset_local_update_alloc] +theorem localUpdate_alloc {X Y X' : MS} : + (valid X, valid Y) ~l~> (valid (X ⊎ X'), valid (Y ⊎ X')) := + localUpdate <| LawfulMultiSet.ext fun _ => by simp only [multiplicity_disjUnion]; omega + +@[rocq_alias gmultiset_local_update_dealloc] +theorem localUpdate_dealloc {X Y X' : MS} (h : X' ⊆ Y) : + (valid X, valid Y) ~l~> (valid (X \ X'), valid (Y \ X')) := by + refine LocalUpdate.total_valid fun _ _ inc => localUpdate (LawfulMultiSet.ext fun a => ?_) + have hYX := subset_iff.mp (included_iff_subset.mp inc) a + have hX'Y := subset_iff.mp h a + simp only [multiplicity_disjUnion, multiplicity_difference] + omega + +end LeibnizMultiSet + +namespace LeibnizMultiSet +open Algebra + +variable {MS : Type _} [LawfulFiniteMultiSet MS A] + +@[rocq_alias big_opMS_singletons] +theorem bigOpMS_singletons (X : MS) : + ([^ CMRA.op mset] x ∈ X, (valid {x} : LeibnizMultiSet MS)) = valid X := by + induction X using multiset_ind with + | empty => exact BigOpMS.bigOpMS_empty + | disjUnion_singleton a X ih => rw [BigOpMS.bigOpMS_insert, ih, op_disjUnion] + +end LeibnizMultiSet diff --git a/Iris/Iris/BI/Lib/Fractional.lean b/Iris/Iris/BI/Lib/Fractional.lean index 2522c4be2..e0b556f77 100644 --- a/Iris/Iris/BI/Lib/Fractional.lean +++ b/Iris/Iris/BI/Lib/Fractional.lean @@ -134,3 +134,55 @@ theorem fractional_divide_equal {Φ : Qp → PROP} [Fractional Φ] (q : Qp) (n : grind end Divide + +/-! ## Internal fractional + +`internalFractional Φ` internalises `Fractional Φ` into the logic, so that it can be kept in an +invariant and transported along an internal `∗-∗`. -/ + +section InternalFractional +variable {PROP : Type _} [BI PROP] {Φ Ψ : Qp → PROP} + +@[rocq_alias internal_fractional] +def internalFractional (Φ : Qp → PROP) : PROP := iprop(□ ∀ p q, Φ (p + q) ∗-∗ Φ p ∗ Φ q) + +@[rocq_alias internal_fractional_ne] +instance internalFractional_ne : NonExpansive (internalFractional (PROP := PROP)) where + ne _ _ _ h := intuitionistically_ne.ne <| + forall_ne fun p => forall_ne fun q => wandIff_ne.ne (h _) (sep_ne.ne (h p) (h q)) + +#rocq_ignore internal_fractional_proper "OFE equivalence is Lean equality; use `congrArg`." + +@[rocq_alias internal_fractional_affine] +instance internalFractional_affine : Affine (internalFractional Φ) := by + unfold internalFractional; infer_instance + +@[rocq_alias internal_fractional_persistent] +instance internalFractional_persistent : Persistent (internalFractional Φ) := by + unfold internalFractional; infer_instance + +@[rocq_alias fractional_internal_fractional] +theorem fractional_internalFractional (h : Fractional Φ) : ⊢ internalFractional Φ := by + unfold internalFractional + iintro !> %p %q + iapply equiv_wandIff (h.fractional p q) + +@[rocq_alias internal_fractional_iff] +theorem internalFractional_iff : + □ (∀ q, Φ q ∗-∗ Ψ q) ⊢ internalFractional Φ -∗ internalFractional Ψ := by + unfold internalFractional + iintro #Hiff #Hdup !> %p %q + isplit + · iintro HΨ + icases Hdup $$ %p %q (Hiff $$ %(p + q) HΨ) with ⟨H1, H2⟩ + isplitl [H1] + · iapply Hiff $$ H1 + · iapply Hiff $$ H2 + · iintro ⟨H1, H2⟩ + iapply Hiff + iapply Hdup + isplitl [H1] + · iapply Hiff $$ H1 + · iapply Hiff $$ H2 + +end InternalFractional diff --git a/Iris/Iris/HeapLang/Lib.lean b/Iris/Iris/HeapLang/Lib.lean index fb454b2ef..9737782c8 100644 --- a/Iris/Iris/HeapLang/Lib.lean +++ b/Iris/Iris/HeapLang/Lib.lean @@ -9,6 +9,8 @@ public import Iris.HeapLang.Lib.Lock public import Iris.HeapLang.Lib.NondetBool public import Iris.HeapLang.Lib.Par public import Iris.HeapLang.Lib.Quicksort +public import Iris.HeapLang.Lib.RwLock +public import Iris.HeapLang.Lib.RwSpinLock public import Iris.HeapLang.Lib.Spawn public import Iris.HeapLang.Lib.SpinLock public import Iris.HeapLang.Lib.Unwrap diff --git a/Iris/Iris/HeapLang/Lib/RwLock.lean b/Iris/Iris/HeapLang/Lib/RwLock.lean new file mode 100644 index 000000000..9a52f0101 --- /dev/null +++ b/Iris/Iris/HeapLang/Lib/RwLock.lean @@ -0,0 +1,110 @@ +/- +Copyright (c) 2026. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: +-/ +module + +public import Iris.BI.Lib.Fractional +public import Iris.ProgramLogic.WeakestPre +public import Iris.HeapLang.Notation +public import Iris.HeapLang.Instances + +namespace Iris.HeapLang + +open BI OFE + +@[expose] public section + +/-- A general interface for a reader-writer lock. + +Only one instance of this class should ever be in scope. To write a library that is generic over +the lock, just add a `[RwLock GF]` parameter around the code and an `(L : rwlockG GF)` parameter +around the proofs. + +When writing an instance of this class, please take care not to shadow the class projections +(e.g. use a `newlock` in a dedicated namespace), and do not register the instance — just make it +a `def` that others can register later. -/ +@[rocq_alias heap_lang.rwlock] +class RwLock (GF : BundledGFunctors) [IrisGS_gen hlc Exp GF] where + -- Operations + newlock : Val + acquireReader : Val + releaseReader : Val + acquireWriter : Val + releaseWriter : Val + -- Ghost state: `rwlockG` collects the assumptions on `GF`, and `name` associates + -- `readerLocked` and `writerLocked` with `isRwLock`. + rwlockG : BundledGFunctors → Type + name : Type + -- Predicates. There is no namespace parameter because we only expose program specs, which + -- anyway have the full mask. + isRwLock : rwlockG GF → name → Val → (Qp → IProp GF) → IProp GF + readerLocked : rwlockG GF → name → Qp → IProp GF + writerLocked : rwlockG GF → name → IProp GF + -- General properties of the predicates + isRwLock_persistent {L} γ lk Φ : Persistent (isRwLock L γ lk Φ) + isRwLock_iff {L} γ lk Φ Ψ : + isRwLock L γ lk Φ ⊢ (▷ □ ∀ q, Φ q ∗-∗ Ψ q) -∗ isRwLock L γ lk Ψ + readerLocked_timeless {L} γ q : Timeless (readerLocked L γ q) + writerLocked_timeless {L} γ : Timeless (writerLocked L γ) + writerLocked_exclusive {L} γ : writerLocked L γ ∗ writerLocked L γ ⊢@{IProp GF} False + writerLocked_not_readerLocked {L} γ q : + writerLocked L γ ∗ readerLocked L γ q ⊢@{IProp GF} False + -- Program specs + newlock_spec {L} (Φ : Qp → IProp GF) {P ioΦ ioq} [AsFractional P ioΦ Φ ioq 1] : + {{ P }} hl(&newlock #()) {{ lk γ, RET lk; isRwLock L γ lk Φ }} + acquireReader_spec {L} γ lk Φ : + {{ isRwLock L γ lk Φ }} hl(&acquireReader &lk) + {{ q, RET hl_val(#()); readerLocked L γ q ∗ Φ q }} + releaseReader_spec {L} γ lk Φ q : + {{ isRwLock L γ lk Φ ∗ readerLocked L γ q ∗ Φ q }} hl(&releaseReader &lk) + {{ RET hl_val(#()); True }} + acquireWriter_spec {L} γ lk Φ : + {{ isRwLock L γ lk Φ }} hl(&acquireWriter &lk) + {{ RET hl_val(#()); writerLocked L γ ∗ Φ 1 }} + releaseWriter_spec {L} γ lk Φ : + {{ isRwLock L γ lk Φ ∗ writerLocked L γ ∗ Φ 1 }} hl(&releaseWriter &lk) + {{ RET hl_val(#()); True }} + +section lemmas + +variable [IrisGS_gen hlc Exp GF] [rw : RwLock GF] (L : rw.rwlockG GF) + +instance instPersistentIsRwLock γ lk Φ : Persistent (rw.isRwLock L γ lk Φ) := + rw.isRwLock_persistent γ lk Φ + +instance instTimelessReaderLocked γ q : Timeless (rw.readerLocked L γ q) := + rw.readerLocked_timeless γ q + +instance instTimelessWriterLocked γ : Timeless (rw.writerLocked L γ) := + rw.writerLocked_timeless γ + +@[rocq_alias heap_lang.is_rw_lock_contractive] +instance isRwLock_contractive γ lk : Contractive (rw.isRwLock L γ lk) := by + rw [contractive_internalEq (PROP := IProp GF)] + iintro %Φ₁ %Φ₂ #HEQ + ihave #HΦ : iprop(▷ ∀ q, Φ₁ q ≡ Φ₂ q) $$ [HEQ] + · iapply later_mono (discreteFun_equivI Φ₁ Φ₂).mp + iexact HEQ + iapply prop_ext + imodintro + isplit + · iintro #H + iapply rw.isRwLock_iff $$ H + iintro !> !> %q + irewrite [HΦ $$ %q] + · exact ⟨fun _ _ _ h => wandIff_ne.ne h .rfl⟩ + · iapply equiv_wandIff; exact .rfl + · iintro #H + iapply rw.isRwLock_iff $$ H + iintro !> !> %q + irewrite [HΦ $$ %q] + · exact ⟨fun _ _ _ h => wandIff_ne.ne .rfl h⟩ + · iapply equiv_wandIff; exact .rfl + +#rocq_ignore heap_lang.is_rw_lock_proper "OFE is Leibniz; use equality" + +end lemmas + +end diff --git a/Iris/Iris/HeapLang/Lib/RwSpinLock.lean b/Iris/Iris/HeapLang/Lib/RwSpinLock.lean new file mode 100644 index 000000000..b05cef234 --- /dev/null +++ b/Iris/Iris/HeapLang/Lib/RwSpinLock.lean @@ -0,0 +1,549 @@ +/- +Copyright (c) 2026. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: +-/ +module + +public import Iris.Algebra.LeibnizMultiSet +public import Iris.HeapLang.Lib.RwLock +public import Iris.HeapLang.PrimitiveLaws +public import Iris.HeapLang.ProofMode +public import Iris.Instances.Lib.Invariants +public import Iris.Std.GenMultiSetsInstances +public import Iris.Std.Namespaces + +namespace Iris.HeapLang + +open BI Iris Std ProgramLogic CMRA OFE LeibnizMultiSet FiniteMultiSet + +@[expose] public section + +namespace RwSpinLock + +@[rocq_alias heap_lang.newlock] +def newlock : Val := hl_val( + λ _, ref(#0)) + +@[rocq_alias heap_lang.try_acquire_reader] +def tryAcquireReader : Val := hl_val( + λ l, + let n := !l; + if #0 ≤ n + then cas(l, n, n + #1) + else #false) + +@[rocq_alias heap_lang.acquire_reader] +def acquireReader : Val := hl_val( + rec acquire l := + if (&tryAcquireReader l) + then #() + else acquire l) + +@[rocq_alias heap_lang.release_reader] +def releaseReader : Val := hl_val( + λ l, faa(l, #(-1 : Int)); #()) + +@[rocq_alias heap_lang.try_acquire_writer] +def tryAcquireWriter : Val := hl_val( + λ l, cas(l, #0, #(-1 : Int))) + +@[rocq_alias heap_lang.acquire_writer] +def acquireWriter : Val := hl_val( + rec acquire l := + if (&tryAcquireWriter l) + then #() + else acquire l) + +@[rocq_alias heap_lang.release_writer] +def releaseWriter : Val := hl_val( + λ l, l ← #0) + +/-- The multiset of fractions that have been handed out to readers. -/ +abbrev ReaderFracs := ListPerm Qp + +abbrev RwSpinLockF : COFE.OFunctorPre := constOF (Auth (LeibnizMultiSet ReaderFracs)) + +@[rocq_alias heap_lang.rw_spin_lockG] +class RwSpinLockG (GF : BundledGFunctors) where [elemG : ElemG GF RwSpinLockF] + +attribute [reducible, instance] RwSpinLockG.elemG + +#rocq_ignore heap_lang.«rw_spin_lockΣ» + "Superseded by the `RwSpinLockG` typeclass on `BundledGFunctors`." +#rocq_ignore heap_lang.«subG_rw_spin_lockΣ» + "Superseded by Lean's direct `ElemG` typeclass synthesis." + +section proof + +variable {GF : BundledGFunctors} [HeapLangGS hlc GF] [RwSpinLockG GF] + +def rwLockN : Namespace := nroot .@ "rw_lock" + +/-- Shorthand for ghost ownership of the reader-set authority. -/ +abbrev own (γ : GName) (a : Auth (LeibnizMultiSet ReaderFracs)) : IProp GF := + iOwn (F := RwSpinLockF) γ a + +/-- We need *some* ghost state that allows us to establish a contradiction in the left disjunct +(where the lock is write-locked) when proving `releaseReader_spec`, so we use a fraction of the +empty authoritative reader set (the rest goes to `writerLocked`). Any fraction would do, but the +benefit of giving over half to `writerLocked` (and keeping less than half here) is that we can +prove `writerLocked_exclusive`. -/ +@[rocq_alias heap_lang.rw_state_inv] +def rwStateInv (γ : GName) (l : Loc) (Φ : Qp → IProp GF) : IProp GF := iprop% + ∃ z : Int, l ↦ some hl_val(#z) ∗ + (⌜z = -1⌝ ∗ own γ (●{.own Qp.quarter} valid ∅) + ∨ ⌜0 ≤ z⌝ ∗ ∃ (q : Qp) (g : ReaderFracs), + own γ (● valid g) ∗ + ⌜size g = z.toNat⌝ ∗ + ⌜fold Qp.add q g = 1⌝ ∗ + Φ q) + +/-- The `▷` in front of `internalFractional` is preserved even when taking steps, which makes it +easier to re-establish. -/ +@[rocq_alias heap_lang.is_rw_lock] +def isRwLock (γ : GName) (lk : Val) (Φ : Qp → IProp GF) : IProp GF := iprop% + ▷ internalFractional Φ ∗ ∃ l : Loc, ⌜lk = hl_val(#l)⌝ ∗ inv rwLockN (rwStateInv γ l Φ) + +@[rocq_alias heap_lang.is_rw_lock_persistent] +instance instIsRwLockPersistent (γ : GName) (lk : Val) (Φ : Qp → IProp GF) : + Persistent (isRwLock γ lk Φ) := by unfold isRwLock; infer_instance + +@[rocq_alias heap_lang.reader_locked] +def readerLocked (γ : GName) (q : Qp) : IProp GF := own γ (◯ valid {q}) + +@[rocq_alias heap_lang.writer_locked] +def writerLocked (γ : GName) : IProp GF := own γ (●{.own Qp.threeQuarters} valid ∅) + +instance instReaderLockedTimeless (γ : GName) (q : Qp) : + Timeless (readerLocked (GF := GF) γ q) := by unfold readerLocked; infer_instance + +instance instWriterLockedTimeless (γ : GName) : + Timeless (writerLocked (GF := GF) γ) := by unfold writerLocked; infer_instance + +/-- Full authoritative ownership of the empty reader set splits into the quarter kept by +`rwStateInv` and the three quarters owned by `writerLocked`. -/ +theorem own_auth_empty_split (γ : GName) : + own (GF := GF) γ (●{.own Qp.quarter} valid (∅ : ReaderFracs)) ∗ + own γ (●{.own Qp.threeQuarters} valid ∅) ⊣⊢ own γ (● valid (∅ : ReaderFracs)) := by + have hsplit : (● valid (∅ : ReaderFracs) : Auth (LeibnizMultiSet ReaderFracs)) + = (●{.own Qp.quarter} valid (∅ : ReaderFracs)) • ●{.own Qp.threeQuarters} valid ∅ := by + rw [← Auth.auth_dfrac_op, DFrac.op_own, Qp.quarter_add_threeQuarters] + rw [hsplit] + exact iOwn_op.symm + +@[rocq_alias heap_lang.writer_locked_exclusive] +theorem writerLocked_exclusive (γ : GName) : + writerLocked γ ∗ writerLocked γ ⊢@{IProp GF} False := by + unfold writerLocked + iintro ⟨H1, H2⟩ + icombine H1 H2 gives %Hvalid + rw [Auth.auth_dfrac_op_valid, DFrac.op_own, DFrac.valid_own] at Hvalid + grind + +@[rocq_alias heap_lang.writer_locked_not_reader_locked] +theorem writerLocked_not_readerLocked (γ : GName) (q : Qp) : + writerLocked γ ∗ readerLocked γ q ⊢@{IProp GF} False := by + unfold writerLocked readerLocked + iintro ⟨H1, H2⟩ + icombine H1 H2 gives %Hvalid + have hq := subset_iff.mp + (included_iff_subset.mp (Auth.both_dfrac_valid_discrete.mp Hvalid).2.1) q + rw [multiplicity_singleton_eq, multiplicity_empty] at hq + omega + +@[rocq_alias heap_lang.is_rw_lock_iff] +theorem isRwLock_iff (γ : GName) (lk : Val) (Φ Ψ : Qp → IProp GF) : + isRwLock γ lk Φ ⊢ (▷ □ ∀ q, Φ q ∗-∗ Ψ q) -∗ isRwLock γ lk Ψ := by + unfold isRwLock rwStateInv + iintro ⟨#HΦdup, %l, %Heq, #Hlockinv⟩ #Hiff + subst Heq + isplitl [] + · inext + iapply internalFractional_iff $$ Hiff HΦdup + iexists l + isplitl [] + · itrivial + iapply inv_iff $$ Hlockinv + inext + imodintro + isplit + · iintro ⟨%z, Hl, (Hneg | ⟨Hge, %q, %g, Hauth, Hsize, Hfold, HΦ⟩)⟩ + · iexists z + iframe Hl Hneg + iexists z + iframe Hl + iright + iframe Hge + iexists q, g + iframe Hauth Hsize Hfold + iapply Hiff $$ HΦ + · iintro ⟨%z, Hl, (Hneg | ⟨Hge, %q, %g, Hauth, Hsize, Hfold, HΨ⟩)⟩ + · iexists z + iframe Hl Hneg + iexists z + iframe Hl + iright + iframe Hge + iexists q, g + iframe Hauth Hsize Hfold + iapply Hiff $$ HΨ + +/-! ## Helper lemmas for "auth of a multiset" -/ + +@[rocq_alias heap_lang.auth_valid_gmultiset_singleton] +theorem auth_valid_singleton {MS : Type _} [LawfulMultiSet MS A] {dq : DFrac} {v : A} {g : MS} + (h : ✓ ((●{dq} valid g : Auth (LeibnizMultiSet MS)) • ◯ valid {v})) : v ∈ g := + singleton_subset_iff.mp (included_iff_subset.mp (Auth.both_dfrac_valid_discrete.mp h).2.1) + +@[rocq_alias heap_lang.own_auth_gmultiset_singleton_2] +theorem own_auth_singleton_2 {γ : GName} {dq : DFrac} {v : Qp} {g : ReaderFracs} : + own (GF := GF) γ (●{dq} valid g) ∗ own γ (◯ valid {v}) ⊢ ⌜v ∈ g⌝ := by + iintro ⟨Hauth, Hfrag⟩ + icombine Hauth Hfrag gives %Hvalid + ipureintro + exact auth_valid_singleton Hvalid + +@[rocq_alias heap_lang.newlock_spec] +theorem newlock_spec (Φ : Qp → IProp GF) {P : IProp GF} {ioΦ ioq} + [hP : AsFractional P ioΦ Φ ioq 1] : + {{ P }} hl(&newlock #()) {{ lk γ, RET lk; isRwLock γ lk Φ }} := by + iintro %φ HP Hφ + wp_rec + imod iOwn_alloc (F := RwSpinLockF) (● valid ∅) (Auth.auth_valid.mpr trivial) with ⟨%γ, Hγ⟩ + wp_alloc l with Hl + imod inv_alloc rwLockN ⊤ (rwStateInv γ l Φ) $$ [Hl Hγ HP] with #Hinv + · unfold rwStateInv + iexists (0 : Int) + iframe Hl + iright + isplitl [] + · ipureintro + omega + iexists 1, (∅ : ReaderFracs) + iframe Hγ + isplitl [] + · ipureintro + exact size_empty + isplitl [] + · ipureintro + exact fold_empty + iapply hP.as_fractional.mp $$ HP + imodintro + iapply Hφ + unfold isRwLock + isplitl [] + · inext + iapply fractional_internalFractional hP.as_fractional_fractional + iexists l + iframe Hinv + itrivial + +@[rocq_alias heap_lang.try_acquire_reader_spec] +theorem tryAcquireReader_spec (γ : GName) (lk : Val) (Φ : Qp → IProp GF) : + {{ isRwLock γ lk Φ }} hl(&tryAcquireReader &lk) + {{ (b : Bool), RET hl_val(#b); + if b then iprop(∃ q, readerLocked γ q ∗ Φ q) else iprop(True) }} := by + unfold isRwLock internalFractional + iintro %φ ⟨#HΦdup, %l, %Heq, #Hlockinv⟩ Hφ + subst Heq + wp_rec + wp_bind !_ + iapply wp_atomic + imod inv_acc $$ Hlockinv with ⟨G1, G2⟩ + · simp + unfold rwStateInv + imodintro + icases G1 with ⟨%z, Hl, Hz⟩ + wp_load + imod G2 $$ [Hl Hz] + · iexists z + iframe Hl Hz + imodintro + wp_pures + by_cases hle : (0 : Int) ≤ z + case neg => + rw [decide_eq_false hle] + wp_pures + iapply Hφ + simp only [Bool.false_eq_true, ↓reduceIte] + itrivial + rw [decide_eq_true hle] + wp_pures + wp_bind cmpXchg(_, _, _) + iapply wp_atomic + imod inv_acc $$ Hlockinv with ⟨G1, G2⟩ + · simp + imodintro + icases G1 with ⟨%z', Hl, Hz⟩ + wp_cmpxchg with hsuc hfail + · obtain rfl : z = z' := by simpa using hsuc.symm + icases Hz with (⟨%Hneg, -⟩ | ⟨-, %q, %g, Hauth, %Hsize, %Hfold, HΦ⟩) + · omega + ihave HΦ : iprop(Φ (q.half + q.half)) $$ [HΦ] + · rw [Qp.half_add_half] + iexact HΦ + icases HΦdup $$ %q.half %q.half HΦ with ⟨HΦ, HΦgive⟩ + have halloc : (● valid g : Auth (LeibnizMultiSet ReaderFracs)) ~~> + (● valid (g ⊎ {q.half})) • ◯ valid ({q.half} : ReaderFracs) := + Auth.auth_update_alloc (localUpdate (Y := ∅) disjUnion_empty_right.symm) + imod iOwn_update halloc $$ Hauth with ⟨Hauth, Hview⟩ + imod G2 $$ [Hl Hauth HΦ] + · iexists (z + 1) + iframe Hl + iright + isplitl [] + · ipureintro + omega + iexists q.half, (g ⊎ {q.half}) + iframe Hauth HΦ + isplitl [] + · ipureintro + rw [size_disjUnion, size_singleton, Hsize] + omega + ipureintro + calc fold Qp.add q.half (g ⊎ {q.half}) + = fold Qp.add (fold Qp.add q.half {q.half}) g := + fold_disjUnion fun x y z => Qp.add_left_comm y x z + _ = fold Qp.add q g := + congrArg (fold Qp.add · g) (fold_singleton.trans (Qp.half_add_half q)) + _ = 1 := Hfold + imodintro + wp_pures + iapply Hφ + simp only [↓reduceIte] + unfold readerLocked + iexists q.half + iframe Hview HΦgive + · imod G2 $$ [Hl Hz] + · iexists z' + iframe Hl Hz + imodintro + wp_pures + iapply Hφ + simp only [Bool.false_eq_true, ↓reduceIte] + itrivial + +@[rocq_alias heap_lang.acquire_reader_spec] +theorem acquireReader_spec (γ : GName) (lk : Val) (Φ : Qp → IProp GF) : + {{ isRwLock γ lk Φ }} hl(&acquireReader &lk) + {{ q, RET hl_val(#()); readerLocked γ q ∗ Φ q }} := by + iintro %φ #Hislock Hφ + iloeb as IH + wp_rec + wp_bind &tryAcquireReader _ + iapply tryAcquireReader_spec $$ Hislock + iintro !> %b Hb + cases b + · wp_pure + iapply IH + inext + iexact Hφ + · wp_pure + imodintro + simp only [↓reduceIte] + icases Hb with ⟨%q, Hlocked, HΦ⟩ + iapply Hφ $$ %q + iframe Hlocked HΦ + +@[rocq_alias heap_lang.release_reader_spec] +theorem releaseReader_spec (γ : GName) (lk : Val) (Φ : Qp → IProp GF) (q : Qp) : + {{ isRwLock γ lk Φ ∗ readerLocked γ q ∗ Φ q }} hl(&releaseReader &lk) + {{ RET hl_val(#()); True }} := by + unfold isRwLock internalFractional readerLocked + iintro %φ ⟨⟨#HΦdup, %l, %Heq, #Hlockinv⟩, Hlocked, HΦ⟩ Hφ + subst Heq + wp_rec + wp_bind faa(_, _) + iapply wp_atomic + imod inv_acc $$ Hlockinv with ⟨G1, G2⟩ + · simp + unfold rwStateInv + imodintro + icases G1 with ⟨%z, Hl, Hz⟩ + wp_faa + icases Hz with (⟨-, Hempty⟩ | ⟨%Hge, %q', %g, Hauth, %Hsize, %Hsum, HΦq'⟩) + · ihave %Hmem : ⌜q ∈ (∅ : ReaderFracs)⌝ $$ [Hempty Hlocked] + · iapply own_auth_singleton_2 + iframe Hempty Hlocked + rw [mem_iff_multiplicity_pos, multiplicity_empty] at Hmem + omega + ihave %Hmem : ⌜q ∈ g⌝ $$ [Hauth Hlocked] + · iapply own_auth_singleton_2 + iframe Hauth Hlocked + have hpos : 0 < z := by + have hne : size g ≠ 0 := fun h => by + rw [size_eq_zero_iff.mp h, mem_iff_multiplicity_pos, multiplicity_empty] at Hmem + omega + omega + have hdealloc : + ((● valid g : Auth (LeibnizMultiSet ReaderFracs)) • ◯ valid ({q} : ReaderFracs)) ~~> + ● valid (g \ {q}) := + Auth.auth_update_dealloc (localUpdate (Y' := ∅) (by + rw [disjUnion_empty_right, disjUnion_comm, ← disjUnion_singleton_difference Hmem])) + imod iOwn_update_op (F := RwSpinLockF) hdealloc $$ [$Hauth $Hlocked] with Hauth + ihave HΦsum : iprop(Φ (q + q')) $$ [HΦ HΦq'] + · iapply HΦdup $$ %q %q' [$HΦ $HΦq'] + imod G2 $$ [Hl Hauth HΦsum] + · iexists (z + -1) + iframe Hl + iright + isplitl [] + · ipureintro + omega + iexists (q + q'), (g \ {q}) + iframe Hauth HΦsum + isplitl [] + · ipureintro + rw [size_difference (singleton_subset_iff.mpr Hmem), size_singleton, Hsize] + omega + ipureintro + calc fold Qp.add (Qp.add q q') (g \ {q}) + = Qp.add q (fold Qp.add q' (g \ {q})) := + fold_comm_acc (g := Qp.add q) fun x y => Qp.add_left_comm x q y + _ = fold Qp.add (fold Qp.add q' (g \ {q})) {q} := fold_singleton.symm + _ = fold Qp.add q' ({q} ⊎ (g \ {q})) := + (fold_disjUnion fun x y z => Qp.add_left_comm y x z).symm + _ = fold Qp.add q' g := + congrArg (fold Qp.add q') (disjUnion_singleton_difference Hmem).symm + _ = 1 := Hsum + imodintro + wp_pures + iapply Hφ + itrivial + +@[rocq_alias heap_lang.try_acquire_writer_spec] +theorem tryAcquireWriter_spec (γ : GName) (lk : Val) (Φ : Qp → IProp GF) : + {{ isRwLock γ lk Φ }} hl(&tryAcquireWriter &lk) + {{ (b : Bool), RET hl_val(#b); + if b then iprop(writerLocked γ ∗ Φ 1) else iprop(True) }} := by + unfold isRwLock + iintro %φ ⟨#HΦdup, %l, %Heq, #Hlockinv⟩ Hφ + subst Heq + wp_rec + wp_bind cmpXchg(_, _, _) + iapply wp_atomic + imod inv_acc $$ Hlockinv with ⟨G1, G2⟩ + · simp + unfold rwStateInv + imodintro + icases G1 with ⟨%z, Hl, Hz⟩ + wp_cmpxchg with hsuc hfail + · obtain rfl : z = 0 := by simpa using hsuc + icases Hz with (⟨%Hneg, -⟩ | ⟨-, %q, %g, Hauth, %Hsize, %Hfold, HΦ⟩) + · omega + obtain rfl : g = ∅ := size_eq_zero_iff.mp (by simpa using Hsize) + rw [fold_empty] at Hfold + subst Hfold + icases (own_auth_empty_split γ).mpr $$ Hauth with ⟨Hauth, Hgive⟩ + imod G2 $$ [Hl Hauth] + · iexists (-1) + iframe Hl + ileft + iframe Hauth + itrivial + imodintro + wp_pures + iapply Hφ + simp only [↓reduceIte] + unfold writerLocked + iframe Hgive HΦ + · imod G2 $$ [Hl Hz] + · iexists z + iframe Hl Hz + imodintro + wp_pures + iapply Hφ + simp only [Bool.false_eq_true, ↓reduceIte] + itrivial + +@[rocq_alias heap_lang.acquire_writer_spec] +theorem acquireWriter_spec (γ : GName) (lk : Val) (Φ : Qp → IProp GF) : + {{ isRwLock γ lk Φ }} hl(&acquireWriter &lk) + {{ RET hl_val(#()); writerLocked γ ∗ Φ 1 }} := by + iintro %φ #Hislock Hφ + iloeb as IH + wp_rec + wp_bind &tryAcquireWriter _ + iapply tryAcquireWriter_spec $$ Hislock + iintro !> %b Hb + cases b + · wp_pure + iapply IH + inext + iexact Hφ + · wp_pure + imodintro + simp only [↓reduceIte] + iapply Hφ + iframe Hb + +@[rocq_alias heap_lang.release_writer_spec] +theorem releaseWriter_spec (γ : GName) (lk : Val) (Φ : Qp → IProp GF) : + {{ isRwLock γ lk Φ ∗ writerLocked γ ∗ Φ 1 }} hl(&releaseWriter &lk) + {{ RET hl_val(#()); True }} := by + unfold isRwLock writerLocked + iintro %φ ⟨⟨#HΦdup, %l, %Heq, #Hlockinv⟩, Hlocked, HΦ⟩ Hφ + subst Heq + wp_rec + iapply wp_atomic + imod inv_acc $$ Hlockinv with ⟨G1, G2⟩ + · simp + unfold rwStateInv + imodintro + icases G1 with ⟨%z, Hl, Hz⟩ + wp_store + icases Hz with (⟨-, Hquarter⟩ | ⟨-, %q, %g, Hauth, -, -, -⟩) + · ihave Hauth : iprop(own γ (● valid (∅ : ReaderFracs))) $$ [Hquarter Hlocked] + · iapply (own_auth_empty_split γ).mp + iframe Hquarter Hlocked + imod G2 $$ [Hl Hauth HΦ] + · iexists (0 : Int) + iframe Hl + iright + isplitl [] + · ipureintro + omega + iexists 1, (∅ : ReaderFracs) + iframe Hauth HΦ + isplitl [] + · ipureintro + exact size_empty + ipureintro + exact fold_empty + imodintro + iapply Hφ + itrivial + · icombine Hauth Hlocked gives %Hvalid + rw [Auth.auth_dfrac_op_valid, DFrac.op_own, DFrac.valid_own] at Hvalid + grind + +end proof + +@[rocq_alias heap_lang.rw_spin_lock, implicit_reducible] +def instRwLock [HeapLangGS hlc GF] : RwLock GF where + newlock := newlock + acquireReader := acquireReader + releaseReader := releaseReader + acquireWriter := acquireWriter + releaseWriter := releaseWriter + rwlockG := RwSpinLockG + name := GName + isRwLock _ γ lk Φ := isRwLock γ lk Φ + readerLocked _ γ q := readerLocked γ q + writerLocked _ γ := writerLocked γ + isRwLock_persistent γ lk Φ := instIsRwLockPersistent γ lk Φ + isRwLock_iff γ lk Φ Ψ := isRwLock_iff γ lk Φ Ψ + readerLocked_timeless γ q := instReaderLockedTimeless γ q + writerLocked_timeless γ := instWriterLockedTimeless γ + writerLocked_exclusive γ := writerLocked_exclusive γ + writerLocked_not_readerLocked γ q := writerLocked_not_readerLocked γ q + newlock_spec {_} Φ {P ioΦ ioq} [AsFractional P ioΦ Φ ioq 1] := + newlock_spec (ioΦ := ioΦ) (ioq := ioq) Φ + acquireReader_spec γ lk Φ := acquireReader_spec γ lk Φ + releaseReader_spec γ lk Φ q := releaseReader_spec γ lk Φ q + acquireWriter_spec γ lk Φ := acquireWriter_spec γ lk Φ + releaseWriter_spec γ lk Φ := releaseWriter_spec γ lk Φ + +end RwSpinLock +end diff --git a/Iris/Iris/Std/GenMultiSets.lean b/Iris/Iris/Std/GenMultiSets.lean index beb8330dd..97747f90b 100644 --- a/Iris/Iris/Std/GenMultiSets.lean +++ b/Iris/Iris/Std/GenMultiSets.lean @@ -93,6 +93,38 @@ theorem mem_inter_iff {x : A} {X Y : MS} : x ∈ (X ∩ Y) ↔ x ∈ X ∧ x ∈ multiplicity_intersection] omega +theorem disjUnion_comm {X Y : MS} : X ⊎ Y = Y ⊎ X := + LawfulMultiSet.ext fun _ => by rw [multiplicity_disjUnion, multiplicity_disjUnion]; omega + +theorem disjUnion_assoc {X Y Z : MS} : (X ⊎ Y) ⊎ Z = X ⊎ (Y ⊎ Z) := + LawfulMultiSet.ext fun _ => by simp only [multiplicity_disjUnion]; omega + +theorem disjUnion_empty_left {X : MS} : (∅ : MS) ⊎ X = X := + LawfulMultiSet.ext fun _ => by rw [multiplicity_disjUnion, multiplicity_empty]; omega + +theorem disjUnion_empty_right {X : MS} : X ⊎ (∅ : MS) = X := + LawfulMultiSet.ext fun _ => by rw [multiplicity_disjUnion, multiplicity_empty]; omega + +theorem disjUnion_subset_left {X Y : MS} : X ⊆ X ⊎ Y := + subset_iff.mpr fun _ => by rw [multiplicity_disjUnion]; omega + +theorem disjUnion_left_inj {X Y Z : MS} (h : X ⊎ Y = X ⊎ Z) : Y = Z := + LawfulMultiSet.ext fun a => by + have := congrArg (MultiSet.multiplicity a) h + rw [multiplicity_disjUnion, multiplicity_disjUnion] at this + omega + +theorem singleton_subset_iff {x : A} {X : MS} : ({x} : MS) ⊆ X ↔ x ∈ X where + mp h := by + have hx := subset_iff.mp h x + rw [multiplicity_singleton_eq] at hx + rw [mem_iff_multiplicity_pos] + omega + mpr h := subset_iff.mpr fun a => by + by_cases hax : a = x + · subst hax; rw [multiplicity_singleton_eq]; exact h + · rw [multiplicity_singleton_ne hax]; omega + theorem disjUnion_difference_of_subseteq {X Y : MS} (h : Y ⊆ X) : X = Y ⊎ (X \ Y) := by refine LawfulMultiSet.ext fun a => ?_ rw [multiplicity_disjUnion, multiplicity_difference] @@ -122,7 +154,7 @@ theorem eq_empty_of_toList_nil {X : MS} (h : toList X = []) : X = ∅ := by rw [← mem_iff_multiplicity_pos, ← mem_toList, h]; simp omega -theorem multiset_ind {motive : MS → Prop} (empty : motive ∅) +@[elab_as_elim] theorem multiset_ind {motive : MS → Prop} (empty : motive ∅) (disjUnion_singleton : ∀ a X, motive X → motive ({a} ⊎ X)) (X : MS) : motive X := by match hl : toList X with | [] => exact eq_empty_of_toList_nil hl ▸ empty @@ -137,4 +169,59 @@ decreasing_by end FiniteLemmas +namespace FiniteMultiSet + +/-- The cardinality (size) of a finite multiset, defined as the length of its list +representation. -/ +def size [FiniteMultiSet MS A] (X : MS) : Nat := + (toList X).length + +/-- Fold over a finite multiset. Unlike `FiniteSet.fold`, the accumulator comes last, so that +`fold` on a commutative monoid reads as a sum. -/ +def fold [FiniteMultiSet MS A] {β : Type _} (f : A → β → β) (b : β) (X : MS) : β := + (toList X).foldr f b + +section Lemmas + +variable {MS : Type _} {A : Type _} [LawfulFiniteMultiSet MS A] + +theorem size_empty : size (∅ : MS) = 0 := by rw [size, toList_empty, List.length_nil] + +theorem size_singleton {a : A} : size ({a} : MS) = 1 := by + rw [size, toList_singleton, List.length_singleton] + +theorem size_disjUnion {X Y : MS} : size (X ⊎ Y) = size X + size Y := by + rw [size, toList_disjUnion.length_eq, List.length_append, size, size] + +theorem size_eq_zero_iff {X : MS} : size X = 0 ↔ X = ∅ where + mp h := eq_empty_of_toList_nil (List.eq_nil_of_length_eq_zero h) + mpr h := h ▸ size_empty + +theorem size_difference {X Y : MS} (h : Y ⊆ X) : size (X \ Y) = size X - size Y := by + rw [congrArg size (disjUnion_difference_of_subseteq h), size_disjUnion] + omega + +variable {β : Type _} {f : A → β → β} {b : β} + +theorem fold_empty : fold f b (∅ : MS) = b := by rw [fold, toList_empty, List.foldr_nil] + +theorem fold_singleton {a : A} : fold f b ({a} : MS) = f a b := by + rw [fold, toList_singleton, List.foldr_cons, List.foldr_nil] + +theorem fold_disjUnion (hf : ∀ x y z, f y (f x z) = f x (f y z)) {X Y : MS} : + fold f b (X ⊎ Y) = fold f (fold f b Y) X := by + simp only [fold] + rw [toList_disjUnion.foldr_eq' (fun x _ y _ => hf x y), List.foldr_append] + +theorem fold_comm_acc {g : β → β} (hg : ∀ x y, f x (g y) = g (f x y)) {X : MS} : + fold f (g b) X = g (fold f b X) := by + rw [fold, fold] + induction toList X with + | nil => rfl + | cons a l ih => rw [List.foldr_cons, List.foldr_cons, ih, hg] + +end Lemmas + +end FiniteMultiSet + end Iris.Std From 2e2bbea68d298f7b5b5e84dac0ebf14296934300 Mon Sep 17 00:00:00 2001 From: Markus de Medeiros Date: Tue, 11 Aug 2026 11:54:19 -0400 Subject: [PATCH 2/8] fix build --- Iris/Iris/HeapLang/Lib/RwSpinLock.lean | 34 +++++++++++++------------- 1 file changed, 17 insertions(+), 17 deletions(-) diff --git a/Iris/Iris/HeapLang/Lib/RwSpinLock.lean b/Iris/Iris/HeapLang/Lib/RwSpinLock.lean index b05cef234..29f50402c 100644 --- a/Iris/Iris/HeapLang/Lib/RwSpinLock.lean +++ b/Iris/Iris/HeapLang/Lib/RwSpinLock.lean @@ -1,7 +1,7 @@ /- Copyright (c) 2026. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: +Authors: Markus de Medeiros -/ module @@ -92,9 +92,9 @@ prove `writerLocked_exclusive`. -/ @[rocq_alias heap_lang.rw_state_inv] def rwStateInv (γ : GName) (l : Loc) (Φ : Qp → IProp GF) : IProp GF := iprop% ∃ z : Int, l ↦ some hl_val(#z) ∗ - (⌜z = -1⌝ ∗ own γ (●{.own Qp.quarter} valid ∅) + (⌜z = -1⌝ ∗ own γ (●{.own Qp.quarter} (.ofSet ∅)) ∨ ⌜0 ≤ z⌝ ∗ ∃ (q : Qp) (g : ReaderFracs), - own γ (● valid g) ∗ + own γ (● .ofSet g) ∗ ⌜size g = z.toNat⌝ ∗ ⌜fold Qp.add q g = 1⌝ ∗ Φ q) @@ -110,10 +110,10 @@ instance instIsRwLockPersistent (γ : GName) (lk : Val) (Φ : Qp → IProp GF) : Persistent (isRwLock γ lk Φ) := by unfold isRwLock; infer_instance @[rocq_alias heap_lang.reader_locked] -def readerLocked (γ : GName) (q : Qp) : IProp GF := own γ (◯ valid {q}) +def readerLocked (γ : GName) (q : Qp) : IProp GF := own γ (◯ .ofSet {q}) @[rocq_alias heap_lang.writer_locked] -def writerLocked (γ : GName) : IProp GF := own γ (●{.own Qp.threeQuarters} valid ∅) +def writerLocked (γ : GName) : IProp GF := own γ (●{.own Qp.threeQuarters} .ofSet ∅) instance instReaderLockedTimeless (γ : GName) (q : Qp) : Timeless (readerLocked (GF := GF) γ q) := by unfold readerLocked; infer_instance @@ -124,10 +124,10 @@ instance instWriterLockedTimeless (γ : GName) : /-- Full authoritative ownership of the empty reader set splits into the quarter kept by `rwStateInv` and the three quarters owned by `writerLocked`. -/ theorem own_auth_empty_split (γ : GName) : - own (GF := GF) γ (●{.own Qp.quarter} valid (∅ : ReaderFracs)) ∗ - own γ (●{.own Qp.threeQuarters} valid ∅) ⊣⊢ own γ (● valid (∅ : ReaderFracs)) := by - have hsplit : (● valid (∅ : ReaderFracs) : Auth (LeibnizMultiSet ReaderFracs)) - = (●{.own Qp.quarter} valid (∅ : ReaderFracs)) • ●{.own Qp.threeQuarters} valid ∅ := by + own (GF := GF) γ (●{.own Qp.quarter} .ofSet (∅ : ReaderFracs)) ∗ + own γ (●{.own Qp.threeQuarters} .ofSet ∅) ⊣⊢ own γ (● .ofSet (∅ : ReaderFracs)) := by + have hsplit : (● .ofSet (∅ : ReaderFracs) : Auth (LeibnizMultiSet ReaderFracs)) + = (●{.own Qp.quarter} LeibnizMultiSet.ofSet (∅ : ReaderFracs)) • ●{.own Qp.threeQuarters} LeibnizMultiSet.ofSet ∅ := by rw [← Auth.auth_dfrac_op, DFrac.op_own, Qp.quarter_add_threeQuarters] rw [hsplit] exact iOwn_op.symm @@ -193,12 +193,12 @@ theorem isRwLock_iff (γ : GName) (lk : Val) (Φ Ψ : Qp → IProp GF) : @[rocq_alias heap_lang.auth_valid_gmultiset_singleton] theorem auth_valid_singleton {MS : Type _} [LawfulMultiSet MS A] {dq : DFrac} {v : A} {g : MS} - (h : ✓ ((●{dq} valid g : Auth (LeibnizMultiSet MS)) • ◯ valid {v})) : v ∈ g := + (h : ✓ ((●{dq} .ofSet g : Auth (LeibnizMultiSet MS)) • ◯ LeibnizMultiSet.ofSet {v})) : v ∈ g := singleton_subset_iff.mp (included_iff_subset.mp (Auth.both_dfrac_valid_discrete.mp h).2.1) @[rocq_alias heap_lang.own_auth_gmultiset_singleton_2] theorem own_auth_singleton_2 {γ : GName} {dq : DFrac} {v : Qp} {g : ReaderFracs} : - own (GF := GF) γ (●{dq} valid g) ∗ own γ (◯ valid {v}) ⊢ ⌜v ∈ g⌝ := by + own (GF := GF) γ (●{dq} .ofSet g) ∗ own γ (◯ .ofSet {v}) ⊢ ⌜v ∈ g⌝ := by iintro ⟨Hauth, Hfrag⟩ icombine Hauth Hfrag gives %Hvalid ipureintro @@ -210,7 +210,7 @@ theorem newlock_spec (Φ : Qp → IProp GF) {P : IProp GF} {ioΦ ioq} {{ P }} hl(&newlock #()) {{ lk γ, RET lk; isRwLock γ lk Φ }} := by iintro %φ HP Hφ wp_rec - imod iOwn_alloc (F := RwSpinLockF) (● valid ∅) (Auth.auth_valid.mpr trivial) with ⟨%γ, Hγ⟩ + imod iOwn_alloc (F := RwSpinLockF) (● .ofSet ∅) (Auth.auth_valid.mpr trivial) with ⟨%γ, Hγ⟩ wp_alloc l with Hl imod inv_alloc rwLockN ⊤ (rwStateInv γ l Φ) $$ [Hl Hγ HP] with #Hinv · unfold rwStateInv @@ -284,8 +284,8 @@ theorem tryAcquireReader_spec (γ : GName) (lk : Val) (Φ : Qp → IProp GF) : · rw [Qp.half_add_half] iexact HΦ icases HΦdup $$ %q.half %q.half HΦ with ⟨HΦ, HΦgive⟩ - have halloc : (● valid g : Auth (LeibnizMultiSet ReaderFracs)) ~~> - (● valid (g ⊎ {q.half})) • ◯ valid ({q.half} : ReaderFracs) := + have halloc : (● .ofSet g : Auth (LeibnizMultiSet ReaderFracs)) ~~> + (● LeibnizMultiSet.ofSet (g ⊎ {q.half})) • ◯ LeibnizMultiSet.ofSet ({q.half} : ReaderFracs) := Auth.auth_update_alloc (localUpdate (Y := ∅) disjUnion_empty_right.symm) imod iOwn_update halloc $$ Hauth with ⟨Hauth, Hview⟩ imod G2 $$ [Hl Hauth HΦ] @@ -377,8 +377,8 @@ theorem releaseReader_spec (γ : GName) (lk : Val) (Φ : Qp → IProp GF) (q : Q omega omega have hdealloc : - ((● valid g : Auth (LeibnizMultiSet ReaderFracs)) • ◯ valid ({q} : ReaderFracs)) ~~> - ● valid (g \ {q}) := + ((● .ofSet g : Auth (LeibnizMultiSet ReaderFracs)) • ◯ LeibnizMultiSet.ofSet ({q} : ReaderFracs)) ~~> + ● .ofSet (g \ {q}) := Auth.auth_update_dealloc (localUpdate (Y' := ∅) (by rw [disjUnion_empty_right, disjUnion_comm, ← disjUnion_singleton_difference Hmem])) imod iOwn_update_op (F := RwSpinLockF) hdealloc $$ [$Hauth $Hlocked] with Hauth @@ -494,7 +494,7 @@ theorem releaseWriter_spec (γ : GName) (lk : Val) (Φ : Qp → IProp GF) : icases G1 with ⟨%z, Hl, Hz⟩ wp_store icases Hz with (⟨-, Hquarter⟩ | ⟨-, %q, %g, Hauth, -, -, -⟩) - · ihave Hauth : iprop(own γ (● valid (∅ : ReaderFracs))) $$ [Hquarter Hlocked] + · ihave Hauth : iprop(own γ (● .ofSet (∅ : ReaderFracs))) $$ [Hquarter Hlocked] · iapply (own_auth_empty_split γ).mp iframe Hquarter Hlocked imod G2 $$ [Hl Hauth HΦ] From 34a006091a127a1f7dc27e797429bfcfd542a235 Mon Sep 17 00:00:00 2001 From: Markus de Medeiros Date: Tue, 11 Aug 2026 13:12:05 -0400 Subject: [PATCH 3/8] auto-cleanup --- Iris/Iris/HeapLang/Lib/RwSpinLock.lean | 417 ++++++++++--------------- 1 file changed, 162 insertions(+), 255 deletions(-) diff --git a/Iris/Iris/HeapLang/Lib/RwSpinLock.lean b/Iris/Iris/HeapLang/Lib/RwSpinLock.lean index 29f50402c..fcaf8489f 100644 --- a/Iris/Iris/HeapLang/Lib/RwSpinLock.lean +++ b/Iris/Iris/HeapLang/Lib/RwSpinLock.lean @@ -59,7 +59,6 @@ def acquireWriter : Val := hl_val( def releaseWriter : Val := hl_val( λ l, l ← #0) -/-- The multiset of fractions that have been handed out to readers. -/ abbrev ReaderFracs := ListPerm Qp abbrev RwSpinLockF : COFE.OFunctorPre := constOF (Auth (LeibnizMultiSet ReaderFracs)) @@ -76,20 +75,18 @@ attribute [reducible, instance] RwSpinLockG.elemG section proof +-- `iinv` exhausts the default recursion budget on the goals below. +set_option maxRecDepth 2000 + variable {GF : BundledGFunctors} [HeapLangGS hlc GF] [RwSpinLockG GF] def rwLockN : Namespace := nroot .@ "rw_lock" -/-- Shorthand for ghost ownership of the reader-set authority. -/ abbrev own (γ : GName) (a : Auth (LeibnizMultiSet ReaderFracs)) : IProp GF := iOwn (F := RwSpinLockF) γ a -/-- We need *some* ghost state that allows us to establish a contradiction in the left disjunct -(where the lock is write-locked) when proving `releaseReader_spec`, so we use a fraction of the -empty authoritative reader set (the rest goes to `writerLocked`). Any fraction would do, but the -benefit of giving over half to `writerLocked` (and keeping less than half here) is that we can -prove `writerLocked_exclusive`. -/ -@[rocq_alias heap_lang.rw_state_inv] +/-- The quarter kept while write-locked contradicts `readerLocked`; `writerLocked` owns the rest. -/ +@[rocq_alias heap_lang.rw_state_inv, reducible] def rwStateInv (γ : GName) (l : Loc) (Φ : Qp → IProp GF) : IProp GF := iprop% ∃ z : Int, l ↦ some hl_val(#z) ∗ (⌜z = -1⌝ ∗ own γ (●{.own Qp.quarter} (.ofSet ∅)) @@ -99,8 +96,7 @@ def rwStateInv (γ : GName) (l : Loc) (Φ : Qp → IProp GF) : IProp GF := iprop ⌜fold Qp.add q g = 1⌝ ∗ Φ q) -/-- The `▷` in front of `internalFractional` is preserved even when taking steps, which makes it -easier to re-establish. -/ +/-- The `▷` before `internalFractional` survives steps, which eases re-establishing it. -/ @[rocq_alias heap_lang.is_rw_lock] def isRwLock (γ : GName) (lk : Val) (Φ : Qp → IProp GF) : IProp GF := iprop% ▷ internalFractional Φ ∗ ∃ l : Loc, ⌜lk = hl_val(#l)⌝ ∗ inv rwLockN (rwStateInv γ l Φ) @@ -121,88 +117,120 @@ instance instReaderLockedTimeless (γ : GName) (q : Qp) : instance instWriterLockedTimeless (γ : GName) : Timeless (writerLocked (GF := GF) γ) := by unfold writerLocked; infer_instance -/-- Full authoritative ownership of the empty reader set splits into the quarter kept by -`rwStateInv` and the three quarters owned by `writerLocked`. -/ +/-! ## Helper lemmas for "auth of a multiset" -/ + +@[rocq_alias heap_lang.auth_valid_gmultiset_singleton] +theorem auth_valid_singleton {MS : Type _} [LawfulMultiSet MS A] {dq : DFrac} {v : A} {g : MS} + (h : ✓ ((●{dq} .ofSet g : Auth (LeibnizMultiSet MS)) • ◯ LeibnizMultiSet.ofSet {v})) : v ∈ g := + singleton_subset_iff.mp (included_iff_subset.mp (Auth.both_dfrac_valid_discrete.mp h).2.1) + +@[rocq_alias heap_lang.own_auth_gmultiset_singleton_2] +theorem own_auth_singleton_2 {γ : GName} {dq : DFrac} {v : Qp} {g : ReaderFracs} : + own (GF := GF) γ (●{dq} .ofSet g) ∗ own γ (◯ .ofSet {v}) ⊢ ⌜v ∈ g⌝ := by + iintro ⟨Hauth, Hfrag⟩ + icombine Hauth Hfrag gives %Hvalid + ipureintro + exact auth_valid_singleton Hvalid + +theorem auth_alloc_singleton {g : ReaderFracs} {v : Qp} : + (● .ofSet g : Auth (LeibnizMultiSet ReaderFracs)) ~~> + (● LeibnizMultiSet.ofSet (g ⊎ {v})) • ◯ LeibnizMultiSet.ofSet {v} := + Auth.auth_update_alloc (localUpdate (Y := ∅) disjUnion_empty_right.symm) + +theorem auth_dealloc_singleton {g : ReaderFracs} {v : Qp} (h : v ∈ g) : + ((● .ofSet g : Auth (LeibnizMultiSet ReaderFracs)) • ◯ LeibnizMultiSet.ofSet {v}) ~~> + ● LeibnizMultiSet.ofSet (g \ {v}) := + Auth.auth_update_dealloc (localUpdate (Y' := ∅) (by + rw [disjUnion_empty_right, disjUnion_comm, ← disjUnion_singleton_difference h])) + theorem own_auth_empty_split (γ : GName) : own (GF := GF) γ (●{.own Qp.quarter} .ofSet (∅ : ReaderFracs)) ∗ own γ (●{.own Qp.threeQuarters} .ofSet ∅) ⊣⊢ own γ (● .ofSet (∅ : ReaderFracs)) := by have hsplit : (● .ofSet (∅ : ReaderFracs) : Auth (LeibnizMultiSet ReaderFracs)) - = (●{.own Qp.quarter} LeibnizMultiSet.ofSet (∅ : ReaderFracs)) • ●{.own Qp.threeQuarters} LeibnizMultiSet.ofSet ∅ := by + = (●{.own Qp.quarter} LeibnizMultiSet.ofSet (∅ : ReaderFracs)) • + ●{.own Qp.threeQuarters} LeibnizMultiSet.ofSet ∅ := by rw [← Auth.auth_dfrac_op, DFrac.op_own, Qp.quarter_add_threeQuarters] rw [hsplit] exact iOwn_op.symm -@[rocq_alias heap_lang.writer_locked_exclusive] -theorem writerLocked_exclusive (γ : GName) : - writerLocked γ ∗ writerLocked γ ⊢@{IProp GF} False := by - unfold writerLocked - iintro ⟨H1, H2⟩ - icombine H1 H2 gives %Hvalid +theorem own_auth_auth_False {γ : GName} {q₁ q₂ : Qp} {g₁ g₂ : ReaderFracs} + (h : ¬ (q₁ + q₂).val ≤ 1) : + own γ (●{.own q₁} .ofSet g₁) ∗ own γ (●{.own q₂} .ofSet g₂) ⊢@{IProp GF} False := by + iintro ⟨H₁, H₂⟩ + icombine H₁ H₂ gives %Hvalid rw [Auth.auth_dfrac_op_valid, DFrac.op_own, DFrac.valid_own] at Hvalid grind +theorem own_auth_empty_frag_False {γ : GName} {dq : DFrac} {v : Qp} : + own γ (●{dq} .ofSet (∅ : ReaderFracs)) ∗ own γ (◯ .ofSet {v}) ⊢@{IProp GF} False := by + iintro H + ihave %Hmem := own_auth_singleton_2 $$ H + simp [mem_iff_multiplicity_pos, multiplicity_empty] at Hmem + +/-! ## Re-establishing the lock invariant -/ + +theorem rwStateInv_readLocked {γ : GName} {l : Loc} {Φ : Qp → IProp GF} {z : Int} {q : Qp} + {g : ReaderFracs} (hz : 0 ≤ z) (hsize : size g = z.toNat) (hfold : fold Qp.add q g = 1) : + l ↦ some hl_val(#z) ∗ own γ (● .ofSet g) ∗ Φ q ⊢ rwStateInv γ l Φ := by + unfold rwStateInv + iintro ⟨Hl, Hauth, HΦ⟩ + iexists z; iframe Hl + iright; iframe %hz + iexists q, g; iframe ∗ % + +theorem rwStateInv_unlocked {γ : GName} {l : Loc} {Φ : Qp → IProp GF} : + l ↦ some hl_val(#(0 : Int)) ∗ own γ (● .ofSet (∅ : ReaderFracs)) ∗ Φ 1 + ⊢ rwStateInv γ l Φ := + rwStateInv_readLocked (by omega) (by rw [size_empty]; rfl) fold_empty + +theorem rwStateInv_writeLocked {γ : GName} {l : Loc} {Φ : Qp → IProp GF} : + l ↦ some hl_val(#(-1 : Int)) ∗ own γ (●{.own Qp.quarter} .ofSet (∅ : ReaderFracs)) + ⊢ rwStateInv γ l Φ := by + unfold rwStateInv + iintro ⟨Hl, Hauth⟩ + iexists (-1); iframe Hl + ileft; iframe Hauth; itrivial + +theorem rwStateInv_mono {γ : GName} {l : Loc} (Φ Ψ : Qp → IProp GF) : + (∀ q, Φ q -∗ Ψ q) ⊢ rwStateInv γ l Φ -∗ rwStateInv γ l Ψ := by + unfold rwStateInv + iintro Hmono ⟨%z, Hl, (Hneg | ⟨Hge, %q, %g, Hauth, Hsize, Hfold, HΦ⟩)⟩ + · iexists z; iframe Hl Hneg + iexists z; iframe Hl + iright; iframe Hge + iexists q, g; iframe Hauth Hsize Hfold + iapply Hmono $$ HΦ + +@[rocq_alias heap_lang.writer_locked_exclusive] +theorem writerLocked_exclusive (γ : GName) : + writerLocked γ ∗ writerLocked γ ⊢@{IProp GF} False := + own_auth_auth_False (by grind) + @[rocq_alias heap_lang.writer_locked_not_reader_locked] theorem writerLocked_not_readerLocked (γ : GName) (q : Qp) : - writerLocked γ ∗ readerLocked γ q ⊢@{IProp GF} False := by - unfold writerLocked readerLocked - iintro ⟨H1, H2⟩ - icombine H1 H2 gives %Hvalid - have hq := subset_iff.mp - (included_iff_subset.mp (Auth.both_dfrac_valid_discrete.mp Hvalid).2.1) q - rw [multiplicity_singleton_eq, multiplicity_empty] at hq - omega + writerLocked γ ∗ readerLocked γ q ⊢@{IProp GF} False := + own_auth_empty_frag_False @[rocq_alias heap_lang.is_rw_lock_iff] theorem isRwLock_iff (γ : GName) (lk : Val) (Φ Ψ : Qp → IProp GF) : isRwLock γ lk Φ ⊢ (▷ □ ∀ q, Φ q ∗-∗ Ψ q) -∗ isRwLock γ lk Ψ := by - unfold isRwLock rwStateInv + unfold isRwLock iintro ⟨#HΦdup, %l, %Heq, #Hlockinv⟩ #Hiff subst Heq isplitl [] - · inext - iapply internalFractional_iff $$ Hiff HΦdup + · inext; iapply internalFractional_iff $$ Hiff HΦdup iexists l - isplitl [] - · itrivial + isplitl []; itrivial iapply inv_iff $$ Hlockinv inext imodintro isplit - · iintro ⟨%z, Hl, (Hneg | ⟨Hge, %q, %g, Hauth, Hsize, Hfold, HΦ⟩)⟩ - · iexists z - iframe Hl Hneg - iexists z - iframe Hl - iright - iframe Hge - iexists q, g - iframe Hauth Hsize Hfold - iapply Hiff $$ HΦ - · iintro ⟨%z, Hl, (Hneg | ⟨Hge, %q, %g, Hauth, Hsize, Hfold, HΨ⟩)⟩ - · iexists z - iframe Hl Hneg - iexists z - iframe Hl - iright - iframe Hge - iexists q, g - iframe Hauth Hsize Hfold - iapply Hiff $$ HΨ - -/-! ## Helper lemmas for "auth of a multiset" -/ - -@[rocq_alias heap_lang.auth_valid_gmultiset_singleton] -theorem auth_valid_singleton {MS : Type _} [LawfulMultiSet MS A] {dq : DFrac} {v : A} {g : MS} - (h : ✓ ((●{dq} .ofSet g : Auth (LeibnizMultiSet MS)) • ◯ LeibnizMultiSet.ofSet {v})) : v ∈ g := - singleton_subset_iff.mp (included_iff_subset.mp (Auth.both_dfrac_valid_discrete.mp h).2.1) - -@[rocq_alias heap_lang.own_auth_gmultiset_singleton_2] -theorem own_auth_singleton_2 {γ : GName} {dq : DFrac} {v : Qp} {g : ReaderFracs} : - own (GF := GF) γ (●{dq} .ofSet g) ∗ own γ (◯ .ofSet {v}) ⊢ ⌜v ∈ g⌝ := by - iintro ⟨Hauth, Hfrag⟩ - icombine Hauth Hfrag gives %Hvalid - ipureintro - exact auth_valid_singleton Hvalid + · iintro Hinv + iapply rwStateInv_mono $$ [] Hinv + iintro %q HΦ; iapply Hiff $$ HΦ + · iintro Hinv + iapply rwStateInv_mono $$ [] Hinv + iintro %q HΨ; iapply Hiff $$ HΨ @[rocq_alias heap_lang.newlock_spec] theorem newlock_spec (Φ : Qp → IProp GF) {P : IProp GF} {ioΦ ioq} @@ -213,116 +241,66 @@ theorem newlock_spec (Φ : Qp → IProp GF) {P : IProp GF} {ioΦ ioq} imod iOwn_alloc (F := RwSpinLockF) (● .ofSet ∅) (Auth.auth_valid.mpr trivial) with ⟨%γ, Hγ⟩ wp_alloc l with Hl imod inv_alloc rwLockN ⊤ (rwStateInv γ l Φ) $$ [Hl Hγ HP] with #Hinv - · unfold rwStateInv - iexists (0 : Int) - iframe Hl - iright - isplitl [] - · ipureintro - omega - iexists 1, (∅ : ReaderFracs) - iframe Hγ - isplitl [] - · ipureintro - exact size_empty - isplitl [] - · ipureintro - exact fold_empty + · iapply rwStateInv_unlocked + iframe Hl Hγ iapply hP.as_fractional.mp $$ HP imodintro iapply Hφ unfold isRwLock isplitl [] - · inext - iapply fractional_internalFractional hP.as_fractional_fractional - iexists l - iframe Hinv - itrivial + · inext; iapply fractional_internalFractional hP.as_fractional_fractional + iexists l; iframe Hinv; itrivial @[rocq_alias heap_lang.try_acquire_reader_spec] theorem tryAcquireReader_spec (γ : GName) (lk : Val) (Φ : Qp → IProp GF) : {{ isRwLock γ lk Φ }} hl(&tryAcquireReader &lk) {{ (b : Bool), RET hl_val(#b); if b then iprop(∃ q, readerLocked γ q ∗ Φ q) else iprop(True) }} := by - unfold isRwLock internalFractional + unfold isRwLock internalFractional readerLocked rwStateInv iintro %φ ⟨#HΦdup, %l, %Heq, #Hlockinv⟩ Hφ subst Heq wp_rec wp_bind !_ - iapply wp_atomic - imod inv_acc $$ Hlockinv with ⟨G1, G2⟩ - · simp - unfold rwStateInv - imodintro - icases G1 with ⟨%z, Hl, Hz⟩ + iinv Hlockinv with ⟨%z, Hl, Hz⟩ Hclose + · simp; infer_instance wp_load - imod G2 $$ [Hl Hz] - · iexists z - iframe Hl Hz + imod Hclose $$ [$Hl $Hz] with - imodintro wp_pures by_cases hle : (0 : Int) ≤ z case neg => rw [decide_eq_false hle] wp_pures - iapply Hφ - simp only [Bool.false_eq_true, ↓reduceIte] - itrivial + iapply Hφ; simp only [Bool.false_eq_true, ↓reduceIte]; itrivial rw [decide_eq_true hle] wp_pures wp_bind cmpXchg(_, _, _) - iapply wp_atomic - imod inv_acc $$ Hlockinv with ⟨G1, G2⟩ - · simp - imodintro - icases G1 with ⟨%z', Hl, Hz⟩ + iinv Hlockinv with ⟨%z', Hl, Hz⟩ Hclose + · simp; infer_instance wp_cmpxchg with hsuc hfail · obtain rfl : z = z' := by simpa using hsuc.symm icases Hz with (⟨%Hneg, -⟩ | ⟨-, %q, %g, Hauth, %Hsize, %Hfold, HΦ⟩) · omega - ihave HΦ : iprop(Φ (q.half + q.half)) $$ [HΦ] - · rw [Qp.half_add_half] - iexact HΦ - icases HΦdup $$ %q.half %q.half HΦ with ⟨HΦ, HΦgive⟩ - have halloc : (● .ofSet g : Auth (LeibnizMultiSet ReaderFracs)) ~~> - (● LeibnizMultiSet.ofSet (g ⊎ {q.half})) • ◯ LeibnizMultiSet.ofSet ({q.half} : ReaderFracs) := - Auth.auth_update_alloc (localUpdate (Y := ∅) disjUnion_empty_right.symm) - imod iOwn_update halloc $$ Hauth with ⟨Hauth, Hview⟩ - imod G2 $$ [Hl Hauth HΦ] - · iexists (z + 1) - iframe Hl - iright - isplitl [] - · ipureintro - omega - iexists q.half, (g ⊎ {q.half}) - iframe Hauth HΦ - isplitl [] - · ipureintro - rw [size_disjUnion, size_singleton, Hsize] - omega - ipureintro - calc fold Qp.add q.half (g ⊎ {q.half}) - = fold Qp.add (fold Qp.add q.half {q.half}) g := - fold_disjUnion fun x y z => Qp.add_left_comm y x z - _ = fold Qp.add q g := - congrArg (fold Qp.add · g) (fold_singleton.trans (Qp.half_add_half q)) - _ = 1 := Hfold + ihave ⟨HΦ, HΦgive⟩ : iprop(Φ q.half ∗ Φ q.half) $$ [HΦ] + · iapply HΦdup $$ %q.half %q.half + rw [Qp.half_add_half]; iexact HΦ + imod iOwn_update (auth_alloc_singleton (v := q.half)) $$ Hauth with ⟨Hauth, Hview⟩ + have hsize : size (g ⊎ {q.half}) = (z + 1).toNat := by + rw [size_disjUnion, size_singleton, Hsize]; omega + have hfold : fold Qp.add q.half (g ⊎ {q.half}) = 1 := by + rw [fold_disjUnion (f := Qp.add) fun x y z => Qp.add_left_comm y x z, fold_singleton, + show Qp.add q.half q.half = q from Qp.half_add_half q] + exact Hfold + imod Hclose $$ [Hl Hauth HΦ] with - + · iapply rwStateInv_readLocked (by omega) hsize hfold; iframe imodintro wp_pures - iapply Hφ - simp only [↓reduceIte] - unfold readerLocked - iexists q.half - iframe Hview HΦgive - · imod G2 $$ [Hl Hz] - · iexists z' - iframe Hl Hz + iapply Hφ; simp only [↓reduceIte] + iexists q.half; iframe Hview HΦgive + · imod Hclose $$ [$Hl $Hz] with - imodintro wp_pures - iapply Hφ - simp only [Bool.false_eq_true, ↓reduceIte] - itrivial + iapply Hφ; simp only [Bool.false_eq_true, ↓reduceIte]; itrivial @[rocq_alias heap_lang.acquire_reader_spec] theorem acquireReader_spec (γ : GName) (lk : Val) (Φ : Qp → IProp GF) : @@ -335,99 +313,64 @@ theorem acquireReader_spec (γ : GName) (lk : Val) (Φ : Qp → IProp GF) : iapply tryAcquireReader_spec $$ Hislock iintro !> %b Hb cases b - · wp_pure - iapply IH - inext - iexact Hφ - · wp_pure - imodintro - simp only [↓reduceIte] + · wp_pure; iapply IH; inext; iexact Hφ + · wp_pure; imodintro; simp only [↓reduceIte] icases Hb with ⟨%q, Hlocked, HΦ⟩ - iapply Hφ $$ %q - iframe Hlocked HΦ + iapply Hφ $$ %q; iframe Hlocked HΦ @[rocq_alias heap_lang.release_reader_spec] theorem releaseReader_spec (γ : GName) (lk : Val) (Φ : Qp → IProp GF) (q : Qp) : {{ isRwLock γ lk Φ ∗ readerLocked γ q ∗ Φ q }} hl(&releaseReader &lk) {{ RET hl_val(#()); True }} := by - unfold isRwLock internalFractional readerLocked + unfold isRwLock internalFractional readerLocked rwStateInv iintro %φ ⟨⟨#HΦdup, %l, %Heq, #Hlockinv⟩, Hlocked, HΦ⟩ Hφ subst Heq wp_rec wp_bind faa(_, _) - iapply wp_atomic - imod inv_acc $$ Hlockinv with ⟨G1, G2⟩ - · simp - unfold rwStateInv - imodintro - icases G1 with ⟨%z, Hl, Hz⟩ + iinv Hlockinv with ⟨%z, Hl, Hz⟩ Hclose + · simp; infer_instance wp_faa icases Hz with (⟨-, Hempty⟩ | ⟨%Hge, %q', %g, Hauth, %Hsize, %Hsum, HΦq'⟩) - · ihave %Hmem : ⌜q ∈ (∅ : ReaderFracs)⌝ $$ [Hempty Hlocked] - · iapply own_auth_singleton_2 - iframe Hempty Hlocked - rw [mem_iff_multiplicity_pos, multiplicity_empty] at Hmem - omega - ihave %Hmem : ⌜q ∈ g⌝ $$ [Hauth Hlocked] - · iapply own_auth_singleton_2 - iframe Hauth Hlocked - have hpos : 0 < z := by - have hne : size g ≠ 0 := fun h => by - rw [size_eq_zero_iff.mp h, mem_iff_multiplicity_pos, multiplicity_empty] at Hmem - omega - omega - have hdealloc : - ((● .ofSet g : Auth (LeibnizMultiSet ReaderFracs)) • ◯ LeibnizMultiSet.ofSet ({q} : ReaderFracs)) ~~> - ● .ofSet (g \ {q}) := - Auth.auth_update_dealloc (localUpdate (Y' := ∅) (by - rw [disjUnion_empty_right, disjUnion_comm, ← disjUnion_singleton_difference Hmem])) - imod iOwn_update_op (F := RwSpinLockF) hdealloc $$ [$Hauth $Hlocked] with Hauth + · iexfalso; iapply own_auth_empty_frag_False $$ [$Hempty $Hlocked] + ihave %Hmem := own_auth_singleton_2 $$ [$Hauth $Hlocked] + imod iOwn_update_op (F := RwSpinLockF) (auth_dealloc_singleton Hmem) + $$ [$Hauth $Hlocked] with Hauth ihave HΦsum : iprop(Φ (q + q')) $$ [HΦ HΦq'] · iapply HΦdup $$ %q %q' [$HΦ $HΦq'] - imod G2 $$ [Hl Hauth HΦsum] - · iexists (z + -1) - iframe Hl - iright - isplitl [] - · ipureintro - omega - iexists (q + q'), (g \ {q}) - iframe Hauth HΦsum - isplitl [] - · ipureintro - rw [size_difference (singleton_subset_iff.mpr Hmem), size_singleton, Hsize] - omega - ipureintro + have hpos : 0 < z := by + have : size g ≠ 0 := fun h => by + simp [size_eq_zero_iff.mp h, mem_iff_multiplicity_pos, multiplicity_empty] at Hmem + omega + have hsize : size (g \ {q}) = (z + -1).toNat := by + rw [size_difference (singleton_subset_iff.mpr Hmem), size_singleton, Hsize]; omega + have hfold : fold Qp.add (q + q') (g \ {q}) = 1 := calc fold Qp.add (Qp.add q q') (g \ {q}) = Qp.add q (fold Qp.add q' (g \ {q})) := fold_comm_acc (g := Qp.add q) fun x y => Qp.add_left_comm x q y _ = fold Qp.add (fold Qp.add q' (g \ {q})) {q} := fold_singleton.symm _ = fold Qp.add q' ({q} ⊎ (g \ {q})) := - (fold_disjUnion fun x y z => Qp.add_left_comm y x z).symm + (fold_disjUnion (f := Qp.add) fun x y z => Qp.add_left_comm y x z).symm _ = fold Qp.add q' g := congrArg (fold Qp.add q') (disjUnion_singleton_difference Hmem).symm _ = 1 := Hsum + imod Hclose $$ [Hl Hauth HΦsum] with - + · iapply rwStateInv_readLocked (by omega) hsize hfold; iframe imodintro wp_pures - iapply Hφ - itrivial + iapply Hφ; itrivial @[rocq_alias heap_lang.try_acquire_writer_spec] theorem tryAcquireWriter_spec (γ : GName) (lk : Val) (Φ : Qp → IProp GF) : {{ isRwLock γ lk Φ }} hl(&tryAcquireWriter &lk) {{ (b : Bool), RET hl_val(#b); if b then iprop(writerLocked γ ∗ Φ 1) else iprop(True) }} := by - unfold isRwLock + unfold isRwLock writerLocked rwStateInv iintro %φ ⟨#HΦdup, %l, %Heq, #Hlockinv⟩ Hφ subst Heq wp_rec wp_bind cmpXchg(_, _, _) - iapply wp_atomic - imod inv_acc $$ Hlockinv with ⟨G1, G2⟩ - · simp - unfold rwStateInv - imodintro - icases G1 with ⟨%z, Hl, Hz⟩ + iinv Hlockinv with ⟨%z, Hl, Hz⟩ Hclose + · simp; infer_instance wp_cmpxchg with hsuc hfail · obtain rfl : z = 0 := by simpa using hsuc icases Hz with (⟨%Hneg, -⟩ | ⟨-, %q, %g, Hauth, %Hsize, %Hfold, HΦ⟩) @@ -436,26 +379,16 @@ theorem tryAcquireWriter_spec (γ : GName) (lk : Val) (Φ : Qp → IProp GF) : rw [fold_empty] at Hfold subst Hfold icases (own_auth_empty_split γ).mpr $$ Hauth with ⟨Hauth, Hgive⟩ - imod G2 $$ [Hl Hauth] - · iexists (-1) - iframe Hl - ileft - iframe Hauth - itrivial + imod Hclose $$ [Hl Hauth] with - + · iapply rwStateInv_writeLocked; iframe imodintro wp_pures - iapply Hφ - simp only [↓reduceIte] - unfold writerLocked + iapply Hφ; simp only [↓reduceIte] iframe Hgive HΦ - · imod G2 $$ [Hl Hz] - · iexists z - iframe Hl Hz + · imod Hclose $$ [$Hl $Hz] with - imodintro wp_pures - iapply Hφ - simp only [Bool.false_eq_true, ↓reduceIte] - itrivial + iapply Hφ; simp only [Bool.false_eq_true, ↓reduceIte]; itrivial @[rocq_alias heap_lang.acquire_writer_spec] theorem acquireWriter_spec (γ : GName) (lk : Val) (Φ : Qp → IProp GF) : @@ -468,55 +401,29 @@ theorem acquireWriter_spec (γ : GName) (lk : Val) (Φ : Qp → IProp GF) : iapply tryAcquireWriter_spec $$ Hislock iintro !> %b Hb cases b - · wp_pure - iapply IH - inext - iexact Hφ - · wp_pure - imodintro - simp only [↓reduceIte] - iapply Hφ - iframe Hb + · wp_pure; iapply IH; inext; iexact Hφ + · wp_pure; imodintro; simp only [↓reduceIte] + iapply Hφ; iframe Hb @[rocq_alias heap_lang.release_writer_spec] theorem releaseWriter_spec (γ : GName) (lk : Val) (Φ : Qp → IProp GF) : {{ isRwLock γ lk Φ ∗ writerLocked γ ∗ Φ 1 }} hl(&releaseWriter &lk) {{ RET hl_val(#()); True }} := by - unfold isRwLock writerLocked + unfold isRwLock writerLocked rwStateInv iintro %φ ⟨⟨#HΦdup, %l, %Heq, #Hlockinv⟩, Hlocked, HΦ⟩ Hφ subst Heq wp_rec - iapply wp_atomic - imod inv_acc $$ Hlockinv with ⟨G1, G2⟩ - · simp - unfold rwStateInv - imodintro - icases G1 with ⟨%z, Hl, Hz⟩ + iinv Hlockinv with ⟨%z, Hl, Hz⟩ Hclose + · simp; infer_instance wp_store icases Hz with (⟨-, Hquarter⟩ | ⟨-, %q, %g, Hauth, -, -, -⟩) · ihave Hauth : iprop(own γ (● .ofSet (∅ : ReaderFracs))) $$ [Hquarter Hlocked] - · iapply (own_auth_empty_split γ).mp - iframe Hquarter Hlocked - imod G2 $$ [Hl Hauth HΦ] - · iexists (0 : Int) - iframe Hl - iright - isplitl [] - · ipureintro - omega - iexists 1, (∅ : ReaderFracs) - iframe Hauth HΦ - isplitl [] - · ipureintro - exact size_empty - ipureintro - exact fold_empty + · iapply (own_auth_empty_split γ).mp; iframe Hquarter Hlocked + imod Hclose $$ [Hl Hauth HΦ] with - + · iapply rwStateInv_unlocked; iframe imodintro - iapply Hφ - itrivial - · icombine Hauth Hlocked gives %Hvalid - rw [Auth.auth_dfrac_op_valid, DFrac.op_own, DFrac.valid_own] at Hvalid - grind + iapply Hφ; itrivial + · iexfalso; iapply own_auth_auth_False (q₁ := 1) (by grind) $$ [$Hauth $Hlocked] end proof From c02342049ee1effc8edff03321dd27c6484eb4d1 Mon Sep 17 00:00:00 2001 From: Markus de Medeiros Date: Tue, 11 Aug 2026 13:27:23 -0400 Subject: [PATCH 4/8] more --- Iris/Iris/HeapLang/Lib/RwSpinLock.lean | 15 ++++++++------- Iris/Iris/Std/GenMultiSets.lean | 4 ++++ 2 files changed, 12 insertions(+), 7 deletions(-) diff --git a/Iris/Iris/HeapLang/Lib/RwSpinLock.lean b/Iris/Iris/HeapLang/Lib/RwSpinLock.lean index fcaf8489f..237912fcb 100644 --- a/Iris/Iris/HeapLang/Lib/RwSpinLock.lean +++ b/Iris/Iris/HeapLang/Lib/RwSpinLock.lean @@ -135,13 +135,15 @@ theorem own_auth_singleton_2 {γ : GName} {dq : DFrac} {v : Qp} {g : ReaderFracs theorem auth_alloc_singleton {g : ReaderFracs} {v : Qp} : (● .ofSet g : Auth (LeibnizMultiSet ReaderFracs)) ~~> (● LeibnizMultiSet.ofSet (g ⊎ {v})) • ◯ LeibnizMultiSet.ofSet {v} := - Auth.auth_update_alloc (localUpdate (Y := ∅) disjUnion_empty_right.symm) + Auth.auth_update_alloc (localUpdate_alloc (X := g) (Y := ∅) (X' := {v})) -theorem auth_dealloc_singleton {g : ReaderFracs} {v : Qp} (h : v ∈ g) : +theorem auth_dealloc_singleton {g : ReaderFracs} {v : Qp} : ((● .ofSet g : Auth (LeibnizMultiSet ReaderFracs)) • ◯ LeibnizMultiSet.ofSet {v}) ~~> - ● LeibnizMultiSet.ofSet (g \ {v}) := - Auth.auth_update_dealloc (localUpdate (Y' := ∅) (by - rw [disjUnion_empty_right, disjUnion_comm, ← disjUnion_singleton_difference h])) + ● LeibnizMultiSet.ofSet (g \ {v}) := by + refine Auth.auth_update_dealloc ?_ + have h := localUpdate_dealloc (X := g) (Y := ({v} : ReaderFracs)) (X' := {v}) + (subset_iff.mpr fun _ => Nat.le_refl _) + rwa [difference_self] at h theorem own_auth_empty_split (γ : GName) : own (GF := GF) γ (●{.own Qp.quarter} .ofSet (∅ : ReaderFracs)) ∗ @@ -333,8 +335,7 @@ theorem releaseReader_spec (γ : GName) (lk : Val) (Φ : Qp → IProp GF) (q : Q icases Hz with (⟨-, Hempty⟩ | ⟨%Hge, %q', %g, Hauth, %Hsize, %Hsum, HΦq'⟩) · iexfalso; iapply own_auth_empty_frag_False $$ [$Hempty $Hlocked] ihave %Hmem := own_auth_singleton_2 $$ [$Hauth $Hlocked] - imod iOwn_update_op (F := RwSpinLockF) (auth_dealloc_singleton Hmem) - $$ [$Hauth $Hlocked] with Hauth + imod iOwn_update_op (F := RwSpinLockF) auth_dealloc_singleton $$ [$Hauth $Hlocked] with Hauth ihave HΦsum : iprop(Φ (q + q')) $$ [HΦ HΦq'] · iapply HΦdup $$ %q %q' [$HΦ $HΦq'] have hpos : 0 < z := by diff --git a/Iris/Iris/Std/GenMultiSets.lean b/Iris/Iris/Std/GenMultiSets.lean index ce4f7a616..b420a95a7 100644 --- a/Iris/Iris/Std/GenMultiSets.lean +++ b/Iris/Iris/Std/GenMultiSets.lean @@ -136,6 +136,10 @@ theorem singleton_subset_iff {x : A} {X : MS} : ({x} : MS) ⊆ X ↔ x ∈ X whe · subst hax; rw [multiplicity_singleton_eq]; exact h · rw [multiplicity_singleton_ne hax]; omega +@[grind =] +theorem difference_self {X : MS} : X \ X = (∅ : MS) := + LawfulMultiSet.ext fun _ => by rw [multiplicity_difference, multiplicity_empty]; omega + theorem disjUnion_difference_of_subseteq {X Y : MS} (h : Y ⊆ X) : X = Y ⊎ (X \ Y) := by refine LawfulMultiSet.ext fun a => ?_ grind [subset_iff.mp h a, multiplicity_disjUnion, multiplicity_difference] From db85865e75cfe8c708961ed08fa1d4f6de3d31af Mon Sep 17 00:00:00 2001 From: Markus de Medeiros Date: Tue, 11 Aug 2026 13:53:40 -0400 Subject: [PATCH 5/8] move around --- Iris/Iris/Algebra/Lib.lean | 1 + Iris/Iris/Algebra/Lib/MultiSetAuth.lean | 46 +++++++++++++++++++++++++ Iris/Iris/HeapLang/Lib/RwSpinLock.lean | 27 +++------------ Iris/Iris/Std/GenMultiSets.lean | 7 ++++ 4 files changed, 58 insertions(+), 23 deletions(-) create mode 100644 Iris/Iris/Algebra/Lib/MultiSetAuth.lean diff --git a/Iris/Iris/Algebra/Lib.lean b/Iris/Iris/Algebra/Lib.lean index 30d76e7d6..07ef378f2 100644 --- a/Iris/Iris/Algebra/Lib.lean +++ b/Iris/Iris/Algebra/Lib.lean @@ -4,4 +4,5 @@ public import Iris.Algebra.Lib.DFracAgree public import Iris.Algebra.Lib.ExclAuth public import Iris.Algebra.Lib.FracAuth public import Iris.Algebra.Lib.MonoNat +public import Iris.Algebra.Lib.MultiSetAuth public import Iris.Algebra.Lib.UFracAuth diff --git a/Iris/Iris/Algebra/Lib/MultiSetAuth.lean b/Iris/Iris/Algebra/Lib/MultiSetAuth.lean new file mode 100644 index 000000000..9ca6b28bb --- /dev/null +++ b/Iris/Iris/Algebra/Lib/MultiSetAuth.lean @@ -0,0 +1,46 @@ +/- +Copyright (c) 2026. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Markus de Medeiros +-/ +module + +public import Iris.Algebra.Auth +public import Iris.Algebra.LeibnizMultiSet +meta import Iris.Std.RocqPorting + +@[expose] public section + +/-! +# Authoritative multisets + +The authority owns a multiset and each fragment owns some of its elements: adding an element to +the authority hands out the matching singleton fragment, and returning it removes the element. +-/ + +open Iris Std CMRA + +namespace LeibnizMultiSet + +variable {MS : Type _} [LawfulMultiSet MS A] + +@[rocq_alias heap_lang.auth_valid_gmultiset_singleton] +theorem auth_valid_singleton {dq : DFrac} {v : A} {g : MS} + (h : ✓ ((●{dq} .ofSet g : Auth (LeibnizMultiSet MS)) • ◯ LeibnizMultiSet.ofSet {v})) : v ∈ g := + singleton_subset_iff.mp (included_iff_subset.mp (Auth.both_dfrac_valid_discrete.mp h).2.1) + +theorem auth_alloc_singleton {v : A} {g : MS} : + (● .ofSet g : Auth (LeibnizMultiSet MS)) ~~> + (● LeibnizMultiSet.ofSet (g ⊎ {v})) • ◯ LeibnizMultiSet.ofSet {v} := by + refine Auth.auth_update_alloc ?_ + have h := localUpdate_alloc (X := g) (Y := (∅ : MS)) (X' := {v}) + rwa [disjUnion_empty_left] at h + +theorem auth_dealloc_singleton {v : A} {g : MS} : + ((● .ofSet g : Auth (LeibnizMultiSet MS)) • ◯ LeibnizMultiSet.ofSet {v}) ~~> + ● LeibnizMultiSet.ofSet (g \ {v}) := by + refine Auth.auth_update_dealloc ?_ + have h := localUpdate_dealloc (X := g) (Y := ({v} : MS)) (X' := {v}) subset_refl + rwa [difference_self] at h + +end LeibnizMultiSet diff --git a/Iris/Iris/HeapLang/Lib/RwSpinLock.lean b/Iris/Iris/HeapLang/Lib/RwSpinLock.lean index 237912fcb..6bc0d1a2a 100644 --- a/Iris/Iris/HeapLang/Lib/RwSpinLock.lean +++ b/Iris/Iris/HeapLang/Lib/RwSpinLock.lean @@ -5,7 +5,7 @@ Authors: Markus de Medeiros -/ module -public import Iris.Algebra.LeibnizMultiSet +public import Iris.Algebra.Lib.MultiSetAuth public import Iris.HeapLang.Lib.RwLock public import Iris.HeapLang.PrimitiveLaws public import Iris.HeapLang.ProofMode @@ -117,12 +117,7 @@ instance instReaderLockedTimeless (γ : GName) (q : Qp) : instance instWriterLockedTimeless (γ : GName) : Timeless (writerLocked (GF := GF) γ) := by unfold writerLocked; infer_instance -/-! ## Helper lemmas for "auth of a multiset" -/ - -@[rocq_alias heap_lang.auth_valid_gmultiset_singleton] -theorem auth_valid_singleton {MS : Type _} [LawfulMultiSet MS A] {dq : DFrac} {v : A} {g : MS} - (h : ✓ ((●{dq} .ofSet g : Auth (LeibnizMultiSet MS)) • ◯ LeibnizMultiSet.ofSet {v})) : v ∈ g := - singleton_subset_iff.mp (included_iff_subset.mp (Auth.both_dfrac_valid_discrete.mp h).2.1) +/-! ## Ghost-state lemmas for the reader set -/ @[rocq_alias heap_lang.own_auth_gmultiset_singleton_2] theorem own_auth_singleton_2 {γ : GName} {dq : DFrac} {v : Qp} {g : ReaderFracs} : @@ -132,19 +127,6 @@ theorem own_auth_singleton_2 {γ : GName} {dq : DFrac} {v : Qp} {g : ReaderFracs ipureintro exact auth_valid_singleton Hvalid -theorem auth_alloc_singleton {g : ReaderFracs} {v : Qp} : - (● .ofSet g : Auth (LeibnizMultiSet ReaderFracs)) ~~> - (● LeibnizMultiSet.ofSet (g ⊎ {v})) • ◯ LeibnizMultiSet.ofSet {v} := - Auth.auth_update_alloc (localUpdate_alloc (X := g) (Y := ∅) (X' := {v})) - -theorem auth_dealloc_singleton {g : ReaderFracs} {v : Qp} : - ((● .ofSet g : Auth (LeibnizMultiSet ReaderFracs)) • ◯ LeibnizMultiSet.ofSet {v}) ~~> - ● LeibnizMultiSet.ofSet (g \ {v}) := by - refine Auth.auth_update_dealloc ?_ - have h := localUpdate_dealloc (X := g) (Y := ({v} : ReaderFracs)) (X' := {v}) - (subset_iff.mpr fun _ => Nat.le_refl _) - rwa [difference_self] at h - theorem own_auth_empty_split (γ : GName) : own (GF := GF) γ (●{.own Qp.quarter} .ofSet (∅ : ReaderFracs)) ∗ own γ (●{.own Qp.threeQuarters} .ofSet ∅) ⊣⊢ own γ (● .ofSet (∅ : ReaderFracs)) := by @@ -167,7 +149,7 @@ theorem own_auth_empty_frag_False {γ : GName} {dq : DFrac} {v : Qp} : own γ (●{dq} .ofSet (∅ : ReaderFracs)) ∗ own γ (◯ .ofSet {v}) ⊢@{IProp GF} False := by iintro H ihave %Hmem := own_auth_singleton_2 $$ H - simp [mem_iff_multiplicity_pos, multiplicity_empty] at Hmem + simp at Hmem /-! ## Re-establishing the lock invariant -/ @@ -339,8 +321,7 @@ theorem releaseReader_spec (γ : GName) (lk : Val) (Φ : Qp → IProp GF) (q : Q ihave HΦsum : iprop(Φ (q + q')) $$ [HΦ HΦq'] · iapply HΦdup $$ %q %q' [$HΦ $HΦq'] have hpos : 0 < z := by - have : size g ≠ 0 := fun h => by - simp [size_eq_zero_iff.mp h, mem_iff_multiplicity_pos, multiplicity_empty] at Hmem + have : size g ≠ 0 := fun h => by simp [size_eq_zero_iff.mp h] at Hmem omega have hsize : size (g \ {q}) = (z + -1).toNat := by rw [size_difference (singleton_subset_iff.mpr Hmem), size_singleton, Hsize]; omega diff --git a/Iris/Iris/Std/GenMultiSets.lean b/Iris/Iris/Std/GenMultiSets.lean index b420a95a7..73ce3c946 100644 --- a/Iris/Iris/Std/GenMultiSets.lean +++ b/Iris/Iris/Std/GenMultiSets.lean @@ -70,8 +70,15 @@ instance instHasSubsetMultiSet [MultiSet MS A] : HasSubset MS := theorem subset_iff [MultiSet MS A] {X Y : MS} : X ⊆ Y ↔ ∀ a, MultiSet.multiplicity a X ≤ MultiSet.multiplicity a Y := Iff.rfl +@[refl] +theorem subset_refl [MultiSet MS A] {X : MS} : X ⊆ X := subset_iff.mpr fun _ => Nat.le_refl _ + variable [LawfulMultiSet MS A] +@[simp] +theorem not_mem_empty {a : A} : a ∉ (∅ : MS) := by + rw [mem_iff_multiplicity_pos, multiplicity_empty]; omega + @[grind =] theorem mem_singleton_iff {x a : A} : x ∈ ({a} : MS) ↔ x = a := by rw [mem_iff_multiplicity_pos] From 5ba17ab3e09b5dc4c1115aec493307fa9ef5a6bf Mon Sep 17 00:00:00 2001 From: Markus de Medeiros Date: Tue, 11 Aug 2026 19:37:07 -0400 Subject: [PATCH 6/8] minor --- Iris/Iris/HeapLang/Lib/RwLock.lean | 28 ++++++++------------------ Iris/Iris/HeapLang/Lib/RwSpinLock.lean | 6 ++---- 2 files changed, 10 insertions(+), 24 deletions(-) diff --git a/Iris/Iris/HeapLang/Lib/RwLock.lean b/Iris/Iris/HeapLang/Lib/RwLock.lean index 9a52f0101..134bbbbc3 100644 --- a/Iris/Iris/HeapLang/Lib/RwLock.lean +++ b/Iris/Iris/HeapLang/Lib/RwLock.lean @@ -1,7 +1,7 @@ /- Copyright (c) 2026. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: +Authors: Markus de Medeiros -/ module @@ -16,36 +16,25 @@ open BI OFE @[expose] public section -/-- A general interface for a reader-writer lock. - -Only one instance of this class should ever be in scope. To write a library that is generic over -the lock, just add a `[RwLock GF]` parameter around the code and an `(L : rwlockG GF)` parameter -around the proofs. - -When writing an instance of this class, please take care not to shadow the class projections -(e.g. use a `newlock` in a dedicated namespace), and do not register the instance — just make it -a `def` that others can register later. -/ +/-- A general interface for a reader-writer lock. -/ @[rocq_alias heap_lang.rwlock] -class RwLock (GF : BundledGFunctors) [IrisGS_gen hlc Exp GF] where +structure RwLock (GF : BundledGFunctors) [IrisGS_gen hlc Exp GF] where -- Operations newlock : Val acquireReader : Val releaseReader : Val acquireWriter : Val releaseWriter : Val - -- Ghost state: `rwlockG` collects the assumptions on `GF`, and `name` associates - -- `readerLocked` and `writerLocked` with `isRwLock`. + -- Ghost state rwlockG : BundledGFunctors → Type name : Type - -- Predicates. There is no namespace parameter because we only expose program specs, which - -- anyway have the full mask. + -- Predicates isRwLock : rwlockG GF → name → Val → (Qp → IProp GF) → IProp GF readerLocked : rwlockG GF → name → Qp → IProp GF writerLocked : rwlockG GF → name → IProp GF -- General properties of the predicates isRwLock_persistent {L} γ lk Φ : Persistent (isRwLock L γ lk Φ) - isRwLock_iff {L} γ lk Φ Ψ : - isRwLock L γ lk Φ ⊢ (▷ □ ∀ q, Φ q ∗-∗ Ψ q) -∗ isRwLock L γ lk Ψ + isRwLock_iff {L} γ lk Φ Ψ : isRwLock L γ lk Φ ⊢ (▷ □ ∀ q, Φ q ∗-∗ Ψ q) -∗ isRwLock L γ lk Ψ readerLocked_timeless {L} γ q : Timeless (readerLocked L γ q) writerLocked_timeless {L} γ : Timeless (writerLocked L γ) writerLocked_exclusive {L} γ : writerLocked L γ ∗ writerLocked L γ ⊢@{IProp GF} False @@ -69,7 +58,7 @@ class RwLock (GF : BundledGFunctors) [IrisGS_gen hlc Exp GF] where section lemmas -variable [IrisGS_gen hlc Exp GF] [rw : RwLock GF] (L : rw.rwlockG GF) +variable [IrisGS_gen hlc Exp GF] (rw : RwLock GF) (L : rw.rwlockG GF) instance instPersistentIsRwLock γ lk Φ : Persistent (rw.isRwLock L γ lk Φ) := rw.isRwLock_persistent γ lk Φ @@ -85,8 +74,7 @@ instance isRwLock_contractive γ lk : Contractive (rw.isRwLock L γ lk) := by rw [contractive_internalEq (PROP := IProp GF)] iintro %Φ₁ %Φ₂ #HEQ ihave #HΦ : iprop(▷ ∀ q, Φ₁ q ≡ Φ₂ q) $$ [HEQ] - · iapply later_mono (discreteFun_equivI Φ₁ Φ₂).mp - iexact HEQ + · iapply later_mono (discreteFun_equivI Φ₁ Φ₂).mp $$ [$] iapply prop_ext imodintro isplit diff --git a/Iris/Iris/HeapLang/Lib/RwSpinLock.lean b/Iris/Iris/HeapLang/Lib/RwSpinLock.lean index 6bc0d1a2a..b2a69a795 100644 --- a/Iris/Iris/HeapLang/Lib/RwSpinLock.lean +++ b/Iris/Iris/HeapLang/Lib/RwSpinLock.lean @@ -75,7 +75,7 @@ attribute [reducible, instance] RwSpinLockG.elemG section proof --- `iinv` exhausts the default recursion budget on the goals below. +-- FIXME: `iinv` exhausts the default recursion budget on the goals below. set_option maxRecDepth 2000 variable {GF : BundledGFunctors} [HeapLangGS hlc GF] [RwSpinLockG GF] @@ -96,7 +96,6 @@ def rwStateInv (γ : GName) (l : Loc) (Φ : Qp → IProp GF) : IProp GF := iprop ⌜fold Qp.add q g = 1⌝ ∗ Φ q) -/-- The `▷` before `internalFractional` survives steps, which eases re-establishing it. -/ @[rocq_alias heap_lang.is_rw_lock] def isRwLock (γ : GName) (lk : Val) (Φ : Qp → IProp GF) : IProp GF := iprop% ▷ internalFractional Φ ∗ ∃ l : Loc, ⌜lk = hl_val(#l)⌝ ∗ inv rwLockN (rwStateInv γ l Φ) @@ -131,8 +130,7 @@ theorem own_auth_empty_split (γ : GName) : own (GF := GF) γ (●{.own Qp.quarter} .ofSet (∅ : ReaderFracs)) ∗ own γ (●{.own Qp.threeQuarters} .ofSet ∅) ⊣⊢ own γ (● .ofSet (∅ : ReaderFracs)) := by have hsplit : (● .ofSet (∅ : ReaderFracs) : Auth (LeibnizMultiSet ReaderFracs)) - = (●{.own Qp.quarter} LeibnizMultiSet.ofSet (∅ : ReaderFracs)) • - ●{.own Qp.threeQuarters} LeibnizMultiSet.ofSet ∅ := by + = (●{.own Qp.quarter} ofSet (∅ : ReaderFracs)) • ●{.own Qp.threeQuarters} ofSet ∅ := by rw [← Auth.auth_dfrac_op, DFrac.op_own, Qp.quarter_add_threeQuarters] rw [hsplit] exact iOwn_op.symm From ed9d0a6c0ede45116105cebef324b169cacfa703 Mon Sep 17 00:00:00 2001 From: Markus de Medeiros Date: Wed, 12 Aug 2026 10:04:45 -0400 Subject: [PATCH 7/8] fix annotations due to new scripts --- Iris/Iris/HeapLang/Lib/RwSpinLock.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Iris/Iris/HeapLang/Lib/RwSpinLock.lean b/Iris/Iris/HeapLang/Lib/RwSpinLock.lean index b2a69a795..47763b345 100644 --- a/Iris/Iris/HeapLang/Lib/RwSpinLock.lean +++ b/Iris/Iris/HeapLang/Lib/RwSpinLock.lean @@ -21,7 +21,7 @@ open BI Iris Std ProgramLogic CMRA OFE LeibnizMultiSet FiniteMultiSet namespace RwSpinLock -@[rocq_alias heap_lang.newlock] +@[rocq_alias heap_lang.rw_spin_lock.newlock] def newlock : Val := hl_val( λ _, ref(#0)) @@ -214,7 +214,7 @@ theorem isRwLock_iff (γ : GName) (lk : Val) (Φ Ψ : Qp → IProp GF) : iapply rwStateInv_mono $$ [] Hinv iintro %q HΨ; iapply Hiff $$ HΨ -@[rocq_alias heap_lang.newlock_spec] +@[rocq_alias heap_lang.rw_spin_lock.newlock_spec] theorem newlock_spec (Φ : Qp → IProp GF) {P : IProp GF} {ioΦ ioq} [hP : AsFractional P ioΦ Φ ioq 1] : {{ P }} hl(&newlock #()) {{ lk γ, RET lk; isRwLock γ lk Φ }} := by From 9053bb40893d79dbd0a9cf4dbbafa3fef5ee6c4c Mon Sep 17 00:00:00 2001 From: Markus de Medeiros Date: Wed, 12 Aug 2026 10:05:39 -0400 Subject: [PATCH 8/8] remove inv option --- Iris/Iris/HeapLang/Lib/RwSpinLock.lean | 3 --- 1 file changed, 3 deletions(-) diff --git a/Iris/Iris/HeapLang/Lib/RwSpinLock.lean b/Iris/Iris/HeapLang/Lib/RwSpinLock.lean index 47763b345..2ecedaaa0 100644 --- a/Iris/Iris/HeapLang/Lib/RwSpinLock.lean +++ b/Iris/Iris/HeapLang/Lib/RwSpinLock.lean @@ -75,9 +75,6 @@ attribute [reducible, instance] RwSpinLockG.elemG section proof --- FIXME: `iinv` exhausts the default recursion budget on the goals below. -set_option maxRecDepth 2000 - variable {GF : BundledGFunctors} [HeapLangGS hlc GF] [RwSpinLockG GF] def rwLockN : Namespace := nroot .@ "rw_lock"