From c240b850e9ae09020778fc6965dda374d00a8a08 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 30 Sep 2026 11:13:43 +0000 Subject: [PATCH 1/7] Prove the Skip rule MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `wp_skip` claimed `φ ⊣⊢ wp skip φ`. The reverse entailment is stronger than the paper's Skip rule, is unused, and does not hold in this model (`wp` holds vacuously of preconditions that no distribution realizes). It is now the paper's rule `φ ⊢ wp skip φ`, proved: running `skip` from `μ` produces the distributions above `μ`, and `μ` has no mass on `⊥`, so it is maximal. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_019Gipsr3EwstFw5DuwGNoug --- PcolIris/Logic/WeakestPre.lean | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/PcolIris/Logic/WeakestPre.lean b/PcolIris/Logic/WeakestPre.lean index 7d3c503..68a39fa 100644 --- a/PcolIris/Logic/WeakestPre.lean +++ b/PcolIris/Logic/WeakestPre.lean @@ -40,16 +40,16 @@ notation 𝓘 " ⊢{{" φ "}} " c " {{" ψ "}}" => φ ⊢ wp 𝓘 c ψ variable {𝓘 : Inv} {F : ProbSpace → Prop} {c : Cmd Act} +/-- The `Skip` rule. -/ lemma wp_skip (φ : OProp) : - φ ⊣⊢ wp_base 𝓘 F Cmd.skip φ := by - constructor - · intro 𝓟 hφ μ 𝓟fr 𝓙 _ hf ν hν - refine ⟨𝓟, 𝓙, ?_, hφ⟩ - rw [Cmd.withInv, Cmd.to_pom, Pom.Semantics.lin_skip, bind_pure] at hν - obtain ⟨μ, rfl⟩ := PMF.to_distr_inv hf.refines.bot_0 - have heq : ν = μ.to_distr := sorry - rwa [heq] - · intro 𝓟 hφ; sorry + φ ⊢ wp_base 𝓘 F Cmd.skip φ := by + intro 𝓟 hφ μ 𝓟fr 𝓙 _ hf ν hν + refine ⟨𝓟, 𝓙, ?_, hφ⟩ + rw [Cmd.withInv, Cmd.to_pom, Pom.Semantics.lin_skip, bind_pure] at hν + have hle : μ ≤ ν := by + have : ν ∈ (ConvexPowerset.singleton' μ).set := hν + rwa [ConvexPowerset.singleton'_set_eq] at this + rwa [← proper_dist_maximal hf.refines.bot_0 hle] lemma wp_seq {c₁ c₂ : Cmd Act} {ψ : OProp} : wp_base 𝓘 F c₁ (wp_base 𝓘 F c₂ ψ) ⊢ wp_base 𝓘 F (Cmd.seq c₁ c₂) ψ := by From 878b3ad6366a81f448f7faf051c3c369cc8875b6 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 30 Sep 2026 15:02:35 +0000 Subject: [PATCH 2/7] =?UTF-8?q?Independence=20of=20spaces=20without=20prob?= =?UTF-8?q?abilistic=20information;=20split=20=E2=8C=88P=20=E2=88=97=20Q?= =?UTF-8?q?=E2=8C=89?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * `ProbSpace.product_trivialOn_le`: a space without probabilistic information is independent of every other space: if `X ≤ Z` and the memories of `T` are restrictions of those of `Z`, then `X ⊗ T ≤ Z`. * `ProbSpace.forget Z U`: the part of `Z` over the variables `U`, keeping only which memories are possible. * `OProp.sure_sep_elim`: `⌈P ∗ Q⌉ ⊢ ⌈P⌉ ∗ ⌈Q⌉` when `P` and `Q` have footprints; the two factors are the forgotten parts of the space over the two footprints. `sure_sep` (both directions) now takes the footprints, and `MProp.Footprint.sep` gives the footprint of `P ∗ Q`. * `Mem.union_le`. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_019Gipsr3EwstFw5DuwGNoug --- PcolIris/Examples/VonNeumann.lean | 6 +- PcolIris/OProp/Laws.lean | 147 +++++++++++++++++++----------- PcolIris/OProp/TrivialSpace.lean | 82 +++++++++++++++++ PcolIris/Semantics/Mem.lean | 7 ++ 4 files changed, 188 insertions(+), 54 deletions(-) diff --git a/PcolIris/Examples/VonNeumann.lean b/PcolIris/Examples/VonNeumann.lean index 6247bf6..6147416 100644 --- a/PcolIris/Examples/VonNeumann.lean +++ b/PcolIris/Examples/VonNeumann.lean @@ -551,7 +551,11 @@ lemma wp_body_nondet {L : Finset ℚ} {F : ProbSpace → Prop} (eps : ℚ) the loop body. -/ lemma phi1_split : phi1 ⊢ iprop(⌈own ($"p'")⌉ ∗ (⌈own ($"x")⌉ ∗ ⌈own ($"y")⌉)) := Iris.BI.Entails.trans (OProp.sure_weaken phi1_resources) - (Iris.BI.Entails.trans OProp.sure_sep.1 (Iris.BI.sep_mono_right OProp.sure_sep.1)) + (Iris.BI.Entails.trans + (OProp.sure_sep (MProp.Footprint.own_var _) + ((MProp.Footprint.own_var _).sep (MProp.Footprint.own_var _) (by simp))).1 + (Iris.BI.sep_mono_right + (OProp.sure_sep (MProp.Footprint.own_var _) (MProp.Footprint.own_var _)).1)) /-- **The loop body.** Starting from the loop invariant at rank `1`, one iteration of the loop exits with probability at least `2 * eps * (1 - eps)`. -/ diff --git a/PcolIris/OProp/Laws.lean b/PcolIris/OProp/Laws.lean index c680e83..27381d5 100644 --- a/PcolIris/OProp/Laws.lean +++ b/PcolIris/OProp/Laws.lean @@ -55,6 +55,69 @@ lemma state_le_product_right {p q : ProbSpace} (hdisj : Disjoint p.dom q.dom) (n end ProbSpace +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 sep {P Q : MProp} {V W : Set Var} (hP : P.Footprint V) (hQ : Q.Footprint W) + (hVW : Disjoint V W) : iprop(P ∗ Q).Footprint (V ∪ W) := by + intro σ + constructor + · rintro ⟨σ₁, σ₂, hd, hle, h₁, h₂⟩ + have hP' : P σ := P.upcl ((Mem.le_union_left σ₁ σ₂).trans hle) h₁ + have hQ' : Q σ := Q.upcl ((Mem.le_union_right hd).trans hle) h₂ + refine ⟨Set.union_subset ((hP σ).mp hP').1 ((hQ σ).mp hQ').1, + σ.restrict V, σ.restrict W, ?_, ?_, ((hP σ).mp hP').2, ((hQ σ).mp hQ').2⟩ + · exact hVW.mono (Mem.dom_restrict_subset σ V) (Mem.dom_restrict_subset σ W) + · rw [Mem.restrict_union_restrict] + · rintro ⟨-, h⟩ + exact iprop(P ∗ Q).upcl (Mem.restrict_le σ (V ∪ W)) h + +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 OProp /-- @@ -83,11 +146,37 @@ lemma sure_sep_intro {P Q : MProp} : iprop(⌈P⌉ ∗ ⌈Q⌉) ⊢ ⌈ iprop(P · 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 - · exact sure_sep_intro +/-- A certainty about a separating conjunction can be split into independent certainties, when +the two assertions talk about fixed sets of variables: the two parts are the spaces without +probabilistic information over those variables. -/ +lemma sure_sep_elim {P Q : MProp} {V W : Set Var} (hP : P.Footprint V) (hQ : Q.Footprint W) : + ⌈ iprop(P ∗ Q) ⌉ ⊢ iprop(⌈P⌉ ∗ ⌈Q⌉) := by + intro 𝓟 h + -- The components of a memory satisfying `P ∗ Q` satisfy `P` and `Q` + have hsplit : ∀ k ∈ 𝓟.support, P (𝓟.state k) ∧ Q (𝓟.state k) := by + intro k hk + obtain ⟨σ₁, σ₂, hd, hle, h₁, h₂⟩ := h hk + exact ⟨P.upcl ((Mem.le_union_left σ₁ σ₂).trans hle) h₁, + Q.upcl ((Mem.le_union_right hd).trans hle) h₂⟩ + obtain ⟨k₀, hk₀⟩ := ProbSpace.support_nonempty 𝓟 + obtain ⟨σ₁, σ₂, hd, hle, h₁, h₂⟩ := h hk₀ + have hV : V ⊆ 𝓟.dom := by + rw [← 𝓟.dom_valid k₀]; exact ((hP _).mp (hsplit k₀ hk₀).1).1 + have hW : W ⊆ 𝓟.dom := by + rw [← 𝓟.dom_valid k₀]; exact ((hQ _).mp (hsplit k₀ hk₀).2).1 + have hVW : Disjoint V W := hd.mono ((hP _).mp h₁).1 ((hQ _).mp h₂).1 + refine ⟨ProbSpace.forget 𝓟 V hV, ProbSpace.forget 𝓟 W hW, hVW, + ProbSpace.product_forget_le (ProbSpace.forget_le 𝓟 hV) hW, fun k _ ↦ ?_, fun k _ ↦ ?_⟩ + · obtain ⟨k', hk', heq⟩ := ProbSpace.forget_state_restrict 𝓟 hV k + change P ((ProbSpace.forget 𝓟 V hV).state k) + rw [heq]; exact ((hP _).mp (hsplit k' hk').1).2 + · obtain ⟨k', hk', heq⟩ := ProbSpace.forget_state_restrict 𝓟 hW k + change Q ((ProbSpace.forget 𝓟 W hW).state k) + rw [heq]; exact ((hQ _).mp (hsplit k' hk').2).2 + +lemma sure_sep {P Q : MProp} {V W : Set Var} (hP : P.Footprint V) (hQ : Q.Footprint W) : + ⌈ iprop(P ∗ Q) ⌉ ⊣⊢ ⌈P⌉ ∗ ⌈Q⌉ := + ⟨sure_sep_elim hP hQ, sure_sep_intro⟩ /-- A frame can be pushed into the branches of an outcome conjunction. -/ lemma oplus_distrib {ι : Type} [Countable ι] (ξ : PMF ι) (φ : ι → OProp) (ψ : OProp) : @@ -173,54 +262,6 @@ lemma oplus_reindex {ι : Type} [Countable ι] {ξ : PMF ι} (e : ι ≃ ι) (h 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 diff --git a/PcolIris/OProp/TrivialSpace.lean b/PcolIris/OProp/TrivialSpace.lean index 7448461..277dbe8 100644 --- a/PcolIris/OProp/TrivialSpace.lean +++ b/PcolIris/OProp/TrivialSpace.lean @@ -64,6 +64,88 @@ lemma trivialOn_le {𝓠 : ProbSpace} (hdom : V ⊆ 𝓠.dom) (g : ℕ → ℕ) · rw [Set.preimage_empty, measure_empty, measure_empty] · rw [Set.preimage_univ, measure_univ, measure_univ] +/-! ### Independence of spaces without probabilistic information -/ + +/-- A space without probabilistic information is independent of every other space: if `X` is +below `Z`, and the memories of `T` are (almost surely) restrictions of those of `Z` to other +variables, then `X ⊗ T` is below `Z`. -/ +theorem product_trivialOn_le {X Z : ProbSpace} (hX : X ≤ Z) (hU : V ⊆ Z.dom) (t : ℕ → ℕ) + (ht : ∀ k ∈ Z.support, f (t k) ≤ Z.state k) : (X ⊗ trivialOn V f hf) ≤ Z := by + obtain ⟨g, hg⟩ := hX + haveI := isProbabilityMeasure_meas X + haveI := isProbabilityMeasure_meas (trivialOn V f hf) + have hgm : @Measurable ℕ ℕ Z.mspace X.mspace g := fun E hE ↦ hg.mspace E hE + have htm : @Measurable ℕ ℕ Z.mspace (trivialOn V f hf).mspace t := by + intro s hs + rcases trivialOn_measurableSet hs with rfl | rfl + · exact Z.mspace.measurableSet_empty + · exact @MeasurableSet.univ ℕ Z.mspace + have hmeas : @Measurable ℕ (ℕ × ℕ) Z.mspace (X.mspace.prod (trivialOn V f hf).mspace) + (fun k ↦ (g k, t k)) := + @Measurable.prodMk ℕ Z.mspace ℕ ℕ X.mspace (trivialOn V f hf).mspace g t hgm htm + have hmap : MP Z.mspace (X.mspace.prod (trivialOn V f hf).mspace) (fun k ↦ (g k, t k)) + Z.meas (@Measure.prod ℕ ℕ X.mspace (trivialOn V f hf).mspace X.meas + (trivialOn V f hf).meas) := by + refine @MeasurePreserving.mk ℕ (ℕ × ℕ) Z.mspace (X.mspace.prod (trivialOn V f hf).mspace) + _ _ _ hmeas ?_ + symm + refine @ext_of_generate_finite _ (X.mspace.prod (trivialOn V f hf).mspace) _ _ + (Set.image2 (fun x1 x2 ↦ x1 ×ˢ x2) {s | @MeasurableSet ℕ X.mspace s} + {t | @MeasurableSet ℕ (trivialOn V f hf).mspace t}) + (@generateFrom_prod ℕ ℕ X.mspace (trivialOn V f hf).mspace).symm + (@isPiSystem_prod ℕ ℕ X.mspace (trivialOn V f hf).mspace) inferInstance ?_ ?_ + · rintro _ ⟨A, hA, B, hB, rfl⟩ + rw [@Measure.map_apply ℕ (ℕ × ℕ) Z.mspace (X.mspace.prod (trivialOn V f hf).mspace) + Z.meas _ hmeas _ (@MeasurableSet.prod ℕ ℕ X.mspace (trivialOn V f hf).mspace A B hA hB), + @Measure.prod_prod ℕ ℕ X.mspace (trivialOn V f hf).mspace X.meas _ _ A B] + rcases trivialOn_measurableSet (V := V) (f := f) (hf := hf) hB with rfl | rfl + · simp + · rw [measure_univ, mul_one, Set.mk_preimage_prod, Set.preimage_univ, Set.inter_univ] + exact (hg.measurePreserving.measure_preimage + (@MeasurableSet.nullMeasurableSet ℕ X.mspace X.meas A hA)).symm + · rw [@Measure.map_apply ℕ (ℕ × ℕ) Z.mspace (X.mspace.prod (trivialOn V f hf).mspace) + Z.meas _ hmeas _ MeasurableSet.univ, Set.preimage_univ, measure_univ, measure_univ] + refine ⟨fun k ↦ Nat.pairEquiv (g k, t k), + relabels_of_measurePreserving (IsCompletionOf.product X (trivialOn V f hf)) + ((measurePreserving_pair X _).comp hmap) (Set.union_subset hg.dom hU) ?_⟩ + intro k hk + rw [product_state, Equiv.symm_apply_apply] + exact Mem.union_le (hg.state k hk) (ht k hk) + +/-- The part of `Z` over the variables `U`, forgetting all probabilistic information: its +memories are the (possible) memories of `Z`, restricted to `U`. -/ +noncomputable def forget (Z : ProbSpace) (U : Set Var) (hU : U ⊆ Z.dom) : ProbSpace := + open Classical in + trivialOn U + (fun k ↦ (Z.state (if k ∈ Z.support then k else (support_nonempty Z).some)).restrict U) + (fun k ↦ by rw [Mem.restrict_dom, Z.dom_valid]; exact Set.inter_eq_right.mpr hU) + +lemma forget_state_restrict (Z : ProbSpace) {U : Set Var} (hU : U ⊆ Z.dom) (k : ℕ) : + ∃ k' ∈ Z.support, (forget Z U hU).state k = (Z.state k').restrict U := by + classical + by_cases hk : k ∈ Z.support + · exact ⟨k, hk, by simp only [forget, trivialOn, if_pos hk]⟩ + · exact ⟨_, (support_nonempty Z).some_mem, by simp only [forget, trivialOn, if_neg hk]⟩ + +lemma forget_state_of_mem (Z : ProbSpace) {U : Set Var} (hU : U ⊆ Z.dom) {k : ℕ} + (hk : k ∈ Z.support) : (forget Z U hU).state k = (Z.state k).restrict U := by + classical + simp only [forget, trivialOn, if_pos hk] + +lemma support_forget (Z : ProbSpace) {U : Set Var} (hU : U ⊆ Z.dom) : + (forget Z U hU).support = Set.univ := support_trivialOn + +lemma forget_le (Z : ProbSpace) {U : Set Var} (hU : U ⊆ Z.dom) : forget Z U hU ≤ Z := + trivialOn_le hU id fun k hk ↦ by + change (forget Z U hU).state k ≤ _ + rw [forget_state_of_mem Z hU hk]; exact Mem.restrict_le _ _ + +lemma product_forget_le {X Z : ProbSpace} (hX : X ≤ Z) {U : Set Var} (hU : U ⊆ Z.dom) : + (X ⊗ forget Z U hU) ≤ Z := + product_trivialOn_le hX hU id fun k hk ↦ by + change (forget Z U hU).state k ≤ _ + rw [forget_state_of_mem Z hU hk]; exact Mem.restrict_le _ _ + end ProbSpace end Pcol diff --git a/PcolIris/Semantics/Mem.lean b/PcolIris/Semantics/Mem.lean index 878ee56..66a53b7 100644 --- a/PcolIris/Semantics/Mem.lean +++ b/PcolIris/Semantics/Mem.lean @@ -321,6 +321,13 @@ lemma restrict_le (σ : Mem) (X : Set Var) : σ.restrict X ≤ σ := by · rwa [restrict_apply_of_mem _ h] at hx · rw [restrict_apply_of_notMem _ h] at hx; exact absurd hx (by simp) +lemma union_le {σ₁ σ₂ σ : Mem} (h₁ : σ₁ ≤ σ) (h₂ : σ₂ ≤ σ) : (σ₁ ⊎ σ₂) ≤ σ := by + rw [le_iff] at h₁ h₂ ⊢ + intro x v hx + by_cases hs : x ∈ σ₁.dom + · rw [union_apply_of_mem_dom hs] at hx; exact h₁ x v hx + · rw [union_apply_of_notMem_dom hs] at hx; exact h₂ x v hx + end Mem end Pcol From 66cb87b5d3e89977a3600dcaf7c2c1587d7784c8 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 30 Sep 2026 15:04:27 +0000 Subject: [PATCH 3/7] Laws: a precise frame can be pulled out of an outcome conjunction MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `oplus_distrib'`: `⨁ (φ v ∗ ψ) ⊢ (⨁ φ) ∗ ψ` for precise `ψ` (the paper's law for factoring precise assertions out of outcome conjunctions). The frame is satisfied by the least model `𝓠` of `ψ` in every branch. The rest of branch `v` is completed by the variables it does not constrain (`forget`, which is independent of everything) so that all branches own the same variables, and the branches are shifted to disjoint outcomes; the product with `𝓠` is then below the original sum by distributivity and monotonicity of sums. This also proves `oplus_collapse`, `nondet_distrib'` and `nondet_collapse`, which were stated in terms of it. `ProbSpace.product_swap_right` rearranges nested products. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_019Gipsr3EwstFw5DuwGNoug --- PcolIris/OProp/Laws.lean | 64 +++++++++++++++++++++++++++++++-- PcolIris/OProp/ProductLaws.lean | 7 ++++ 2 files changed, 68 insertions(+), 3 deletions(-) diff --git a/PcolIris/OProp/Laws.lean b/PcolIris/OProp/Laws.lean index 27381d5..f71647e 100644 --- a/PcolIris/OProp/Laws.lean +++ b/PcolIris/OProp/Laws.lean @@ -189,9 +189,67 @@ lemma oplus_distrib {ι : Type} [Countable ι] (ξ : PMF ι) (φ : ι → 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} [Countable ι] (ξ : PMF ι) (φ : ι → OProp) (ψ : OProp) (h : ψ.Precise) : - (⨁[ ξ ] fun v ↦ iprop(φ v ∗ ψ)) ⊢ (⨁[ ξ ] φ) ∗ ψ := by - sorry +/-- A precise frame can be pulled out of the branches of an outcome conjunction. The frame +is satisfied by the same (least) space in every branch, and the rest of each branch, completed +by the variables it does not constrain, is independent of it. -/ +lemma oplus_distrib' {ι : Type} [Countable ι] (ξ : PMF ι) (φ : ι → OProp) (ψ : OProp) + (h : ψ.Precise) : (⨁[ ξ ] fun v ↦ iprop(φ v ∗ ψ)) ⊢ (⨁[ ξ ] φ) ∗ ψ := by + classical + rintro 𝓟 ⟨𝓡, W, hdsj, hdom, hsum, hφψ⟩ + obtain ⟨v₀, hv₀⟩ := ξ.support_nonempty + choose m₁ m₂ hd hle h₁ h₂ using hφψ + obtain ⟨𝓠, hQ⟩ := h _ (h₂ v₀ hv₀) + have hQle : ∀ v (hv : v ∈ ξ.support), 𝓠 ≤ m₂ v hv := fun v hv ↦ (hQ _).mpr (h₂ v hv) + have hsubW : ∀ v (hv : v ∈ ξ.support), (m₁ v hv).dom ∪ (m₂ v hv).dom ⊆ W := fun v hv ↦ by + rw [← hdom v]; exact ProbSpace.dom_mono (hle v hv) + have hQW : 𝓠.dom ⊆ W := + (ProbSpace.dom_mono (hQle v₀ hv₀)).trans (Set.subset_union_right.trans (hsubW v₀ hv₀)) + set D := W \ 𝓠.dom with hD + have hm₁Q : ∀ v (hv : v ∈ ξ.support), Disjoint (m₁ v hv).dom 𝓠.dom := + fun v hv ↦ (hd v hv).mono_right (ProbSpace.dom_mono (hQle v hv)) + have hm₁D : ∀ v (hv : v ∈ ξ.support), (m₁ v hv).dom ⊆ D := fun v hv x hx ↦ + ⟨Set.subset_union_left.trans (hsubW v hv) hx, Set.disjoint_left.mp (hm₁Q v hv) hx⟩ + have hDR : ∀ v, D \ ∅ ⊆ (𝓡 v).dom := fun v ↦ by + rw [hdom v, Set.diff_empty]; exact Set.diff_subset + -- In each branch, the part of the space that does not belong to the frame + let A : ∀ v, v ∈ ξ.support → ProbSpace := fun v hv ↦ + m₁ v hv ⊗ ProbSpace.forget (𝓡 v) (D \ (m₁ v hv).dom) + ((Set.diff_subset_diff_right (Set.empty_subset _)).trans (hDR v)) + have hAdom : ∀ v hv, (A v hv).dom = D := fun v hv ↦ Set.union_diff_cancel (hm₁D v hv) + have hAφ : ∀ v hv, φ v (A v hv) := fun v hv ↦ + (φ v).mono (ProbSpace.le_product_left _ _) (h₁ v hv) + have hAQ : ∀ v hv, (A v hv ⊗ 𝓠) ≤ 𝓡 v := by + intro v hv + have hF : Disjoint 𝓠.dom (D \ (m₁ v hv).dom) := + Set.disjoint_left.mpr fun x hx hx' ↦ hx'.1.2 hx + refine (ProbSpace.product_swap_right hF ?_).trans ?_ + · exact Set.disjoint_union_right.mpr ⟨hm₁Q v hv, + Set.disjoint_left.mpr fun x hx hx' ↦ hx'.2 hx⟩ + · exact ProbSpace.product_forget_le + ((ProbSpace.product_mono_right (hQle v hv) (hm₁Q v hv)).trans (hle v hv)) _ + let A' : ι → ProbSpace := fun v ↦ if hv : v ∈ ξ.support then A v hv else A v₀ hv₀ + have hA'dom : ∀ v, (A' v).dom = D := fun v ↦ by + simp only [A']; split_ifs with hv + · exact hAdom v hv + · exact hAdom v₀ hv₀ + obtain ⟨code, hcode⟩ := Countable.exists_injective_nat ι + let S : ι → ProbSpace := fun v ↦ (A' 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 = D := hA'dom + refine ⟨ProbSpace.sum ξ S D hSdisj hSdom, 𝓠, Set.disjoint_sdiff_left, ?_, + ⟨S, D, hSdisj, hSdom, le_refl _, fun v hv ↦ ?_⟩, (hQ 𝓠).mp (le_refl _)⟩ + · refine (ProbSpace.sum_product_le_sumProd ξ S 𝓠 D hSdisj hSdom).trans + ((ProbSpace.sum_mono (ProbSpace.sum_prod_disjoint 𝓠 hSdisj) hdsj + (ProbSpace.sum_prod_dom 𝓠 hSdom) hdom (Set.union_subset Set.diff_subset hQW) + fun v hv ↦ ?_).trans hsum) + have hv' : v ∈ ξ.support := (PMF.mem_support_iff _ _).mpr hv + have hA' : A' v = A v hv' := dif_pos hv' + refine (ProbSpace.product_mono_left (ProbSpace.shift_le _ _) ?_).trans ?_ + · rw [hA'dom]; exact Set.disjoint_sdiff_left + · rw [hA']; exact hAQ v hv' + · have hA' : A' v = A v hv := dif_pos hv + exact (φ v).mono (ProbSpace.le_shift _ _) (hA' ▸ hAφ v hv) lemma oplus_weaken {ξ : PMF Val} {φ ψ : Val → OProp} (h : ∀ v ∈ ξ.support, φ v ⊢ ψ v) : (⨁[ξ] φ) ⊢ ⨁[ξ] ψ := by diff --git a/PcolIris/OProp/ProductLaws.lean b/PcolIris/OProp/ProductLaws.lean index e59dc05..e262e6d 100644 --- a/PcolIris/OProp/ProductLaws.lean +++ b/PcolIris/OProp/ProductLaws.lean @@ -397,6 +397,13 @@ theorem product_assoc' (p q r : ProbSpace) : (p ⊗ (q ⊗ r)) ≤ ((p ⊗ q) Equiv.prodAssoc_apply, id_eq, Mem.union_assoc] exact le_refl _ +/-- Swapping the two right factors of a nested product. -/ +lemma product_swap_right {a b c : ProbSpace} (hbc : Disjoint b.dom c.dom) + (ha : Disjoint a.dom (b.dom ∪ c.dom)) : ((a ⊗ c) ⊗ b) ≤ ((a ⊗ b) ⊗ c) := + (product_assoc a c b).trans + ((product_mono_right (product_comm hbc) (by rwa [Set.union_comm] at ha)).trans + (product_assoc' a b c)) + /-! ### Projections and the unit -/ /-- A product carries at least the information of its left factor. -/ From bf0da41a7027176675b4980ca28b915361c8901e Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 30 Sep 2026 15:09:02 +0000 Subject: [PATCH 4/7] Point-mass sums; prove nondet_intro in the von Neumann example MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `ProbSpace.sum_pure_le`: a sum over a point mass is below its summand (the other summands are irrelevant, and the rest of the space is null). With it, `nondet_intro` (`φ i ⊢ & φ`), which the example had to assume, is proved: a space is a one-point mixture of a shifted copy of itself. The obstruction described in the example (memories compared at null outcomes, no relabeling) was removed by the new order. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_019Gipsr3EwstFw5DuwGNoug --- PcolIris/Examples/VonNeumann.lean | 13 +++++++++++-- PcolIris/OProp/SumLaws.lean | 23 +++++++++++++++++++++++ 2 files changed, 34 insertions(+), 2 deletions(-) diff --git a/PcolIris/Examples/VonNeumann.lean b/PcolIris/Examples/VonNeumann.lean index 6147416..6507119 100644 --- a/PcolIris/Examples/VonNeumann.lean +++ b/PcolIris/Examples/VonNeumann.lean @@ -341,8 +341,17 @@ 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} [Countable iota] {phi : iota → OProp} (i : iota) : phi i ⊢ OProp.nondet phi := - sorry +lemma nondet_intro {iota : Type} [Countable iota] {phi : iota → OProp} (i : iota) : + phi i ⊢ OProp.nondet phi := by + intro 𝓟 h + obtain ⟨code, hcode⟩ := Countable.exists_injective_nat iota + refine ⟨PMF.pure i, fun v ↦ 𝓟.shift (code v), 𝓟.dom, + fun hij ↦ ProbSpace.disjoint_support_shift _ _ (hcode.ne hij), fun _ ↦ rfl, ?_, ?_⟩ + · exact (ProbSpace.sum_pure_le _ _ i).trans (ProbSpace.shift_le _ _) + · intro v hv + rw [PMF.support_pure, Set.mem_singleton_iff] at hv + subst hv + exact (phi v).mono (ProbSpace.le_shift _ _) h /-- Nondeterministic choices are convex: a mixture of unions of mixtures is again one. -/ lemma Convex.nondet {iota : Type} [Countable iota] {phi : iota → OProp} : Convex (OProp.nondet phi) := sorry diff --git a/PcolIris/OProp/SumLaws.lean b/PcolIris/OProp/SumLaws.lean index 49da442..25467c1 100644 --- a/PcolIris/OProp/SumLaws.lean +++ b/PcolIris/OProp/SumLaws.lean @@ -170,6 +170,29 @@ theorem sum_mono {𝓟 𝓠 : ι → ProbSpace} {V W : Set Var} 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 +/-- A sum over a point mass is (below) its summand. -/ +theorem sum_pure_le {𝓟 : ι → ProbSpace} {V : Set Var} + (hP : ∀ {i j : ι}, i ≠ j → Disjoint (𝓟 i).support (𝓟 j).support) + (hdP : ∀ i, (𝓟 i).dom = V) (i : ι) : sum (PMF.pure i) 𝓟 V hP hdP ≤ 𝓟 i := by + classical + have hmeas : ∀ E, (sumMSpace (PMF.pure i) 𝓟).MeasurableSet' E → + (𝓟 i).mspace.MeasurableSet' E := by + intro E hE + have h1 := hE i (by simp) + have hnull : (𝓟 i).meas (E \ (𝓟 i).support) = 0 := + measure_mono_null (Set.diff_subset_compl _ _) (meas_compl_support _) + have h2 := (𝓟 i).complete.out _ hnull + have := @MeasurableSet.union ℕ (𝓟 i).mspace _ _ h1 h2 + rwa [Set.inter_union_sdiff] at this + refine le_of_id hmeas (fun E hE ↦ ?_) (hdP i).symm.subset + (fun n hn ↦ le_of_eq (sumState_of_mem hP hn)) + refine ENNReal.coe_injective ?_ + rw [prob_coe, prob_coe] + change sumMeasure (PMF.pure i) 𝓟 E = _ + rw [sumMeasure_apply _ _ hE, sumMeasureFun, tsum_eq_single i] + · rw [PMF.pure_apply_self, one_mul, meas_inter_support] + · intro j hj; rw [PMF.pure_apply_of_ne _ _ hj, zero_mul] + end SumMono end ProbSpace From c8e1634b7c93b0433a783455d04cb75ebb1820fc Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 30 Sep 2026 15:10:42 +0000 Subject: [PATCH 5/7] Prove the Frame rule MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `wp_frame`: `φ ∗ wp c ψ ⊢ wp c (φ ∗ ψ)`. The program is run with its frame extended by the space of `φ` (`Framed.right`), and the result is regrouped with the new `Framed.unright`, which moves the left factor of the frame back into the program's space. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_019Gipsr3EwstFw5DuwGNoug --- PcolIris/Logic/Framed.lean | 15 +++++++++++++++ PcolIris/Logic/WeakestPre.lean | 12 ++++++++++-- 2 files changed, 25 insertions(+), 2 deletions(-) diff --git a/PcolIris/Logic/Framed.lean b/PcolIris/Logic/Framed.lean index d1440ab..a5720c2 100644 --- a/PcolIris/Logic/Framed.lean +++ b/PcolIris/Logic/Framed.lean @@ -72,6 +72,21 @@ lemma right {𝓟₁ 𝓟₂ : ProbSpace} (hd : Disjoint 𝓟₁.dom 𝓟₂.dom have hf' : Framed 𝓘 (𝓟₂ ⊗ 𝓟₁) 𝓟fr 𝓙 μ := hf.mono hc exact hf'.left hd.symm +/-- Moving the left factor of the frame into the program's space. -/ +lemma unright {𝓟₁ 𝓟₂ : ProbSpace} (hd₁ : Disjoint 𝓟₁.dom 𝓟fr.dom) + (hf : Framed 𝓘 𝓟₂ (𝓟₁ ⊗ 𝓟fr) 𝓙 μ) : Framed 𝓘 (𝓟₁ ⊗ 𝓟₂) 𝓟fr 𝓙 μ := by + have hd : Disjoint 𝓟₂.dom (𝓟₁.dom ∪ 𝓟fr.dom) := hf.disj_frame + have h₂₁ : Disjoint 𝓟₂.dom 𝓟₁.dom := (Set.disjoint_union_right.mp hd).1 + have h₂f : Disjoint 𝓟₂.dom 𝓟fr.dom := (Set.disjoint_union_right.mp hd).2 + refine ⟨hf.inv, Set.disjoint_union_left.mpr ⟨hd₁, h₂f⟩, ?_, ?_⟩ + · have h := hf.disj_inv + change Disjoint (𝓟₂.dom ∪ (𝓟₁.dom ∪ 𝓟fr.dom)) 𝓙.dom at h + change Disjoint ((𝓟₁.dom ∪ 𝓟₂.dom) ∪ 𝓟fr.dom) 𝓙.dom + rwa [Set.union_comm 𝓟₁.dom 𝓟₂.dom, Set.union_assoc] + · refine Distr.Refines.mono (ProbSpace.product_mono_left ?_ hf.disj_inv) hf.refines + exact (ProbSpace.product_mono_left (ProbSpace.product_comm h₂₁) + (Set.disjoint_union_left.mpr ⟨h₂f, hd₁⟩)).trans (ProbSpace.product_assoc 𝓟₂ 𝓟₁ 𝓟fr) + end Framed end Pcol diff --git a/PcolIris/Logic/WeakestPre.lean b/PcolIris/Logic/WeakestPre.lean index 68a39fa..3d6b232 100644 --- a/PcolIris/Logic/WeakestPre.lean +++ b/PcolIris/Logic/WeakestPre.lean @@ -176,10 +176,18 @@ lemma wp_strengthen (h : ψ.Precise) : wp_weak 𝓘 c ψ ⊢ wp 𝓘 c ψ := by sorry +/-- The `Frame` rule: a frame that is independent of the program's resources is preserved. -/ lemma wp_frame : φ ∗ wp 𝓘 c ψ ⊢ wp 𝓘 c iprop(φ ∗ ψ) := by - -- Plan: run the program with the frame `𝓕 ⊗ 𝓟₁`, and rearrange the products. - sorry + rintro 𝓟 ⟨𝓟₁, 𝓟₂, hd, hle, hφ, hwp⟩ μ 𝓕 𝓙 _ hf ν hν + have hf' := hf.mono hle + have hd₁ : Disjoint 𝓟₁.dom 𝓕.dom := + hf'.disj_frame.mono_left (Set.subset_union_left : 𝓟₁.dom ⊆ 𝓟₁.dom ∪ 𝓟₂.dom) + -- Run the program with the frame extended by `𝓟₁` + obtain ⟨𝓠, 𝓙', hf'', hψ⟩ := hwp μ (𝓟₁ ⊗ 𝓕) 𝓙 True.intro (hf'.right hd) ν hν + have hd' : Disjoint 𝓟₁.dom 𝓠.dom := + (Set.disjoint_union_right.mp hf''.disj_frame).1.symm + exact ⟨𝓟₁ ⊗ 𝓠, 𝓙', hf''.unright hd₁, 𝓟₁, 𝓠, hd', le_refl _, hφ, hψ⟩ /-- **Assignment rule that preserves the value of the assigned expression.** From c6b106eb811bdd87e51bfb1d366cc63a455ea536 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 30 Sep 2026 15:13:38 +0000 Subject: [PATCH 6/7] wp: the postcondition owns no more variables than the precondition Programs do not acquire variables, matching the paper's fixed memory footprint. With this, the postconditions of the two threads in wp_par own disjoint variables, which closes the disjointness sorry there. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_019Gipsr3EwstFw5DuwGNoug --- DESIGN.md | 4 +++ PcolIris/Logic/WeakestPre.lean | 45 ++++++++++++++++++++-------------- 2 files changed, 30 insertions(+), 19 deletions(-) diff --git a/DESIGN.md b/DESIGN.md index afa954a..b38e4e4 100644 --- a/DESIGN.md +++ b/DESIGN.md @@ -59,6 +59,10 @@ 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⌉`. +The postcondition space may own no variables beyond those of the precondition space +(`𝓠.dom ⊆ 𝓟.dom`). In the paper this is implicit, since a program runs on a fixed memory +footprint; here it is what makes the postconditions of two parallel threads independent. + ## Invariants Invariants are ordered by factorization (`Inv.LE_Inv`): `𝓘 ≤ 𝓙` when `𝓘` is `𝓙 ∗ 𝓚` for diff --git a/PcolIris/Logic/WeakestPre.lean b/PcolIris/Logic/WeakestPre.lean index 3d6b232..2261d7a 100644 --- a/PcolIris/Logic/WeakestPre.lean +++ b/PcolIris/Logic/WeakestPre.lean @@ -22,9 +22,12 @@ def wp_base (𝓘 : Inv) (F : ProbSpace → Prop) (c : Cmd Act) (ψ : OProp) : O -- Take any `ν` that results from running the program ∀ ν ∈ ConvexPowerset.singleton' μ >>= 𝓛 (c.withInv 𝓘).to_pom, -- Then `ν` refines some probability space `𝓠`, which satisfies the postcondition `ψ`, - -- together with the same frame and a space satisfying the invariant - ∃ 𝓠 𝓙', Framed 𝓘 𝓠 𝓟fr 𝓙' ν ∧ ψ 𝓠 - upcl := fun hle h μ 𝓟fr 𝓙 hF hf ν hν ↦ h μ 𝓟fr 𝓙 hF (hf.mono hle) ν hν + -- together with the same frame and a space satisfying the invariant. The program does + -- not acquire variables: `𝓠` owns no more variables than `𝓟`. + ∃ 𝓠 𝓙', Framed 𝓘 𝓠 𝓟fr 𝓙' ν ∧ 𝓠.dom ⊆ 𝓟.dom ∧ ψ 𝓠 + upcl := fun hle h μ 𝓟fr 𝓙 hF hf ν hν ↦ + let ⟨𝓠, 𝓙', hf', hdom, hψ⟩ := h μ 𝓟fr 𝓙 hF (hf.mono hle) ν hν + ⟨𝓠, 𝓙', hf', hdom.trans (ProbSpace.dom_mono hle), hψ⟩ /-- The standard "strong" wp allows any frame -/ def wp (𝓘 : Inv) : Cmd Act → OProp → OProp := wp_base 𝓘 (fun _ ↦ True) @@ -44,7 +47,7 @@ variable {𝓘 : Inv} {F : ProbSpace → Prop} {c : Cmd Act} lemma wp_skip (φ : OProp) : φ ⊢ wp_base 𝓘 F Cmd.skip φ := by intro 𝓟 hφ μ 𝓟fr 𝓙 _ hf ν hν - refine ⟨𝓟, 𝓙, ?_, hφ⟩ + refine ⟨𝓟, 𝓙, ?_, subset_rfl, hφ⟩ rw [Cmd.withInv, Cmd.to_pom, Pom.Semantics.lin_skip, bind_pure] at hν have hle : μ ≤ ν := by have : ν ∈ (ConvexPowerset.singleton' μ).set := hν @@ -55,9 +58,10 @@ lemma wp_seq {c₁ c₂ : Cmd Act} {ψ : OProp} : wp_base 𝓘 F c₁ (wp_base 𝓘 F c₂ ψ) ⊢ wp_base 𝓘 F (Cmd.seq c₁ c₂) ψ := by intro 𝓟 h μ 𝓟fr 𝓙 hF href ν; rw [Cmd.withInv, Cmd.to_pom, Pom.lin_seq, ← bind_assoc] intro hν; rcases ConvexPowerset.mem_bind.mp hν with ⟨ξ, hξ, f, hf, rfl⟩ - have ⟨𝓡, 𝓙', href', h'⟩ := h μ 𝓟fr 𝓙 hF href ξ hξ - refine h' ξ 𝓟fr 𝓙' hF href' _ ?_ - exact ConvexPowerset.mem_bind.mpr ⟨ξ, ConvexPowerset.self_mem_singleton' _, f, hf, rfl⟩ + have ⟨𝓡, 𝓙', href', hdom, h'⟩ := h μ 𝓟fr 𝓙 hF href ξ hξ + obtain ⟨𝓠, 𝓙'', hf'', hdom', hψ⟩ := h' ξ 𝓟fr 𝓙' hF href' _ + (ConvexPowerset.mem_bind.mpr ⟨ξ, ConvexPowerset.self_mem_singleton' _, f, hf, rfl⟩) + exact ⟨𝓠, 𝓙'', hf'', hdom'.trans hdom, hψ⟩ lemma wp_if_true {b : Expr} {c₁ c₂ : Cmd Act} {φ ψ : OProp} : ⌈b == Expr.literal 1⌉ ∧ wp_base 𝓘 F c₁ ψ ⊢ wp_base 𝓘 F (Cmd.if_stmt b c₁ c₂) ψ := by @@ -122,8 +126,8 @@ lemma wp_par {𝓘 : Inv} {c₁ c₂ : Cmd Act} {ψ₁ ψ₂ : OProp} 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 ⟨𝓡₁, _, -, hdom₁, hψ₁'⟩ := h₁ μ _ 𝓙 True.intro (hf'.left hdisj) ν₁ hν₁ + obtain ⟨𝓡₂, _, -, hdom₂, 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; @@ -132,21 +136,23 @@ lemma wp_par {𝓘 : Inv} {c₁ c₂ : Cmd Act} {ψ₁ ψ₂ : OProp} ∀ ν₁ ∈ ConvexPowerset.singleton' μ₁ >>= 𝓛 (c₁.withInv 𝓘).to_pom, ∃ 𝓙₁', Framed 𝓘 𝓠₁ 𝓕 𝓙₁' ν₁ := by intro 𝓕 𝓙₁ μ₁ hf₁ ν₁ hν₁ - obtain ⟨𝓠, 𝓙₁', hf', hψ⟩ := h₁ μ₁ 𝓕 𝓙₁ True.intro hf₁ ν₁ hν₁ + obtain ⟨𝓠, 𝓙₁', hf', -, hψ⟩ := h₁ μ₁ 𝓕 𝓙₁ True.intro hf₁ ν₁ hν₁ exact ⟨𝓙₁', hf'.mono ((hQ₁ 𝓠).mpr hψ)⟩ have hthread₂ : ∀ (𝓕 𝓙₂ : ProbSpace) (μ₂ : Distr Mem), Framed 𝓘 𝓟₂ 𝓕 𝓙₂ μ₂ → ∀ ν₂ ∈ ConvexPowerset.singleton' μ₂ >>= 𝓛 (c₂.withInv 𝓘).to_pom, ∃ 𝓙₂', Framed 𝓘 𝓠₂ 𝓕 𝓙₂' ν₂ := by intro 𝓕 𝓙₂ μ₂ hf₂ ν₂ hν₂ - obtain ⟨𝓠, 𝓙₂', hf', hψ⟩ := h₂ μ₂ 𝓕 𝓙₂ True.intro hf₂ ν₂ hν₂ + obtain ⟨𝓠, 𝓙₂', hf', -, hψ⟩ := h₂ μ₂ 𝓕 𝓙₂ True.intro hf₂ ν₂ hν₂ 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' 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'', - 𝓠₁, 𝓠₂, sorry, le_refl _, (hQ₁ 𝓠₁).mp (le_refl _), (hQ₂ 𝓠₂).mp (le_refl _)⟩ + -- The least models own no more variables than the preconditions of the two threads + have hsub₁ : 𝓠₁.dom ⊆ 𝓟₁.dom := (ProbSpace.dom_mono ((hQ₁ _).mpr hψ₁')).trans hdom₁ + have hsub₂ : 𝓠₂.dom ⊆ 𝓟₂.dom := (ProbSpace.dom_mono ((hQ₂ _).mpr hψ₂')).trans hdom₂ + refine ⟨𝓠₁ ⊗ 𝓠₂, 𝓙', hf'', ?_, + 𝓠₁, 𝓠₂, hdisj.mono hsub₁ hsub₂, le_refl _, (hQ₁ 𝓠₁).mp (le_refl _), (hQ₂ 𝓠₂).mp (le_refl _)⟩ + exact (Set.union_subset_union hsub₁ hsub₂).trans (ProbSpace.dom_mono hle) /- STRUCTURAL RULES -/ @@ -154,8 +160,8 @@ variable {ι : Type} [Countable ι] {𝓘 : Inv} {F : ProbSpace → Prop} {c : C lemma wp_conseq (h : φ ⊢ ψ) : wp_base 𝓘 F c φ ⊢ wp_base 𝓘 F c ψ := by intro 𝓟 hc μ 𝓟fr 𝓙 hF hf ν hν - have ⟨𝓠, 𝓙', hf', hφ⟩ := hc μ 𝓟fr 𝓙 hF hf ν hν - exact ⟨𝓠, 𝓙', hf', h 𝓠 hφ⟩ + have ⟨𝓠, 𝓙', hf', hdom, hφ⟩ := hc μ 𝓟fr 𝓙 hF hf ν hν + exact ⟨𝓠, 𝓙', hf', hdom, h 𝓠 hφ⟩ lemma wp_split {ψ : ι → OProp} : (⨁[ ξ ] fun v ↦ wp_base 𝓘 F c (ψ v)) ⊢ wp_base 𝓘 F c (⨁[ ξ ] ψ) := by @@ -184,10 +190,11 @@ lemma wp_frame : have hd₁ : Disjoint 𝓟₁.dom 𝓕.dom := hf'.disj_frame.mono_left (Set.subset_union_left : 𝓟₁.dom ⊆ 𝓟₁.dom ∪ 𝓟₂.dom) -- Run the program with the frame extended by `𝓟₁` - obtain ⟨𝓠, 𝓙', hf'', hψ⟩ := hwp μ (𝓟₁ ⊗ 𝓕) 𝓙 True.intro (hf'.right hd) ν hν + obtain ⟨𝓠, 𝓙', hf'', hdom, hψ⟩ := hwp μ (𝓟₁ ⊗ 𝓕) 𝓙 True.intro (hf'.right hd) ν hν have hd' : Disjoint 𝓟₁.dom 𝓠.dom := (Set.disjoint_union_right.mp hf''.disj_frame).1.symm - exact ⟨𝓟₁ ⊗ 𝓠, 𝓙', hf''.unright hd₁, 𝓟₁, 𝓠, hd', le_refl _, hφ, hψ⟩ + refine ⟨𝓟₁ ⊗ 𝓠, 𝓙', hf''.unright hd₁, ?_, 𝓟₁, 𝓠, hd', le_refl _, hφ, hψ⟩ + exact (Set.union_subset_union_right _ hdom).trans (ProbSpace.dom_mono hle) /-- **Assignment rule that preserves the value of the assigned expression.** From f78b4d8af343d3f5fb923ba0762ecb694ff880df Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 30 Sep 2026 15:21:19 +0000 Subject: [PATCH 7/7] wp: programs do not deallocate variables MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Add Distr.Keeps μ ν (every variable allocated in all memories of μ is allocated in all memories of ν) to wp_base and to Lemma C.6. The paper gets this for free from its fixed memory domain. It is needed for the Split rule: the postconditions of the branches may own fewer variables than the preconditions, and must be padded back to a common domain from the final memories. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_019Gipsr3EwstFw5DuwGNoug --- DESIGN.md | 13 +++++++-- PcolIris/Logic/Framed.lean | 12 ++++++++ PcolIris/Logic/LemmaC6.lean | 11 ++++---- PcolIris/Logic/WeakestPre.lean | 51 +++++++++++++++++----------------- 4 files changed, 54 insertions(+), 33 deletions(-) diff --git a/DESIGN.md b/DESIGN.md index b38e4e4..67b5e19 100644 --- a/DESIGN.md +++ b/DESIGN.md @@ -59,9 +59,16 @@ 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⌉`. -The postcondition space may own no variables beyond those of the precondition space -(`𝓠.dom ⊆ 𝓟.dom`). In the paper this is implicit, since a program runs on a fixed memory -footprint; here it is what makes the postconditions of two parallel threads independent. +The paper runs programs on memories with a fixed domain. Here memories are partial, so +`wp` states two facts that the paper gets for free: + +- the postcondition space owns no variables beyond those of the precondition space + (`𝓠.dom ⊆ 𝓟.dom`); this is what makes the postconditions of two parallel threads + independent; +- the program does not deallocate variables (`Distr.Keeps μ ν`: every variable that is + allocated in all initial memories is allocated in all final memories). The postcondition + space may be smaller than the precondition space, so without this fact the branches of an + outcome conjunction could not be brought back to a common domain (`Split`). ## Invariants diff --git a/PcolIris/Logic/Framed.lean b/PcolIris/Logic/Framed.lean index a5720c2..6e065bb 100644 --- a/PcolIris/Logic/Framed.lean +++ b/PcolIris/Logic/Framed.lean @@ -22,6 +22,18 @@ lemma Inv.footprint (𝓘 : Inv) : 𝓘.to_MProp.Footprint 𝓘.dom := by rw [Mem.restrict_dom] at this exact Set.inter_eq_right.mp this +/-- Every memory that `ν` gives positive probability owns the variables `D`. -/ +def Distr.Owns (ν : Distr Mem) (D : Set Var) : Prop := + ∀ m : Mem, ν (m : WithBot Mem) ≠ 0 → D ⊆ m.dom + +/-- A run from `μ` to `ν` does not deallocate variables. -/ +def Distr.Keeps (μ ν : Distr Mem) : Prop := + ∀ D, Distr.Owns μ D → Distr.Owns ν D + +lemma Distr.Keeps.refl (μ : Distr Mem) : Distr.Keeps μ μ := fun _ h ↦ h + +lemma Distr.Keeps.trans {μ ν ρ : Distr Mem} (h₁ : Distr.Keeps μ ν) (h₂ : Distr.Keeps ν ρ) : Distr.Keeps μ ρ := + fun D h ↦ h₂ D (h₁ D h) /-- `Framed 𝓘 𝓟 𝓟fr 𝓙 μ` states that the distribution `μ` refines the product of a space `𝓟` diff --git a/PcolIris/Logic/LemmaC6.lean b/PcolIris/Logic/LemmaC6.lean index 789e7d2..a46084a 100644 --- a/PcolIris/Logic/LemmaC6.lean +++ b/PcolIris/Logic/LemmaC6.lean @@ -23,8 +23,9 @@ open Linearization invariant `𝓘`, and let `μ` be an initial distribution framed by `𝓟₁ ⊗ 𝓟₂`, a frame `𝓟fr` and a space `𝓙` satisfying the invariant. If, for an arbitrary frame `𝓕`, running thread `k` on any distribution framed by `𝓟ₖ` and `𝓕` yields a distribution framed by `𝓠ₖ` and -`𝓕`, then running the two threads in parallel on `μ` yields a distribution framed by -`𝓠₁ ⊗ 𝓠₂` and `𝓟fr`. +`𝓕` (without deallocating variables), then running the two threads in parallel on `μ` +yields a distribution framed by `𝓠₁ ⊗ 𝓠₂` and `𝓟fr` (again without deallocating +variables). The side conditions of the original statement (each thread only acts on the variables it owns, and only tests its own variables) are replaced here by the requirement that the two @@ -39,11 +40,11 @@ theorem lemma_C6 {𝓘 : Inv} {p₁ p₂ : Pom (Label (WithInv Act) Test)} {𝓟₁ 𝓟₂ 𝓠₁ 𝓠₂ 𝓟fr 𝓙 : ProbSpace} {μ : Distr Mem} (hμ : Framed 𝓘 (𝓟₁ ⊗ 𝓟₂) 𝓟fr 𝓙 μ) (h₁ : ∀ (𝓕 𝓙₁ : ProbSpace) (μ₁ : Distr Mem), Framed 𝓘 𝓟₁ 𝓕 𝓙₁ μ₁ → - ∀ ν₁ ∈ ConvexPowerset.singleton' μ₁ >>= 𝓛 p₁, ∃ 𝓙₁', Framed 𝓘 𝓠₁ 𝓕 𝓙₁' ν₁) + ∀ ν₁ ∈ ConvexPowerset.singleton' μ₁ >>= 𝓛 p₁, Distr.Keeps μ₁ ν₁ ∧ ∃ 𝓙₁', Framed 𝓘 𝓠₁ 𝓕 𝓙₁' ν₁) (h₂ : ∀ (𝓕 𝓙₂ : ProbSpace) (μ₂ : Distr Mem), Framed 𝓘 𝓟₂ 𝓕 𝓙₂ μ₂ → - ∀ ν₂ ∈ ConvexPowerset.singleton' μ₂ >>= 𝓛 p₂, ∃ 𝓙₂', Framed 𝓘 𝓠₂ 𝓕 𝓙₂' ν₂) : + ∀ ν₂ ∈ ConvexPowerset.singleton' μ₂ >>= 𝓛 p₂, Distr.Keeps μ₂ ν₂ ∧ ∃ 𝓙₂', Framed 𝓘 𝓠₂ 𝓕 𝓙₂' ν₂) : ∀ ν ∈ ConvexPowerset.singleton' μ >>= 𝓛 (Pom.Semantics.par p₁ p₂), - ∃ 𝓙', Framed 𝓘 (𝓠₁ ⊗ 𝓠₂) 𝓟fr 𝓙' ν := by + Distr.Keeps μ ν ∧ ∃ 𝓙', Framed 𝓘 (𝓠₁ ⊗ 𝓠₂) 𝓟fr 𝓙' ν := by sorry end Pcol diff --git a/PcolIris/Logic/WeakestPre.lean b/PcolIris/Logic/WeakestPre.lean index 2261d7a..ebdd077 100644 --- a/PcolIris/Logic/WeakestPre.lean +++ b/PcolIris/Logic/WeakestPre.lean @@ -21,13 +21,14 @@ def wp_base (𝓘 : Inv) (F : ProbSpace → Prop) (c : Cmd Act) (ψ : OProp) : O Framed 𝓘 𝓟 𝓟fr 𝓙 μ → -- Take any `ν` that results from running the program ∀ ν ∈ ConvexPowerset.singleton' μ >>= 𝓛 (c.withInv 𝓘).to_pom, - -- Then `ν` refines some probability space `𝓠`, which satisfies the postcondition `ψ`, - -- together with the same frame and a space satisfying the invariant. The program does - -- not acquire variables: `𝓠` owns no more variables than `𝓟`. - ∃ 𝓠 𝓙', Framed 𝓘 𝓠 𝓟fr 𝓙' ν ∧ 𝓠.dom ⊆ 𝓟.dom ∧ ψ 𝓠 + -- Then the program has not deallocated variables, and `ν` refines some probability + -- space `𝓠`, which satisfies the postcondition `ψ`, together with the same frame and a + -- space satisfying the invariant. The program does not acquire variables either: `𝓠` + -- owns no more variables than `𝓟`. + Distr.Keeps μ ν ∧ ∃ 𝓠 𝓙', Framed 𝓘 𝓠 𝓟fr 𝓙' ν ∧ 𝓠.dom ⊆ 𝓟.dom ∧ ψ 𝓠 upcl := fun hle h μ 𝓟fr 𝓙 hF hf ν hν ↦ - let ⟨𝓠, 𝓙', hf', hdom, hψ⟩ := h μ 𝓟fr 𝓙 hF (hf.mono hle) ν hν - ⟨𝓠, 𝓙', hf', hdom.trans (ProbSpace.dom_mono hle), hψ⟩ + let ⟨hk, 𝓠, 𝓙', hf', hdom, hψ⟩ := h μ 𝓟fr 𝓙 hF (hf.mono hle) ν hν + ⟨hk, 𝓠, 𝓙', hf', hdom.trans (ProbSpace.dom_mono hle), hψ⟩ /-- The standard "strong" wp allows any frame -/ def wp (𝓘 : Inv) : Cmd Act → OProp → OProp := wp_base 𝓘 (fun _ ↦ True) @@ -47,21 +48,21 @@ variable {𝓘 : Inv} {F : ProbSpace → Prop} {c : Cmd Act} lemma wp_skip (φ : OProp) : φ ⊢ wp_base 𝓘 F Cmd.skip φ := by intro 𝓟 hφ μ 𝓟fr 𝓙 _ hf ν hν - refine ⟨𝓟, 𝓙, ?_, subset_rfl, hφ⟩ rw [Cmd.withInv, Cmd.to_pom, Pom.Semantics.lin_skip, bind_pure] at hν have hle : μ ≤ ν := by have : ν ∈ (ConvexPowerset.singleton' μ).set := hν rwa [ConvexPowerset.singleton'_set_eq] at this - rwa [← proper_dist_maximal hf.refines.bot_0 hle] + rw [← proper_dist_maximal hf.refines.bot_0 hle] + exact ⟨Distr.Keeps.refl μ, 𝓟, 𝓙, hf, subset_rfl, hφ⟩ lemma wp_seq {c₁ c₂ : Cmd Act} {ψ : OProp} : wp_base 𝓘 F c₁ (wp_base 𝓘 F c₂ ψ) ⊢ wp_base 𝓘 F (Cmd.seq c₁ c₂) ψ := by intro 𝓟 h μ 𝓟fr 𝓙 hF href ν; rw [Cmd.withInv, Cmd.to_pom, Pom.lin_seq, ← bind_assoc] intro hν; rcases ConvexPowerset.mem_bind.mp hν with ⟨ξ, hξ, f, hf, rfl⟩ - have ⟨𝓡, 𝓙', href', hdom, h'⟩ := h μ 𝓟fr 𝓙 hF href ξ hξ - obtain ⟨𝓠, 𝓙'', hf'', hdom', hψ⟩ := h' ξ 𝓟fr 𝓙' hF href' _ + have ⟨hk, 𝓡, 𝓙', href', hdom, h'⟩ := h μ 𝓟fr 𝓙 hF href ξ hξ + obtain ⟨hk', 𝓠, 𝓙'', hf'', hdom', hψ⟩ := h' ξ 𝓟fr 𝓙' hF href' _ (ConvexPowerset.mem_bind.mpr ⟨ξ, ConvexPowerset.self_mem_singleton' _, f, hf, rfl⟩) - exact ⟨𝓠, 𝓙'', hf'', hdom'.trans hdom, hψ⟩ + exact ⟨Distr.Keeps.trans hk hk', 𝓠, 𝓙'', hf'', hdom'.trans hdom, hψ⟩ lemma wp_if_true {b : Expr} {c₁ c₂ : Cmd Act} {φ ψ : OProp} : ⌈b == Expr.literal 1⌉ ∧ wp_base 𝓘 F c₁ ψ ⊢ wp_base 𝓘 F (Cmd.if_stmt b c₁ c₂) ψ := by @@ -126,31 +127,31 @@ lemma wp_par {𝓘 : Inv} {c₁ c₂ : Cmd Act} {ψ₁ ψ₂ : OProp} have hf' := hf.mono hle obtain ⟨ν₁, hν₁⟩ := (ConvexPowerset.singleton' μ >>= 𝓛 (c₁.withInv 𝓘).to_pom).nonempty obtain ⟨ν₂, hν₂⟩ := (ConvexPowerset.singleton' μ >>= 𝓛 (c₂.withInv 𝓘).to_pom).nonempty - obtain ⟨𝓡₁, _, -, hdom₁, hψ₁'⟩ := h₁ μ _ 𝓙 True.intro (hf'.left hdisj) ν₁ hν₁ - obtain ⟨𝓡₂, _, -, hdom₂, hψ₂'⟩ := h₂ μ _ 𝓙 True.intro (hf'.right hdisj) ν₂ hν₂ + obtain ⟨-, 𝓡₁, _, -, hdom₁, hψ₁'⟩ := h₁ μ _ 𝓙 True.intro (hf'.left hdisj) ν₁ hν₁ + obtain ⟨-, 𝓡₂, _, -, hdom₂, 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 𝓘 𝓟₁ 𝓕 𝓙₁ μ₁ → ∀ ν₁ ∈ ConvexPowerset.singleton' μ₁ >>= 𝓛 (c₁.withInv 𝓘).to_pom, - ∃ 𝓙₁', Framed 𝓘 𝓠₁ 𝓕 𝓙₁' ν₁ := by + Distr.Keeps μ₁ ν₁ ∧ ∃ 𝓙₁', Framed 𝓘 𝓠₁ 𝓕 𝓙₁' ν₁ := by intro 𝓕 𝓙₁ μ₁ hf₁ ν₁ hν₁ - obtain ⟨𝓠, 𝓙₁', hf', -, hψ⟩ := h₁ μ₁ 𝓕 𝓙₁ True.intro hf₁ ν₁ hν₁ - exact ⟨𝓙₁', hf'.mono ((hQ₁ 𝓠).mpr hψ)⟩ + obtain ⟨hk, 𝓠, 𝓙₁', hf', -, hψ⟩ := h₁ μ₁ 𝓕 𝓙₁ True.intro hf₁ ν₁ hν₁ + exact ⟨hk, 𝓙₁', hf'.mono ((hQ₁ 𝓠).mpr hψ)⟩ have hthread₂ : ∀ (𝓕 𝓙₂ : ProbSpace) (μ₂ : Distr Mem), Framed 𝓘 𝓟₂ 𝓕 𝓙₂ μ₂ → ∀ ν₂ ∈ ConvexPowerset.singleton' μ₂ >>= 𝓛 (c₂.withInv 𝓘).to_pom, - ∃ 𝓙₂', Framed 𝓘 𝓠₂ 𝓕 𝓙₂' ν₂ := by + Distr.Keeps μ₂ ν₂ ∧ ∃ 𝓙₂', Framed 𝓘 𝓠₂ 𝓕 𝓙₂' ν₂ := by intro 𝓕 𝓙₂ μ₂ hf₂ ν₂ hν₂ - obtain ⟨𝓠, 𝓙₂', hf', -, hψ⟩ := h₂ μ₂ 𝓕 𝓙₂ True.intro hf₂ ν₂ hν₂ - exact ⟨𝓙₂', hf'.mono ((hQ₂ 𝓠).mpr hψ)⟩ + obtain ⟨hk, 𝓠, 𝓙₂', hf', -, hψ⟩ := h₂ μ₂ 𝓕 𝓙₂ True.intro hf₂ ν₂ hν₂ + exact ⟨hk, 𝓙₂', 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' hthread₁ hthread₂ ν hν + obtain ⟨hk, 𝓙', hf''⟩ := lemma_C6 hf' hthread₁ hthread₂ ν hν -- The least models own no more variables than the preconditions of the two threads have hsub₁ : 𝓠₁.dom ⊆ 𝓟₁.dom := (ProbSpace.dom_mono ((hQ₁ _).mpr hψ₁')).trans hdom₁ have hsub₂ : 𝓠₂.dom ⊆ 𝓟₂.dom := (ProbSpace.dom_mono ((hQ₂ _).mpr hψ₂')).trans hdom₂ - refine ⟨𝓠₁ ⊗ 𝓠₂, 𝓙', hf'', ?_, + refine ⟨hk, 𝓠₁ ⊗ 𝓠₂, 𝓙', hf'', ?_, 𝓠₁, 𝓠₂, hdisj.mono hsub₁ hsub₂, le_refl _, (hQ₁ 𝓠₁).mp (le_refl _), (hQ₂ 𝓠₂).mp (le_refl _)⟩ exact (Set.union_subset_union hsub₁ hsub₂).trans (ProbSpace.dom_mono hle) @@ -160,8 +161,8 @@ variable {ι : Type} [Countable ι] {𝓘 : Inv} {F : ProbSpace → Prop} {c : C lemma wp_conseq (h : φ ⊢ ψ) : wp_base 𝓘 F c φ ⊢ wp_base 𝓘 F c ψ := by intro 𝓟 hc μ 𝓟fr 𝓙 hF hf ν hν - have ⟨𝓠, 𝓙', hf', hdom, hφ⟩ := hc μ 𝓟fr 𝓙 hF hf ν hν - exact ⟨𝓠, 𝓙', hf', hdom, h 𝓠 hφ⟩ + have ⟨hk, 𝓠, 𝓙', hf', hdom, hφ⟩ := hc μ 𝓟fr 𝓙 hF hf ν hν + exact ⟨hk, 𝓠, 𝓙', hf', hdom, h 𝓠 hφ⟩ lemma wp_split {ψ : ι → OProp} : (⨁[ ξ ] fun v ↦ wp_base 𝓘 F c (ψ v)) ⊢ wp_base 𝓘 F c (⨁[ ξ ] ψ) := by @@ -190,10 +191,10 @@ lemma wp_frame : have hd₁ : Disjoint 𝓟₁.dom 𝓕.dom := hf'.disj_frame.mono_left (Set.subset_union_left : 𝓟₁.dom ⊆ 𝓟₁.dom ∪ 𝓟₂.dom) -- Run the program with the frame extended by `𝓟₁` - obtain ⟨𝓠, 𝓙', hf'', hdom, hψ⟩ := hwp μ (𝓟₁ ⊗ 𝓕) 𝓙 True.intro (hf'.right hd) ν hν + obtain ⟨hk, 𝓠, 𝓙', hf'', hdom, hψ⟩ := hwp μ (𝓟₁ ⊗ 𝓕) 𝓙 True.intro (hf'.right hd) ν hν have hd' : Disjoint 𝓟₁.dom 𝓠.dom := (Set.disjoint_union_right.mp hf''.disj_frame).1.symm - refine ⟨𝓟₁ ⊗ 𝓠, 𝓙', hf''.unright hd₁, ?_, 𝓟₁, 𝓠, hd', le_refl _, hφ, hψ⟩ + refine ⟨hk, 𝓟₁ ⊗ 𝓠, 𝓙', hf''.unright hd₁, ?_, 𝓟₁, 𝓠, hd', le_refl _, hφ, hψ⟩ exact (Set.union_subset_union_right _ hdom).trans (ProbSpace.dom_mono hle) /--