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/DESIGN.md b/DESIGN.md index 3a869be..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 @@ -57,6 +59,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 diff --git a/PcolIris/Examples/EntropyMixer.lean b/PcolIris/Examples/EntropyMixer.lean index 716f4fd..718ee66 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.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 := 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 : @@ -250,10 +252,10 @@ 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 _)) + 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..6247bf6 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,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 _ +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 := @@ -162,7 +194,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) @@ -238,7 +270,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 @@ -255,14 +287,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)) @@ -309,14 +341,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 @@ -513,7 +545,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/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/Logic/WeakestPre.lean b/PcolIris/Logic/WeakestPre.lean index 0bcc3a6..7d3c503 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} : @@ -118,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 𝓘 𝓟₁ 𝓕 𝓙₁ μ₁ → @@ -137,15 +142,15 @@ 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 -/ -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ν @@ -197,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 cdeabd9..c680e83 100644 --- a/PcolIris/OProp/Laws.lean +++ b/PcolIris/OProp/Laws.lean @@ -1,11 +1,36 @@ import PcolIris.OProp.OProp import PcolIris.OProp.ProbSpaceLemmas import PcolIris.OProp.ProductLaws +import PcolIris.OProp.TrivialSpace +import PcolIris.OProp.SumLaws 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,17 +74,33 @@ 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 -lemma oplus_distrib {ι : Type} (ξ : PMF ι) (φ : ι → OProp) (ψ : OProp) : - (⨁[ ξ ] φ) ∗ ψ ⊢ ⨁[ ξ ] fun v ↦ iprop(φ v ∗ ψ) := sorry +/-- A frame can be pushed into the branches of an outcome conjunction. -/ +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 + 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) : +lemma oplus_distrib' {ι : Type} [Countable ι] (ξ : PMF ι) (φ : ι → OProp) (ψ : OProp) (h : ψ.Precise) : (⨁[ ξ ] fun v ↦ iprop(φ v ∗ ψ)) ⊢ (⨁[ ξ ] φ) ∗ ψ := by sorry @@ -70,24 +111,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ξ @@ -100,7 +141,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)) ?_ @@ -108,7 +149,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ξ @@ -116,7 +157,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 _, ?_, ?_⟩ @@ -132,14 +173,156 @@ 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 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 + 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), 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 𝓠 + 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 sure {P : MProp} {V : Set Var} (hP : P.Footprint V) (hV : V.Finite) : + (OProp.sure P).Precise := + (sureDom hP hV).precise -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 +/-- 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 8ae7720..0386248 100644 --- a/PcolIris/OProp/OProp.lean +++ b/PcolIris/OProp/OProp.lean @@ -222,10 +222,24 @@ 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 +/-- 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. -/ +def oplus {ι : Type} [Countable ι] (ξ : PMF ι) (φ : ι → OProp) : OProp where prop 𝓟 := ∃ 𝓠 V h hd, ProbSpace.sum ξ 𝓠 V h hd ≤ 𝓟 ∧ ∀ v ∈ ξ.support, φ v (𝓠 v) @@ -238,7 +252,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⟩ 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 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/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..878ee56 100644 --- a/PcolIris/Semantics/Mem.lean +++ b/PcolIris/Semantics/Mem.lean @@ -294,6 +294,33 @@ 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 + +/-- 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] + +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 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