Formalisation of the statements of all Bluebell rules except Program WP rules and Derived WP rules by Coda-Coda · Pull Request #268 · Verified-zkEVM/iris-lean

Coda-Coda · 2026-06-26T03:03:05Z

This PR includes a formalisation of the statements of all Bluebell rules except Program WP rules and Derived WP rules, along with all the underlying aspects needed for expressing the statements of these rules. The rules correspond to those in Fig. 9, Fig. 10 (except the Program WP rules), and Fig. 11 of the Bluebell paper.

It also includes proofs of some of these rules, which have primarily been proved using AI (indicated as appropriate by an Assisted-by: ... at the end of related commit messages).

The remaining rules yet to be formalised require the integration of VCV-io before they are able to be expressed, and are left for a future PR.

- Follow the naming convention more closely (not dogmatic, feel free to disregard in the future): + defs are whateverThisCaseIsCalled + lemmas are in_this_case + lemmas are named e.g. like this: `lemma f_eq_add_of_P (h : P) : f a = a + b`` (i.e. conclusion_of_assumptions) where conclusion reads symbols left to right and never mentions argument names - Do not rely on autoimplicits, e.g. mention `{a b}`` in `lemma foo {a b} : a + 1 = b`` - `μ = ν.cast _` instead of the ugly `@Measure.map ...` - comments 'tied' to a def/theorem should be /-- written like this -/, this style with /-- attaches the comment to the def when you hover it

…s to remove some ugly casts - e.g. you want `Preorder (PSpace Ω)`, but Preorder is defined as a 'type'-class, so there's a cast injected here. - Hit some proofs with a big stick.

Ferinko/measure my space r

…is-lean into measureMySpace

Assisted-by: Aristotle (Harmonic)

… ∑' (b : B), μ (a, b)) 1`

Assisted-by: Aristotle (Harmonic)

…... 1` Assisted-by: Aristotle (Harmonic)

…Sum ... 1 := ...` Improving clarity, so that they read more like the paper.

Note that the paper has a typo in C-DIST-PROJ. In the paper's rendition of the rule, the `μ` in the modality and the one in the assertion are meant to be different variables. In other words, in the paper, both occurences of `μ(x)` should not be the same `μ` as the two subscript `μ`s following `𝒞`. This is why we have `μ₁` and `μ₂` here.

Co-authored-by: Julian Sutherland <julian@nethermind.io> Co-authored-by: Daniel Britten <daniel.britten@nethermind.io>

github-actions · 2026-06-26T03:04:26Z

🤖 PR Summary

⚠️ PR title does not follow conventional commit format type[(scope)]: subject. Got: Formalisation of the statements of all Bluebell rules except Program WP rules and Derived WP rules

sorry delta: -4 (29 removed, 25 added) — net proof progress

Failed to generate AI summary. Please check the per-file summaries and statistics below.

Statistics

Metric	Count
📝 Files Changed	15
✅ Lines Added	5086
❌ Lines Removed	2783

Lean Declarations

✏️ Removed: 177 declaration(s)

src/Bluebell/Algebra/CMRA.lean (6)

