From 22cd0103c3b5d4ba30bfc41cb3d19c276b59b257 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 30 Sep 2026 01:48:08 +0000 Subject: [PATCH 01/10] Invariants: factorization order, proving invariant monotonicity MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The order on invariants was projection: `𝓘 ≤ 𝓙` when `𝓙` is the restriction of `𝓘` to fewer variables. Invariant-sensitive execution is not monotone along that order, so the `sorry` in `Inv.replace_monotone` (which every `wp` depended on, through the `MonoSem` instance) could not be filled. Counterexample: `𝓘` constrains `a` and `b` to be equal, `𝓙` only says `a ∈ {0, 1}`; replacing the invariant part of `{a=0, b=0}` under `𝓙` can produce `{a=1, b=0}`, which it cannot under `𝓘`. The order is now factorization (`Inv.LE_Inv`): `𝓘 ≤ 𝓙` when `𝓘` is `𝓙 ∗ 𝓚` for some invariant `𝓚` on the other variables, which is the situation of Lemma 5.3 of the paper (`I ∗ J`). With it: * `Inv.replace_le` / `Inv.checkReplace_monotone`: checking and then replacing the invariant is monotone (replacing alone is not, which is why the old lemma is gone); * the `MonoSem` instance is proved; * the DCPO structure is simplified: a directed set of invariants has a greatest element (the one with the fewest variables, preferring nonempty ones), which is its supremum; * `Cmd.withInv_monotone` is proved, including the `while` and action cases (`pom_singleton_mono`), and `Inv.le_emp` gives the step needed in `wp_share`. `Semantics/Invariant.lean` no longer contains any `sorry`, and `wp_seq` is now proved without axioms beyond Lean's standard ones. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_019Gipsr3EwstFw5DuwGNoug --- PcolIris/Logic/WeakestPre.lean | 3 +- PcolIris/Semantics/Invariant.lean | 361 ++++++++++++++++++------------ PcolIris/Semantics/Mem.lean | 9 + 3 files changed, 222 insertions(+), 151 deletions(-) diff --git a/PcolIris/Logic/WeakestPre.lean b/PcolIris/Logic/WeakestPre.lean index 0bcc3a6..b5a18d9 100644 --- a/PcolIris/Logic/WeakestPre.lean +++ b/PcolIris/Logic/WeakestPre.lean @@ -98,8 +98,7 @@ lemma wp_share {𝓘 : Inv} {F : ProbSpace → Prop} {c : Cmd Act} {ψ : OProp} refine le_iff_supset.mp ?_ hν apply ConvexPowerset.bind_monotone (le_refl _) apply (Pom.lin_continuous (act := WithInv Act) (test := Test)).monotone - apply Cmd.withInv_monotone; refine ⟨Set.empty_subset _, ?_⟩ - intro σ; sorry + exact Cmd.withInv_monotone c (Inv.le_emp 𝓘) sorry lemma wp_atom {𝓘 : Inv} {F : ProbSpace → Prop} {a : Act} {ψ : OProp} : diff --git a/PcolIris/Semantics/Invariant.lean b/PcolIris/Semantics/Invariant.lean index 2d3a5f9..1ec78ec 100644 --- a/PcolIris/Semantics/Invariant.lean +++ b/PcolIris/Semantics/Invariant.lean @@ -41,156 +41,135 @@ def to_MProp (𝓘 : Inv) : MProp := { simpa only [Membership.mem, Set.Mem, ← heq] } +/-- The order on invariants: `𝓘 ≤ 𝓙` when `𝓘` factors as `𝓙 ∗ 𝓚` for an invariant `𝓚` on the +remaining variables. Concretely, `𝓙` owns fewer variables, every memory satisfying `𝓘` +restricts to one satisfying `𝓙`, and replacing the `𝓙`-part of a memory satisfying `𝓘` by any +memory satisfying `𝓙` again satisfies `𝓘`. + +This is the order along which invariant-sensitive execution is monotone (Lemma 5.3 of the +paper, stated there for `I ∗ J`): a larger invariant allows more interference. A mere +projection would not do, since other threads could then change the variables of `𝓙` without +preserving the correlations that `𝓘` imposes with the other variables. -/ +structure LE_Inv (𝓘 𝓙 : Inv) : Prop where + dom : 𝓙.dom ⊆ 𝓘.dom + proj : ∀ {σ}, 𝓘.prop σ → 𝓙.prop (σ.restrict 𝓙.dom) + mix : ∀ {σ τ}, 𝓘.prop σ → 𝓙.prop τ → 𝓘.prop (τ ⊎ σ) + instance : LE Inv where - le 𝓙 𝓘 := - 𝓘.dom ⊆ 𝓙.dom ∧ - ∀ {σ}, 𝓘.prop σ ↔ ∃ τ : Mem, σ = τ.restrict 𝓘.dom ∧ 𝓙.prop τ + le := LE_Inv + +/-- Replacing the whole memory of an invariant by another one. -/ +lemma union_eq_of_prop {𝓘 : Inv} {σ τ : Mem} (hτ : 𝓘.prop τ) (hσ : σ.dom = 𝓘.dom) : + (τ ⊎ σ) = τ := by + funext x + by_cases hx : x ∈ τ.dom + · exact Mem.union_apply_of_mem_dom hx + · rw [Mem.union_apply_of_notMem_dom hx, Mem.notMem_dom_iff.mp hx] + rw [𝓘.dom_valid hτ, ← hσ] at hx + exact Mem.notMem_dom_iff.mp hx + +/-- Restricting a memory to the domain of an invariant it satisfies does not change it. -/ +lemma restrict_of_prop {𝓘 : Inv} {σ : Mem} (h : 𝓘.prop σ) : σ.restrict 𝓘.dom = σ := by + rw [← 𝓘.dom_valid h, Mem.restrict_self] + +/-- The memories of `𝓙` that are restrictions of memories of `𝓘` and the memories of `𝓘`. -/ +lemma restrict_union_restrict {𝓙 : Inv} {σ τ : Mem} (hτ : 𝓙.prop τ) (hsub : 𝓙.dom ⊆ σ.dom) : + (τ ⊎ σ).restrict 𝓙.dom = τ := by + rw [Mem.restrict_union_left (𝓙.dom_valid hτ)] instance : Preorder Inv where le_refl 𝓘 := by - constructor - · exact Set.Subset.refl _ - · intro σ; constructor - · intro h; have hdom := 𝓘.dom_valid h - exact ⟨σ, hdom.symm ▸ σ.restrict_self.symm, h⟩ - · rintro ⟨τ, rfl, h⟩; have hdom := 𝓘.dom_valid h - rwa [← hdom, Mem.restrict_self] + refine ⟨Set.Subset.refl _, fun h ↦ by rwa [restrict_of_prop h], fun hσ hτ ↦ ?_⟩ + rwa [union_eq_of_prop hτ (𝓘.dom_valid hσ)] le_trans 𝓘 𝓙 𝓚 hle₁ hle₂ := by - constructor - · exact hle₂.1.trans hle₁.1 - · intro σ; rw [hle₂.2] - conv => lhs; arg 1; ext τ; rw [hle₁.2] - simp only [↓existsAndEq, true_and, Mem.restrict_restrict, - Set.inter_eq_self_of_subset_right hle₂.1] + refine ⟨hle₂.dom.trans hle₁.dom, fun h ↦ ?_, fun {σ τ} hσ hτ ↦ ?_⟩ + · have := hle₂.proj (hle₁.proj h) + rwa [Mem.restrict_restrict, Set.inter_eq_self_of_subset_right hle₂.dom] at this + · -- mix `τ` into the `𝓙`-part of `σ`, and then that into `σ` + have hρ : 𝓙.prop (τ ⊎ σ.restrict 𝓙.dom) := hle₂.mix (hle₁.proj hσ) hτ + have := hle₁.mix hσ hρ + rwa [Mem.union_assoc, Mem.union_restrict_self] at this instance : PartialOrder Inv where le_antisymm 𝓘 𝓙 hle hge := by - have heq := Set.Subset.antisymm hge.1 hle.1 + have heq := Set.Subset.antisymm hge.dom hle.dom ext1 · exact heq - · ext σ; rw [hle.2]; constructor - · intro h; refine ⟨σ, ?_, h⟩ - rw [← heq, ← 𝓘.dom_valid h, Mem.restrict_self] - · rintro ⟨σ, rfl, h⟩ - rwa [← heq, ← 𝓘.dom_valid h, Mem.restrict_self] - -/-- A directed set of invariants contains an element whose domain is contained in the -domain of every element of the set. -/ -lemma exists_min_dom (d : DSet Inv) : ∃ L ∈ d, ∀ 𝓙 ∈ d, L.dom ⊆ 𝓙.dom := by - have hne : {n : ℕ | ∃ 𝓙 ∈ d, 𝓙.dom.ncard = n}.Nonempty := by - obtain ⟨𝓙, h𝓙⟩ := d.nonempty; exact ⟨𝓙.dom.ncard, 𝓙, h𝓙, rfl⟩ - obtain ⟨L, hL, hcard⟩ := Nat.sInf_mem hne - refine ⟨L, hL, ?_⟩ - intro 𝓙 h𝓙 - obtain ⟨M, hM, hle₁, hle₂⟩ := d.directed _ hL _ h𝓙 - have hsub : M.dom ⊆ L.dom := hle₁.1 - have hle : L.dom.ncard ≤ M.dom.ncard := by - rw [hcard]; exact Nat.sInf_le ⟨M, hM, rfl⟩ - have heq := Set.eq_of_subset_of_ncard_le hsub hle L.dom_finite - rw [← heq]; exact hle₂.1 - -/-- Two comparable invariants with the same domain are equal. -/ -lemma eq_of_le_of_dom_eq {L M : Inv} (hle : L ≤ M) (hdom : M.dom = L.dom) : M = L := by + · ext σ; constructor + · intro h; have := hle.proj h; rwa [← heq, restrict_of_prop h] at this + · intro h; have := hge.proj h; rwa [heq, restrict_of_prop h] at this + +/-- The invariant without variables is the largest one. -/ +lemma le_emp (𝓘 : Inv) : 𝓘 ≤ emp := by + refine ⟨Set.empty_subset _, fun _ ↦ ?_, fun {σ τ} hσ hτ ↦ ?_⟩ + · show Mem.dom _ = ∅ + rw [Mem.restrict_dom]; exact Set.inter_empty _ + · have hτ' : τ = Mem.emp := by + funext x; exact Mem.notMem_dom_iff.mp (by rw [show τ.dom = ∅ from hτ]; exact id) + rwa [hτ', Mem.emp_union] + +/-- Two comparable invariants with the same domain are equal, unless the smaller one is +empty (an empty invariant is below every invariant with fewer variables). -/ +lemma eq_of_le_of_dom_eq {L M : Inv} (hle : L ≤ M) (hdom : M.dom = L.dom) + (hne : (∃ ρ, L.prop ρ) ∨ ¬ ∃ σ, M.prop σ) : M = L := by ext1 · exact hdom - · ext σ; rw [hle.2]; constructor - · rintro ⟨τ, rfl, h⟩; rwa [hdom, ← L.dom_valid h, Mem.restrict_self] - · intro h; exact ⟨σ, by rw [hdom, ← L.dom_valid h, Mem.restrict_self], h⟩ - -instance : DCPO Inv where - dSup d := { - dom := ⋂ 𝓘 ∈ d, 𝓘.dom - prop σ := - σ.dom = (⋂ 𝓘 ∈ d, 𝓘.dom) ∧ - ∀ 𝓘 ∈ d, ∃ τ, σ = τ.restrict σ.dom ∧ 𝓘.prop τ - dom_finite := by - have ⟨𝓘, hd⟩ := d.nonempty - apply 𝓘.dom_finite.subset; exact Set.biInter_subset_of_mem hd - dom_valid := by intro σ ⟨hdom, _⟩; exact hdom - prop_finite := by - have ⟨𝓘, hd⟩ := d.nonempty - refine Set.Finite.subset (𝓘.prop_finite.image (Mem.restrict · (⋂ 𝓘 ∈ d, 𝓘.dom))) ?_ - rintro σ ⟨hdom, hprop⟩ - obtain ⟨τ, heq, hτ⟩ := hprop _ hd - rw [hdom] at heq - exact ⟨τ, hτ, heq.symm⟩ - } + · ext σ + rcases hne with ⟨ρ, hρ⟩ | hM + · constructor + · intro h + have := hle.mix hρ h + rwa [union_eq_of_prop h (by rw [L.dom_valid hρ, hdom])] at this + · intro h + have := hle.proj h + rwa [hdom, restrict_of_prop h] at this + · constructor + · intro h; exact absurd ⟨σ, h⟩ hM + · intro h + have := hle.proj h + exact absurd ⟨_, this⟩ hM + +open Classical in +/-- The key used to find the greatest element of a directed set of invariants: invariants +with fewer variables are larger, and among invariants with the same variables, nonempty ones +are larger. -/ +noncomputable def key (𝓘 : Inv) : ℕ := + 2 * 𝓘.dom.ncard + if ∃ σ, 𝓘.prop σ then 0 else 1 + +lemma key_lt_of_dom_ssubset {L M : Inv} (h : M.dom ⊂ L.dom) : M.key < L.key := by + have := Set.ncard_lt_ncard h L.dom_finite + unfold key; split_ifs <;> omega + +/-- A directed set of invariants has a greatest element. -/ +lemma exists_greatest (d : DSet Inv) : ∃ L ∈ d, ∀ 𝓙 ∈ d, 𝓙 ≤ L := by + have hne : {n : ℕ | ∃ 𝓙 ∈ d, 𝓙.key = n}.Nonempty := by + obtain ⟨𝓙, h𝓙⟩ := d.nonempty; exact ⟨𝓙.key, 𝓙, h𝓙, rfl⟩ + obtain ⟨L, hL, hkey⟩ := Nat.sInf_mem hne + refine ⟨L, hL, fun 𝓙 h𝓙 ↦ ?_⟩ + obtain ⟨M, hM, hle₁, hle₂⟩ := d.directed _ h𝓙 _ hL + have hmin : L.key ≤ M.key := by rw [hkey]; exact Nat.sInf_le ⟨M, hM, rfl⟩ + have hdom : M.dom = L.dom := by + by_contra hne + exact absurd (key_lt_of_dom_ssubset (Set.ssubset_iff_subset_ne.mpr ⟨hle₂.dom, hne⟩)) (by omega) + have heq : M = L := by + refine eq_of_le_of_dom_eq hle₂ hdom ?_ + by_contra hc + push_neg at hc + obtain ⟨hL', ⟨σ, hσ⟩⟩ := hc + have : M.key < L.key := by + unfold key; rw [hdom, if_pos ⟨σ, hσ⟩, if_neg (by simpa using hL')]; omega + omega + exact heq ▸ hle₁ + +noncomputable instance : DCPO Inv where + dSup d := (exists_greatest d).choose lubOfDirected d := by - constructor - · intro 𝓘 hd; constructor - · exact Set.biInter_subset_of_mem hd - · intro σ; simp only; constructor - · intro ⟨hdom, hprop⟩; have ⟨τ, heq, h⟩ := hprop _ hd - refine ⟨τ, ?_, h⟩; rw [heq, hdom] - · rintro ⟨τ, rfl, hprop⟩; constructor - · rw [Mem.restrict_dom]; apply Set.inter_eq_self_of_subset_right - rw [𝓘.dom_valid hprop]; exact Set.biInter_subset_of_mem hd - · intro 𝓙 h𝓙 - have ⟨𝓚, h𝓚, ⟨hsub₁, hprop₁⟩, hsub₂, hprop₂⟩ := d.directed _ hd _ h𝓙 - have hp𝓚 := hprop₁.mpr ⟨τ, rfl, hprop⟩ - have ⟨ρ, heq, h⟩ := hprop₂.mp hp𝓚 - refine ⟨ρ, ?_, h⟩; rw [Mem.restrict_dom] - conv => - lhs; arg 2; - exact (Set.biInter_subset_of_mem h𝓚 (t := Inv.dom) |> - Set.inter_eq_self_of_subset_right).symm - rw [← Mem.restrict_restrict, heq, Mem.restrict_restrict] - refine congrArg₂ _ rfl ?_ - rw [Set.inter_eq_self_of_subset_right, Set.inter_eq_self_of_subset_right] - · rfl - · rw [𝓘.dom_valid hprop]; exact Set.biInter_subset_of_mem hd - · exact Set.biInter_subset_of_mem h𝓚 - · intro 𝓘 hup; constructor - · intro x hx; apply Set.mem_biInter; intro 𝓙 h𝓙 - exact (hup h𝓙).1 hx - · intro σ - have ⟨𝓙, h𝓙⟩ := d.nonempty; have ⟨hsub, hprop⟩ := hup h𝓙; constructor - · intro h; obtain ⟨τ, rfl, hp⟩ := hprop.mp h - refine ⟨τ.restrict (⋂ 𝓙 ∈ d, 𝓙.dom), ?_, ?_⟩ - · rw [Mem.restrict_restrict]; congr - symm; apply Set.inter_eq_self_of_subset_right - apply Set.subset_iInter₂; intro 𝓚 h𝓚; exact (hup h𝓚).1 - · constructor - · rw [Mem.restrict_dom]; apply Set.inter_eq_self_of_subset_right - rw [𝓙.dom_valid hp]; exact Set.biInter_subset_of_mem h𝓙 - · intro 𝓚 h𝓚 - obtain ⟨L, hL, hle₁, hle₂⟩ := d.directed _ h𝓙 _ h𝓚 - have hDL : (⋂ 𝓚 ∈ d, 𝓚.dom) ⊆ L.dom := Set.biInter_subset_of_mem hL - have h₁ : L.prop (τ.restrict L.dom) := hle₁.2.mpr ⟨τ, rfl, hp⟩ - obtain ⟨ρ, heqρ, hρ⟩ := hle₂.2.mp h₁ - refine ⟨ρ, ?_, hρ⟩ - have hdomτ : Mem.dom (τ.restrict (⋂ 𝓚 ∈ d, 𝓚.dom)) - = ⋂ 𝓚 ∈ d, 𝓚.dom := by - rw [Mem.restrict_dom, 𝓙.dom_valid hp] - exact Set.inter_eq_self_of_subset_right (Set.biInter_subset_of_mem h𝓙) - rw [hdomτ] - calc τ.restrict (⋂ 𝓚 ∈ d, 𝓚.dom) - = Mem.restrict (τ.restrict L.dom) (⋂ 𝓚 ∈ d, 𝓚.dom) := by - rw [Mem.restrict_restrict, Set.inter_eq_self_of_subset_right hDL] - _ = Mem.restrict (ρ.restrict L.dom) (⋂ 𝓚 ∈ d, 𝓚.dom) := by rw [heqρ] - _ = ρ.restrict (⋂ 𝓚 ∈ d, 𝓚.dom) := by - rw [Mem.restrict_restrict, Set.inter_eq_self_of_subset_right hDL] - · rintro ⟨τ, rfl, hdom, h⟩ - have ⟨ρ, heq, hp⟩ := h _ h𝓙; refine hprop.mpr ⟨ρ, ?_, hp⟩ - rw [heq, Mem.restrict_restrict]; congr - apply Set.inter_eq_self_of_subset_right; rw [hdom] - apply Set.subset_iInter₂; intro 𝓚 h𝓚; exact (hup h𝓚).1 - - - -lemma ge_of_subset {𝓘 𝓙 : Inv} (hle : 𝓘 ≤ 𝓙) : - 𝓙.prop = fun σ ↦ ∃ τ : Mem, σ = τ.restrict 𝓙.dom ∧ 𝓘.prop τ := by - ext σ; rw [hle.2] + obtain ⟨hL, hmax⟩ := (exists_greatest d).choose_spec + exact ⟨fun _ h ↦ hmax _ h, fun _ hu ↦ hu hL⟩ /-- The supremum of a directed set of invariants is attained: it is a member of the set. -/ -lemma dSup_mem (d : DSet Inv) : ∃ L ∈ d, d.dSup = L := by - obtain ⟨L, hL, hmin⟩ := exists_min_dom d - have hub : ∀ 𝓙 ∈ d, 𝓙 ≤ L := by - intro 𝓙 h𝓙 - obtain ⟨M, hM, hle₁, hle₂⟩ := d.directed _ h𝓙 _ hL - have heq := eq_of_le_of_dom_eq hle₂ (Set.Subset.antisymm hle₂.1 (hmin _ hM)) - exact heq ▸ hle₁ - exact ⟨L, hL, le_antisymm (DSet.dSup_le hub) (DSet.le_dSup hL)⟩ +lemma dSup_mem (d : DSet Inv) : ∃ L ∈ d, d.dSup = L := + ⟨_, (exists_greatest d).choose_spec.1, rfl⟩ instance : ScottCompact Inv where scottCompact 𝓘 := by @@ -203,11 +182,11 @@ noncomputable def check (𝓘 : Inv) (σ : Mem) : ConvexPowerset Mem := if 𝓘.prop (σ.restrict 𝓘.dom) then pure σ else ⊥ lemma check_monotone (σ : Mem) : Monotone (check · σ) := by - intro 𝓘 𝓙 ⟨hsub, hprop⟩; simp only [check] + intro 𝓘 𝓙 hle; simp only [check] by_cases h : 𝓘.prop (σ.restrict 𝓘.dom) · rw [if_pos h] - have h' := hprop.mpr ⟨_, rfl, h⟩ - rw [Mem.restrict_restrict, Set.inter_eq_self_of_subset_right hsub] at h' + have h' := hle.proj h + rw [Mem.restrict_restrict, Set.inter_eq_self_of_subset_right hle.dom] at h' rw [if_pos h'] · rw [if_neg h]; exact bot_le @@ -216,8 +195,73 @@ noncomputable def replace (𝓘 : Inv) (σ : Mem) : ConvexPowerset Mem := Nondet.nondet fun (τ : 𝓘.prop_finite.toFinset) ↦ pure (τ ⊎ σ) -lemma replace_monotone (σ : Mem) : Monotone (replace · σ) := by - intro 𝓘 𝓙 hle; simp only [replace]; sorry +lemma bot_bind {α β : Type} (f : α → ConvexPowerset β) : (⊥ : ConvexPowerset α) >>= f = ⊥ := by + refine le_antisymm (le_iff_supset.mpr fun ν _ ↦ ?_) bot_le + refine ConvexPowerset.mem_bind.mpr ⟨PMF.pure ⊥, Set.mem_univ _, fun _ ↦ ν, ?_, ?_⟩ + · intro x hx + rw [PMF.support_pure, Set.mem_singleton_iff] at hx + subst hx; exact Set.mem_univ _ + · rw [PMF.pure_bind] + +/-- If `σ` satisfies the larger invariant `𝓘`, then every way of replacing the `𝓙`-part of `σ` +is also a way of replacing its `𝓘`-part. -/ +lemma replace_le {𝓘 𝓙 : Inv} (hle : 𝓘 ≤ 𝓙) {σ : Mem} (h : 𝓘.prop (σ.restrict 𝓘.dom)) : + replace 𝓘 σ ≤ replace 𝓙 σ := by + classical + have hmemI : ∀ {τ}, 𝓘.prop τ → τ ∈ 𝓘.prop_finite.toFinset := + fun hτ ↦ 𝓘.prop_finite.mem_toFinset.mpr hτ + have hmemJ : ∀ {τ}, τ ∈ 𝓙.prop_finite.toFinset → 𝓙.prop τ := + fun hτ ↦ 𝓙.prop_finite.mem_toFinset.mp hτ + have hI : Nonempty 𝓘.prop_finite.toFinset := ⟨⟨_, hmemI h⟩⟩ + have hJ : Nonempty 𝓙.prop_finite.toFinset := by + have := hle.proj h + rw [Mem.restrict_restrict, Set.inter_eq_self_of_subset_right hle.dom] at this + exact ⟨⟨_, 𝓙.prop_finite.mem_toFinset.mpr this⟩⟩ + -- The embedding of the memories of `𝓙` into those of `𝓘` + let e : 𝓙.prop_finite.toFinset → 𝓘.prop_finite.toFinset := fun τ ↦ + ⟨τ.val ⊎ σ.restrict 𝓘.dom, hmemI (hle.mix h (hmemJ τ.2))⟩ + have he : ∀ τ, ((e τ).val ⊎ σ) = (τ.val ⊎ σ) := by + intro τ + change ((τ.val ⊎ σ.restrict 𝓘.dom) ⊎ σ) = _ + rw [Mem.union_assoc, Mem.union_restrict_self] + have hinj : Function.Injective e := by + intro τ τ' heq + have h' := congrArg (fun (ρ : 𝓘.prop_finite.toFinset) ↦ ρ.val.restrict 𝓙.dom) heq + simp only [e] at h' + rw [Mem.restrict_union_left (𝓙.dom_valid (hmemJ τ.2)), + Mem.restrict_union_left (𝓙.dom_valid (hmemJ τ'.2))] at h' + exact Subtype.ext h' + rw [le_iff_supset] + intro ν hν + change ν ∈ (if _ : Nonempty _ then ConvexPowerset.nondet _ else ⊥ : ConvexPowerset Mem) + change ν ∈ (if _ : Nonempty _ then ConvexPowerset.nondet _ else ⊥ : ConvexPowerset Mem) at hν + rw [dif_pos hI] + rw [dif_pos hJ] at hν + obtain ⟨ξ, k, hk, rfl⟩ := ConvexPowerset.mem_nondet.mp hν + refine ConvexPowerset.mem_nondet.mpr ⟨ξ.map e, Function.extend e k (fun _ ↦ ξ.bind k), ?_, ?_⟩ + · intro i hi + rw [PMF.support_map] at hi + obtain ⟨j, hj, rfl⟩ := hi + simp only [Function.comp_apply] + rw [hinj.extend_apply, he] + exact hk j hj + · rw [PMF.bind_map] + congr 1 + funext j + exact (hinj.extend_apply _ _ j).symm + +/-- Checking and then replacing the invariant is monotone in the invariant: a larger +invariant allows more interference (Lemma 5.3 of the paper). -/ +lemma checkReplace_monotone (σ : Mem) : Monotone (fun (𝓘 : Inv) ↦ check 𝓘 σ >>= replace 𝓘) := by + intro 𝓘 𝓙 hle + simp only + by_cases h : 𝓘.prop (σ.restrict 𝓘.dom) + · have h' := hle.proj h + rw [Mem.restrict_restrict, Set.inter_eq_self_of_subset_right hle.dom] at h' + rw [check, if_pos h, pure_bind, check, if_pos h', pure_bind] + exact replace_le hle h + · rw [check, if_neg h, bot_bind] + exact bot_le end Inv @@ -286,12 +330,25 @@ noncomputable instance {act : Type} [Preorder act] [Sem act Mem (ConvexPowerset MonoSem (WithInv act) Mem (ConvexPowerset Mem) where sem_mono := by rintro ⟨a, 𝓘⟩ ⟨_, 𝓙⟩ ⟨rfl, hle⟩ σ - apply ConvexPowerset.bind_monotone (Inv.check_monotone _ hle) - intro σ; simp only - apply ConvexPowerset.bind_monotone (Inv.replace_monotone _ hle) - intro σ; simp only; apply ConvexPowerset.bind_monotone - · exact le_refl _ - · intro τ; exact Inv.check_monotone _ hle + show (Inv.check 𝓘 σ >>= fun σ ↦ Inv.replace 𝓘 σ >>= fun σ ↦ + Sem.sem a σ >>= fun τ ↦ Inv.check 𝓘 τ) ≤ + (Inv.check 𝓙 σ >>= fun σ ↦ Inv.replace 𝓙 σ >>= fun σ ↦ + Sem.sem a σ >>= fun τ ↦ Inv.check 𝓙 τ) + rw [← bind_assoc (Inv.check 𝓘 σ) (Inv.replace 𝓘), ← bind_assoc (Inv.check 𝓙 σ) (Inv.replace 𝓙)] + refine ConvexPowerset.bind_monotone (Inv.checkReplace_monotone σ hle) ?_ + intro σ; apply ConvexPowerset.bind_monotone (le_refl _) + intro τ; exact Inv.check_monotone _ hle + +/-- A singleton pomset is monotone in its label. -/ +lemma pom_singleton_mono {l : Type} [PartialOrder l] [OrderBot l] {ℓ ℓ' : l} (h : ℓ ≤ ℓ') : + Pom.singleton ℓ ≤ Pom.singleton ℓ' := by + refine ⟨Lpo.singleton default ℓ, rfl, Lpo.singleton default ℓ', rfl, ?_⟩ + refine ⟨Set.Subset.refl _, fun _ _ _ h ↦ h.elim, fun _ _ _ _ ↦ rfl, fun x ↦ ?_, + fun _ _ ↦ rfl, fun _ hx ↦ Or.inl hx⟩ + change (if default = x then ℓ else ⊥) ≤ (if default = x then ℓ' else ⊥) + split_ifs + · exact h + · exact le_refl _ namespace Cmd @@ -320,11 +377,17 @@ lemma withInv_monotone {act : Type} (c : Cmd act) : Monotone (Cmd.to_pom ∘ c.w | while_loop e c ih => simp only [withInv, to_pom] apply OmegaCompletePartialOrder.ωSup_le_ωSup_of_le; intro n; use n - sorry + change (Pom.Semantics.while_body _ _)^[n] ⊥ ≤ (Pom.Semantics.while_body _ _)^[n] ⊥ + induction n with + | zero => exact le_refl _ + | succ n ihn => + rw [Function.iterate_succ', Function.comp_apply, Function.iterate_succ', + Function.comp_apply] + unfold Pom.Semantics.while_body Pom.Semantics.if_stmt Pom.Semantics.seq + exact Pom.guard_monotone _ (le_refl _) (Pom.seq_monotone ih ihn) (le_refl _) | act a => simp only [withInv, to_pom] - -- This case is easy, but we need to add a lemma to the pomset library - sorry + exact pom_singleton_mono (show (⟨a, 𝓘⟩ : WithInv act) ≤ ⟨a, 𝓙⟩ from ⟨rfl, hle⟩) end Cmd diff --git a/PcolIris/Semantics/Mem.lean b/PcolIris/Semantics/Mem.lean index 1286218..30746ab 100644 --- a/PcolIris/Semantics/Mem.lean +++ b/PcolIris/Semantics/Mem.lean @@ -294,6 +294,15 @@ lemma le_union_right (hd : Disjoint σ.dom τ.dom) : τ ≤ (σ ⊎ τ) := by rw [union_comm hd] exact le_union_left τ σ +/-- Putting a restriction of a memory in front of the memory itself does not change it. -/ +lemma union_restrict_self (σ : Mem) (X : Set Var) : (σ.restrict X ⊎ σ) = σ := by + funext x + by_cases hx : x ∈ (σ.restrict X).dom + · rw [union_apply_of_mem_dom hx] + have hX : x ∈ X := dom_restrict_subset σ X hx + exact restrict_apply_of_mem σ hX + · exact union_apply_of_notMem_dom hx + end Mem end Pcol From e83132d04c7a90cfcd9526394215160438ca156a Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 30 Sep 2026 01:54:20 +0000 Subject: [PATCH 02/10] Locality: fill the memory bookkeeping in the frame lemmas The remaining `sorry`s in `sem_withInv_frame` and `sem_withInv_indep` were pointwise identities about overwriting the invariant part of a memory. They follow from a new general lemma, `Mem.union_restrict_of_subset`: restricting commutes with overwriting by a memory that lives inside the restriction. With this, `Pom.par_comp` (Lemma C.5) is proved without `sorry`. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_019Gipsr3EwstFw5DuwGNoug --- PcolIris/Logic/Locality.lean | 24 ++++++++++++------------ PcolIris/Semantics/Mem.lean | 11 +++++++++++ 2 files changed, 23 insertions(+), 12 deletions(-) diff --git a/PcolIris/Logic/Locality.lean b/PcolIris/Logic/Locality.lean index 1d2d8b6..3b33893 100644 --- a/PcolIris/Logic/Locality.lean +++ b/PcolIris/Logic/Locality.lean @@ -138,16 +138,8 @@ theorem sem_withInv_frame {a : Act} {𝓘 : Inv} {W : Set Var} (hD : 𝓘.dom have hdomnW : Mem.dom (show Mem from n.restrict W) = W := by rw [Mem.restrict_dom, hdomn] exact Set.inter_eq_self_of_subset_right hm - have hn : (τ.val ⊎ (m.restrict W)) = n.restrict W := by - funext x - by_cases hx : x ∈ W - · rw [Mem.restrict_apply_of_mem _ hx] - by_cases hxD : x ∈ 𝓘.dom - · rw [hn_def]; sorry - · sorry - · rw [Mem.restrict_apply_of_notMem _ hx] - have hxD : x ∉ 𝓘.dom := fun hc ↦ hx (hD hc) - sorry + have hn : (τ.val ⊎ (m.restrict W)) = n.restrict W := + Mem.union_restrict_of_subset (hτdom ▸ hD) m rw [hn] conv_lhs => rw [h₁ n] rw [bind_assoc, bind_assoc] @@ -160,7 +152,7 @@ theorem sem_withInv_frame {a : Act} {𝓘 : Inv} {W : Set Var} (hD : 𝓘.dom refine Mem.union_congr_right ?_ intro x hx rw [hm₃] at hx - sorry + rw [hn_def, Mem.union_apply_of_notMem_dom (fun h ↦ hx (hD (hτdom ▸ h)))] rw [Inv.check, Inv.check, hrestr] by_cases hp : 𝓘.prop (m₃.restrict 𝓘.dom) · rw [if_pos hp, if_pos hp, pure_bind, hunion] @@ -213,8 +205,16 @@ theorem sem_withInv_indep {a : Act} {𝓘 : Inv} {X : Set Var} {p p' : Mem} rw [sem_withInv_eq_ite, sem_withInv_eq_ite, if_pos hi, if_pos hi'] congr 1 funext τ + have hτdom : Mem.dom τ.val = 𝓘.dom := 𝓘.dom_valid ((Set.Finite.mem_toFinset _).mp τ.property) have hhav : (τ.val ⊎ p) = (τ.val ⊎ p') := by - funext x; sorry + refine Mem.union_congr_right fun x hx ↦ ?_ + rw [hτdom] at hx + by_cases hxX : x ∈ X + · have := congrFun hX x + rwa [Mem.restrict_apply_of_mem _ hxX, Mem.restrict_apply_of_mem _ hxX] at this + · have hxp : x ∉ p.dom := by rw [hp]; exact fun h ↦ h.elim hxX hx + have hxp' : x ∉ p'.dom := by rw [hp']; exact fun h ↦ h.elim hxX hx + rw [Mem.notMem_dom_iff.mp hxp, Mem.notMem_dom_iff.mp hxp'] rw [hhav] /-! ### The locality hypotheses are satisfiable diff --git a/PcolIris/Semantics/Mem.lean b/PcolIris/Semantics/Mem.lean index 30746ab..36444fb 100644 --- a/PcolIris/Semantics/Mem.lean +++ b/PcolIris/Semantics/Mem.lean @@ -303,6 +303,17 @@ lemma union_restrict_self (σ : Mem) (X : Set Var) : (σ.restrict X ⊎ σ) = σ exact restrict_apply_of_mem σ hX · exact union_apply_of_notMem_dom hx +/-- Restricting commutes with overwriting by a memory that lives inside the restriction. -/ +lemma union_restrict_of_subset {τ : Mem} (hτ : τ.dom ⊆ X) (σ : Mem) : + (τ ⊎ σ.restrict X) = (τ ⊎ σ).restrict X := by + funext x + by_cases hτx : x ∈ τ.dom + · rw [union_apply_of_mem_dom hτx, restrict_apply_of_mem _ (hτ hτx), union_apply_of_mem_dom hτx] + · rw [union_apply_of_notMem_dom hτx] + by_cases hx : x ∈ X + · rw [restrict_apply_of_mem _ hx, restrict_apply_of_mem _ hx, union_apply_of_notMem_dom hτx] + · rw [restrict_apply_of_notMem _ hx, restrict_apply_of_notMem _ hx] + end Mem end Pcol From db0c09ab49eb4bbd9203e6fd5b13e7f90b51cdcb Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 30 Sep 2026 01:57:29 +0000 Subject: [PATCH 03/10] Add a script listing the declarations that use sorry Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_019Gipsr3EwstFw5DuwGNoug --- .github/workflows/build.yml | 1 + README.md | 3 ++- scripts/Sorries.lean | 21 +++++++++++++++++++++ 3 files changed, 24 insertions(+), 1 deletion(-) create mode 100644 scripts/Sorries.lean diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index 9dafd67..a6b32f0 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -16,3 +16,4 @@ jobs: - name: Report declarations that still use sorry run: | lake env lean scripts/Axioms.lean + lake env lean scripts/Sorries.lean diff --git a/README.md b/README.md index c3cd7af..b08fd13 100644 --- a/README.md +++ b/README.md @@ -6,4 +6,5 @@ See [DESIGN.md](DESIGN.md) for the places where the formalization deliberately d from the paper. The main results and the axioms they depend on (in particular, whether they still use -`sorry`) can be listed with `lake env lean scripts/Axioms.lean`. +`sorry`) can be listed with `lake env lean scripts/Axioms.lean`, and the declarations that +use `sorry` directly with `lake env lean scripts/Sorries.lean`. diff --git a/scripts/Sorries.lean b/scripts/Sorries.lean new file mode 100644 index 0000000..5a0a1c0 --- /dev/null +++ b/scripts/Sorries.lean @@ -0,0 +1,21 @@ +/- +Lists the declarations of this project that use `sorry` directly (as opposed to depending on +another declaration that does). Run with `lake env lean scripts/Sorries.lean`. +-/ +import PcolIris + +open Lean Elab Command + +elab "#list_sorries" : command => do + let env ← getEnv + let mut out : Array Name := #[] + for (n, ci) in env.constants.toList do + let some idx := env.getModuleIdxFor? n | continue + let mod := env.header.moduleNames[idx.toNat]! + if !(`PcolIris).isPrefixOf mod then continue + if n.isInternal then continue + if ci.getUsedConstantsAsSet.contains ``sorryAx then out := out.push n + let sorted := out.qsort (·.toString < ·.toString) + logInfo m!"{sorted.size} declarations use sorry directly:\n{sorted.toList}" + +#list_sorries From e23463596861782982fabe704fce835e293f1467 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 30 Sep 2026 02:00:38 +0000 Subject: [PATCH 04/10] Laws: prove oplus_distrib and the introduction half of sure_sep MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * `sumProd_le_sum_product` / `sum_product_le_sumProd` restate the distributive law of products over sums (`sum_prod_distribute`) as inequalities for the new order. * `oplus_distrib`: a frame can be pushed into the branches of an outcome conjunction. * `sure_sep_intro`: `⌈P⌉ ∗ ⌈Q⌉ ⊢ ⌈P ∗ Q⌉`. The other direction of `sure_sep` needs the two assertions to have fixed footprints (it has to split the probability space along the variables), and stays `sorry` for now. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_019Gipsr3EwstFw5DuwGNoug --- PcolIris/OProp/Laws.lean | 45 +++++++++++++++++++++++++++++++++++++--- 1 file changed, 42 insertions(+), 3 deletions(-) diff --git a/PcolIris/OProp/Laws.lean b/PcolIris/OProp/Laws.lean index cdeabd9..801f12e 100644 --- a/PcolIris/OProp/Laws.lean +++ b/PcolIris/OProp/Laws.lean @@ -6,6 +6,29 @@ namespace Pcol namespace ProbSpace +/-- The distributive law of products over sums, as a pair of inequalities. -/ +lemma sumProd_le_sum_product {ι : Type} (ξ : PMF ι) (𝓟 : ι → ProbSpace) (𝓠 : ProbSpace) + (V : Set Var) (h : ∀ {i j : ι}, i ≠ j → Disjoint (𝓟 i).support (𝓟 j).support) + (hdom : ∀ i : ι, (𝓟 i).dom = V) : + sumProd ξ 𝓟 𝓠 V h hdom ≤ (sum ξ 𝓟 V h hdom ⊗ 𝓠) := by + obtain ⟨hms, hmeas, hd, hsupp, hst⟩ := sum_prod_distribute ξ 𝓟 𝓠 V h hdom + refine le_of_id (fun E hE ↦ hms ▸ hE) (fun E _ ↦ ?_) hd.symm.subset + (fun k hk ↦ le_of_eq (hst k hk).symm) + refine ENNReal.coe_injective ?_ + rw [prob_coe, prob_coe] + exact (hmeas E).symm + +lemma sum_product_le_sumProd {ι : Type} (ξ : PMF ι) (𝓟 : ι → ProbSpace) (𝓠 : ProbSpace) + (V : Set Var) (h : ∀ {i j : ι}, i ≠ j → Disjoint (𝓟 i).support (𝓟 j).support) + (hdom : ∀ i : ι, (𝓟 i).dom = V) : + (sum ξ 𝓟 V h hdom ⊗ 𝓠) ≤ sumProd ξ 𝓟 𝓠 V h hdom := by + obtain ⟨hms, hmeas, hd, hsupp, hst⟩ := sum_prod_distribute ξ 𝓟 𝓠 V h hdom + refine le_of_id (fun E hE ↦ hms.symm ▸ hE) (fun E _ ↦ ?_) hd.subset + (fun k hk ↦ le_of_eq (hst k (hsupp ▸ hk))) + refine ENNReal.coe_injective ?_ + rw [prob_coe, prob_coe] + exact hmeas E + /-- The left factor of a product is contained in the product state. -/ lemma state_le_product_left (p q : ProbSpace) (n : ℕ) : p.state (Nat.pairEquiv.symm n).1 ≤ (p ⊗ q).state n := by @@ -49,15 +72,31 @@ lemma sure_weaken {P Q : MProp} (h : P ⊢ Q) : ⌈P⌉ ⊢ ⌈Q⌉ := by intro 𝓟 hP i hi; apply Set.mem_preimage.mpr exact hP hi |> Set.mem_preimage.mp |> h _ +/-- Two separately owned certainties give a certainty about their separating conjunction. -/ +lemma sure_sep_intro {P Q : MProp} : iprop(⌈P⌉ ∗ ⌈Q⌉) ⊢ ⌈ iprop(P ∗ Q) ⌉ := by + rintro 𝓟 ⟨𝓟₁, 𝓟₂, hdisj, ⟨g, hg⟩, hP, hQ⟩ n hn + obtain ⟨h1, h2⟩ := ProbSpace.mem_support_product_iff.mp (hg.mem_support hn) + refine ⟨_, _, ?_, ?_, hP h1, hQ h2⟩ + · rw [𝓟₁.dom_valid, 𝓟₂.dom_valid]; exact hdisj + · have := hg.state n hn + rwa [ProbSpace.product_state] at this + lemma sure_sep {P Q : MProp} : ⌈ iprop(P ∗ Q) ⌉ ⊣⊢ ⌈P⌉ ∗ ⌈Q⌉ := by constructor · intro 𝓟 hsure; sorry - · intro 𝓟 ⟨𝓟₁, 𝓟₂, hdisj, hle, hP, hQ⟩ k hk - sorry + · exact sure_sep_intro +/-- A frame can be pushed into the branches of an outcome conjunction. -/ lemma oplus_distrib {ι : Type} (ξ : PMF ι) (φ : ι → OProp) (ψ : OProp) : - (⨁[ ξ ] φ) ∗ ψ ⊢ ⨁[ ξ ] fun v ↦ iprop(φ v ∗ ψ) := sorry + (⨁[ ξ ] φ) ∗ ψ ⊢ ⨁[ ξ ] fun v ↦ iprop(φ v ∗ ψ) := by + rintro 𝓟 ⟨m₁, m₂, hd, hle, ⟨𝓠, V, hdsj, hdom, hsum, hφ⟩, hψ⟩ + have hV : V ⊆ m₁.dom := ProbSpace.dom_mono hsum + refine ⟨fun v ↦ 𝓠 v ⊗ m₂, V ∪ m₂.dom, ProbSpace.sum_prod_disjoint m₂ hdsj, + ProbSpace.sum_prod_dom m₂ hdom, ?_, fun v hv ↦ ?_⟩ + · exact (ProbSpace.sumProd_le_sum_product ξ 𝓠 m₂ V hdsj hdom).trans + ((ProbSpace.product_mono_left hsum hd).trans hle) + · exact ⟨𝓠 v, m₂, (hdom v).symm ▸ hd.mono_left hV, le_refl _, hφ v hv, hψ⟩ lemma oplus_distrib' {ι : Type} (ξ : PMF ι) (φ : ι → OProp) (ψ : OProp) (h : ψ.Precise) : (⨁[ ξ ] fun v ↦ iprop(φ v ∗ ψ)) ⊢ (⨁[ ξ ] φ) ∗ ψ := by From ab3f01de3d4125a76ae5162374cc9fdef4492e26 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 30 Sep 2026 02:10:38 +0000 Subject: [PATCH 05/10] Probability spaces without probabilistic information MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `ProbSpace.trivialOn V f` has the trivial σ-algebra `{∅, ℕ}` and memories `f`: it records which memories over `V` are possible, but no probabilities. Every outcome is in its support (`support_trivialOn`), and it is below any space that owns `V` and whose memories almost surely extend memories of `f` (`trivialOn_le`). These spaces are the least models of almost sure assertions. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_019Gipsr3EwstFw5DuwGNoug --- PcolIris/OProp/TrivialSpace.lean | 69 ++++++++++++++++++++++++++++++++ PcolIris/Semantics/Mem.lean | 7 ++++ 2 files changed, 76 insertions(+) create mode 100644 PcolIris/OProp/TrivialSpace.lean diff --git a/PcolIris/OProp/TrivialSpace.lean b/PcolIris/OProp/TrivialSpace.lean new file mode 100644 index 0000000..7448461 --- /dev/null +++ b/PcolIris/OProp/TrivialSpace.lean @@ -0,0 +1,69 @@ +/- +Probability spaces without probabilistic information. + +`ProbSpace.trivialOn V f` has the trivial σ-algebra `{∅, ℕ}`: it only records which memories +(over the variables `V`) are possible, not how likely they are. Every outcome is in its +support. Such spaces are the least models of almost sure assertions (`Precise.sure`), and +they are independent of every other space. +-/ +import PcolIris.OProp.ProductLaws + +namespace Pcol + +open MeasureTheory + +namespace ProbSpace + +/-- The probability space with trivial σ-algebra whose outcome `i` has memory `f i`. -/ +noncomputable def trivialOn (V : Set Var) (f : ℕ → Mem) (hf : ∀ i, (f i).dom = V) : + ProbSpace where + mspace := ⊥ + μ := ⟨@Measure.dirac ℕ ⊥ 0, @Measure.dirac.isProbabilityMeasure ℕ ⊥ 0⟩ + dom := V + state := f + dom_valid := hf + complete := by + constructor + intro s hs + by_cases hne : s = ∅ + · rw [hne]; exact @MeasurableSet.empty ℕ ⊥ + · exfalso + obtain ⟨n, hn⟩ := Set.nonempty_iff_ne_empty.mpr hne + obtain ⟨t, hst, ht, ht0⟩ := @exists_measurable_superset_of_null ℕ ⊥ _ s hs + rcases (@MeasurableSpace.measurableSet_bot_iff ℕ t).mp ht with rfl | rfl + · exact hst hn + · rw [measure_univ] at ht0; exact one_ne_zero ht0 + +variable {V : Set Var} {f : ℕ → Mem} {hf : ∀ i, (f i).dom = V} + +lemma trivialOn_measurableSet {E : Set ℕ} (hE : (trivialOn V f hf).mspace.MeasurableSet' E) : + E = ∅ ∨ E = Set.univ := + (@MeasurableSpace.measurableSet_bot_iff ℕ E).mp hE + +/-- Every outcome of a space without probabilistic information is possible. -/ +lemma support_trivialOn : (trivialOn V f hf).support = Set.univ := by + refine Set.eq_univ_of_forall fun n ↦ Set.mem_sInter.mpr ?_ + rintro E ⟨hE, h1⟩ + rcases trivialOn_measurableSet hE with rfl | rfl + · exfalso + have : ((trivialOn V f hf).μ ∅ : ENNReal) = 0 := by rw [prob_coe]; exact measure_empty + rw [h1] at this; exact one_ne_zero this + · exact Set.mem_univ n + +/-- A space without probabilistic information is below any space that owns its variables and +whose memories (almost surely) extend memories of the space. -/ +lemma trivialOn_le {𝓠 : ProbSpace} (hdom : V ⊆ 𝓠.dom) (g : ℕ → ℕ) + (hg : ∀ i ∈ 𝓠.support, f (g i) ≤ 𝓠.state i) : trivialOn V f hf ≤ 𝓠 := by + refine ⟨g, fun E hE ↦ ?_, fun E hE ↦ ?_, hdom, hg⟩ + · rcases trivialOn_measurableSet hE with rfl | rfl + · exact 𝓠.mspace.measurableSet_empty + · exact @MeasurableSet.univ ℕ 𝓠.mspace + · refine ENNReal.coe_injective ?_ + rw [prob_coe, prob_coe] + rcases trivialOn_measurableSet hE with rfl | rfl + · rw [Set.preimage_empty, measure_empty, measure_empty] + · rw [Set.preimage_univ, measure_univ, measure_univ] + +end ProbSpace + +end Pcol diff --git a/PcolIris/Semantics/Mem.lean b/PcolIris/Semantics/Mem.lean index 36444fb..878ee56 100644 --- a/PcolIris/Semantics/Mem.lean +++ b/PcolIris/Semantics/Mem.lean @@ -314,6 +314,13 @@ lemma union_restrict_of_subset {τ : Mem} (hτ : τ.dom ⊆ X) (σ : Mem) : · rw [restrict_apply_of_mem _ hx, restrict_apply_of_mem _ hx, union_apply_of_notMem_dom hτx] · rw [restrict_apply_of_notMem _ hx, restrict_apply_of_notMem _ hx] +lemma restrict_le (σ : Mem) (X : Set Var) : σ.restrict X ≤ σ := by + rw [le_iff] + intro x v hx + by_cases h : x ∈ X + · rwa [restrict_apply_of_mem _ h] at hx + · rw [restrict_apply_of_notMem _ h] at hx; exact absurd hx (by simp) + end Mem end Pcol From 91791141642e5441818afdf3a4758fb2c9f6abb9 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 30 Sep 2026 02:10:38 +0000 Subject: [PATCH 06/10] =?UTF-8?q?Precision:=20the=20paper's=20definition,?= =?UTF-8?q?=20and=20proofs=20for=20=E2=8C=88P=E2=8C=89=20and=20=E2=88=97?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `Precise` now follows Definition 4.1: if `φ` is satisfiable, then it has a least model. Previously it also required satisfiability, which made e.g. the invariant of the von Neumann example imprecise for an empty set of biases. * `Precise.sure` was false as stated (`⌈x = 1 ∨ y = 1⌉` has no least model). As in the paper, where `⌈P⌉` is interpreted over the variables of `P`, it now requires `P` to have a finite footprint (`MProp.Footprint`); the least model is the space without probabilistic information whose memories are those satisfying `P`. Footprint lemmas are provided for `emp`, `x == v`, `own x`, conjunctions, equations `e == c`, and invariants. * `Precise.sep` is proved: the least model is the product of the least models. * `wp_par` obtains the satisfiability of the postconditions by running each thread alone, using the new `Framed.left` / `Framed.right`, which split a framed product between the two threads. The examples supply the footprints of their precise assertions. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_019Gipsr3EwstFw5DuwGNoug --- PcolIris/Examples/EntropyMixer.lean | 8 +- PcolIris/Examples/VonNeumann.lean | 37 ++++++++- PcolIris/Logic/Framed.lean | 33 ++++++++ PcolIris/Logic/WeakestPre.lean | 16 ++-- PcolIris/OProp/Laws.lean | 112 +++++++++++++++++++++++++++- PcolIris/OProp/OProp.lean | 4 +- 6 files changed, 196 insertions(+), 14 deletions(-) diff --git a/PcolIris/Examples/EntropyMixer.lean b/PcolIris/Examples/EntropyMixer.lean index 716f4fd..9d13da0 100644 --- a/PcolIris/Examples/EntropyMixer.lean +++ b/PcolIris/Examples/EntropyMixer.lean @@ -72,10 +72,12 @@ lemma inv_of_y_eq (v : Val) (hv : v = 0 ∨ v = 1) : /-- The postcondition `ψ` is precise: it is a probabilistic sum of the (precise) assertions `⌈$"z" == v⌉`. -/ -lemma ψ_precise : ψ.Precise := Precise.oplus fun _ _ ↦ Precise.sure _ +lemma ψ_precise : ψ.Precise := Precise.oplus fun _ _ ↦ + Precise.sure (MProp.Footprint.var_equals_literal _ _) (Set.finite_singleton _) /-- The unit of the separating conjunction is precise. -/ -lemma emp_precise : (Iris.BI.BIBase.emp : OProp).Precise := Precise.sure _ +lemma emp_precise : (Iris.BI.BIBase.emp : OProp).Precise := + Precise.sure MProp.Footprint.emp Set.finite_empty /-- The invariant `𝓘` guarantees that `y` holds one of the two values `0` and `1`. -/ lemma exists_y_of_inv : @@ -253,7 +255,7 @@ and the postcondition `ψ` of the weakest precondition is precise as well. -/ lemma collapse_post {F : ProbSpace → Prop} {ι : Type} {c : Cmd Act} : OProp.nondet (fun (_ : ι) => iprop(wp_base 𝓘 F c ψ ∗ ⌈𝓘.to_MProp⌉)) ⊢ iprop(wp_base 𝓘 F c ψ ∗ ⌈𝓘.to_MProp⌉) := - Iris.BI.Entails.trans (OProp.nondet_distrib' _ _ (Precise.sure _)) + Iris.BI.Entails.trans (OProp.nondet_distrib' _ _ (Precise.sure (Inv.footprint 𝓘) 𝓘.dom_finite)) (Iris.BI.sep_mono_left (wp_nondet ψ_precise)) /-- The first thread, given only the nondeterministic knowledge that `y` holds one of the diff --git a/PcolIris/Examples/VonNeumann.lean b/PcolIris/Examples/VonNeumann.lean index 7b18d4d..c9a1697 100644 --- a/PcolIris/Examples/VonNeumann.lean +++ b/PcolIris/Examples/VonNeumann.lean @@ -122,6 +122,35 @@ lemma eqTest_eval {σ : Mem} {a b : Val} (hx : σ "x" = some a) (hy : σ "y" = s eqTest ($"x") ($"y") σ = some (if a = b then 1 else 0) := by simp [eqTest, Expr.var, hx, hy] +lemma eqTest_mono : Expr.Mono (eqTest ($"x") ($"y")) := by + intro σ τ v hle h + obtain ⟨a, ha⟩ : ∃ a, σ "x" = some a := by + cases hx : σ "x" with + | none => simp [eqTest, Expr.var, hx] at h + | some a => exact ⟨a, rfl⟩ + obtain ⟨b, hb⟩ : ∃ b, σ "y" = some b := by + cases hy : σ "y" with + | none => simp [eqTest, Expr.var, ha, hy] at h + | some b => exact ⟨b, rfl⟩ + rw [eqTest_eval ha hb] at h + rw [eqTest_eval (Mem.le_iff.mp hle _ _ ha) (Mem.le_iff.mp hle _ _ hb), h] + +lemma eqTest_vars_finite : ({"x", "y"} : Set Var).Finite := Set.toFinite _ + +lemma eqTest_footprint (c : Val) : + (eqTest ($"x") ($"y") == Expr.literal c).Footprint {"x", "y"} := by + refine MProp.Footprint.equals_literal eqTest_mono (fun σ ↦ ?_) (fun σ h ↦ ?_) c + · simp [eqTest, Expr.var, Mem.restrict_apply_of_mem] + · intro z hz + rcases hz with rfl | rfl + · cases hx : σ "x" with + | none => simp [eqTest, Expr.var, hx] at h + | some a => exact Mem.mem_dom_of_eq_some hx + · cases hy : σ "y" with + | none => + cases hx : σ "x" <;> simp [eqTest, Expr.var, hx, hy] at h + | some b => exact Mem.mem_dom_of_eq_some hy + /-- When the two coins disagree, the guard of the loop is false. -/ lemma guard_false {b : Val} (hb : b = 0 ∨ b = 1) : (iprop(($"x" == Expr.literal b) ∧ ($"y" == Expr.literal (1 - b))) : MProp) ⊢ @@ -148,7 +177,9 @@ lemma guard_true : exact MProp.upClose_of ⟨by rw [h]; rfl, by rw [h]; rfl⟩ /-- `φ₀` is precise. -/ -lemma phi0_precise : phi0.Precise := Precise.oplus fun _ _ ↦ Precise.sure _ +lemma phi0_precise : phi0.Precise := Precise.oplus fun _ _ ↦ + Precise.sure ((MProp.Footprint.var_equals_literal _ _).and + (MProp.Footprint.var_equals_literal _ _)) ((Set.finite_singleton _).union (Set.finite_singleton _)) /-- After the loop, `x` is a fair coin flip. -/ lemma phi0_fair : phi0 ⊢ ($"x") ~ Bern 0.5 := @@ -162,7 +193,7 @@ lemma loopInv_rank (r : Set.Icc (0 : ℕ) 1) : · rw [if_pos h, h] have h1 : phi0 ⊢ (⨁[Bern 0.5] (fun (_ : Val) => ⌈eqTest ($"x") ($"y") == Expr.literal 0⌉)) := OProp.oplus_weaken' fun b hb ↦ OProp.sure_weaken (guard_false (Bern_support hb)) - have h2 := Iris.BI.Entails.trans h1 (OProp.oplus_collapse (Precise.sure _)) + have h2 := Iris.BI.Entails.trans h1 (OProp.oplus_collapse (Precise.sure (eqTest_footprint 0) eqTest_vars_finite)) rw [Nat.cast_zero] exact h2 · have h1 : (r : ℕ) = 1 := le_antisymm r.2.2 (Nat.one_le_iff_ne_zero.mpr h) @@ -513,7 +544,7 @@ lemma wp_body_nondet {L : Finset ℚ} {F : ProbSpace → Prop} (eps : ℚ) refine Iris.BI.Entails.trans (OProp.nondet_distrib _ _) ?_ refine Iris.BI.Entails.trans (OProp.nondet_weaken (fun v ↦ wp_body_branch (F := F) eps v.val heps heps' v.2 (hL v.val v.2).1 (hL v.val v.2).2)) ?_ - exact wp_nsplit2 (Convex.sep_precise (Convex.wp (bodyPost'_convex _)) (Precise.sure _)) + exact wp_nsplit2 (Convex.sep_precise (Convex.wp (bodyPost'_convex _)) (Precise.sure (Inv.footprint (inv L)) (inv L).dom_finite)) /-- The loop invariant at rank `1` provides the ownership of the three variables written by the loop body. -/ diff --git a/PcolIris/Logic/Framed.lean b/PcolIris/Logic/Framed.lean index ddcfc23..d1440ab 100644 --- a/PcolIris/Logic/Framed.lean +++ b/PcolIris/Logic/Framed.lean @@ -8,9 +8,21 @@ paper). import PcolIris.OProp.OProp import PcolIris.OProp.ProductLaws import PcolIris.Semantics.Invariant +import PcolIris.OProp.Laws namespace Pcol +/-- An invariant only talks about its own variables. -/ +lemma Inv.footprint (𝓘 : Inv) : 𝓘.to_MProp.Footprint 𝓘.dom := by + intro σ + change 𝓘.prop (σ.restrict 𝓘.dom) ↔ 𝓘.dom ⊆ σ.dom ∧ 𝓘.prop ((σ.restrict 𝓘.dom).restrict 𝓘.dom) + rw [Mem.restrict_restrict, Set.inter_self] + refine ⟨fun h ↦ ⟨?_, h⟩, fun h ↦ h.2⟩ + have := 𝓘.dom_valid h + rw [Mem.restrict_dom] at this + exact Set.inter_eq_right.mp this + + /-- `Framed 𝓘 𝓟 𝓟fr 𝓙 μ` states that the distribution `μ` refines the product of a space `𝓟` (owned by the program), a frame `𝓟fr`, and a space `𝓙` in which the invariant `𝓘` holds @@ -39,6 +51,27 @@ lemma mono (h : 𝓟 ≤ 𝓟') (hf : Framed 𝓘 𝓟' 𝓟fr 𝓙 μ) : Framed (ProbSpace.product_mono_left (ProbSpace.product_mono_left h hf.disj_frame) hf.disj_inv) hf.refines +/-- The left factor of a framed product is framed by the right factor and the frame. -/ +lemma left {𝓟₁ 𝓟₂ : ProbSpace} (hd : Disjoint 𝓟₁.dom 𝓟₂.dom) + (hf : Framed 𝓘 (𝓟₁ ⊗ 𝓟₂) 𝓟fr 𝓙 μ) : Framed 𝓘 𝓟₁ (𝓟₂ ⊗ 𝓟fr) 𝓙 μ where + inv := hf.inv + disj_frame := Set.disjoint_union_right.mpr + ⟨hd, hf.disj_frame.mono_left Set.subset_union_left⟩ + disj_inv := by + have := hf.disj_inv + change Disjoint (𝓟₁.dom ∪ (𝓟₂.dom ∪ 𝓟fr.dom)) 𝓙.dom + change Disjoint ((𝓟₁.dom ∪ 𝓟₂.dom) ∪ 𝓟fr.dom) 𝓙.dom at this + rwa [Set.union_assoc] at this + refines := Distr.Refines.mono + (ProbSpace.product_mono_left (ProbSpace.product_assoc' 𝓟₁ 𝓟₂ 𝓟fr) hf.disj_inv) hf.refines + +/-- The right factor of a framed product is framed by the left factor and the frame. -/ +lemma right {𝓟₁ 𝓟₂ : ProbSpace} (hd : Disjoint 𝓟₁.dom 𝓟₂.dom) + (hf : Framed 𝓘 (𝓟₁ ⊗ 𝓟₂) 𝓟fr 𝓙 μ) : Framed 𝓘 𝓟₂ (𝓟₁ ⊗ 𝓟fr) 𝓙 μ := by + have hc : (𝓟₂ ⊗ 𝓟₁) ≤ (𝓟₁ ⊗ 𝓟₂) := ProbSpace.product_comm hd + have hf' : Framed 𝓘 (𝓟₂ ⊗ 𝓟₁) 𝓟fr 𝓙 μ := hf.mono hc + exact hf'.left hd.symm + end Framed end Pcol diff --git a/PcolIris/Logic/WeakestPre.lean b/PcolIris/Logic/WeakestPre.lean index b5a18d9..f131639 100644 --- a/PcolIris/Logic/WeakestPre.lean +++ b/PcolIris/Logic/WeakestPre.lean @@ -117,9 +117,15 @@ lemma wp_par {𝓘 : Inv} {c₁ c₂ : Cmd Act} {ψ₁ ψ₂ : OProp} (hψ₁ : ψ₁.Precise) (hψ₂ : ψ₂.Precise) : wp 𝓘 c₁ ψ₁ ∗ wp 𝓘 c₂ ψ₂ ⊢ wp 𝓘 (c₁.par c₂) iprop(ψ₁ ∗ ψ₂) := by intro 𝓟 ⟨𝓟₁, 𝓟₂, hdisj, hle, h₁, h₂⟩ μ 𝓟fr 𝓙 _ hf ν hν - -- `𝓠₁` and `𝓠₂` are the least probability spaces satisfying `ψ₁` and `ψ₂` - obtain ⟨𝓠₁, hQ₁⟩ := hψ₁ - obtain ⟨𝓠₂, hQ₂⟩ := hψ₂ + -- Running each thread alone shows that `ψ₁` and `ψ₂` are satisfiable, so by precision + -- they have least models `𝓠₁` and `𝓠₂` + have hf' := hf.mono hle + obtain ⟨ν₁, hν₁⟩ := (ConvexPowerset.singleton' μ >>= 𝓛 (c₁.withInv 𝓘).to_pom).nonempty + obtain ⟨ν₂, hν₂⟩ := (ConvexPowerset.singleton' μ >>= 𝓛 (c₂.withInv 𝓘).to_pom).nonempty + obtain ⟨_, _, -, hψ₁'⟩ := h₁ μ _ 𝓙 True.intro (hf'.left hdisj) ν₁ hν₁ + obtain ⟨_, _, -, hψ₂'⟩ := h₂ μ _ 𝓙 True.intro (hf'.right hdisj) ν₂ hν₂ + obtain ⟨𝓠₁, hQ₁⟩ := hψ₁ _ hψ₁' + obtain ⟨𝓠₂, hQ₂⟩ := hψ₂ _ hψ₂' -- Each thread, run in isolation with an arbitrary frame, establishes its postcondition; -- by precision, the least such postcondition space is `𝓠ₖ` have hthread₁ : ∀ (𝓕 𝓙₁ : ProbSpace) (μ₁ : Distr Mem), Framed 𝓘 𝓟₁ 𝓕 𝓙₁ μ₁ → @@ -136,10 +142,10 @@ lemma wp_par {𝓘 : Inv} {c₁ c₂ : Cmd Act} {ψ₁ ψ₂ : OProp} exact ⟨𝓙₂', hf'.mono ((hQ₂ 𝓠).mpr hψ)⟩ -- The parallel composition is handled by Lemma C.6 rw [Cmd.withInv, Cmd.to_pom] at hν - obtain ⟨𝓙', hf'⟩ := lemma_C6 (hf.mono hle) hthread₁ hthread₂ ν hν + obtain ⟨𝓙', hf''⟩ := lemma_C6 hf' hthread₁ hthread₂ ν hν -- We still need to prove that `𝓠₁` and `𝓠₂` own disjoint variables, which requires -- knowing that the footprint of a postcondition is contained in that of the precondition - exact ⟨𝓠₁ ⊗ 𝓠₂, 𝓙', hf', + exact ⟨𝓠₁ ⊗ 𝓠₂, 𝓙', hf'', 𝓠₁, 𝓠₂, sorry, le_refl _, (hQ₁ 𝓠₁).mp (le_refl _), (hQ₂ 𝓠₂).mp (le_refl _)⟩ /- STRUCTURAL RULES -/ diff --git a/PcolIris/OProp/Laws.lean b/PcolIris/OProp/Laws.lean index 801f12e..e31d0b1 100644 --- a/PcolIris/OProp/Laws.lean +++ b/PcolIris/OProp/Laws.lean @@ -1,6 +1,7 @@ import PcolIris.OProp.OProp import PcolIris.OProp.ProbSpaceLemmas import PcolIris.OProp.ProductLaws +import PcolIris.OProp.TrivialSpace namespace Pcol @@ -171,11 +172,118 @@ lemma oplus_reindex {ι : Type} {ξ : PMF ι} (e : ι ≃ ι) (hξ : ∀ i, ξ ( end OProp +namespace MProp + +/-- The pure assertion `P` only talks about the variables `V`: it requires them to be +allocated, and only depends on their values. -/ +def Footprint (P : MProp) (V : Set Var) : Prop := + ∀ σ, P σ ↔ V ⊆ σ.dom ∧ P (σ.restrict V) + +namespace Footprint + +lemma emp : (Iris.BI.BIBase.emp : MProp).Footprint ∅ := + fun _ ↦ ⟨fun _ ↦ ⟨Set.empty_subset _, trivial⟩, fun _ ↦ trivial⟩ + +lemma var_equals_literal (x : Var) (v : Val) : ($ x == Expr.literal v).Footprint {x} := by + intro σ + rw [Expr.var_equals_literal_iff, Expr.var_equals_literal_iff, + Mem.restrict_apply_of_mem _ (Set.mem_singleton x)] + exact ⟨fun h ↦ ⟨Set.singleton_subset_iff.mpr (Mem.mem_dom_of_eq_some h), h⟩, fun h ↦ h.2⟩ + +lemma own_var (x : Var) : (own ($ x)).Footprint {x} := by + intro σ + rw [own_var_iff, own_var_iff, Mem.restrict_apply_of_mem _ (Set.mem_singleton x)] + refine ⟨fun h ↦ ⟨Set.singleton_subset_iff.mpr ?_, h⟩, fun h ↦ h.2⟩ + exact Mem.mem_dom_iff.mpr (Option.isSome_iff_ne_none.mp h) + +/-- An equation between an expression and a literal only talks about the variables that the +expression reads. -/ +lemma equals_literal {e : Expr} {V : Set Var} (hmono : Expr.Mono e) + (hread : ∀ σ, e σ = e (σ.restrict V)) (hdef : ∀ σ, (e σ).isSome → V ⊆ σ.dom) (c : Val) : + (e == Expr.literal c).Footprint V := by + intro σ + rw [Expr.equals_iff hmono (Expr.literal_mono c), Expr.equals_iff hmono (Expr.literal_mono c), + ← hread σ] + exact ⟨fun h ↦ ⟨hdef σ h.1, h⟩, fun h ↦ h.2⟩ + +lemma and {P Q : MProp} {V W : Set Var} (hP : P.Footprint V) (hQ : Q.Footprint W) : + iprop(P ∧ Q).Footprint (V ∪ W) := by + intro σ + change P σ ∧ Q σ ↔ V ∪ W ⊆ σ.dom ∧ (P (σ.restrict (V ∪ W)) ∧ Q (σ.restrict (V ∪ W))) + rw [hP σ, hQ σ, hP (σ.restrict (V ∪ W)), hQ (σ.restrict (V ∪ W)), Mem.restrict_restrict, + Mem.restrict_restrict, Mem.restrict_dom, + Set.inter_eq_right.mpr (Set.subset_union_left : V ⊆ V ∪ W), + Set.inter_eq_right.mpr (Set.subset_union_right : W ⊆ V ∪ W)] + simp only [Set.union_subset_iff, Set.subset_inter_iff] + tauto + +end Footprint + +end MProp + namespace Precise -lemma sure (P : MProp) : (OProp.sure P).Precise := sorry +/-- An almost sure assertion is precise, provided that the pure assertion only talks about a +fixed finite set of variables (in the paper, `⌈P⌉` is interpreted over +the variables of `P`). Its least model records which memories over those variables are +possible, but no probabilities. -/ +lemma sure {P : MProp} {V : Set Var} (hP : P.Footprint V) (hV : V.Finite) : + (OProp.sure P).Precise := by + classical + intro 𝓠₀ h₀ + have hsat : ∃ σ, P σ := by + obtain ⟨k, hk⟩ := ProbSpace.support_nonempty 𝓠₀ + exact ⟨_, h₀ hk⟩ + let S : Set Mem := {τ | τ.dom = V ∧ P τ} + have hcount : S.Countable := by + haveI : Finite V := hV.to_subtype + refine Set.Countable.mono (s₂ := {τ : Mem | τ.dom = V}) (fun τ h ↦ h.1) ?_ + have hinj : Function.Injective + (fun (τ : {τ : Mem | τ.dom = V}) ↦ fun (x : V) ↦ τ.val x) := by + intro τ τ' h; apply Subtype.ext; funext x + by_cases hx : x ∈ V + · exact congrFun h ⟨x, hx⟩ + · have h₁ : x ∉ τ.val.dom := by rw [τ.2]; exact hx + have h₂ : x ∉ τ'.val.dom := by rw [τ'.2]; exact hx + rw [Mem.notMem_dom_iff.mp h₁, Mem.notMem_dom_iff.mp h₂] + exact Set.countable_coe_iff.mp hinj.countable + obtain ⟨σ, hσ⟩ := hsat + have hσS : σ.restrict V ∈ S := + ⟨by rw [Mem.restrict_dom]; exact Set.inter_eq_right.mpr ((hP σ).mp hσ).1, + ((hP σ).mp hσ).2⟩ + obtain ⟨f, hf⟩ := hcount.exists_eq_range ⟨_, hσS⟩ + have hfS : ∀ i, f i ∈ S := fun i ↦ hf ▸ Set.mem_range_self i + refine ⟨ProbSpace.trivialOn V f (fun i ↦ (hfS i).1), fun 𝓠 ↦ ⟨?_, fun h ↦ ?_⟩⟩ + · rintro ⟨g, hg⟩ k hk + exact P.upcl (hg.state k hk) (hfS (g k)).2 + · obtain ⟨k0, hk0⟩ := ProbSpace.support_nonempty 𝓠 + have hdom : V ⊆ 𝓠.dom := by + rw [← 𝓠.dom_valid k0]; exact ((hP _).mp (h hk0)).1 + have hmem : ∀ i ∈ 𝓠.support, (𝓠.state i).restrict V ∈ Set.range f := by + intro i hi + rw [← hf] + refine ⟨?_, ((hP _).mp (h hi)).2⟩ + rw [Mem.restrict_dom, 𝓠.dom_valid]; exact Set.inter_eq_right.mpr hdom + let g : ℕ → ℕ := fun i ↦ if hi : i ∈ 𝓠.support then (hmem i hi).choose else 0 + refine ProbSpace.trivialOn_le hdom g (fun i hi ↦ ?_) + simp only [g, dif_pos hi] + rw [(hmem i hi).choose_spec] + exact Mem.restrict_le _ _ -lemma sep {φ ψ : OProp} (hφ : φ.Precise) (hψ : ψ.Precise) : iprop(φ ∗ ψ).Precise := by sorry +/-- Separating conjunctions of precise assertions are precise: the least model is the product +of the least models. -/ +lemma sep {φ ψ : OProp} (hφ : φ.Precise) (hψ : ψ.Precise) : iprop(φ ∗ ψ).Precise := by + rintro 𝓠 ⟨m₁, m₂, hd, -, h₁, h₂⟩ + obtain ⟨𝓟₁, hP₁⟩ := hφ m₁ h₁ + obtain ⟨𝓟₂, hP₂⟩ := hψ m₂ h₂ + have hd' : Disjoint 𝓟₁.dom 𝓟₂.dom := + (hd.mono_left (ProbSpace.dom_mono ((hP₁ m₁).mpr h₁))).mono_right + (ProbSpace.dom_mono ((hP₂ m₂).mpr h₂)) + refine ⟨𝓟₁ ⊗ 𝓟₂, fun 𝓠' ↦ ⟨fun hle ↦ ?_, ?_⟩⟩ + · exact ⟨𝓟₁, 𝓟₂, hd', hle, (hP₁ 𝓟₁).mp (le_refl _), (hP₂ 𝓟₂).mp (le_refl _)⟩ + · rintro ⟨n₁, n₂, hdn, hle, hn₁, hn₂⟩ + exact (ProbSpace.product_mono ((hP₁ n₁).mpr hn₁) ((hP₂ n₂).mpr hn₂) + (hdn.mono_right (ProbSpace.dom_mono ((hP₂ n₂).mpr hn₂)))).trans hle lemma oplus {ι : Type} {ξ : PMF ι} {φ : ι → OProp} (h : ∀ v ∈ ξ.support, (φ v).Precise) : (⨁[ξ] φ).Precise := by sorry diff --git a/PcolIris/OProp/OProp.lean b/PcolIris/OProp/OProp.lean index 8ae7720..9926deb 100644 --- a/PcolIris/OProp/OProp.lean +++ b/PcolIris/OProp/OProp.lean @@ -222,8 +222,10 @@ instance : Iris.BI.BIAffine OProp where affine := by intro φ; constructor; intro _ _ _ _; trivial +/-- Precision (Definition 4.1): if `φ` is satisfiable, then it has a least model, i.e. the +models of `φ` are exactly the spaces above some space `𝓟`. -/ def Precise (φ : OProp) : Prop := - ∃ 𝓟 : ProbSpace, ∀ 𝓠, 𝓟 ≤ 𝓠 ↔ φ 𝓠 + ∀ 𝓠, φ 𝓠 → ∃ 𝓟 : ProbSpace, ∀ 𝓠', 𝓟 ≤ 𝓠' ↔ φ 𝓠' def oplus {ι : Type} (ξ : PMF ι) (φ : ι → OProp) : OProp where prop 𝓟 := ∃ 𝓠 V h hd, From 63dde879c1363525ca1ddcb5625b62e0fa277db4 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 30 Sep 2026 02:13:43 +0000 Subject: [PATCH 07/10] DESIGN: record the invariant order and the treatment of precision Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_019Gipsr3EwstFw5DuwGNoug --- DESIGN.md | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/DESIGN.md b/DESIGN.md index 3a869be..b00a371 100644 --- a/DESIGN.md +++ b/DESIGN.md @@ -57,6 +57,20 @@ Following Iris, specifications are stated with a weakest-precondition predicate that the initial and final distributions refine (`Framed`): the part of the state that satisfies the invariant is any space `𝓙` with `⌈I⌉ 𝓙`, as in `P ⊨ φ ∗ ⌈I⌉`. +## Invariants + +Invariants are ordered by factorization (`Inv.LE_Inv`): `𝓘 ≤ 𝓙` when `𝓘` is `𝓙 ∗ 𝓚` for +some invariant `𝓚` on the other variables. This is the order along which +invariant-sensitive execution is monotone (Lemma 5.3, stated in the paper for `I ∗ J`); a +mere projection order would let other threads break the correlations that `𝓘` imposes. + +## Precision + +`Precise` follows Definition 4.1: if an assertion is satisfiable, it has a least model. +`⌈P⌉` is precise when `P` has a finite footprint (`MProp.Footprint`); in the paper this is +implicit, since `⌈P⌉` is interpreted over the variables of `P`. Its least model is a space +without probabilistic information (`ProbSpace.trivialOn`). + ## Expressions Expressions are shallowly embedded as functions `Mem → Option Val`, which need not be From 6f4b9c55d88f1b0ab8716aec9431f4878058a7d1 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 30 Sep 2026 11:08:46 +0000 Subject: [PATCH 08/10] Outcome conjunctions range over countable index types MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `ProbSpace.sum` requires its summands to have pairwise disjoint (and nonempty) sets of outcomes in `ℕ`. Over an uncountable index type no such family exists, so `⨁[ξ] φ` and `& φ` were unsatisfiable there. They now require `[Countable ι]`, which holds for all index types used in practice (values, booleans, finite sets of biases, ranks), and which allows summands to be moved to disjoint parts of `ℕ` by an injection. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_019Gipsr3EwstFw5DuwGNoug --- DESIGN.md | 2 ++ PcolIris/Examples/EntropyMixer.lean | 2 +- PcolIris/Examples/VonNeumann.lean | 12 ++++++------ PcolIris/Logic/WeakestPre.lean | 6 +++--- PcolIris/OProp/Laws.lean | 20 ++++++++++---------- PcolIris/OProp/OProp.lean | 7 +++++-- 6 files changed, 27 insertions(+), 22 deletions(-) diff --git a/DESIGN.md b/DESIGN.md index b00a371..afa954a 100644 --- a/DESIGN.md +++ b/DESIGN.md @@ -23,6 +23,8 @@ Consequences: disjoint sets of memories. The branches of a sum are therefore always distinguishable, and the partitioning side conditions of the paper (`ψ ⇒ ⌈e ↦ X⌉` in `Split1`, `NSplit1` and `Exists`, and in the precision rule for `⨁`) are not needed. +- Outcome conjunctions `⨁[ξ] φ` and `& φ` range over countable index types, so that the + summands can always be given disjoint sets of outcomes. - The product `𝓟 ⊗ 𝓠` encodes pairs of outcomes with `Nat.pairEquiv`, so it is commutative and associative only up to relabeling. The order `𝓟 ≤ 𝓠` therefore allows a measure-preserving relabeling of the outcomes (`ProbSpace.Relabels`), and compares the diff --git a/PcolIris/Examples/EntropyMixer.lean b/PcolIris/Examples/EntropyMixer.lean index 9d13da0..c9ae8ad 100644 --- a/PcolIris/Examples/EntropyMixer.lean +++ b/PcolIris/Examples/EntropyMixer.lean @@ -252,7 +252,7 @@ abbrev Bit : Set Val := {0, 1} /-- A nondeterministic choice between (identical) postconditions of the shape "weakest precondition, and the invariant holds" can be collapsed: the invariant is precise, and the postcondition `ψ` of the weakest precondition is precise as well. -/ -lemma collapse_post {F : ProbSpace → Prop} {ι : Type} {c : Cmd Act} : +lemma collapse_post {F : ProbSpace → Prop} {ι : Type} [Countable ι] {c : Cmd Act} : OProp.nondet (fun (_ : ι) => iprop(wp_base 𝓘 F c ψ ∗ ⌈𝓘.to_MProp⌉)) ⊢ iprop(wp_base 𝓘 F c ψ ∗ ⌈𝓘.to_MProp⌉) := Iris.BI.Entails.trans (OProp.nondet_distrib' _ _ (Precise.sure (Inv.footprint 𝓘) 𝓘.dom_finite)) diff --git a/PcolIris/Examples/VonNeumann.lean b/PcolIris/Examples/VonNeumann.lean index c9a1697..2f251f7 100644 --- a/PcolIris/Examples/VonNeumann.lean +++ b/PcolIris/Examples/VonNeumann.lean @@ -269,7 +269,7 @@ nondeterministic mixture. We therefore introduce convexity and derive the corre rule from `wp_nsplit`. -/ /-- An assertion is convex when it is closed under probabilistic mixtures. -/ -def Convex (ψ : OProp) : Prop := ∀ {ι : Type} (ξ : PMF ι), (⨁[ξ] (fun (_ : ι) => ψ)) ⊢ ψ +def Convex (ψ : OProp) : Prop := ∀ {ι : Type} [Countable ι] (ξ : PMF ι), (⨁[ξ] (fun (_ : ι) => ψ)) ⊢ ψ /-- A precise assertion is convex. -/ lemma Convex.of_precise {ψ : OProp} (h : ψ.Precise) : Convex ψ := fun _ ↦ OProp.oplus_collapse h @@ -286,14 +286,14 @@ lemma Convex.sep_precise {φ ψ : OProp} (hφ : Convex φ) (hψ : ψ.Precise) : (Iris.BI.sep_mono_left (hφ ξ)) /-- A nondeterministic choice between copies of a convex assertion collapses. -/ -lemma nondet_collapse_convex {ι : Type} {ψ : OProp} (h : Convex ψ) : +lemma nondet_collapse_convex {ι : Type} [Countable ι] {ψ : OProp} (h : Convex ψ) : OProp.nondet (fun (_ : ι) ↦ ψ) ⊢ ψ := by rintro P ⟨ξ, hξ⟩ exact h ξ P hξ /-- **The `NSplit2` rule**: a nondeterministic choice in the precondition can be analysed branch by branch, provided the postcondition is convex. -/ -lemma wp_nsplit2 {ι : Type} {ψ : OProp} {J : Inv} {F : ProbSpace → Prop} {c : Cmd Act} +lemma wp_nsplit2 {ι : Type} [Countable ι] {ψ : OProp} {J : Inv} {F : ProbSpace → Prop} {c : Cmd Act} (h : Convex ψ) : OProp.nondet (fun (_ : ι) ↦ wp_base J F c ψ) ⊢ wp_base J F c ψ := Iris.BI.Entails.trans wp_nsplit (wp_conseq (nondet_collapse_convex h)) @@ -340,14 +340,14 @@ same defect that the development itself documents for `sum_prod_distribute`. -/ /-- **Introduction of a nondeterministic choice**: every branch of a nondeterministic choice entails the choice itself. (In the semantics of the paper `&` is a union of sets of probability spaces, so this is immediate.) -/ -lemma nondet_intro {iota : Type} {phi : iota → OProp} (i : iota) : phi i ⊢ OProp.nondet phi := +lemma nondet_intro {iota : Type} [Countable iota] {phi : iota → OProp} (i : iota) : phi i ⊢ OProp.nondet phi := sorry /-- Nondeterministic choices are convex: a mixture of unions of mixtures is again one. -/ -lemma Convex.nondet {iota : Type} {phi : iota → OProp} : Convex (OProp.nondet phi) := sorry +lemma Convex.nondet {iota : Type} [Countable iota] {phi : iota → OProp} : Convex (OProp.nondet phi) := sorry /-- A probabilistic mixture of convex assertions is convex. -/ -lemma Convex.oplus {iota : Type} {xi : PMF iota} {phi : iota → OProp} +lemma Convex.oplus {iota : Type} [Countable iota] {xi : PMF iota} {phi : iota → OProp} (h : ∀ i, Convex (phi i)) : Convex (⨁[xi] phi) := sorry /-- **Weakening of the probability of a two-branch mixture**, i.e. the passage from the diff --git a/PcolIris/Logic/WeakestPre.lean b/PcolIris/Logic/WeakestPre.lean index f131639..7d3c503 100644 --- a/PcolIris/Logic/WeakestPre.lean +++ b/PcolIris/Logic/WeakestPre.lean @@ -150,7 +150,7 @@ lemma wp_par {𝓘 : Inv} {c₁ c₂ : Cmd Act} {ψ₁ ψ₂ : OProp} /- STRUCTURAL RULES -/ -variable {ι : Type} {𝓘 : Inv} {F : ProbSpace → Prop} {c : Cmd Act} {ξ : PMF ι} {φ ψ : OProp} +variable {ι : Type} [Countable ι] {𝓘 : Inv} {F : ProbSpace → Prop} {c : Cmd Act} {ξ : PMF ι} {φ ψ : OProp} lemma wp_conseq (h : φ ⊢ ψ) : wp_base 𝓘 F c φ ⊢ wp_base 𝓘 F c ψ := by intro 𝓟 hc μ 𝓟fr 𝓙 hF hf ν hν @@ -202,11 +202,11 @@ lemma wp_assign_pres {𝓘 : Inv} {F : ProbSpace → Prop} (x : Var) (e : Expr) If the postcondition is precise, then it is enough to establish the weakest precondition in each branch of a nondeterministic choice. -/ -lemma wp_nondet {κ : Type} {ψ : OProp} (h : ψ.Precise) : +lemma wp_nondet {κ : Type} [Countable κ] {ψ : OProp} (h : ψ.Precise) : OProp.nondet (fun (_ : κ) => wp_base 𝓘 F c ψ) ⊢ wp_base 𝓘 F c ψ := Iris.BI.Entails.trans wp_nsplit (wp_conseq (OProp.nondet_collapse h)) -lemma wp_exists {ι : Type} {P : ι → MProp} : +lemma wp_exists {ι : Type} [Countable ι] {P : ι → MProp} : ((& fun i ↦ ⌈P i⌉) -∗ wp_base 𝓘 F c ψ) ⊢ ⌈ iprop( ∃ i, P i ) ⌉ -∗ wp_weak 𝓘 c ψ := by sorry diff --git a/PcolIris/OProp/Laws.lean b/PcolIris/OProp/Laws.lean index e31d0b1..a0d8f77 100644 --- a/PcolIris/OProp/Laws.lean +++ b/PcolIris/OProp/Laws.lean @@ -89,7 +89,7 @@ lemma sure_sep {P Q : MProp} : · exact sure_sep_intro /-- A frame can be pushed into the branches of an outcome conjunction. -/ -lemma oplus_distrib {ι : Type} (ξ : PMF ι) (φ : ι → OProp) (ψ : OProp) : +lemma oplus_distrib {ι : Type} [Countable ι] (ξ : PMF ι) (φ : ι → OProp) (ψ : OProp) : (⨁[ ξ ] φ) ∗ ψ ⊢ ⨁[ ξ ] fun v ↦ iprop(φ v ∗ ψ) := by rintro 𝓟 ⟨m₁, m₂, hd, hle, ⟨𝓠, V, hdsj, hdom, hsum, hφ⟩, hψ⟩ have hV : V ⊆ m₁.dom := ProbSpace.dom_mono hsum @@ -99,7 +99,7 @@ lemma oplus_distrib {ι : Type} (ξ : PMF ι) (φ : ι → OProp) (ψ : OProp) : ((ProbSpace.product_mono_left hsum hd).trans hle) · exact ⟨𝓠 v, m₂, (hdom v).symm ▸ hd.mono_left hV, le_refl _, hφ v hv, hψ⟩ -lemma oplus_distrib' {ι : Type} (ξ : PMF ι) (φ : ι → OProp) (ψ : OProp) (h : ψ.Precise) : +lemma oplus_distrib' {ι : Type} [Countable ι] (ξ : PMF ι) (φ : ι → OProp) (ψ : OProp) (h : ψ.Precise) : (⨁[ ξ ] fun v ↦ iprop(φ v ∗ ψ)) ⊢ (⨁[ ξ ] φ) ∗ ψ := by sorry @@ -110,24 +110,24 @@ lemma oplus_weaken {ξ : PMF Val} {φ ψ : Val → OProp} (h : ∀ v ∈ ξ.supp intro v hv; exact h v hv (𝓠 v) <| hφ v hv /-- `oplus_weaken`, for an arbitrary index type. -/ -lemma oplus_weaken' {ι : Type} {ξ : PMF ι} {φ ψ : ι → OProp} +lemma oplus_weaken' {ι : Type} [Countable ι] {ξ : PMF ι} {φ ψ : ι → OProp} (h : ∀ v ∈ ξ.support, φ v ⊢ ψ v) : (⨁[ξ] φ) ⊢ ⨁[ξ] ψ := by intro 𝓟 ⟨𝓠, V, hdsj, hdom, hsum, hφ⟩ exact ⟨𝓠, V, hdsj, hdom, hsum, fun v hv ↦ h v hv (𝓠 v) (hφ v hv)⟩ /-- Nondeterministic choice is monotone. -/ -lemma nondet_weaken {ι : Type} {φ ψ : ι → OProp} (h : ∀ i, φ i ⊢ ψ i) : (& φ) ⊢ & ψ := by +lemma nondet_weaken {ι : Type} [Countable ι] {φ ψ : ι → OProp} (h : ∀ i, φ i ⊢ ψ i) : (& φ) ⊢ & ψ := by rintro 𝓟 ⟨ξ, hξ⟩ exact ⟨ξ, oplus_weaken' (fun v _ ↦ h v) 𝓟 hξ⟩ /-- A frame can be pushed into the branches of a nondeterministic choice. -/ -lemma nondet_distrib {ι : Type} (φ : ι → OProp) (ψ : OProp) : +lemma nondet_distrib {ι : Type} [Countable ι] (φ : ι → OProp) (ψ : OProp) : iprop((& φ) ∗ ψ) ⊢ & fun v ↦ iprop(φ v ∗ ψ) := by rintro 𝓟 ⟨𝓟₁, 𝓟₂, hdisj, hle, ⟨ξ, hξ⟩, hψ⟩ exact ⟨ξ, oplus_distrib ξ φ ψ 𝓟 ⟨𝓟₁, 𝓟₂, hdisj, hle, hξ, hψ⟩⟩ /-- A precise frame can be pulled out of the branches of a nondeterministic choice. -/ -lemma nondet_distrib' {ι : Type} (φ : ι → OProp) (ψ : OProp) (h : ψ.Precise) : +lemma nondet_distrib' {ι : Type} [Countable ι] (φ : ι → OProp) (ψ : OProp) (h : ψ.Precise) : (& fun v ↦ iprop(φ v ∗ ψ)) ⊢ iprop((& φ) ∗ ψ) := by rintro 𝓟 ⟨ξ, hξ⟩ obtain ⟨𝓟₁, 𝓟₂, hdisj, hle, h₁, h₂⟩ := oplus_distrib' ξ φ ψ h 𝓟 hξ @@ -140,7 +140,7 @@ probabilistic sum satisfies the precise assertion `ψ`, then so does the sum its This is the special case of `oplus_distrib'` where the family is the unit of the separating conjunction. -/ -lemma oplus_collapse {ι : Type} {ξ : PMF ι} {ψ : OProp} (h : ψ.Precise) : +lemma oplus_collapse {ι : Type} [Countable ι] {ξ : PMF ι} {ψ : OProp} (h : ψ.Precise) : (⨁[ξ] fun _ ↦ ψ) ⊢ ψ := by refine Iris.BI.Entails.trans (oplus_weaken' (φ := fun _ ↦ ψ) (ψ := fun _ ↦ iprop(Iris.BI.BIBase.emp ∗ ψ)) (fun _ _ ↦ Iris.BI.emp_sep.2)) ?_ @@ -148,7 +148,7 @@ lemma oplus_collapse {ι : Type} {ξ : PMF ι} {ψ : OProp} (h : ψ.Precise) : Iris.BI.sep_elim_right /-- A precise assertion is closed under nondeterministic mixtures. -/ -lemma nondet_collapse {ι : Type} {ψ : OProp} (h : ψ.Precise) : nondet (fun (_ : ι) => ψ) ⊢ ψ := by +lemma nondet_collapse {ι : Type} [Countable ι] {ψ : OProp} (h : ψ.Precise) : nondet (fun (_ : ι) => ψ) ⊢ ψ := by rintro 𝓟 ⟨ξ, hξ⟩ exact oplus_collapse h 𝓟 hξ @@ -156,7 +156,7 @@ lemma nondet_collapse {ι : Type} {ψ : OProp} (h : ψ.Precise) : nondet (fun (_ Reindexing a probabilistic sum along a bijection of the index type that preserves the distribution. -/ -lemma oplus_reindex {ι : Type} {ξ : PMF ι} (e : ι ≃ ι) (hξ : ∀ i, ξ (e i) = ξ i) +lemma oplus_reindex {ι : Type} [Countable ι] {ξ : PMF ι} (e : ι ≃ ι) (hξ : ∀ i, ξ (e i) = ξ i) (φ : ι → OProp) : (⨁[ξ] fun v ↦ φ (e v)) ⊢ ⨁[ξ] φ := by rintro 𝓟 ⟨𝓠, V, hdsj, hdom, hsum, hφ⟩ refine ⟨fun w ↦ 𝓠 (e.symm w), V, ?_, fun i ↦ hdom _, ?_, ?_⟩ @@ -285,7 +285,7 @@ lemma sep {φ ψ : OProp} (hφ : φ.Precise) (hψ : ψ.Precise) : iprop(φ ∗ exact (ProbSpace.product_mono ((hP₁ n₁).mpr hn₁) ((hP₂ n₂).mpr hn₂) (hdn.mono_right (ProbSpace.dom_mono ((hP₂ n₂).mpr hn₂)))).trans hle -lemma oplus {ι : Type} {ξ : PMF ι} {φ : ι → OProp} (h : ∀ v ∈ ξ.support, (φ v).Precise) : +lemma oplus {ι : Type} [Countable ι] {ξ : PMF ι} {φ : ι → OProp} (h : ∀ v ∈ ξ.support, (φ v).Precise) : (⨁[ξ] φ).Precise := by sorry end Precise diff --git a/PcolIris/OProp/OProp.lean b/PcolIris/OProp/OProp.lean index 9926deb..7458520 100644 --- a/PcolIris/OProp/OProp.lean +++ b/PcolIris/OProp/OProp.lean @@ -227,7 +227,10 @@ models of `φ` are exactly the spaces above some space `𝓟`. -/ def Precise (φ : OProp) : Prop := ∀ 𝓠, φ 𝓠 → ∃ 𝓟 : ProbSpace, ∀ 𝓠', 𝓟 ≤ 𝓠' ↔ φ 𝓠' -def oplus {ι : Type} (ξ : PMF ι) (φ : ι → OProp) : OProp where +/-- The outcome conjunction `⨁[ξ] φ`: the space is (at least) a `ξ`-weighted sum of spaces +satisfying the `φ v`. The index type is countable, so that the summands can always be given +disjoint sets of outcomes. -/ +def oplus {ι : Type} [Countable ι] (ξ : PMF ι) (φ : ι → OProp) : OProp where prop 𝓟 := ∃ 𝓠 V h hd, ProbSpace.sum ξ 𝓠 V h hd ≤ 𝓟 ∧ ∀ v ∈ ξ.support, φ v (𝓠 v) @@ -240,7 +243,7 @@ def distributed_as (e : Expr) (ξ : PMF Val) : OProp := infixl:70 " ~ " => distributed_as -def nondet {ι : Type} (φ : ι → OProp) : OProp where +def nondet {ι : Type} [Countable ι] (φ : ι → OProp) : OProp where prop 𝓟 := ∃ ξ : PMF ι, oplus ξ φ 𝓟 upcl := fun hle ⟨ξ, h⟩ ↦ ⟨ξ, (oplus ξ φ).mono hle h⟩ From 5ae36b7a31cf788bc896102ceb9afaa325b5e5fd Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 30 Sep 2026 11:10:12 +0000 Subject: [PATCH 09/10] Sums: shifting spaces to disjoint outcomes, and monotonicity (Lemma B.5) * `ProbSpace.shift p c` renames the outcome `n` of `p` to the pair `(c, n)`. It carries the same information as `p` (`shift_le`, `le_shift`), and shifts by different `c` have disjoint supports (`disjoint_support_shift`), so the summands of an outcome conjunction can always be made disjoint. * `ProbSpace.sum_mono` (Lemma B.5): a sum grows when each summand of positive weight grows. The relabeling of the sum is assembled from the relabelings of the summands, which is possible because the summands have disjoint supports. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_019Gipsr3EwstFw5DuwGNoug --- PcolIris/OProp/SumLaws.lean | 177 ++++++++++++++++++++++++++++++++++++ 1 file changed, 177 insertions(+) create mode 100644 PcolIris/OProp/SumLaws.lean diff --git a/PcolIris/OProp/SumLaws.lean b/PcolIris/OProp/SumLaws.lean new file mode 100644 index 0000000..49da442 --- /dev/null +++ b/PcolIris/OProp/SumLaws.lean @@ -0,0 +1,177 @@ +/- +Laws of sums of probability spaces: moving a space to a chosen part of the outcomes +(`ProbSpace.shift`), and monotonicity of sums (Lemma B.5 of the paper). +-/ +import PcolIris.OProp.ProductLaws + +namespace Pcol + +open MeasureTheory + +namespace ProbSpace + +/-! ### Supports -/ + +lemma meas_compl_support (p : ProbSpace) : p.meas p.supportᶜ = 0 := by + rw [measure_compl (support_measurableSet p) (measure_ne_top _ _), measure_support p, + measure_univ, tsub_self] + +lemma meas_inter_support (p : ProbSpace) (A : Set ℕ) : + (@ProbabilityMeasure.toMeasure ℕ p.mspace p.μ) (A ∩ p.support) = + (@ProbabilityMeasure.toMeasure ℕ p.mspace p.μ) A := + measure_inter_conull (meas_compl_support p) + +/-! ### Shifting a space to the outcomes `(c, n)` -/ + +/-- The encoding of the outcome `n` in the `c`-th copy of `ℕ`. -/ +def shiftMap (c : ℕ) (n : ℕ) : ℕ := Nat.pairEquiv (c, n) + +lemma shiftMap_injective (c : ℕ) : Function.Injective (shiftMap c) := by + intro n n' h + have := congrArg Prod.snd (Nat.pairEquiv.injective h) + exact this + +/-- The space `p`, with its outcome `n` renamed to `shiftMap c n`. -/ +noncomputable def shift (p : ProbSpace) (c : ℕ) : ProbSpace where + mspace := p.mspace.map (shiftMap c) + μ := ⟨@Measure.map ℕ ℕ p.mspace (p.mspace.map (shiftMap c)) (shiftMap c) p.meas, by + constructor + rw [@Measure.map_apply ℕ ℕ p.mspace (p.mspace.map (shiftMap c)) p.meas (shiftMap c) + (measurable_iff_le_map.mpr le_rfl) Set.univ MeasurableSet.univ, Set.preimage_univ] + exact @measure_univ ℕ p.mspace p.meas p.μ.2⟩ + dom := p.dom + state m := p.state (Nat.pairEquiv.symm m).2 + dom_valid _ := p.dom_valid _ + complete := by + constructor + intro s hs + have hle := @Measure.le_map_apply ℕ ℕ p.mspace (p.mspace.map (shiftMap c)) p.meas + (shiftMap c) ⟨shiftMap c, measurable_iff_le_map.mpr le_rfl, Filter.EventuallyEq.rfl⟩ s + have h0 : p.meas (shiftMap c ⁻¹' s) = 0 := le_antisymm (hs ▸ hle) bot_le + exact p.complete.out _ h0 + +lemma shift_measurableSet {p : ProbSpace} {c : ℕ} {E : Set ℕ} : + (p.shift c).mspace.MeasurableSet' E ↔ p.mspace.MeasurableSet' (shiftMap c ⁻¹' E) := + Iff.rfl + +lemma shift_meas (p : ProbSpace) (c : ℕ) {E : Set ℕ} + (hE : (p.shift c).mspace.MeasurableSet' E) : (p.shift c).meas E = p.meas (shiftMap c ⁻¹' E) := + @Measure.map_apply ℕ ℕ p.mspace (p.mspace.map (shiftMap c)) p.meas (shiftMap c) + (measurable_iff_le_map.mpr le_rfl) E hE + +lemma shift_state (p : ProbSpace) (c n : ℕ) : (p.shift c).state (shiftMap c n) = p.state n := by + change p.state (Nat.pairEquiv.symm (Nat.pairEquiv (c, n))).2 = p.state n + rw [Equiv.symm_apply_apply] + +/-- The outcomes of a shifted space lie in the `c`-th copy of `ℕ`. -/ +lemma support_shift_subset (p : ProbSpace) (c : ℕ) : + (p.shift c).support ⊆ Set.range (shiftMap c) := by + have hm : (p.shift c).mspace.MeasurableSet' (Set.range (shiftMap c)) := by + rw [shift_measurableSet, Set.preimage_range]; exact @MeasurableSet.univ ℕ p.mspace + refine support_subset hm ?_ + rw [shift_meas p c hm, Set.preimage_range] + exact measure_univ + +lemma disjoint_support_shift (p q : ProbSpace) {c c' : ℕ} (h : c ≠ c') : + Disjoint (p.shift c).support (q.shift c').support := by + refine Set.disjoint_left.mpr fun m hm hm' ↦ ?_ + obtain ⟨n, rfl⟩ := support_shift_subset p c hm + obtain ⟨n', hn'⟩ := support_shift_subset q c' hm' + exact h (congrArg Prod.fst (Nat.pairEquiv.injective hn')).symm + +lemma shift_le (p : ProbSpace) (c : ℕ) : p.shift c ≤ p := by + refine ⟨shiftMap c, fun E hE ↦ hE, fun E hE ↦ ?_, le_rfl, fun n _ ↦ le_of_eq (shift_state p c n)⟩ + refine ENNReal.coe_injective ?_ + rw [prob_coe, prob_coe] + exact (shift_meas p c hE).symm + +lemma le_shift (p : ProbSpace) (c : ℕ) : p ≤ p.shift c := by + refine ⟨fun m ↦ (Nat.pairEquiv.symm m).2, fun E hE ↦ ?_, fun E hE ↦ ?_, le_rfl, + fun m _ ↦ le_refl _⟩ + · change p.mspace.MeasurableSet' (shiftMap c ⁻¹' ((fun m ↦ (Nat.pairEquiv.symm m).2) ⁻¹' E)) + convert hE using 1 + ext n; simp [shiftMap] + · have hE' : (p.shift c).mspace.MeasurableSet' ((fun m ↦ (Nat.pairEquiv.symm m).2) ⁻¹' E) := by + change p.mspace.MeasurableSet' (shiftMap c ⁻¹' ((fun m ↦ (Nat.pairEquiv.symm m).2) ⁻¹' E)) + convert hE using 1 + ext n; simp [shiftMap] + refine ENNReal.coe_injective ?_ + rw [prob_coe, prob_coe] + change (p.shift c).meas _ = p.meas E + rw [shift_meas p c hE'] + congr 1 + ext n; simp [shiftMap] + +/-! ### Monotonicity of sums (Lemma B.5) -/ + +section SumMono + +variable {ι : Type} {ξ : PMF ι} + +lemma sumState_of_mem {𝓟 : ι → ProbSpace} {V : Set Var} + (h : ∀ {i j : ι}, i ≠ j → Disjoint (𝓟 i).support (𝓟 j).support) {v : ι} {n : ℕ} + (hn : n ∈ (𝓟 v).support) : sumState 𝓟 V n = (𝓟 v).state n := by + classical + have hex : ∃ i, n ∈ (𝓟 i).support := ⟨v, hn⟩ + rw [sumState, dif_pos hex] + have : hex.choose = v := by + by_contra hne; exact Set.disjoint_left.mp (h hne) hex.choose_spec hn + rw [this] + +/-- Sums are monotone: if each summand of positive weight grows, then so does the sum. -/ +theorem sum_mono {𝓟 𝓠 : ι → ProbSpace} {V W : Set Var} + (hP : ∀ {i j : ι}, i ≠ j → Disjoint (𝓟 i).support (𝓟 j).support) + (hQ : ∀ {i j : ι}, i ≠ j → Disjoint (𝓠 i).support (𝓠 j).support) + (hdP : ∀ i, (𝓟 i).dom = V) (hdQ : ∀ i, (𝓠 i).dom = W) (hVW : V ⊆ W) + (h : ∀ v, ξ v ≠ 0 → 𝓟 v ≤ 𝓠 v) : sum ξ 𝓟 V hP hdP ≤ sum ξ 𝓠 W hQ hdQ := by + classical + choose g hg using h + have hgeq : ∀ a b (e : a = b) (ha : ξ a ≠ 0) (hb : ξ b ≠ 0) (n : ℕ), g a ha n = g b hb n := by + intro a b e; subst e; intros; rfl + let G : ℕ → ℕ := fun n ↦ + if hex : ∃ v, ξ v ≠ 0 ∧ n ∈ (𝓠 v).support then g hex.choose hex.choose_spec.1 n else 0 + have hG : ∀ v (hv : ξ v ≠ 0), ∀ n ∈ (𝓠 v).support, G n = g v hv n := by + intro v hv n hn + have hex : ∃ v, ξ v ≠ 0 ∧ n ∈ (𝓠 v).support := ⟨v, hv, hn⟩ + simp only [G, dif_pos hex] + refine hgeq _ _ ?_ _ _ n + by_contra hne; exact Set.disjoint_left.mp (hQ hne) hex.choose_spec.2 hn + have hpre : ∀ v (hv : ξ v ≠ 0) (E : Set ℕ), + G ⁻¹' E ∩ (𝓠 v).support = g v hv ⁻¹' (E ∩ (𝓟 v).support) ∩ (𝓠 v).support := by + intro v hv E; ext n + constructor + · rintro ⟨hE, hn⟩ + refine ⟨⟨?_, (hg v hv).mem_support hn⟩, hn⟩ + rw [← hG v hv n hn]; exact hE + · rintro ⟨⟨hE, -⟩, hn⟩ + exact ⟨by rw [Set.mem_preimage, hG v hv n hn]; exact hE, hn⟩ + have hmeas : ∀ E, (sumMSpace ξ 𝓟).MeasurableSet' E → + (sumMSpace ξ 𝓠).MeasurableSet' (G ⁻¹' E) := by + intro E hE v hv + rw [hpre v hv E] + exact @MeasurableSet.inter ℕ (𝓠 v).mspace _ _ ((hg v hv).mspace _ (hE v hv)) + (support_measurableSet _) + refine ⟨G, hmeas, fun E hE ↦ ?_, hVW, fun n hn ↦ ?_⟩ + · refine ENNReal.coe_injective ?_ + rw [prob_coe, prob_coe] + change sumMeasure ξ 𝓠 (G ⁻¹' E) = sumMeasure ξ 𝓟 E + rw [sumMeasure_apply ξ 𝓠 (hmeas E hE), sumMeasure_apply ξ 𝓟 hE, sumMeasureFun, + sumMeasureFun] + refine tsum_congr fun v ↦ ?_ + by_cases hv : ξ v = 0 + · simp [hv] + · congr 1 + rw [← prob_coe, ← prob_coe, ← ENNReal.coe_inj.mpr ((hg v hv).μ _ (hE v hv)), prob_coe, + prob_coe, hpre v hv E, meas_inter_support] + · rw [support_sum] at hn + simp only [Set.mem_iUnion, Set.mem_setOf_eq, exists_prop] at hn + obtain ⟨v, hv, hn⟩ := hn + change sumState 𝓟 V (G n) ≤ sumState 𝓠 W n + rw [sumState_of_mem hQ hn, hG v hv n hn, sumState_of_mem hP ((hg v hv).mem_support hn)] + exact (hg v hv).state n hn + +end SumMono + +end ProbSpace + +end Pcol From 624f94e51de4ed1a92c88309f735cc0e81f53038 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 30 Sep 2026 11:11:56 +0000 Subject: [PATCH 10/10] Precision of outcome conjunctions MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The summands of a sum own the same variables, so the precision rule for `⨁` needs the least models of the branches to own the same variables. `PreciseDom φ V` is precision where the least model owns exactly `V`; `⌈P⌉` with footprint `V` has it (`Precise.sureDom`), and so does `⨁[ξ] φ` when every branch does (`Precise.oplusDom`). The least model of the outcome conjunction is the sum of the least models of the branches, shifted to disjoint outcomes; minimality follows from monotonicity of sums. As explained in DESIGN.md, the indexed model makes the partitioning side condition of the paper's rule unnecessary. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_019Gipsr3EwstFw5DuwGNoug --- PcolIris/Examples/EntropyMixer.lean | 4 +-- PcolIris/Examples/VonNeumann.lean | 7 +++-- PcolIris/OProp/Laws.lean | 46 +++++++++++++++++++++++++---- PcolIris/OProp/OProp.lean | 9 ++++++ 4 files changed, 56 insertions(+), 10 deletions(-) diff --git a/PcolIris/Examples/EntropyMixer.lean b/PcolIris/Examples/EntropyMixer.lean index c9ae8ad..718ee66 100644 --- a/PcolIris/Examples/EntropyMixer.lean +++ b/PcolIris/Examples/EntropyMixer.lean @@ -72,8 +72,8 @@ lemma inv_of_y_eq (v : Val) (hv : v = 0 ∨ v = 1) : /-- The postcondition `ψ` is precise: it is a probabilistic sum of the (precise) assertions `⌈$"z" == v⌉`. -/ -lemma ψ_precise : ψ.Precise := Precise.oplus fun _ _ ↦ - Precise.sure (MProp.Footprint.var_equals_literal _ _) (Set.finite_singleton _) +lemma ψ_precise : ψ.Precise := (Precise.oplusDom fun _ _ ↦ + Precise.sureDom (MProp.Footprint.var_equals_literal _ _) (Set.finite_singleton _)).precise /-- The unit of the separating conjunction is precise. -/ lemma emp_precise : (Iris.BI.BIBase.emp : OProp).Precise := diff --git a/PcolIris/Examples/VonNeumann.lean b/PcolIris/Examples/VonNeumann.lean index 2f251f7..6247bf6 100644 --- a/PcolIris/Examples/VonNeumann.lean +++ b/PcolIris/Examples/VonNeumann.lean @@ -177,9 +177,10 @@ lemma guard_true : exact MProp.upClose_of ⟨by rw [h]; rfl, by rw [h]; rfl⟩ /-- `φ₀` is precise. -/ -lemma phi0_precise : phi0.Precise := Precise.oplus fun _ _ ↦ - Precise.sure ((MProp.Footprint.var_equals_literal _ _).and - (MProp.Footprint.var_equals_literal _ _)) ((Set.finite_singleton _).union (Set.finite_singleton _)) +lemma phi0_precise : phi0.Precise := (Precise.oplusDom fun _ _ ↦ + Precise.sureDom ((MProp.Footprint.var_equals_literal _ _).and + (MProp.Footprint.var_equals_literal _ _)) + ((Set.finite_singleton _).union (Set.finite_singleton _))).precise /-- After the loop, `x` is a fair coin flip. -/ lemma phi0_fair : phi0 ⊢ ($"x") ~ Bern 0.5 := diff --git a/PcolIris/OProp/Laws.lean b/PcolIris/OProp/Laws.lean index a0d8f77..c680e83 100644 --- a/PcolIris/OProp/Laws.lean +++ b/PcolIris/OProp/Laws.lean @@ -2,6 +2,7 @@ import PcolIris.OProp.OProp import PcolIris.OProp.ProbSpaceLemmas import PcolIris.OProp.ProductLaws import PcolIris.OProp.TrivialSpace +import PcolIris.OProp.SumLaws namespace Pcol @@ -227,8 +228,8 @@ namespace Precise fixed finite set of variables (in the paper, `⌈P⌉` is interpreted over the variables of `P`). Its least model records which memories over those variables are possible, but no probabilities. -/ -lemma sure {P : MProp} {V : Set Var} (hP : P.Footprint V) (hV : V.Finite) : - (OProp.sure P).Precise := by +lemma sureDom {P : MProp} {V : Set Var} (hP : P.Footprint V) (hV : V.Finite) : + (OProp.sure P).PreciseDom V := by classical intro 𝓠₀ h₀ have hsat : ∃ σ, P σ := by @@ -253,7 +254,7 @@ lemma sure {P : MProp} {V : Set Var} (hP : P.Footprint V) (hV : V.Finite) : ((hP σ).mp hσ).2⟩ obtain ⟨f, hf⟩ := hcount.exists_eq_range ⟨_, hσS⟩ have hfS : ∀ i, f i ∈ S := fun i ↦ hf ▸ Set.mem_range_self i - refine ⟨ProbSpace.trivialOn V f (fun i ↦ (hfS i).1), fun 𝓠 ↦ ⟨?_, fun h ↦ ?_⟩⟩ + refine ⟨ProbSpace.trivialOn V f (fun i ↦ (hfS i).1), rfl, fun 𝓠 ↦ ⟨?_, fun h ↦ ?_⟩⟩ · rintro ⟨g, hg⟩ k hk exact P.upcl (hg.state k hk) (hfS (g k)).2 · obtain ⟨k0, hk0⟩ := ProbSpace.support_nonempty 𝓠 @@ -270,6 +271,10 @@ lemma sure {P : MProp} {V : Set Var} (hP : P.Footprint V) (hV : V.Finite) : rw [(hmem i hi).choose_spec] exact Mem.restrict_le _ _ +lemma sure {P : MProp} {V : Set Var} (hP : P.Footprint V) (hV : V.Finite) : + (OProp.sure P).Precise := + (sureDom hP hV).precise + /-- Separating conjunctions of precise assertions are precise: the least model is the product of the least models. -/ lemma sep {φ ψ : OProp} (hφ : φ.Precise) (hψ : ψ.Precise) : iprop(φ ∗ ψ).Precise := by @@ -285,8 +290,39 @@ lemma sep {φ ψ : OProp} (hφ : φ.Precise) (hψ : ψ.Precise) : iprop(φ ∗ exact (ProbSpace.product_mono ((hP₁ n₁).mpr hn₁) ((hP₂ n₂).mpr hn₂) (hdn.mono_right (ProbSpace.dom_mono ((hP₂ n₂).mpr hn₂)))).trans hle -lemma oplus {ι : Type} [Countable ι] {ξ : PMF ι} {φ : ι → OProp} (h : ∀ v ∈ ξ.support, (φ v).Precise) : - (⨁[ξ] φ).Precise := by sorry +/-- Outcome conjunctions of precise assertions owning the same variables are precise: the +least model is the sum of the least models of the branches (moved to disjoint outcomes). +Thanks to the indexed model, no partitioning side condition is needed. -/ +lemma oplusDom {ι : Type} [Countable ι] {ξ : PMF ι} {φ : ι → OProp} {V : Set Var} + (h : ∀ v ∈ ξ.support, (φ v).PreciseDom V) : (⨁[ξ] φ).PreciseDom V := by + classical + rintro 𝓠 ⟨𝓡, W, -, -, -, hφ⟩ + obtain ⟨v₀, hv₀⟩ := ξ.support_nonempty + have hmin : ∀ v ∈ ξ.support, ∃ 𝓟 : ProbSpace, 𝓟.dom = V ∧ ∀ 𝓠', 𝓟 ≤ 𝓠' ↔ φ v 𝓠' := + fun v hv ↦ h v hv _ (hφ v hv) + let P : ι → ProbSpace := fun v ↦ + if hv : v ∈ ξ.support then (hmin v hv).choose else (hmin v₀ hv₀).choose + have hPdom : ∀ v, (P v).dom = V := by + intro v; simp only [P]; split_ifs with hv + · exact (hmin v hv).choose_spec.1 + · exact (hmin v₀ hv₀).choose_spec.1 + have hPmin : ∀ v ∈ ξ.support, ∀ 𝓠', P v ≤ 𝓠' ↔ φ v 𝓠' := by + intro v hv; simp only [P, dif_pos hv]; exact (hmin v hv).choose_spec.2 + obtain ⟨code, hcode⟩ := Countable.exists_injective_nat ι + let S : ι → ProbSpace := fun v ↦ (P v).shift (code v) + have hSdisj : ∀ {i j : ι}, i ≠ j → Disjoint (S i).support (S j).support := + fun hij ↦ ProbSpace.disjoint_support_shift _ _ (hcode.ne hij) + have hSdom : ∀ v, (S v).dom = V := hPdom + refine ⟨ProbSpace.sum ξ S V hSdisj hSdom, rfl, fun 𝓠' ↦ ⟨fun hle ↦ ?_, ?_⟩⟩ + · refine ⟨S, V, hSdisj, hSdom, hle, fun v hv ↦ ?_⟩ + exact (hPmin v hv (S v)).mp (ProbSpace.le_shift _ _) + · rintro ⟨𝓡', W', hdisj', hdom', hsum', hφ'⟩ + have hVW : V ⊆ W' := by + rw [← hPdom v₀, ← hdom' v₀] + exact ProbSpace.dom_mono ((hPmin v₀ hv₀ _).mpr (hφ' v₀ hv₀)) + refine (ProbSpace.sum_mono hSdisj hdisj' hSdom hdom' hVW fun v hv ↦ ?_).trans hsum' + exact (ProbSpace.shift_le _ _).trans ((hPmin v (PMF.mem_support_iff _ _ |>.mpr hv) _).mpr + (hφ' v (PMF.mem_support_iff _ _ |>.mpr hv))) end Precise diff --git a/PcolIris/OProp/OProp.lean b/PcolIris/OProp/OProp.lean index 7458520..0386248 100644 --- a/PcolIris/OProp/OProp.lean +++ b/PcolIris/OProp/OProp.lean @@ -227,6 +227,15 @@ models of `φ` are exactly the spaces above some space `𝓟`. -/ def Precise (φ : OProp) : Prop := ∀ 𝓠, φ 𝓠 → ∃ 𝓟 : ProbSpace, ∀ 𝓠', 𝓟 ≤ 𝓠' ↔ φ 𝓠' +/-- Precision where the least model owns exactly the variables `V`. This is what the +precision rule for outcome conjunctions needs, since the summands of a sum own the same +variables. -/ +def PreciseDom (φ : OProp) (V : Set Var) : Prop := + ∀ 𝓠, φ 𝓠 → ∃ 𝓟 : ProbSpace, 𝓟.dom = V ∧ ∀ 𝓠', 𝓟 ≤ 𝓠' ↔ φ 𝓠' + +lemma PreciseDom.precise {φ : OProp} {V : Set Var} (h : φ.PreciseDom V) : φ.Precise := + fun 𝓠 hφ ↦ let ⟨𝓟, _, h𝓟⟩ := h 𝓠 hφ; ⟨𝓟, h𝓟⟩ + /-- The outcome conjunction `⨁[ξ] φ`: the space is (at least) a `ξ`-weighted sum of spaces satisfying the `φ v`. The index type is countable, so that the summands can always be given disjoint sets of outcomes. -/