diff --git a/Iris/Iris/Algebra/Auth.lean b/Iris/Iris/Algebra/Auth.lean index fe0a7a8af..bb519ab88 100644 --- a/Iris/Iris/Algebra/Auth.lean +++ b/Iris/Iris/Algebra/Auth.lean @@ -84,13 +84,11 @@ instance : UCMRA (Auth A) := View.instUCMRA @[rocq_alias auth_auth] abbrev auth (dq : DFrac) (a : A) : Auth A := View.Auth dq a -abbrev authFull (a : A) : Auth A := Auth (DFrac.own 1) a - @[rocq_alias auth_frag] abbrev frag (b : A) : Auth A := Frag b notation "●{" dq "} " a => auth dq a -notation "● " a => authFull a +notation "● " a => auth (DFrac.own 1) a notation "◯ " b => frag b @[rocq_alias auth_auth_ne] diff --git a/Iris/Iris/Algebra/Frac.lean b/Iris/Iris/Algebra/Frac.lean index 66aae551e..bd085aea1 100644 --- a/Iris/Iris/Algebra/Frac.lean +++ b/Iris/Iris/Algebra/Frac.lean @@ -58,6 +58,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)⟩ @@ -85,7 +91,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. @@ -93,6 +98,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 @@ -105,6 +112,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/Lib.lean b/Iris/Iris/Algebra/Lib.lean index 7fff3ad9f..15864992c 100644 --- a/Iris/Iris/Algebra/Lib.lean +++ b/Iris/Iris/Algebra/Lib.lean @@ -5,5 +5,6 @@ public import Iris.Algebra.Lib.ExclAuth public import Iris.Algebra.Lib.FracAuth public import Iris.Algebra.Lib.MonoList public import Iris.Algebra.Lib.MonoNat +public import Iris.Algebra.Lib.MultiSetAuth public import Iris.Algebra.Lib.MonoZ 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/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..7494367e4 --- /dev/null +++ b/Iris/Iris/HeapLang/Lib/RwLock.lean @@ -0,0 +1,99 @@ +/- +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.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. -/ +@[rocq_alias heap_lang.rwlock] +structure RwLock (GF : BundledGFunctors) [IrisGS_gen hlc Exp GF] where + -- Operations + newlock : Val + acquireReader : Val + releaseReader : Val + acquireWriter : Val + releaseWriter : Val + -- Ghost state + rwlockG : BundledGFunctors → Type + name : Type + -- 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 Ψ + 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Φ : ▷ ∀ q, Φ₁ q ≡ Φ₂ q $$ [HEQ] + · inext + iapply (discreteFun_equivI Φ₁ Φ₂).mp $$ [$] + 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..a0d15afbb --- /dev/null +++ b/Iris/Iris/HeapLang/Lib/RwSpinLock.lean @@ -0,0 +1,429 @@ +/- +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.Lib.MultiSetAuth +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.rw_spin_lock.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 + +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" + +abbrev own (γ : GName) (a : Auth (LeibnizMultiSet ReaderFracs)) : IProp GF := + iOwn (F := RwSpinLockF) γ a + +/-- The quarter kept while write-locked contradicts `readerLocked`; `writerLocked` owns the rest. -/ +@[rocq_alias heap_lang.rw_state_inv] +abbrev rwStateInv (γ : GName) (l : Loc) (Φ : Qp → IProp GF) : IProp GF := iprop% + ∃ z : Int, l ↦ some hl_val(#z) ∗ + (⌜z = -1⌝ ∗ own γ (●{.own Qp.quarter} (.ofSet ∅)) + ∨ ⌜0 ≤ z⌝ ∗ ∃ (q : Qp) (g : ReaderFracs), + own γ (● .ofSet g) ∗ + ⌜size g = z.toNat⌝ ∗ + ⌜fold Qp.add q g = 1⌝ ∗ + Φ q) + +@[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 γ (◯ .ofSet {q}) + +@[rocq_alias heap_lang.writer_locked] +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 + +instance instWriterLockedTimeless (γ : GName) : + Timeless (writerLocked (GF := GF) γ) := by unfold writerLocked; infer_instance + +/-! ## 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} : + 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 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} 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 + +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 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 := + 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 + 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 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.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 + iintro %φ HP Hφ + wp_rec + 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 + · 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 + +@[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 readerLocked rwStateInv + iintro %φ ⟨#HΦdup, %l, %Heq, #Hlockinv⟩ Hφ + subst Heq + wp_rec + wp_bind !_ + iinv Hlockinv with ⟨%z, Hl, Hz⟩ Hclose + wp_load + 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 + rw [decide_eq_true hle] + wp_pures + wp_bind cmpXchg(_, _, _) + iinv Hlockinv with ⟨%z', Hl, Hz⟩ Hclose + 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Φ, 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] + 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 + +@[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 rwStateInv + iintro %φ ⟨⟨#HΦdup, %l, %Heq, #Hlockinv⟩, Hlocked, HΦ⟩ Hφ + subst Heq + wp_rec + wp_bind faa(_, _) + iinv Hlockinv with ⟨%z, Hl, Hz⟩ Hclose + wp_faa + 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 $$ [$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 + 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 + 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 (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 + +@[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 (writerLocked γ ∗ Φ 1) else True }} := by + unfold isRwLock writerLocked rwStateInv + iintro %φ ⟨#HΦdup, %l, %Heq, #Hlockinv⟩ Hφ + subst Heq + wp_lam + wp_bind cmpXchg(_, _, _) + iinv Hlockinv with ⟨%z, >Hl, Hz⟩ Hclose + 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 + ieval (rewrite [← Qp.quarter_add_threeQuarters, ← Frac.op_eq]) at Hauth + -- FIXME: Frac.op_eq should not be needed + icases Hauth with ⟨Hauth, Hgive⟩ + imod Hclose $$ [Hl Hauth] with - + · iapply rwStateInv_writeLocked; iframe + imodintro + wp_pures + iapply Hφ; simp only [↓reduceIte] + iframe Hgive HΦ + · imod Hclose $$ [$Hl $Hz] with - + 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_if_false; iapply IH; itrivial + · wp_if_true; iapply Hφ; + simp only [↓reduceIte]; 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 rwStateInv + iintro %φ ⟨⟨#HΦdup, %l, %Heq, #Hlockinv⟩, Hlocked, HΦ⟩ Hφ + subst Heq + wp_lam + iinv Hlockinv with ⟨%z, >Hl, Hz⟩ Hclose + wp_store + icases Hz with (⟨-, Hquarter⟩ | ⟨-, %-, %-, Hauth, -⟩) + · icombine Hquarter Hlocked as Hown + rw [Qp.quarter_add_threeQuarters] + imod Hclose $$ [Hl Hown HΦ] with - + · iapply rwStateInv_unlocked; iframe + iapply Hφ; itrivial + · iexfalso; iapply own_auth_auth_False (q₁ := 1) (by grind) $$ [$Hauth $Hlocked] + +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 ce4f7a616..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] @@ -136,6 +143,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]