abbrev ProdRel (Φ : α → β → Prop)
instance instLE : LE α
noncomputable instance cmraFun {ι : Type*} {β : ι → Type*} [∀ i, CMRA (β i)] :
noncomputable instance cmraFunUCMRA {ι : Type*} {β : ι → Type*} [∀ i, UCMRA (β i)] :
noncomputable instance cmraProdRel (Φ : α → β → Prop) [CompatibleRel (α
noncomputable instance ucmraFun {ι : Type*} {β : ι → Type*} [∀ i, UCMRA (β i)] :

src/Bluebell/Algebra/HyperAssertion.lean (41)

abbrev HyperAssertion (M : Type*) [LE M]
def and (P Q : HyperAssertion M) : HyperAssertion M
def emp : HyperAssertion M
def entails (P Q : HyperAssertion M) : Prop
def equiv (P Q : HyperAssertion M) : Prop
def imp (P Q : HyperAssertion M) : HyperAssertion M
def isIrrelevant [DecidableEq I] [Fintype I] (J : Set I)
def later (P : HyperAssertion M) : HyperAssertion M
def or (P Q : HyperAssertion M) : HyperAssertion M
def own (b : M) : HyperAssertion M
def persistently (P : HyperAssertion M) : HyperAssertion M
def pred (P : HyperAssertion M) : M → Prop
def pure (φ : Prop) : HyperAssertion M
def relevantIndices [DecidableEq I] [Fintype I] (P : @HyperAssertion (I → M) Bluebell.CMRA.instLE) :
def sExists {β : Sort*} (F : β → HyperAssertion M) : HyperAssertion M
def sExistsProp (X : HyperAssertion M → Prop) : HyperAssertion M
def sForall {β : Sort*} (F : β → HyperAssertion M) : HyperAssertion M
def sForallProp (X : HyperAssertion M → Prop) : HyperAssertion M
def sep (P Q : HyperAssertion M) : HyperAssertion M
def wand (P Q : HyperAssertion M) : HyperAssertion M
def «exists» {β : Sort*} (P : β → HyperAssertion M) : HyperAssertion M
def «forall» {β : Sort*} (P : β → HyperAssertion M) : HyperAssertion M
theorem and_assoc {P Q R : HyperAssertion M} :
theorem and_comm {P Q : HyperAssertion M} : entails (and P Q) (and Q P)
theorem and_true_left {P : HyperAssertion M} :
theorem and_true_right {P : HyperAssertion M} :
theorem isIrrelevant_compl_relevantIndices
theorem isIrrelevant_empty (P : @HyperAssertion (I → M) Bluebell.CMRA.instLE) :
theorem isIrrelevant_union (P : @HyperAssertion (I → M) Bluebell.CMRA.instLE)
theorem mem_of_agree_outside_covered (P : @HyperAssertion (I → M) Bluebell.CMRA.instLE)
theorem or_assoc {P Q R : HyperAssertion M} :
theorem or_comm {P Q : HyperAssertion M} : entails (or P Q) (or Q P)
theorem or_false_left {P : HyperAssertion M} :
theorem or_false_right {P : HyperAssertion M} :
theorem own_entails_of_included {b c : M} (hbc : b ≼ c) : entails (own (M
theorem sep_assoc {P Q R : HyperAssertion M} [CMRA.IsTotal M] :
theorem sep_comm {P Q : HyperAssertion M} : entails (sep P Q) (sep Q P)
theorem sep_emp_left {P : HyperAssertion M} :
theorem sep_emp_right {P : HyperAssertion M} :
theorem sep_mono {P P' Q Q' : HyperAssertion M}
theorem sep_own_own_entails_own_op (b c : M) : entails (sep (own (M

src/Bluebell/Algebra/PSpPm.lean (7)

abbrev PSpPm (α V F : Type*) [UFraction F]
def IndexedPSpPm (I α V F : Type*) [UFraction F]
def IndexedPSpPmRat (I α V : Type*)
def liftProb (μ : I → ProbabilityTheory.ProbabilitySpace (α → V)) : IndexedPSpPmRat I α V
instance compatiblePermRat_CompatibleRel {α V : Type*} [Nonempty V] :
instance compatiblePerm_CompatibleRel {α V F : Type*} [Nonempty V] [UFraction F] :
theorem compatiblePermRat_unit_compat {α V : Type*} [Nonempty V] :

src/Bluebell/Algebra/Permission.lean (15)

@[simp] theorem zeroSupport_one :
abbrev Permission (α F : Type*) [UFraction F]
def PermissionRat (α : Type*)
def hasOwnership (x : DFrac F) : Prop
def isZero (x : DFrac F) : Prop
def nonZeroSupport (p : Permission α F) : α → Prop
def ofFrac (p : α → Frac F) : Permission α F
def one : PermissionRat α
def op (p q : PermissionRat α) : PermissionRat α
def pcore : Option (PermissionRat α)
def valid (p : PermissionRat α) : Prop
def zero : PermissionRat α
def zeroSupport (p : Permission α F) : α → Prop
theorem nonZeroSupport_op_imp (p₁ p₂ : Permission α F) :
theorem zeroSupport_op (p₁ p₂ : Permission α F) :

src/Bluebell/Algebra/Probability.lean (26)

@[simp] lemma compatiblePermRat_none (p : PermissionRat α) :
@[simp] lemma compatiblePermRat_some (P : ProbabilitySpace (α → V)) (p : PermissionRat α)
@[simp] lemma compatiblePerm_none (p : Permission α F) :
@[simp] lemma compatiblePerm_some (P : ProbabilitySpace (α → V)) (p : Permission α F)
@[simp] theorem indepMul_none_left (y : PSp Ω) : indepMul (x
@[simp] theorem indepMul_none_right (x : PSp Ω) : indepMul (y
abbrev PSp (Ω : Type*)
def MeasurableSpace.insensitive {α V : Type*} (m : MeasurableSpace (α → V)) (S : _root_.Set α) : Prop
def compatiblePerm (P : PSp (α → V)) (p : Permission α F) : Prop
def compatiblePermRat (P : PSp (α → V)) (p : PermissionRat α) : Prop
def setEqOutside {α V : Type*} (S : _root_.Set α) (s t : α → V) : Prop
noncomputable def indepMul (x y : PSp Ω) : PSp Ω
theorem DFrac.op_eq_discard_iff {F : Type*} [UFraction F] (x y : Iris.DFrac F) :
theorem NNRat.add_eq_zero_iff (a b : ℚ≥0) : a + b = 0 ↔ a = 0 ∧ b = 0
theorem compatiblePermRat_indepMul (x y z : PSp (α → V)) (p₁ p₂ : PermissionRat α) :
theorem compatiblePermRat_indepProduct {α V : Type*}
theorem compatiblePerm_indepMul (x y z : PSp (α → V)) (p₁ p₂ : Permission α F) :
theorem compatiblePerm_indepProduct {α V F : Type*} [UFraction F]
theorem indepMul_assoc (x y z : PSp Ω) :
theorem indepMul_comm (x y : PSp Ω) : indepMul x y = indepMul y x
theorem indepMul_one_left [Nonempty Ω] (x : PSp Ω) :
theorem indepMul_one_right [Nonempty Ω] (x : PSp Ω) :
theorem insensitive_anti {α V : Type*} (m : MeasurableSpace (α → V))
theorem insensitive_bot {α V : Type*} (S : _root_.Set α) :
theorem insensitive_empty {α V : Type*} (m : MeasurableSpace (α → V)) :
theorem insensitive_sum_inter {α V : Type*}

src/Bluebell/Core/Indexed.lean (2)

def indexedTuple (α : Type*) (I : Finset ℕ)
def indexedTuple.remove (α : Type*) (I : Finset ℕ) (J : Finset ℕ) (_ : J ⊆ I) :

src/Bluebell/Logic/JointCondition.lean (14)

noncomputable def jointCondition {β : Type*} [MeasurableSpace β] [MeasurableSpace V]
noncomputable def liftRelation [Nonempty V] [DecidableEq V] [MeasurableSpace V]
theorem C_and [DecidableEq I] [Fintype I]
theorem C_assoc {β₁ β₂ : Type _} [MeasurableSpace β₁] [MeasurableSpace β₂]
theorem C_conseq (h : ∀ v, K₁ v ⊢ K₂ v) : 𝑪_ μ K₁ ⊢ 𝑪_ μ K₂
theorem C_exists {γ : Type*}
theorem C_forall {γ : Type*}
theorem C_frame {P : HyperAssertion (IndexedPSpPmRat I α V)} :
theorem C_pure {s : _root_.Set β} :
theorem C_sep_assertTrue {i : I} {E : (α → V) → Bool} :
theorem C_transfer {β' : Type*} [MeasurableSpace β'] {μ' : PMF β'}
theorem C_unassoc {β₁ β₂ : Type _} [MeasurableSpace β₁] [MeasurableSpace β₂]
theorem C_unit_left [Countable β] [MeasurableSingletonClass β] {v₀ : β} :
theorem C_unit_right [DecidableEq β] {i : I} {E : (α → V) → β} {μ : PMF β} :

src/Bluebell/Logic/Ownership.lean (14)

def assertExpectation {β : Type*} [MeasurableSpace β] [TopologicalSpace β]
def assertOwn {β : Type*} [MeasurableSpace β] (i : I) (E : (α → V) → β) :
def assertPermission (P : HyperAssertion (IndexedPSpPmRat I α V)) (p : I → PermissionRat α) :
def assertPermissionVar (i : I) (x : α) (q : ℚ≥0) : HyperAssertion (IndexedPSpPmRat I α V)
def assertProbability (i : I) (E : (α → V) → Bool) (prob : ENNReal) :
def assertSampledFrom {β : Type*} [MeasurableSpace β] (i : I) (E : (α → V) → β) (μ : PMF β) :
def ownIndexedProb (P : I → ProbabilityTheory.ProbabilitySpace (α → V)) :
def ownIndexedTuple (P : I → ProbabilityTheory.ProbabilitySpace (α → V)) (p : I → PermissionRat α) :
noncomputable def assertTrue (i : I) (E : (α → V) → Bool) :
theorem sampledFrom_inj {β : Type*} [MeasurableSpace β]
theorem sampledFrom_prod {β₁ β₂ : Type _}
theorem sep_assertTrue_iff {i : I} {E₁ E₂ : (α → V) → Bool} :
theorem sep_of_and [Fintype I]
theorem sep_of_and_assertTrue {i : I} {E : (α → V) → Bool}

src/Bluebell/Logic/WeakestPre.lean (5)

noncomputable def wp (t : IndexedPSpPmRat I α V → IndexedPSpPmRat I α V)
theorem wp_comp : (wp t₁ (wp t₂ Q)) ⊣⊢ (wp (t₁ ∘ t₂) Q)
theorem wp_conj : (wp t₁ Q₁) ∧ (wp t₂ Q₂) ⊣⊢ (wp (sorry) (and Q₁ Q₂))
theorem wp_conseq (h : Q ⊢ Q') : (wp t Q) ⊢ (wp t Q')
theorem wp_frame : P ∗ (wp t Q) ⊢ (wp t (sep P Q))

src/Bluebell/ProbabilityTheory/Coupling.lean (22)

def Coupling (p : SPMF α) (q : SPMF β)
def IsCoupling.supports (c : SPMF (α × β)) (R : Set (α × β)) : Prop
def Lift (p : SPMF α) (R : Set (α × β)) (q : SPMF β) : Prop
def SPMF : Type u → Type u
example (f g : α → β) (h : f = g) : ∀ x, f x = g x
noncomputable def prodMap (p : PMF α) (q : PMF β) : PMF (α × β)
theorem IsCoupling.bind {α₁ α₂ β₁ β₂ : Type u}
theorem IsCoupling.exists_bind {α₁ α₂ β₁ β₂ : Type u}
theorem IsCoupling.map
theorem IsCoupling.none_iff {α β : Type u} {c : SPMF (α × β)} :
theorem IsCoupling.prod (p : PMF α) (q : PMF β) :
theorem IsCoupling.pure_iff {α β : Type u} {a : α} {b : β} {c : SPMF (α × β)} :
theorem IsCoupling.symm {c : SPMF (α × β)} {p : SPMF α} {q : SPMF β}
theorem Lift.bind {p : SPMF α} {q : SPMF β} {R : Set (α × β)}
theorem Lift.graph (p : PMF α) (f : α → β) :
theorem Lift.map {p : PMF α} {q : PMF β} {R : Set (α × β)}
theorem Lift.mono {p : PMF α} {q : PMF β} {R S : Set (α × β)}
theorem Lift.pure_pure {a : α} {b : β} {R : Set (α × β)}
theorem Lift.symm {p : PMF α} {q : PMF β} {R : Set (α × β)}
theorem Lift.top (p : PMF α) (q : PMF β) : Lift p (Set.univ : Set (α × β)) q

…and 27 more not listed.

✏️ Added: 296 declaration(s)

src/Bluebell/Assertion.lean (172)

abbrev Assertion (M : Type*) [OrderedUnitalResourceAlgebra M]
abbrev bProp (I Var Val : Type*) [DecidableEq Var] [Inhabited Val]
abbrev dom (t : I → Option (PSpPm Var Val → PSpPm Var Val))
def BFalse : Assertion M
def BTrue : Assertion M
def PMF.dirac {A : Type*} [Countable A] (x : A) : PMF A
def PMF.toDiscMeasure {A : Type*} (μ : PMF A) : @Measure A ⊤
def PMF.toDiscMeasure_is_probability {A : Type*} (μ : PMF A)
def ValidIndexedPSpPm (I Var Val : Type*) [DecidableEq Var] [Inhabited Val] : Type _
def ValidIndexedPSpPm.PSp (m : ValidIndexedPSpPm I Var Val) (i : I)
def ValidIndexedPSpPm.PSpace (m : ValidIndexedPSpPm I Var Val) (i : I)
def ValidIndexedPSpPm.ms {I Var Val : Type*} [DecidableEq Var] [Inhabited Val]
def ValidIndexedPSpPm.perm (m : ValidIndexedPSpPm I Var Val) (i : I)
def ValidIndexedPSpPm.μ (m : ValidIndexedPSpPm I Var Val) (i : I)
def ValidPSp (Ω : Type*) [Inhabited Ω] : Type _
def ValidPSp.PSpace {Ω : Type*} [Inhabited Ω]
def ValidPSp.ms {Ω : Type*} [Inhabited Ω]
def ValidPSp.μ {Ω : Type*} [Inhabited Ω]
def ValidPSpPm (Var Val : Type*) [DecidableEq Var] [Inhabited Val] : Type _
def ValidPSpPm.PSp {Var Val : Type*} [DecidableEq Var] [Inhabited Val]
def ValidPSpPm.PSpace {Var Val : Type*} [DecidableEq Var] [Inhabited Val]
def ValidPSpPm.ms {Var Val : Type*} [DecidableEq Var] [Inhabited Val]
def ValidPSpPm.perm {Var Val : Type*} [DecidableEq Var] [Inhabited Val]
def ValidPSpPm.μ {Var Val : Type*} [DecidableEq Var] [Inhabited Val]
def almostMeasurable {A : Type*} (E : (Var → Val) → A) (P : PSp (Var → Val)) : Prop
def almostSurely (E : (Var → Val) → Prop) (i : I) : bProp I Var Val
def and (P Q : Assertion M) : Assertion M
def bexists {A : Type*} (K : A → Assertion M) : Assertion M
def bforall {A : Type*} (K : A → Assertion M) : Assertion M
def bident : Assertion M
def bientail (P Q : Assertion M) : Prop
def bimp (P Q : Assertion M) : Assertion M
def bpersistently (P : Assertion M) : Assertion M
def entail {ra : OrderedUnitalResourceAlgebra M} (P Q : @Assertion M ra) : Prop
def fusion {A B : Type*} (μ : PMF A) (κ : A → PMF B) : PMF (A × B)
def hasDistribution {A : Type*} (E : (Var → Val) → A) (i : I) (μ : PMF A)
def hoare {Var Val : Type*}
def hyperTermReferences (t : I → Option (PSpPm Var Val → PSpPm Var Val)) : Set I
def hyperTermSemantics {Var Val : Type*} [DecidableEq Var] [Inhabited Val]
def idx
def irrelevant
def jointConditioning {A Var Val : Type*}
def lift (φ : Prop) : Assertion M
def or (P Q : Assertion M) : Assertion M
def own (b : M) : Assertion M
def ownIndexedPSpPm (P : I → PSp (Var → Val)) (p : IxCompatiblePermission P)
def ownPSp (P : I → PSp (Var → Val)) : bProp I Var Val
def ownRV {A : Type*} (E : (Var → Val) → A) (i : I) : bProp I Var Val
def pabs [DecidableEq I] (P : bProp I Var Val) (X : Set (I × Var)) : Prop
def product {A B : Type*} (μ₁ : PMF A) (μ₂ : PMF B) : PMF (A × B)
def pvar {A : Type*} (E : (Var → Val) → A) : Set Var
def relationalLifting {X : Set (I × Var)} (R : Set (X → Val)) : bProp I Var Val
def sExistsA (Ψ : Assertion M → Prop) : Assertion M
def sForallA (Ψ : Assertion M → Prop) : Assertion M
def sep (P Q : Assertion M) : Assertion M
def wand (P Q : Assertion M) : Assertion M
def wp {Var Val : Type*}
example {P : bProp I Var Val} : ⊢ P -∗ BTrue
lemma emp_implies_own_unit : emp ⊢ own (1 : IndexedPSpPm I Var Val)
lemma sep_affine
lemma true_subst_star
noncomputable def k {A : Type*} : CompatibleKernel A (@validOne I Var Val _ _)
noncomputable def validOne : ValidIndexedPSpPm I Var Val
noncomputable instance assertionBI : Iris.BI (bProp I Var Val) where
noncomputable instance assertionBIBase : Iris.BI.BIBase (bProp I Var Val) where
private def CompatibleKernel.comp {A B : Type*}
private def CompatibleKernel.constSelf {A : Type*} (m : ValidIndexedPSpPm I Var Val) :
private def CompatibleKernel.pmfBind {A B : Type*} {m₀ : ValidIndexedPSpPm I Var Val}
private lemma PMF_bind_comp_of_bijOn {A B : Type*} {μ : PMF A} {μ' : PMF B}
private lemma PMF_toMeasure_bind {A B : Type*} (μ : PMF A) (κ : A → PMF B) :
private lemma PMF_tsum_comp_of_bijOn {A B : Type*} {μ : PMF A} {μ' : PMF B}
private lemma PSpace_eq (m : ValidIndexedPSpPm I Var Val) (i : I) :
private lemma Sure_Merge_fwd {E₁ E₂ : (Var → Val) → Prop} {i : I}
private lemma ValidIndexedPSpPm.ae_PSpace_iff_μ (m : ValidIndexedPSpPm I Var Val) (i : I)
private lemma ValidIndexedPSpPm.aemeasurable_PSpace_iff_μ {A : Type*}
private lemma ValidIndexedPSpPm.map_μ_eq_map_PSpace_μ {A : Type*}
private lemma ValidIndexedPSpPm.mu_apply_eq_PSpace (m : ValidIndexedPSpPm I Var Val)
private lemma ValidIndexedPSpPm.val_psp_eq_some (m : ValidIndexedPSpPm I Var Val) (i : I) :
private lemma ValidPSpPm.PSpace_eq (pp : ValidPSpPm Var Val) :
private lemma ValidPSpPm.ae_PSpace_iff_μ (pp : ValidPSpPm Var Val)
private lemma ValidPSpPm.aemeasurable_PSpace_iff_μ {A : Type*} (pp : ValidPSpPm Var Val)
private lemma ValidPSpPm.map_μ_eq_map_PSpace_μ {A : Type*}
private lemma ValidPSpPm.mu_apply_eq_PSpace (pp : ValidPSpPm Var Val)
private lemma aemeasurable_pmf_bind {A B : Type*} {mB : MeasurableSpace B}
private lemma almostSurely_ae {E : (Var → Val) → Prop} {i : I}
private lemma almostSurely_elim {E : (Var → Val) → Prop} {i : I}
private lemma almostSurely_intro {E : (Var → Val) → Prop} {i : I}
private lemma bind_event_null {A : Type*}
private lemma compat_of_ms (m₀ : ValidIndexedPSpPm I Var Val) (i : I)
private lemma compatiblePerm_update_update_of_ne_zero [DecidableEq I]
private lemma const_bind_top {A β : Type*} {mβ : MeasurableSpace β}
private lemma dirac_bind_top {A β : Type*} [Countable A] {mβ : MeasurableSpace β}
private lemma hasDistribution_elim {A : Type*} {E : (Var → Val) → A} {i : I} {ν : PMF A}
private lemma hasDistribution_intro {A : Type*} {E : (Var → Val) → A} {i : I} {μ : PMF A}
private lemma hasDistribution_witness {A : Type*} {E : (Var → Val) → A} {i : I} {ν : PMF A}
private lemma irrelevant_binary_inter
private lemma irrelevant_idx_compl [Inhabited Var] [Finite I]
private lemma irrelevant_sInter_valid [Inhabited Var] [Finite I]
private lemma isProbabilityMeasure_bind_top {A β : Type*} {mβ : MeasurableSpace β}
private lemma jointConditioning_elem_valid {A : Type*}
private lemma map_eq_map_of_measure_le {A : Type*}
private lemma map_eq_map_of_pspace_le {A : Type*} {p q : PSpace (Var → Val)}
private lemma map_pmf_bind_const {A B : Type*} {mB : MeasurableSpace B}
private lemma mu_isProb (m : ValidIndexedPSpPm I Var Val) (i : I) :
private lemma ownPSp_self (m : ValidIndexedPSpPm I Var Val) :
private lemma pmfBind_kernel_bind {A B : Type*} {m₀ : ValidIndexedPSpPm I Var Val}
private lemma pmf_bind_eq_sum_support {A : Type*}
private lemma pmf_pushforward_hasSum {A B : Type*} (μ : PMF A) (f : A → B) :
private lemma pmf_tsum_subtype_eq_one_iff {A : Type*} {X : Set A} {μ : PMF A} :
private lemma product_eq_bind {A B : Type*} (μ₁ : PMF A) (μ₂ : PMF B) :
private lemma psp_trim_indep {ps : PSpace (Var → Val)} {F : MeasurableSpace (Var → Val)}
private lemma pushforward_eq_map {A B : Type*} (μ : PMF A) (f : A → B) :
private lemma val_eq_point (m : ValidIndexedPSpPm I Var Val) :
theorem And_To_Star [Inhabited Var] [Finite I]
theorem Assoc {A B C : Type*} {μ : PMF A} {κ₁ : A → PMF B} {κ₂ : B → PMF C} :
theorem C_And {A : Type*} {μ : PMF A} {K₁ K₂ : A → bProp I Var Val} :
theorem C_Assoc {A B : Type*} {μ : PMF A} {μ₀ : PMF (A × B)} {κ : A → PMF B} {K : (A × B) → bProp I Var Val} :
theorem C_Cons {α : Type} {K₁ K₂ : α → bProp I Var Val} {μ : PMF α} (h : ∀ v, K₁ v ⊢ K₂ v) :
theorem C_Dist_Proj {A B C : Type*} {μ₁ : PMF (A × B)} {μ₂ : A → (PMF C)} {i : I} {E : A → (Var → Val) → C} :
theorem C_Extract {A B : Type*}
theorem C_False {A : Type*} {μ : PMF A} :
theorem C_For_All {A X : Type*} {μ : PMF A} {Q : (A × X) → bProp I Var Val} :
theorem C_Frame {A : Type*} {μ : PMF A} {P : bProp I Var Val} {K : A → bProp I Var Val} :
theorem C_Fuse {A B : Type*} {μ : PMF A} {κ : A → PMF B} {K : (A × B) → bProp I Var Val} :
theorem C_Pure {A : Type*} {X : Set A} {μ : PMF A} {K : A → bProp I Var Val} :
theorem C_Skolem {A X : Type*} {μ : PMF A} {Q : (A × X) → bProp I Var Val } :
theorem C_Sure_Proj {A B : Type*} {i : I} {μ : PMF (A × B)} {E : A → (Var → Val) → Prop}
theorem C_Sure_Proj_Many {A B : Type*} {i : I} {X : Set (I × Var)} {μ : PMF ((X → Val) × B)} :
theorem C_Swap {A B : Type*} {μ₁ : PMF A} {μ₂ : PMF B} (K : (A × B) → bProp I Var Val) :
theorem C_Transf {A B : Type*}
theorem C_True
theorem C_Unassoc {A B : Type*} {μ : PMF A} {κ : A → PMF B} {K : B → bProp I Var Val} :
theorem C_Unit_L {A : Type*} [Countable A] {v₀ : A} {K : A → bProp I Var Val} :
theorem C_Unit_R {A : Type*} {i : I} {μ : PMF A} {E : (Var → Val) → A} :
theorem C_WP_Swap {A : Type*} [Countable A]
theorem Coupling
theorem Dirac_Dup
theorem Dist_Convex {A : Type*}
theorem Dist_Fun {i : I} {A B: Type*}
theorem Dist_Inj
theorem Dist_Supp {i : I} {A : Type*}
theorem PMF.dirac_eq_one_iff_eq
theorem Prod_Split {i : I} {A B : Type*}
theorem Prod_Unsplit {A B : Type*} {i : I}
theorem RL_Cons {X : Set (I × Var)} {R₁ R₂ : Set (X → Val)} :
theorem RL_Convex {α : Type} {X : Set (I × Var)} {μ : PMF α} {R : Set (X → Val)} :
theorem RL_Eq_Dist {A : Type*} [Inhabited A] [Inhabited X] {X : Set (I × Var)} {μ : PMF A} {ix jy : X} :
theorem RL_Merge {X : Set (I × Var)} {R₁ R₂ : Set (X → Val)} :
theorem RL_Sure_Merge {X : Set (I × Var)} {R : Set (X → Val)} {e : (Var → Val) → Val}
theorem RL_Unary {X : Set Var} [Finite X] {R : Set (X → Val)}

…and 146 more not listed.

sorry Tracking

✅ Removed: 29 `sorry`(s)

src/Bluebell/Logic/JointCondition.lean (14)

noncomputable def jointCondition {β : Type*} [MeasurableSpace β] [MeasurableSpace V] (L71)
theorem C_and [DecidableEq I] [Fintype I] (L131)
theorem C_assoc {β₁ β₂ : Type _} [MeasurableSpace β₁] [MeasurableSpace β₂] (L120)
theorem C_conseq (h : ∀ v, K₁ v ⊢ K₂ v) : 𝑪_ μ K₁ ⊢ 𝑪_ μ K₂ (L101)
theorem C_exists {γ : Type*} (L137)
theorem C_forall {γ : Type*} (L142)
theorem C_frame {P : HyperAssertion (IndexedPSpPmRat I α V)} : (L105)
theorem C_pure {s : _root_.Set β} : (L156)
theorem C_sep_assertTrue {i : I} {E : (α → V) → Bool} : (L152)
theorem C_transfer {β' : Type*} [MeasurableSpace β'] {μ' : PMF β'} (L147)
theorem C_transfer {β' : Type*} [MeasurableSpace β'] {μ' : PMF β'} (L148)
theorem C_unassoc {β₁ β₂ : Type _} [MeasurableSpace β₁] [MeasurableSpace β₂] (L126)
theorem C_unit_left [Countable β] [MeasurableSingletonClass β] {v₀ : β} : (L109)
theorem C_unit_right [DecidableEq β] {i : I} {E : (α → V) → β} {μ : PMF β} : (L113)

src/Bluebell/Logic/Ownership.lean (3)

theorem sampledFrom_inj {β : Type*} [MeasurableSpace β] (L189)
theorem sampledFrom_prod {β₁ β₂ : Type _} (L242)
theorem sep_assertTrue_iff {i : I} {E₁ E₂ : (α → V) → Bool} : (L198)

src/Bluebell/Logic/WeakestPre.lean (2)

theorem wp_comp : (wp t₁ (wp t₂ Q)) ⊣⊢ (wp (t₁ ∘ t₂) Q) (L71)
theorem wp_conj : (wp t₁ Q₁) ∧ (wp t₂ Q₂) ⊣⊢ (wp (sorry) (and Q₁ Q₂)) (L74)

src/Bluebell/ProbabilityTheory/IndepProduct.lean (10)

@[simp] theorem indepProduct_one_left_toMeasureSpace [Nonempty Ω] (m : ProbabilitySpace Ω) : (L311)
@[simp] theorem indepProduct_one_right_toMeasureSpace [Nonempty Ω] (m : ProbabilitySpace Ω) : (L318)
def Measure.IndependentProduct.symm (L163)
theorem indepProduct_assoc (m₁ m₂ m₃ : MeasureSpace Ω) : (L195)
theorem indepProduct_assoc (m₁ m₂ m₃ : ProbabilitySpace Ω) : (L272)
theorem indepProduct_assoc_toMeasureSpace (m₁ m₂ m₃ : ProbabilitySpace Ω) : (L304)
theorem indepProduct_comm (m₁ m₂ : MeasureSpace Ω) : (L188)
theorem indepProduct_comm (m₁ m₂ : ProbabilitySpace Ω) : (L248)
theorem indepProduct_one_left [Nonempty Ω] (m : ProbabilitySpace Ω) : (L256)
theorem indepProduct_one_right [Nonempty Ω] (m : ProbabilitySpace Ω) : (L264)

❌ Added: 25 `sorry`(s)

src/Bluebell/Assertion.lean (25)

theorem C_And {A : Type*} {μ : PMF A} {K₁ K₂ : A → bProp I Var Val} : (L2084)
theorem C_Assoc {A B : Type*} {μ : PMF A} {μ₀ : PMF (A × B)} {κ : A → PMF B} {K : (A × B) → bProp I Var Val} : (L2054)
theorem C_Dist_Proj {A B C : Type*} {μ₁ : PMF (A × B)} {μ₂ : A → (PMF C)} {i : I} {E : A → (Var → Val) → C} : (L2832)
theorem C_Extract {A B : Type*} (L2819)
theorem C_Frame {A : Type*} {μ : PMF A} {P : bProp I Var Val} {K : A → bProp I Var Val} : (L2003)
theorem C_Fuse {A B : Type*} {μ : PMF A} {κ : A → PMF B} {K : (A × B) → bProp I Var Val} : (L2699)
theorem C_Sure_Proj {A B : Type*} {i : I} {μ : PMF (A × B)} {E : A → (Var → Val) → Prop} (L2800)
theorem C_Sure_Proj_Many {A B : Type*} {i : I} {X : Set (I × Var)} {μ : PMF ((X → Val) × B)} : (L2808)
theorem C_Swap {A B : Type*} {μ₁ : PMF A} {μ₂ : PMF B} (K : (A × B) → bProp I Var Val) : (L2705)
theorem C_Unit_R {A : Type*} {i : I} {μ : PMF A} {E : (Var → Val) → A} : (L2046)
theorem C_WP_Swap {A : Type*} [Countable A] (L2406)
theorem Coupling (L2929)
theorem Dist_Supp {i : I} {A : Type*} (L2670)
theorem Prod_Split {i : I} {A B : Type*} (L1924)
theorem Prod_Unsplit {A B : Type*} {i : I} (L2679)
theorem RL_Convex {α : Type} {X : Set (I × Var)} {μ : PMF α} {R : Set (X → Val)} : (L2895)
theorem RL_Eq_Dist {A : Type*} [Inhabited A] [Inhabited X] {X : Set (I × Var)} {μ : PMF A} {ix jy : X} : (L2888)
theorem RL_Merge {X : Set (I × Var)} {R₁ R₂ : Set (X → Val)} : (L2901)
theorem RL_Sure_Merge {X : Set (I × Var)} {R : Set (X → Val)} {e : (Var → Val) → Val} (L2916)
theorem RL_Unary {X : Set Var} [Finite X] {R : Set (X → Val)} (L2880)
theorem Sure_And_Star [DecidableEq I] {i : I} {A : Type*} (L1915)
theorem Sure_Merge (L1906)
theorem Sure_Str_Convex {A : Type*} {μ : PMF A} (L2234)
theorem WP_Conj (L2395)
theorem WP_Nest (L2362)

Coverage Notes

AI file summarization partially analyzed 1 file(s) because their individual diffs exceeded the per-file size budget. Statistics and Lean signal tracking still cover the full PR.

Partially Analyzed Files

src/Bluebell/Assertion.lean (+2955/-0)

📄 **Per-File Summaries**

src/Bluebell.lean: Summary unavailable — error: Error code: 401 - {'error': {'message': 'Missing Authentication header', 'code': 401}}
src/Bluebell/Algebra/CMRA.lean: Summary unavailable — error: Error code: 401 - {'error': {'message': 'Missing Authentication header', 'code': 401}}
src/Bluebell/Algebra/HyperAssertion.lean: Summary unavailable — error: Error code: 401 - {'error': {'message': 'Missing Authentication header', 'code': 401}}
src/Bluebell/Algebra/PSpPm.lean: Summary unavailable — error: Error code: 401 - {'error': {'message': 'Missing Authentication header', 'code': 401}}
src/Bluebell/Algebra/Permission.lean: Summary unavailable — error: Error code: 401 - {'error': {'message': 'Missing Authentication header', 'code': 401}}
src/Bluebell/Algebra/Probability.lean: Summary unavailable — error: Error code: 401 - {'error': {'message': 'Missing Authentication header', 'code': 401}}
src/Bluebell/Assertion.lean: Summary unavailable — error: Error code: 401 - {'error': {'message': 'Missing Authentication header', 'code': 401}}
src/Bluebell/Core/Indexed.lean: Summary unavailable — error: Error code: 401 - {'error': {'message': 'Missing Authentication header', 'code': 401}}
src/Bluebell/Logic/JointCondition.lean: Summary unavailable — error: Error code: 401 - {'error': {'message': 'Missing Authentication header', 'code': 401}}
src/Bluebell/Logic/Ownership.lean: Summary unavailable — error: Error code: 401 - {'error': {'message': 'Missing Authentication header', 'code': 401}}
src/Bluebell/Logic/WeakestPre.lean: Summary unavailable — error: Error code: 401 - {'error': {'message': 'Missing Authentication header', 'code': 401}}
src/Bluebell/MeasureOnSpace.lean: Summary unavailable — error: Error code: 401 - {'error': {'message': 'Missing Authentication header', 'code': 401}}
src/Bluebell/OURA.lean: Summary unavailable — error: Error code: 401 - {'error': {'message': 'Missing Authentication header', 'code': 401}}
src/Bluebell/ProbabilityTheory/Coupling.lean: Summary unavailable — error: Error code: 401 - {'error': {'message': 'Missing Authentication header', 'code': 401}}
src/Bluebell/ProbabilityTheory/IndepProduct.lean: Summary unavailable — error: Error code: 401 - {'error': {'message': 'Missing Authentication header', 'code': 401}}

Last updated: 2026-07-03 04:49 UTC.

github-actions

🤖 AI Review

Overall Summary:
TL;DR: The PR successfully completes a major architectural transition to a new OURA-based framework by deleting legacy CMRA code and introducing clean algebraic foundations. However, the introduction of over 30 unproven theorems (sorry) in the core separation logic and missing concrete program semantics necessitates major revisions.

Mechanical Pre-Check Results: Mechanical pre-checks flagged 34 instances of the sorry escape hatch introduced in src/Bluebell/Assertion.lean for core separation logic rules. Additionally, src/Bluebell/Assertion.lean (2267 lines) and src/Bluebell/MeasureOnSpace.lean (1696 lines) exceed the 1500-line file size limit.

Checklist Coverage: No explicit specification checklist was provided for this PR.

Cross-File Issues: The composition chain correctly links the algebraic model OURA through MeasureOnSpace.lean into the separation logic assertions in Assertion.lean. However, the composition breaks at the program logic level: concrete program weakest precondition rules are left as unverified TODOs, meaning the abstract Hoare logic cannot be applied to concrete probabilistic program evaluations. The extensive use of sorry in foundational rules also transitively compromises the soundness of downstream logic derivations.

Key Lean 4 / Mathlib Issues:

Hard Rule Violation: 34 instances of sorry are used to stub out proofs for core logical inference rules (e.g., Sure_Merge, Sure_And_Star, C_Frame, WP_Nest). This systematically bypasses the Lean kernel's verifier. (src/Bluebell/Assertion.lean:1239-2241 (multiple locations))
Overlapping FunLike instances. A generic instance for FunLike (Assertion M) M Prop is immediately followed by a specialized instance for FunLike (bProp I Var Val) .... Since bProp is an abbreviation for Assertion, these instances overlap exactly and will cause typeclass resolution issues. (src/Bluebell/Assertion.lean:191-197)
Duplicated namespace for the UCMRA instance resulting in the fully qualified name OrderedUnitalResourceAlgebra.OrderedUnitalResourceAlgebra.instUCMRA. This triggers a Lean 4 compiler warning. (src/Bluebell/OURA.lean:419-422)
The instance Valid (I → M) unnecessarily inherits the [OrderedUnitalResourceAlgebra M] typeclass because it is declared inside a section where this variable is active. This overly restricts the pointwise Valid instance. (src/Bluebell/OURA.lean:94-96)
The formalization lacks WP rules for concrete program constructs (e.g., Skip, Seq, Assign, Samp), which are left as TODO: Shallow embedding. This leaves the abstract separation logic with no concrete programming language to evaluate. (src/Bluebell/Assertion.lean:1633-1662)

Overall Verdict: Changes Requested

🔍 **Mechanical Pre-Check Results**

Escape hatches introduced in this PR (triggers hard verdict rule):

sorry introduced in src/Bluebell/Assertion.lean: sorry -- TODO: Rule SURE-MERGE proof
sorry introduced in src/Bluebell/Assertion.lean: sorry -- TODO: Rule SURE-AND-STAR proof
sorry introduced in src/Bluebell/Assertion.lean: sorry -- TODO: Rule PROD-SPLIT proof
sorry introduced in src/Bluebell/Assertion.lean: sorry -- TODO: Rule C-FRAME proof (spec not yet reviewed)
sorry introduced in src/Bluebell/Assertion.lean: sorry -- TODO: Rule C-UNIT-L proof (spec not yet reviewed)
sorry introduced in src/Bluebell/Assertion.lean: sorry -- TODO: Rule C-UNIT-L proof (spec not yet reviewed)
sorry introduced in src/Bluebell/Assertion.lean: sorry -- TODO: Rule C-ASSOC proof (spec not yet reviewed)
sorry introduced in src/Bluebell/Assertion.lean: sorry -- TODO: Rule C-UNASSOC proof (spec not yet reviewed)
sorry introduced in src/Bluebell/Assertion.lean: sorry -- TODO: Rule C-AND proof (spec not yet reviewed)
sorry introduced in src/Bluebell/Assertion.lean: sorry -- TODO: Rule C-SKOLEM proof (spec not yet reviewed)
sorry introduced in src/Bluebell/Assertion.lean: sorry -- TODO: Rule SURE-STR-CONVEX proof
sorry introduced in src/Bluebell/Assertion.lean: sorry -- TODO: Rule C-FOR-ALL proof (spec not yet reviewed)
sorry introduced in src/Bluebell/Assertion.lean: sorry -- TODO: Rule C-PURE proof
sorry introduced in src/Bluebell/Assertion.lean: sorry -- TODO: Rule WP-NEST proof (spec not yet reviewed)
sorry introduced in src/Bluebell/Assertion.lean: sorry -- TODO: Rule WP-CONJ proof
sorry introduced in src/Bluebell/Assertion.lean: sorry -- TODO: Rule C-WP-SWAP proof (spec not yet reviewed)
sorry introduced in src/Bluebell/Assertion.lean: sorry -- TODO: Rule SURE-SUB proof
sorry introduced in src/Bluebell/Assertion.lean: sorry -- TODO: Rule DIST-FUN proof
sorry introduced in src/Bluebell/Assertion.lean: sorry -- TODO: Rule DIRAC-DUP proof
sorry introduced in src/Bluebell/Assertion.lean: sorry -- TODO: Rule DIRAC-SUPP proof
sorry introduced in src/Bluebell/Assertion.lean: sorry -- TODO: Rule PROD-UNSPLIT proof
sorry introduced in src/Bluebell/Assertion.lean: sorry -- TODO: Rule C-FUSE proof (spec not yet reviewed)
sorry introduced in src/Bluebell/Assertion.lean: sorry -- TODO: Rule C-SWAP proof (spec not yet reviewed)
sorry introduced in src/Bluebell/Assertion.lean: sorry -- TODO: Rule DIST-CONVEX proof
sorry introduced in src/Bluebell/Assertion.lean: sorry -- TODO: Rule C-SURE-PROJ proof (spec not yet reviewed)
sorry introduced in src/Bluebell/Assertion.lean: sorry -- TODO: Rule C-SURE-PROJ-MANY proof (spec not yet reviewed)
sorry introduced in src/Bluebell/Assertion.lean: sorry -- TODO: Rule C-EXTRACT proof
sorry introduced in src/Bluebell/Assertion.lean: sorry -- TODO: Rule C-DIST-PROJ proof (spec not yet reviewed)
sorry introduced in src/Bluebell/Assertion.lean: sorry -- TODO: Rule RL-UNARY proof
sorry introduced in src/Bluebell/Assertion.lean: sorry -- TODO: Rule RL-EQ-DIST proof (spec not yet reviewed)
sorry introduced in src/Bluebell/Assertion.lean: sorry -- TODO: Rule RL-CONVEX proof
sorry introduced in src/Bluebell/Assertion.lean: sorry -- TODO: Rule RL-SURE-MERGE proof
sorry introduced in src/Bluebell/Assertion.lean: sorry -- TODO: Rule RL-SURE-MERGE proof
sorry introduced in src/Bluebell/Assertion.lean: sorry -- TODO: Rule COUPLING proof
Large file: src/Bluebell/Assertion.lean is 2267 lines (exceeds 1500-line lint threshold)
Large file: src/Bluebell/MeasureOnSpace.lean is 1696 lines (exceeds 1500-line lint threshold)

Pre-existing escape hatches in touched files (context only, does not affect verdict):

sorry in src/Bluebell/Assertion.lean line 1239: sorry -- TODO: Rule SURE-MERGE proof
sorry in src/Bluebell/Assertion.lean line 1248: sorry -- TODO: Rule SURE-AND-STAR proof
sorry in src/Bluebell/Assertion.lean line 1257: sorry -- TODO: Rule PROD-SPLIT proof
sorry in src/Bluebell/Assertion.lean line 1336: sorry -- TODO: Rule C-FRAME proof (spec not yet reviewed)
sorry in src/Bluebell/Assertion.lean line 1342: sorry -- TODO: Rule C-UNIT-L proof (spec not yet reviewed)
sorry in src/Bluebell/Assertion.lean line 1348: sorry -- TODO: Rule C-UNIT-L proof (spec not yet reviewed)
sorry in src/Bluebell/Assertion.lean line 1356: sorry -- TODO: Rule C-ASSOC proof (spec not yet reviewed)
sorry in src/Bluebell/Assertion.lean line 1362: sorry -- TODO: Rule C-UNASSOC proof (spec not yet reviewed)
sorry in src/Bluebell/Assertion.lean line 1369: sorry -- TODO: Rule C-AND proof (spec not yet reviewed)
sorry in src/Bluebell/Assertion.lean line 1375: sorry -- TODO: Rule C-SKOLEM proof (spec not yet reviewed)
sorry in src/Bluebell/Assertion.lean line 1497: sorry -- TODO: Rule SURE-STR-CONVEX proof
sorry in src/Bluebell/Assertion.lean line 1503: sorry -- TODO: Rule C-FOR-ALL proof (spec not yet reviewed)
sorry in src/Bluebell/Assertion.lean line 1519: sorry -- TODO: Rule C-PURE proof
sorry in src/Bluebell/Assertion.lean line 1585: sorry -- TODO: Rule WP-NEST proof (spec not yet reviewed)
sorry in src/Bluebell/Assertion.lean line 1618: sorry -- TODO: Rule WP-CONJ proof
sorry in src/Bluebell/Assertion.lean line 1629: sorry -- TODO: Rule C-WP-SWAP proof (spec not yet reviewed)
sorry in src/Bluebell/Assertion.lean line 1953: sorry -- TODO: Rule SURE-SUB proof
sorry in src/Bluebell/Assertion.lean line 1965: sorry -- TODO: Rule DIST-FUN proof
sorry in src/Bluebell/Assertion.lean line 1974: sorry -- TODO: Rule DIRAC-DUP proof
sorry in src/Bluebell/Assertion.lean line 1983: sorry -- TODO: Rule DIRAC-SUPP proof
sorry in src/Bluebell/Assertion.lean line 1992: sorry -- TODO: Rule PROD-UNSPLIT proof
sorry in src/Bluebell/Assertion.lean line 2012: sorry -- TODO: Rule C-FUSE proof (spec not yet reviewed)
sorry in src/Bluebell/Assertion.lean line 2018: sorry -- TODO: Rule C-SWAP proof (spec not yet reviewed)
sorry in src/Bluebell/Assertion.lean line 2104: sorry -- TODO: Rule DIST-CONVEX proof
sorry in src/Bluebell/Assertion.lean line 2112: sorry -- TODO: Rule C-SURE-PROJ proof (spec not yet reviewed)
sorry in src/Bluebell/Assertion.lean line 2120: sorry -- TODO: Rule C-SURE-PROJ-MANY proof (spec not yet reviewed)
sorry in src/Bluebell/Assertion.lean line 2131: sorry -- TODO: Rule C-EXTRACT proof
sorry in src/Bluebell/Assertion.lean line 2144: sorry -- TODO: Rule C-DIST-PROJ proof (spec not yet reviewed)
sorry in src/Bluebell/Assertion.lean line 2192: sorry -- TODO: Rule RL-UNARY proof
sorry in src/Bluebell/Assertion.lean line 2200: sorry -- TODO: Rule RL-EQ-DIST proof (spec not yet reviewed)
sorry in src/Bluebell/Assertion.lean line 2207: sorry -- TODO: Rule RL-CONVEX proof
sorry in src/Bluebell/Assertion.lean line 2213: sorry -- TODO: Rule RL-SURE-MERGE proof
sorry in src/Bluebell/Assertion.lean line 2228: sorry -- TODO: Rule RL-SURE-MERGE proof
sorry in src/Bluebell/Assertion.lean line 2241: sorry -- TODO: Rule COUPLING proof

🔗 **Cross-File Analysis**

Cross-File Analysis:
The PR radically restructures the Bluebell project by replacing multiple fragmented logic and algebra files with three core modules: OURA.lean (algebraic structures), MeasureOnSpace.lean (instantiation of resource algebras for probability spaces), and Assertion.lean (the separation logic and rules).

Composition Chain: The algebraic model OrderedUnitalResourceAlgebra flows cleanly into MeasureOnSpace.lean, which builds the concrete model IndexedPSpPm. This model is then correctly consumed by Assertion.lean to define the base proposition type bProp and its Iris BI (separation logic) instances. The chain successfully wires measure theory to separation logic.
Type-Flow: Types and typeclasses flow correctly across the files. However, in OURA.lean, the instUCMRA instance is wrapped in an extra namespace, resulting in the duplicated name OrderedUnitalResourceAlgebra.OrderedUnitalResourceAlgebra.instUCMRA. Additionally, the program semantics in wp (hyperTermSemantics) models programs as deterministic functions PSpPm → PSpPm rather than monadic probabilistic transitions, which is a side-effect of a shallow embedding strategy.
Escape Hatch Impact: Assertion.lean introduces over 30 sorrys for core logical rules (e.g., Sure_Merge, Sure_And_Star, C_Frame, C_Fuse, Coupling). Since these are the primitive axioms of the separation logic, any downstream program verification will transitively depend on these unproven soundness claims, critically weakening the verification guarantees of the framework.
Missing Verification: The PR leaves all concrete program weakest precondition rules (WP_SKIP, WP_SEQ, WP_SAMP, etc.) as commented TODOs. This breaks the composition chain: the abstract separation logic has no concrete programming language to evaluate.

Cross-File Composition Issues:

Duplicated namespace for the UCMRA instance resulting in the fully qualified name OrderedUnitalResourceAlgebra.OrderedUnitalResourceAlgebra.instUCMRA. (src/Bluebell/OURA.lean:419-422)
- Suggested fix: Remove the namespace OrderedUnitalResourceAlgebra block wrapper around the instance or remove the OrderedUnitalResourceAlgebra. prefix from the instance name.

Axiom/Escape Hatch Impact:

Over 30 core logical rules in the separation logic are stubbed with sorry (e.g., Sure_Merge, Sure_And_Star, C_Frame, WP_Nest, Coupling). This propagates unverified assumptions to any downstream Hoare logic derivations, leaving the logic's soundness largely unproven. (src/Bluebell/Assertion.lean:1235-2245 (multiple locations))
- Suggested fix: These axioms must be proven against the IndexedPSpPm model semantics to guarantee the soundness of the Bluebell logic.

External Dependency Issues: None

Missing Cross-File Verification:

The formalization lacks WP rules for concrete program constructs (e.g., Skip, Seq, Assign, Samp), which are left as TODO: Shallow embedding. This breaks the composition chain because the abstract Hoare logic (wp) cannot be applied to concrete probabilistic program evaluations. (src/Bluebell/Assertion.lean:1633-1662)
- Suggested fix: Implement the shallow or deep embedding for the specific probabilistic language constructs and formally prove their corresponding WP rules against the core wp definition.

Cluster: Algebraic Framework and Probability Models (critical)

Do the new OrderedUnitalResourceAlgebra (OURA) and MeasureOnSpace models correctly capture the resource semantics required by the Bluebell logic?

📄 **Review for `src/Bluebell/OURA.lean`**

Analysis:

Mathematical Correctness: The file accurately formalizes the algebraic foundations of a separation logic resource model. It defines Valid and DiscreteCMRA to bridge with Iris's CMRA structure. It introduces OrderedUnitalResourceAlgebra (OURA) as a commutative monoid equipped with a preorder, right-monotone multiplication, and downward-closed validity (a ≤ b → ✓ b → ✓ a). The lifting of OURA to subtypes (subalgebra), dependent products (indexedProduct), and binary products is mathematically sound. The most complex construction, the quotient algebra, is executed perfectly: it correctly requires compatibility proofs for multiplication (hclo), validity (hvalid), and inequalities (hle), ensuring the resulting quotient structure forms a valid OURA.
Lean 4 Best Practices: The code is well-written and makes excellent use of modern Lean 4 idioms, including aesop, grind, and automatic typeclass synthesis for inherited structure fields (e.g., relying on Subtype.preorder instead of manually defining le). However, there are two minor issues. First, there is a duplicated namespace leading to a compiler warning on line 420. Second, due to Lean 4's section variable auto-inclusion rules, the Valid (I → M) instance unintentionally inherits the [OrderedUnitalResourceAlgebra M] typeclass from the section variables, making the instance overly restrictive.
Ambiguities / Escape Hatches: There are no sorrys, axioms, or unverified escape hatches in this file. The logic is robustly verified by the kernel.

Verdict: Needs Minor Revisions

Critical Misformalizations: None

Lean 4 / Mathlib Issues:

The instance OrderedUnitalResourceAlgebra.instUCMRA is declared inside the OrderedUnitalResourceAlgebra namespace, leading to the duplicated name OrderedUnitalResourceAlgebra.OrderedUnitalResourceAlgebra.instUCMRA. This triggers a Lean 4 compiler warning. (src/Bluebell/OURA.lean:420)
- Suggested fix: Rename the instance to just instUCMRA to avoid namespace duplication: instance instUCMRA {M : Type*} [ra : OrderedUnitalResourceAlgebra M] : Iris.UCMRA M := { ... }
The instance Valid (I → M) is declared in a section where [OrderedUnitalResourceAlgebra M] is an active variable. Lean 4's auto-implicit rules will include this typeclass as a parameter because M appears in the instance type. This unnecessarily restricts the pointwise Valid instance to types that are OrderedUnitalResourceAlgebra, whereas it should mathematically apply to any type with just [Valid M]. (src/Bluebell/OURA.lean:94-96)
- Suggested fix: Move this instance outside of the section where variable {I M : Type*} [OrderedUnitalResourceAlgebra M] is declared, so it only depends on the explicitly provided [Valid M].

Nitpicks:

Typo in the docstring for product: 'instnace' instead of 'instance'. (src/Bluebell/OURA.lean:184)

📄 **Review for `src/Bluebell/MeasureOnSpace.lean`**

Analysis:
Step-by-step analysis BEFORE findings:
(1) What does the changed code do mathematically?
The file constructs the independent join of probability measures and applies it to build a resource algebra. A MeasureOnSpace bundles a σ-algebra and a measure on it. PSpace enforces the measure to be a probability measure. isIndependentProduct (notation r =ᵢ p ⊕ᵢ q) specifies what it means for a probability space to be the independent combination of two others (i.e., its σ-algebra is their join, and the measures factorize on the generating sets).
The file establishes the uniqueness and partial associativity of this independent product using Dynkin's π-λ theorem (MeasurableSpace.induction_on_inter). It then lifts this partial binary operation to a total operation on PSp Ω := WithTop (PSpace Ω), where undefined products result in the ⊤ (invalid) element. This forms an OrderedUnitalResourceAlgebra (OURA), which models resource separation for probability spaces.
Finally, it couples PSp with a Permission OURA (fractional permissions via ℚ≥0), creating PSpPm which represents probabilistic states that are compatible with variable permissions (meaning the σ-algebra does not depend on variables for which the permission is exactly 0).

(2) How do changes relate to the spec checklist?
No spec checklist was provided.

(3) What are the riskiest aspects?
The most mathematically demanding aspects are the proofs of associativity and uniqueness of the independent product. These are handled rigorously using the π-λ theorem to extend independence from the generating sets (intersections of measurable sets from the marginal spaces) to the entire generated σ-algebra. Another potential risk is the use of Classical.choose in PSp.mul via the by_cases tactic. However, this is mathematically sound because the uniqueness of the independent product has been proven, ensuring that any chosen space is propositionally equal to any other valid choice.

(4) Any ambiguities in mathematical intent?
None. The code elegantly and accurately formalizes a separation logic model over continuous probabilistic states by correlating fractional permissions with the observable sub-σ-algebras.

I will list a few minor stylistic nitpicks (such as a spelling error and redefining the supremum of σ-algebras).

Verdict: Needs Minor Revisions

Critical Misformalizations: None

Lean 4 / Mathlib Issues: None

Nitpicks:

Typo in theorem name: 'indepenendentProduct_identity' has an extra 'en'. (src/Bluebell/MeasureOnSpace.lean:458)
Redundant definition of the supremum of measurable spaces. MeasurableSpace.sum m₁ m₂ is mathematically and structurally identical to m₁ ⊔ m₂ (the Sup lattice operation for MeasurableSpace in Mathlib). Redefining it is harmless but unidiomatic, as Mathlib already provides algebraic and monotonicity lemmas for ⊔. (src/Bluebell/MeasureOnSpace.lean:42-44)
The use of @[reducible] def is an older Lean 3 idiom. In Lean 4, abbrev is the preferred way to declare reducible definitions. (src/Bluebell/MeasureOnSpace.lean:1406)

📄 **Review for `src/Bluebell/Assertion.lean`**

Analysis:

Mathematical Code Summary: The PR adds a new file src/Bluebell/Assertion.lean, which defines the core probabilistic separation logic assertions (Assertion M and its specialization bProp). It implements the syntax and semantics for the assertions (e.g., own, sep, wand, hasDistribution, jointConditioning), proves that bProp forms an instance of Iris's Boolean Identity (BI) separation logic framework, and states a multitude of specialized Hoare logic and structural derivation rules for this separation logic.
Riskiest Aspects: The most significant issue is the extensive use of sorry throughout the file. There are 34 theorems with stubbed proofs (e.g., Sure_Merge, Sure_And_Star, WP_Nest, C_WP_Swap, etc.). This systematically bypasses the Lean kernel's verifier, meaning these inference rules are mathematically completely unverified and act effectively as axioms. Furthermore, the typeclass FunLike is instantiated twice for what is ultimately the same type, which can lead to overlapping instance errors during typeclass resolution.
Ambiguities in Intent: Given the absence of proofs for many of the rules (like WP_Conj, C_WP_Swap, RL_Unary, etc.), it is difficult to guarantee that the statement formulations are mathematically sound and lack missing hypotheses or logical errors.
Checklist mapping: No checklist provided.

Verdict: Changes Requested

Critical Misformalizations: None

Lean 4 / Mathlib Issues:

Hard Rule Violation — Escape Hatches: The code uses sorry in 34 distinct declarations (e.g., Sure_Merge, Sure_And_Star, Prod_Split, C_Frame, etc.) to stub out proofs. This explicitly bypasses Lean's verification kernel. For formal verification PRs, proofs must be completed or explicitly abstracted into documented axioms if representing a theoretical boundary. (src/Bluebell/Assertion.lean:1239-2241)
- Suggested fix: Remove sorry and provide full proofs for all theorems. If proofs are not yet available and this is a WIP, be aware that it cannot be approved for merging until complete.
Overlapping FunLike instances. You provide a generic instance for FunLike (Assertion M) M Prop and immediately follow it with an instance for FunLike (bProp I Var Val) (IndexedPSpPm I Var Val) Prop. Since bProp is just an abbrev for Assertion and IndexedPSpPm satisfies the OrderedUnitalResourceAlgebra constraint, these instances overlap exactly and will cause typeclass resolution issues or duplication. (src/Bluebell/Assertion.lean:191-197)
- Suggested fix: Remove the specialized instance for bProp, as the generic instance for Assertion M already fully covers it:

-- instance : FunLike (bProp I Var Val) (IndexedPSpPm I Var Val) Prop where
--   coe := fun P => P.carrier
--   coe_injective' := by intro P Q h; aesop

Nitpicks:

Non-standard theorem naming conventions. Theorems such as And_To_Star, Sure_Merge, Dist_Inj, and Sure_Eq_Inj are named using UpperCamelCase with underscores. Standard Lean 4 idiom dictates lowerCamelCase or snake_case (typically snake_case) for theorem and lemma names. (src/Bluebell/Assertion.lean:1042-2241)
Defining wand and bimp with @[simp] eagerly unfolds these definitions during simplification. In BI and separation logic formalizations (like Iris), connective definitions are usually kept opaque to allow reasoning via BI laws rather than unfolding to the raw carrier sets. (src/Bluebell/Assertion.lean:266-281)

Cluster: Legacy Code Cleanup (low)

Does the removal of legacy files cleanly transition the project to the new architecture without leaving dangling references?

📄 **Review for `src/Bluebell.lean`**

Analysis:
The diff modifies the top-level src/Bluebell.lean module to reflect a major architectural transition in the project. It removes 11 legacy imports (such as old CMRA-based definitions and probability theory modules) and replaces them with 3 new core modules: Bluebell.Assertion, Bluebell.OURA, and Bluebell.MeasureOnSpace. Mathematically, this transitions the library's foundation to the new Ordered Unital Resource Algebra (OURA) and the newly structured measure and assertion modules. The changes align with the expected cluster cleanup strategy. Since this is purely a top-level module list update, there is no mathematical logic or complex Lean code directly introduced here, and thus no direct risk of misformalization in this file.

Verdict: Approved

Critical Misformalizations: None

Lean 4 / Mathlib Issues: None

Nitpicks: None

📄 **Review for `src/Bluebell/Algebra/CMRA.lean`**

Analysis:

Mathematical changes: The file src/Bluebell/Algebra/CMRA.lean has been completely deleted. This aligns with the project's architectural transition from CMRA-based definitions to the new OURA (Ordered Unital Resource Algebra) architecture as described in the cluster context.
Riskiest aspects: The main risk with deleting a file is dangling references in other files that previously imported it (e.g., src/Bluebell.lean). However, within the scope of this specific file's diff, the removal itself is clean.
Ambiguities: None.
Spec checklist: N/A.

Verdict: Approved

Critical Misformalizations: None

Lean 4 / Mathlib Issues: None

Nitpicks: None

📄 **Review for `src/Bluebell/Algebra/HyperAssertion.lean`**

Analysis:

What does the changed code do mathematically? The diff completely deletes the file src/Bluebell/Algebra/HyperAssertion.lean, which contained the legacy CMRA-based implementation of hyper-assertions. This code is being superseded by the new OURA-based architecture.
How do changes relate to the spec checklist? N/A (no checklist provided).
What are the riskiest aspects? The only risk is if other files still depend on this module, but the cluster context indicates this is part of a broader cleanup where dependencies have been shifted to Assertion.lean, MeasureOnSpace.lean, and OURA.lean.
Any ambiguities in mathematical intent? None. The deletion is straightforward and intentional.

Verdict: Approved

Critical Misformalizations: None

Lean 4 / Mathlib Issues: None

Nitpicks: None

📄 **Review for `src/Bluebell/Algebra/PSpPm.lean`**

Analysis:

Mathematical Summary: The pull request entirely deletes src/Bluebell/Algebra/PSpPm.lean. This file previously contained legacy CMRA-based predicated product definitions for probability spaces and permissions (PSpPm, PSpPmRat, IndexedPSpPm, and IndexedPSpPmRat), which have been superseded by the new OURA-based architecture in the project.
Riskiest Aspects: The main risk with file deletions is leaving dangling module imports or broken references in the rest of the project. However, this is a planned cleanup of legacy architecture, and the system context indicates that these definitions have been safely superseded.
Ambiguities: None. The removal of dead code is straightforward and reduces the maintenance surface of the formalization.
Spec Checklist: N/A (no checklist provided).

Verdict: Approved

Critical Misformalizations: None

Lean 4 / Mathlib Issues: None

Nitpicks: None

📄 **Review for `src/Bluebell/Algebra/Permission.lean`**

Analysis:

What does the changed code do mathematically? The diff completely deletes src/Bluebell/Algebra/Permission.lean. This file previously contained legacy definitions for permissions based on Iris's DFrac (Permission) and rational-based permissions (PermissionRat) using Multiplicative (α → ℚ≥0).
How do changes relate to the spec checklist? No spec checklist provided.
What are the riskiest aspects? The primary risk with deleting a file is leaving dangling references or breaking downstream imports. However, according to the cluster context, this is a deliberate legacy cleanup transitioning the project from Iris CMRA to the new OURA (Ordered Unital Resource Algebra) architecture, and its functionality has been superseded.
Any ambiguities in mathematical intent? None. The deletion of deprecated code is unambiguous.

Verdict: Approved

Critical Misformalizations: None

Lean 4 / Mathlib Issues: None

Nitpicks: None

📄 **Review for `src/Bluebell/Algebra/Probability.lean`**

Analysis:
The change completely deletes the src/Bluebell/Algebra/Probability.lean file, which contained legacy probability algebra wrappers and definitions like compatiblePerm, PSp, and instances of CMRA for PSp. According to the PR context, this is a legacy code cleanup meant to migrate the architecture to a new OURA-based one. Since the code is being removed entirely and no new definitions or proofs are introduced in this file, there are no mathematical correctness issues, typeclass problems, or Lean idiom violations to review. The removal of this code aligns with the stated goal of the pull request.

Verdict: Approved

Critical Misformalizations: None

Lean 4 / Mathlib Issues: None

Nitpicks: None

📄 **Review for `src/Bluebell/Core/Indexed.lean`**

Analysis:

Mathematical Function: The diff entirely removes the src/Bluebell/Core/Indexed.lean file, which contained legacy definitions for indexedTuple (a function from a Finset ℕ to a type α) and its remove operation (restricting the tuple to a subset difference).
Riskiest Aspects: The only risk is if other parts of the project still depend on this file. However, according to the review cluster context, this is a planned legacy code cleanup transitioning to a new architecture. If dangling references exist, they will be caught by the compiler at the project level, and there are no direct mathematical risks introduced by removing the file itself.
Ambiguities: None. The intent to delete the file is clear.
Checklist: N/A.

Verdict: Approved

Critical Misformalizations: None

Lean 4 / Mathlib Issues: None

Nitpicks: None

📄 **Review for `src/Bluebell/Logic/JointCondition.lean`**

Analysis:

What does the changed code do mathematically? The PR deletes the file src/Bluebell/Logic/JointCondition.lean, which contained legacy definitions for a probability logic modality (jointCondition) and a large number of unimplemented theorems (using sorry). This deletion is part of a larger cleanup transitioning the project to a new OURA-based architecture.
What are the riskiest aspects? The only risk is if other modules in the project still depend on this file. However, based on the global context and cluster information, this is a clean removal of legacy code that has been superseded by new files (Assertion.lean, MeasureOnSpace.lean, OURA.lean).
Any ambiguities in mathematical intent? None. The removal of code heavy with sorrys is unequivocally positive.
Spec checklist mapping: N/A.

Verdict: Approved

Critical Misformalizations: None

Lean 4 / Mathlib Issues: None

Nitpicks: None

📄 **Review for `src/Bluebell/Logic/Ownership.lean`**

Analysis:

Mathematical Summary: The provided diff completely deletes the src/Bluebell/Logic/Ownership.lean file. This file previously contained legacy definitions for ownership of indexed probability spaces and permissions (e.g., ownIndexedTuple, ownIndexedProb, assertSampledFrom) and related hyper-assertions, using an older CMRA architecture.
Riskiest Aspects: The primary risk with deleting files is leaving dangling references or breaking downstream modules. However, based on the global context and cluster description, this is part of a deliberate 'Legacy Code Cleanup' transitioning the project to a new OURA-based architecture (using Assertion.lean, MeasureOnSpace.lean, etc.). If the project compiles after its removal, there is no risk.
Ambiguities: None. The deletion of the file is straightforward.
Relation to Spec: The deletion cleanly removes several legacy definitions and, notably, removes multiple admitted proofs (sorrys) that existed in the legacy file (e.g., sampledFrom_inj, sep_assertTrue_iff, sampledFrom_prod).

Verdict: Approved

Critical Misformalizations: None

Lean 4 / Mathlib Issues: None

Nitpicks: None

📄 **Review for `src/Bluebell/Logic/WeakestPre.lean`**

Analysis:

Mathematically, the diff completely deletes the src/Bluebell/Logic/WeakestPre.lean file, which contained legacy definitions of the weakest precondition (wp) relying on IndexedPSpPmRat. This aligns with the transition to the new OURA-based architecture.
The removal eliminates several incomplete proofs (sorrys in wp_comp and wp_conj), cleanly removing unverified assumptions from the codebase.
Since the file is completely deleted, there are no mathematical misformalizations or Lean 4 idiom violations introduced. The deletion correctly trims legacy code without introducing new code issues.
No spec checklist provided.

Verdict: Approved

Critical Misformalizations: None

Lean 4 / Mathlib Issues: None

Nitpicks: None

📄 **Review for `src/Bluebell/ProbabilityTheory/Coupling.lean`**

Analysis:

What does the changed code do mathematically? The diff completely removes the src/Bluebell/ProbabilityTheory/Coupling.lean file, which contained legacy formalizations of probability couplings for both discrete probability mass functions (PMF) and sub-probability mass functions (SPMF). This included definitions like IsCoupling, Coupling, and relational lifting Lift.
How do changes relate to the spec checklist? No checklist was provided.
What are the riskiest aspects? The primary risk with deleting a file is breaking downstream dependencies. However, based on the cluster context ('Legacy Code Cleanup'), this deletion is expected and intended to transition the project to a new architecture (Assertion.lean, MeasureOnSpace.lean, OURA.lean), safely removing superseded definitions.
Any ambiguities in mathematical intent? None. The intent is clearly to deprecate and delete old unused code.

Verdict: Approved

Critical Misformalizations: None

Lean 4 / Mathlib Issues: None

Nitpicks: None

📄 **Review for `src/Bluebell/ProbabilityTheory/IndepProduct.lean`**

Analysis:

Mathematical changes: The PR entirely deletes the src/Bluebell/ProbabilityTheory/IndepProduct.lean file. This file contained legacy definitions and incomplete theorems (marked with sorry) relating to the independent product of probability measures and measurable spaces.
Riskiest aspects: The primary risk in deleting a file is breaking downstream dependencies. However, the cluster context indicates this is part of a 'Legacy Code Cleanup', where old CMRA and probability theory definitions are being superseded by the new OURA-based architecture in Assertion.lean and MeasureOnSpace.lean.
Ambiguities: None. The deletion cleanly removes incomplete code that is no longer needed.
Checklist: No spec checklist provided.

Verdict: Approved

Critical Misformalizations: None

Lean 4 / Mathlib Issues: None

Nitpicks: None

github-actions · 2026-06-26T03:17:38Z

+    assumption
+}
+
+instance OrderedUnitalResourceAlgebra.instUCMRA


🟡 Issue: The instance OrderedUnitalResourceAlgebra.instUCMRA is declared inside the OrderedUnitalResourceAlgebra namespace, leading to the duplicated name OrderedUnitalResourceAlgebra.OrderedUnitalResourceAlgebra.instUCMRA. This triggers a Lean 4 compiler warning.

Suggested fix: Rename the instance to just instUCMRA to avoid namespace duplication: instance instUCMRA {M : Type*} [ra : OrderedUnitalResourceAlgebra M] : Iris.UCMRA M := { ... }

github-actions · 2026-06-26T03:17:38Z

+variable {I M : Type*} [OrderedUnitalResourceAlgebra M]
+
+instance : MulRightMono M := ⟨fun _ _ _ h ↦ mul_left_mono h⟩
+


🟡 Issue: The instance Valid (I → M) is declared in a section where [OrderedUnitalResourceAlgebra M] is an active variable. Lean 4's auto-implicit rules will include this typeclass as a parameter because M appears in the instance type. This unnecessarily restricts the pointwise Valid instance to types that are OrderedUnitalResourceAlgebra, whereas it should mathematically apply to any type with just [Valid M].

Suggested fix: Move this instance outside of the section where variable {I M : Type*} [OrderedUnitalResourceAlgebra M] is declared, so it only depends on the explicitly provided [Valid M].

github-actions · 2026-06-26T03:17:38Z

+  elim := by intro a b c h i; unfold Function.swap; simp; have := (f i).elim; aesop
+  valid_one i := by aesop
+  valid_mono x y i := by have := fun i ↦ (f i).valid_mono (x i) (y i); aesop
+  valid_mul x := by have := fun i ↦ (f i).valid_mul (x i); aesop


💡 Nitpick: Typo in the docstring for product: 'instnace' instead of 'instance'.

Suggested fix: /-- Technically binary product is just an instance of indexed product, but
it is convenient to redefine it -/

github-actions · 2026-06-26T03:17:38Z

+  have h₂ : u ⊆ Set.univ := by aesop
+  have h₃ : m.1.μ u ≤ m.1.μ Set.univ := measure_mono h₂
+  exact lt_of_le_of_lt (b := 1) (by aesop) (by aesop)
+


💡 Nitpick: Typo in theorem name: 'indepenendentProduct_identity' has an extra 'en'.

Suggested fix: theorem independentProduct_identity [Inhabited Ω] {p : PSpace Ω}

github-actions · 2026-06-26T03:17:38Z

+
+/-- Note: the sum operation generates the smallest σ-algebra consisting the measurable
+    sets in m₁ and m₂. Equivalently, we can also write m₁ ⊔ m₂. -/
+@[simp]


💡 Nitpick: Redundant definition of the supremum of measurable spaces. MeasurableSpace.sum m₁ m₂ is mathematically and structurally identical to m₁ ⊔ m₂ (the Sup lattice operation for MeasurableSpace in Mathlib). Redefining it is harmless but unidiomatic, as Mathlib already provides algebraic and monotonicity lemmas for ⊔.

Suggested fix: Consider replacing instances of m₁.sum m₂ with the standard Mathlib notation m₁ ⊔ m₂.

github-actions · 2026-06-26T03:17:38Z

+  refine isProbabilityMeasure_iff.mpr ?_
+  have := @Measure.map_apply Ω Ω' ps.1.ms (ps.1.ms.map f) ps.1.μ f (fun ⦃t⦄ a => a) Set.univ (by simp)
+  have : ps.1.μ (f ⁻¹' Set.univ) = 1 := by
+    have : f ⁻¹' Set.univ = Set.univ := by simp


💡 Nitpick: The use of @[reducible] def is an older Lean 3 idiom. In Lean 4, abbrev is the preferred way to declare reducible definitions.

Suggested fix: abbrev Permission (α : Type*) := Multiplicative (α → ℚ≥0)

github-actions · 2026-06-26T03:17:38Z

+  {A : Type*}
+  {E₁ E₂ : (Var → Val) → Prop} {i : I}
+  : ⌈E₁⟨i⟩⌉ ∗ ⌈E₂⟨i⟩⌉ ⊣⊢ ⌈(fun s => E₁ s ∧ E₂ s)⟨i⟩⌉ := by
+  sorry -- TODO: Rule SURE-MERGE proof


🟡 Issue: Hard Rule Violation — Escape Hatches: The code uses sorry in 34 distinct declarations (e.g., Sure_Merge, Sure_And_Star, Prod_Split, C_Frame, etc.) to stub out proofs. This explicitly bypasses Lean's verification kernel. For formal verification PRs, proofs must be completed or explicitly abstracted into documented axioms if representing a theoretical boundary.

Suggested fix: Remove sorry and provide full proofs for all theorems. If proofs are not yet available and this is a WIP, be aware that it cannot be approved for merging until complete.

github-actions · 2026-06-26T03:17:39Z

+  carrier := {x | True}
+  upper' := by aesop
+}
+


🟡 Issue: Overlapping FunLike instances. You provide a generic instance for FunLike (Assertion M) M Prop and immediately follow it with an instance for FunLike (bProp I Var Val) (IndexedPSpPm I Var Val) Prop. Since bProp is just an abbrev for Assertion and IndexedPSpPm satisfies the OrderedUnitalResourceAlgebra constraint, these instances overlap exactly and will cause typeclass resolution issues or duplication.

Suggested fix: Remove the specialized instance for bProp, as the generic instance for Assertion M already fully covers it:

-- instance : FunLike (bProp I Var Val) (IndexedPSpPm I Var Val) Prop where -- coe := fun P => P.carrier -- coe_injective' := by intro P Q h; aesop

github-actions · 2026-06-26T03:17:39Z

+    intro i hi₂; dsimp [a₁]
+    split
+    · rename_i hi₁; exact hagree i ⟨hi₁, hi₂⟩
+    · rfl


💡 Nitpick: Non-standard theorem naming conventions. Theorems such as And_To_Star, Sure_Merge, Dist_Inj, and Sure_Eq_Inj are named using UpperCamelCase with underscores. Standard Lean 4 idiom dictates lowerCamelCase or snake_case (typically snake_case) for theorem and lemma names.

Suggested fix: Rename theorems to follow Lean 4 conventions, e.g., and_to_star, sure_merge, dist_inj, etc.

github-actions · 2026-06-26T03:17:39Z

+  carrier := {a | ∀ p, Ψ p → p a}
+  upper' := by
+    intro a b hle ha p hΨ
+    exact p.upper' hle (ha p hΨ)


💡 Nitpick: Defining wand and bimp with @[simp] eagerly unfolds these definitions during simplification. In BI and separation logic formalizations (like Iris), connective definitions are usually kept opaque to allow reasoning via BI laws rather than unfolding to the raw carrier sets.

Suggested fix: Consider removing the @[simp] attribute from wand and bimp unless unfolding to the semantic definition is explicitly desired on every simp call.

…T-FUN, DIRAC-DUP, DIST-CONVEX and forward direction of SURE-MERGE And restrucure some of the helper lemmas under the "Other helper lemmas" heading. Assisted-by: Aristotle (Harmonic)

…lRules` section For comments made before deciding to use "🤖:" to indicate a comment was added by a generative AI tool.

alexanderlhicks

AI-generated review (human verification required): this review was produced by automated repository/paper comparison, Lean declaration inventory, lake build, and #print axioms inspection. It is not a substitute for maintainer judgment, and line-level/contextual interpretation should be checked by the PR author and maintainers.

Thank you for the substantial formalization work: the PR builds successfully and introduces the core model, assertion, and rule interfaces in a coherent structure. I recommend request changes until the admitted rules, paper-correspondence gaps, and statement differences below are addressed.

The main blocking issue is that 25 exported Bluebell rules still depend directly on sorryAx: Sure_Merge, Sure_And_Star, Prod_Split, C_Frame, C_Unit_R, C_Assoc, C_And, Sure_Str_Convex, WP_Nest, WP_Conj, C_WP_Swap, Dist_Supp, Prod_Unsplit, C_Fuse, C_Swap, C_Sure_Proj, C_Sure_Proj_Many, C_Extract, C_Dist_Proj, RL_Unary, RL_Eq_Dist, RL_Convex, RL_Merge, RL_Sure_Merge, and Coupling. Dirac_Dup is also not axiom-clean transitively because it depends on admitted Sure_Merge. Please prove the rules or explicitly narrow the PR scope, then validate every exported rule with #print axioms.

alexanderlhicks · 2026-07-12T02:29:18Z

+  : ⌈E₁⟨i⟩⌉ ∗ ⌈E₂⟨i⟩⌉ ⊣⊢ ⌈(fun s => E₁ s ∧ E₂ s)⟨i⟩⌉ := by
+    constructor
+    · exact Sure_Merge_fwd
+    · sorry -- TODO: Rule SURE-MERGE proof (backwards direction)


Blocking: this exported rule is currently proved by sorry, so it contributes sorryAx to the trusted base. The corresponding paper rule is sure-merge (paper/section/appendix_rules.tex:164–170), and the paper states that these rules are semantic lemmas with soundness proofs (paper/section/appendix_rules.tex:133–139). Please provide the Lean proof and verify with #print axioms Sure_Merge that it is axiom-clean. The same check is needed for the other 24 admitted rules listed in the review summary.

alexanderlhicks · 2026-07-12T02:29:18Z

+def ownPSp (P : I → PSp (Var → Val)) : bProp I Var Val :=
+  iprop(∃ p : IxCompatiblePermission P, ownIndexedPSpPm P p)
+
+def almostMeasurable {A : Type*} (E : (Var → Val) → A) (P : PSp (Var → Val)) : Prop :=


Please establish correspondence with the paper definition before relying on this as the assertion-level notion of almost-measurability. The paper defines an event by measurable sandwiching, ∃ E₁ E₂ ∈ σ, E₁ ⊆ E ⊆ E₂ ∧ μ(E₁)=μ(E₂), and defines function almost-measurability pointwise over all fibers (paper/section/logic.tex:361–379, def:almost-meas). This Lean definition uses AEMeasurable; that may be equivalent under additional assumptions, but the equivalence is not currently proved for the generic spaces here. Either implement the paper definition directly or add and test the required equivalence theorem.

alexanderlhicks · 2026-07-12T02:29:18Z

+/-- Short for "domain" -/
+abbrev dom (t : I → Option (PSpPm Var Val → PSpPm Var Val)) := hyperTermReferences t
+
+def wp {Var Val : Type*}


Please add a correspondence theorem for this WP definition. The paper quantifies over a distribution on the full hyper-store and defines a ≤ μ₀ by embedding it with full permissions (paper/section/logic.tex:765–785, def:wp; summarized also in paper/section/appendix_rules.tex:72–83). This implementation instead quantifies over IndexedPSpPm, carries an explicit frame c, and adds validity conditions on μ₀ and b. Those may form a sound reformulation, but the equivalence/refinement to the paper semantics is currently undocumented and unproved. Please either formalize the paper definition or prove the exact correspondence under the intended model assumptions.

alexanderlhicks · 2026-07-12T02:29:18Z

+    | compl s _ ih => rw [Set.preimage_compl]; exact ih.compl
+    | iUnion g _ ih => rw [Set.preimage_iUnion]; exact MeasurableSet.iUnion ih
+
+def PSpace.compatiblePerm


The paper defines compatibility by existence of a factorization psp = psp' × Triv(S → Val), where S is exactly the set of zero-permission variables (paper/section/logic.tex:182–200, definition Compatibility). This definition instead uses closure under individual Function.updates. That may be equivalent for finite Var, but it is not definitionally the paper definition and may be weaker for infinite variable sets. Please either use the factorization definition or prove the equivalence with explicit assumptions on Var, Val, and the probability-space representation.

alexanderlhicks · 2026-07-12T02:29:18Z

+  {Q : A → bProp I Var Val} {i : I} {E : (Var → Val) → A}
+  :
+  𝒞⟨μ⟩ v; (⌈(fun s => E s = v)⟨i⟩⌉ ∗ wp t (Q v)) ⊢ wp t (𝒞⟨μ⟩ v; (⌈(fun s => E s = v)⟨i⟩⌉ ∗ Q v)) := by
+    sorry -- TODO: Rule C-WP-SWAP proof (spec not yet reviewed)


This is a new statement rather than the c-wp-swap rule in the paper. The paper rule is C μ v.(WP t Q(v) ∧ ownall) ⊢ WP t (C μ v.Q(v)) (paper/section/appendix_rules.tex:336–342, rule c-wp-swap). ownall is defined in paper/section/casestudies.tex:86–92, and the paper explicitly says that omitting it is unsound in the current model (paper/section/casestudies.tex:199–202). The explicit equality frame here may be intended to encode the needed ownership, but that equivalence and the soundness of this generalized statement are not shown. Please either formalize the paper rule or document/prove this new variant, including its relationship to ownall, then remove the sorry.

alexanderlhicks · 2026-07-12T02:29:18Z

+
+-- ### RL-EQ-DIST
+
+theorem RL_Eq_Dist {A : Type*} [Inhabited A] [Inhabited X] {X : Set (I × Var)} {μ : PMF A} {ix jy : X} :


RL_Eq_Dist appears to contain unused parameters {A}, [Inhabited A], [Inhabited X], and {μ : PMF A}. The paper rule requires only i ≠ j and the equality relation (paper/section/appendix_rules.tex:568–575, rule rl-eq-dist). Please remove the unused parameters or explain their semantic role, and make the Lean statement expose the same essential hypotheses as the paper rule.

alexanderlhicks · 2026-07-12T02:29:18Z

+    assumption
+}
+
+instance OrderedUnitalResourceAlgebra.instUCMRA


This declaration emits a duplicate namespace warning (OrderedUnitalResourceAlgebra.OrderedUnitalResourceAlgebra.instUCMRA). Please remove the redundant namespace qualification or rename the declaration so the build is warning-clean.

alexanderlhicks · 2026-07-12T02:29:18Z

+  {μ μ' : PMF A}
+  {i : I} {E : (Var → Val) → A}
+  :
+  𝒞⟨μ⟩ v; E⟨i⟩ ~ μ' ⊢ E⟨i⟩ ~ μ' := by


The binder v is unused in Dist_Convex. Please remove it or rename it to _v so the intended statement is clear and the warning is eliminated.

alexanderlhicks · 2026-07-12T02:29:18Z

+        ValidPSpPm, ValidPSp.PSpace, ValidPSp, Measure.map_const, PSpace.isProbability,
+        measure_univ, one_smul] ;
+
+omit [Finite Var] [Countable Val] in 


Please remove the trailing whitespace on this line so git diff --check is clean.

alexanderlhicks · 2026-07-12T22:05:07Z

Regarding the sorries, I would be curious to know whether any of them are actually blocked in any sense, or whetehr it's mostly been a question of finding some time/compute to tackle them?

Coda-Coda · 2026-07-16T06:53:38Z

Kia ora @alexanderlhicks :)

Regarding the sorries, I would be curious to know whether any of them are actually blocked in any sense, or whetehr it's mostly been a question of finding some time/compute to tackle them?

Currently, none of the rules are blocked. Some were/are definitely easier to prove than others. I can let you know if, after further time/compute, we uncover that any are in fact blocked.

Also, thanks for the AI-generated review, I'll have a look over that in the coming days (I just got back from vacation).

alexanderlhicks

AI-generated follow-up (human verification required): addendum to my earlier review, after re-validating all findings against the current head (965589e).

Validation updates:

The count of admitted rules stands at 25 (the automated review's figure of 34 predates 309e5b4, which proved ~10 rules). The 25 rule names in my original review remain accurate, including C_Unit_R and Dist_Supp, whose in-code TODO labels name the wrong rules (see inline comments).
Dirac_Dup is confirmed to be the only proved rule that transitively depends on an admitted one (the backward direction of Sure_Merge).
The overlapping FunLike instances flagged by the automated review (Assertion.lean:177/181) are confirmed real: bProp is an abbrev of Assertion, so the second instance exactly duplicates the first.

New findings (see inline comments):

RL_Eq_Dist appears misformalized, not merely unproven — its conclusion ranges over distributions of variable names rather than stored values and is likely unprovable as stated, so the sorry is masking a false statement. The same theorem also has a phantom [Inhabited X] binder.
Several sorry TODO labels name the wrong rule, which has already misled automated audits of the admitted-rule inventory.
No Iris.CMRA.Discrete / Iris.OFE.Discrete instance is registered, even though the camera built from DiscreteCMRA is discrete by construction — a small addition that would make "the probability-space resource algebras are discrete cameras" a statement checked by Lean.

alexanderlhicks · 2026-07-19T02:40:48Z

+
+-- ### RL-EQ-DIST
+
+theorem RL_Eq_Dist {A : Type*} [Inhabited A] [Inhabited X] {X : Set (I × Var)} {μ : PMF A} {ix jy : X} :


Blocking: beyond the unused parameters noted in my earlier review, the statement itself appears misformalized. In the conclusion, (fun _ ↦ ix.1.2) has type (Var → Val) → Var, so the existentially bound μ is a PMF Var — a distribution over variable names — and each hasDistribution conjunct asserts that the pushforward of the store measure under a constant function equals μ. That forces μ = δ ix.1.2 and μ = δ jy.1.2 simultaneously, which is unsatisfiable whenever the two variable names differ. The intended expressions are presumably fun s ↦ s ix.1.2 / fun s ↦ s jy.1.2 (compare Coupling, which correctly uses fun s ↦ s x₁).

Separately, [Inhabited X] occurs before {X : Set (I × Var)} is bound, so Lean auto-binds a fresh implicit type X that the later binder shadows — the hypothesis constrains a phantom type and does nothing.

Please fix the statement before attempting the proof; as written the sorry is admitting a false claim rather than deferring a true one.

alexanderlhicks · 2026-07-19T02:40:48Z

+
+theorem C_Unit_R {A : Type*} {i : I} {μ : PMF A} {E : (Var → Val) → A} :
+  E⟨i⟩ ~ μ ⊣⊢ 𝒞⟨μ⟩ v; ⌈(fun s ↦ E s = v)⟨i⟩⌉ := by
+    sorry -- TODO: Rule C-UNIT-L proof (spec not yet reviewed)


This sorry is labeled C-UNIT-L, but the theorem is C_Unit_R (C-UNIT-L is proved above). The same mislabeling occurs at line 2670 (Dist_Supp labeled DIRAC-SUPP) and line 2901 (RL_Merge labeled RL-SURE-MERGE). These stale labels have already caused the automated review to mis-inventory the admitted rules; please correct them so the remaining-work list can be audited by grep.

alexanderlhicks · 2026-07-19T02:40:48Z

+
+open Iris in
+/-- A discrete CMRA can be converted to a regular CMRA -/
+instance DiscreteCMRA.instCMRA {α : Type*} [DiscreteCMRA α] : CMRA α := {


DiscreteCMRA.instCMRA sets ValidN := fun _ x ↦ valid x, and instOFE sets Dist := fun _ ↦ equiv, so the resulting camera is discrete by construction — but no Iris.CMRA.Discrete (or Iris.OFE.Discrete) instance is ever registered. Both should hold definitionally and take only a couple of lines. Adding them would turn "the probability-space resource algebras are discrete cameras" into a statement actually checked by Lean, which is the form of the claim needed for the associated milestone.

shinghinho and others added 30 commits February 4, 2026 19:00

Defining MeasureOnSpace as the new notion of resource

724664e

bump the manifest

969deaf

do not rely on autoImplicit = true

9f22758

- Define PSpace to be a Subtype rather than a Sub_SET_. This allows u…

5bdc92d

…s to remove some ugly casts - e.g. you want `Preorder (PSpace Ω)`, but Preorder is defined as a 'type'-class, so there's a cast injected here. - Hit some proofs with a big stick.

Merge pull request #261 from Verified-zkEVM/Ferinko/measureMySpaceR

5673c5b

Ferinko/measure my space r

Proved identity and commutativity law for independent product

ebc2142

Proved identity and commutativity law for independentProduct

8bb6d36

Unfinished proof of associativity

d704946

Associativity proof

14a0e8d

Associativity proof

4a11d3d

PSp as a discrete camera

8a51c59

Discrete CMRA: product space and subspace

ac2290e

measurable

00a6319

prove 'le_preserves_measure'

30b0daa

PSp as an RA

0f46a64

Compatibility

f8df189

PSpace map

9eaeb56

Lemmas for MeasurableSpace.map

10f78db

hone proof

5a58b14

Introduced independent product notation + cleanup

5d57263

Lemma for PSpace.compatiblePerm

d3fb0e1

Merged and added MeasurableSpace.map_preserves_sum

53c70ae

Bluebell RA

0b85cc9

Generalizing Var and Val

822420f

Partial implementation of quotient DiscreteCMRA

a2e7ca5

Complete proof for OrderedUnitalResourceAlgebrar.quotient

5807ece

Complete proof for OrderedUnitalResourceAlgebrar.quotient

78a8bcb

Assertion

5248eac

Merge branch 'measureMySpace' of https://github.com/Verified-zkEVM/ir…

338523b

…is-lean into measureMySpace

Coda-Coda and others added 18 commits June 15, 2026 16:45

Tweak variable name to match order in the type I × Var

44ee3b2

Formalise statements of C-SWAP and RL-EQ-DIST

bb7813c

Formalise statement of C-FUSE and define fusion

59683b5

Fill sorry in fusion definition showing HasSum f 1

80c5809

Assisted-by: Aristotle (Harmonic)

Formalise statement of C-SURE-PROJ, except proof of `HasSum (fun a =>…

5691f19

… ∑' (b : B), μ (a, b)) 1`

Add proof of HasSum ... 1 to C-SURE-PROJ spec

f51c39f

Assisted-by: Aristotle (Harmonic)

Update TODO to reflect that prf is done

db56e0a

Fill sorrys in statements of SURE-SUB and DIST-FUN showing `HasSum …

3f1e6ce

…... 1` Assisted-by: Aristotle (Harmonic)

Replace inline proofs of HasSum ... 1 with prf and `let prf : Has…

1967521

…Sum ... 1 := ...` Improving clarity, so that they read more like the paper.

Remove unnecessary comments

57b871b

Formalise statement of C-SURE-PROJ-MANY

0aaa6e1

Added definition of pabs and fixed Sure_And_Star accordingly

37af47a

WIP on formalising statement of RL-SURE-MERGE

3fbf774

Formalised the RL-Unary and Coupling rules + refined RL-Sure-Merge

7d5811a

Co-authored-by: Julian Sutherland <julian@nethermind.io> Co-authored-by: Daniel Britten <daniel.britten@nethermind.io>

Update comments to indicate what was finished in the previous commit

8bbf49a

Make TODO comments consistent

136c9a3

Minor cleanup

21b2889

Coda-Coda requested a review from Julek June 26, 2026 03:03

github-actions Bot reviewed Jun 26, 2026

View reviewed changes

Coda-Coda added 4 commits July 3, 2026 16:24

Prove C-UNIT-L, C-UNASSOC, C-SKOLEM, C-FOR-ALL, C-PURE, SURE-SUB, DIS…

309e5b4

…T-FUN, DIRAC-DUP, DIST-CONVEX and forward direction of SURE-MERGE And restrucure some of the helper lemmas under the "Other helper lemmas" heading. Assisted-by: Aristotle (Harmonic)

Add note on the use of generative AI in the BluebellRules section

d7975ef

Add "🤖:" to comments that were added by generative AI in the `Bluebel…

1926d5c

…lRules` section For comments made before deciding to use "🤖:" to indicate a comment was added by a generative AI tool.

Add TODO comment

965589e

alexanderlhicks marked this pull request as ready for review July 11, 2026 23:05

alexanderlhicks requested changes Jul 12, 2026

View reviewed changes

alexanderlhicks reviewed Jul 19, 2026

View reviewed changes

		variable {I M : Type*} [OrderedUnitalResourceAlgebra M]

		instance : MulRightMono M := ⟨fun _ _ _ h ↦ mul_left_mono h⟩


		-- ### RL-EQ-DIST

		theorem RL_Eq_Dist {A : Type*} [Inhabited A] [Inhabited X] {X : Set (I × Var)} {μ : PMF A} {ix jy : X} :

Uh oh!

Conversation

Coda-Coda commented Jun 26, 2026

Uh oh!

github-actions Bot commented Jun 26, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

🤖 PR Summary

Uh oh!

github-actions Bot left a comment

Choose a reason for hiding this comment

🤖 AI Review

Cluster: Algebraic Framework and Probability Models (critical)

Cluster: Legacy Code Cleanup (low)

Uh oh!

github-actions Bot Jun 26, 2026

Choose a reason for hiding this comment

Uh oh!

github-actions Bot Jun 26, 2026

Choose a reason for hiding this comment

Uh oh!

github-actions Bot Jun 26, 2026

Choose a reason for hiding this comment

Uh oh!

github-actions Bot Jun 26, 2026

Choose a reason for hiding this comment

Uh oh!

github-actions Bot Jun 26, 2026

Choose a reason for hiding this comment

Uh oh!

github-actions Bot Jun 26, 2026

Choose a reason for hiding this comment

Uh oh!

github-actions Bot Jun 26, 2026

Choose a reason for hiding this comment

Uh oh!

github-actions Bot Jun 26, 2026

Choose a reason for hiding this comment

Uh oh!

github-actions Bot Jun 26, 2026

Choose a reason for hiding this comment

Uh oh!

github-actions Bot Jun 26, 2026

Choose a reason for hiding this comment

Uh oh!

alexanderlhicks left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

alexanderlhicks commented Jul 12, 2026

Uh oh!

Coda-Coda commented Jul 16, 2026

Uh oh!

alexanderlhicks left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

github-actions Bot commented Jun 26, 2026 •

edited

Loading