Proof obligation for `wp_comp` in `src/Bluebell/Logic/WeakestPre.lean`

[alexanderlhicks]

A proof in src/Bluebell/Logic/WeakestPre.lean contains a sorry.

🤖 AI Analysis:

Statement Explanation

This theorem states the law of composition for the weakest precondition (wp). It asserts that the weakest precondition for two sequentially composed programs is equivalent to nesting their weakest preconditions.

The statement is (wp t₁ (wp t₂ Q)) ⊣⊢ (wp (t₁ ∘ t₂) Q). Let's break this down:

• t₁ and t₂ are program transformers. In Lean, t₁ ∘ t₂ means function composition, so (t₁ ∘ t₂) (m) = t₁ (t₂ (m)). This represents running program t₂ first, then program t₁.
• wp t P is the weakest precondition for program t and postcondition P.
• The standard rule for sequential composition S₁; S₂ is wp(S₁; S₂, R) = wp(S₁, wp(S₂, R)).
• If we let S₁ = t₂ and S₂ = t₁, then the composition is t₂; t₁, which corresponds to t₁ ∘ t₂. The standard rule would then be wp(t₁ ∘ t₂, Q) = wp(t₂, wp(t₁, Q)).
• Your theorem is stated as wp t₁ (wp t₂ Q) ⊣⊢ wp (t₁ ∘ t₂) Q. It seems that the roles of t₁ and t₂ on the left-hand side are swapped compared to the standard formulation. You may want to double-check if the intended statement was (wp t₂ (wp t₁ Q)) ⊣⊢ (wp (t₁ ∘ t₂) Q).

Assuming the statement is a typo and should be (wp t₂ (wp t₁ Q)) ⊣⊢ (wp (t₁ ∘ t₂) Q), the goal is to prove that these two hyper-assertions are equivalent, which means proving entailment in both directions.

Context

This theorem is a cornerstone of any weakest precondition calculus. It provides the rule for handling sequential composition of programs, allowing proofs about complex programs to be broken down into proofs about their constituent parts. In the context of the Bluebell project, which formalizes a probabilistic separation logic, this property is crucial for verifying programs that execute in sequence.

The proof will deeply interact with the definition of wp, which is defined for initial states of the form IndexedPSpPm.liftProb μ₀. A key challenge is that the state after the first program (t₂) runs, t₂ (liftProb μ₀), is not necessarily in this specific "lifted probability" form. Your proof will likely require a way to bridge this gap, perhaps via a more general property of wp or a specific property of the program transformers t.

Proof Suggestion

Assuming the theorem is corrected to (wp t₂ (wp t₁ Q)) ⊣⊢ (wp (t₁ ∘ t₂) Q), the proof involves two parts:

Part 1: (wp t₂ (wp t₁ Q)) ⊢ (wp (t₁ ∘ t₂) Q) (Forward direction)

1. Start by unfolding the definitions. Use unfold entails wp HyperAssertion.pred or intro a h_a; unfold wp at h_a; ... to get to the core propositions.
2. Your hypothesis will be a ∈ wp t₂ (wp t₁ Q). After unfolding, you'll have ∀ μ₀ c, (a • c) ≤ liftProb μ₀ → ∃ b₁, (b₁ • c) ≤ t₂ (liftProb μ₀) ∧ b₁ ∈ wp t₁ Q.
3. Your goal is a ∈ wp (t₁ ∘ t₂) Q, which unfolds to ∀ μ₀ c, (a • c) ≤ liftProb μ₀ → ∃ b, (b • c) ≤ t₁ (t₂ (liftProb μ₀)) ∧ Q b.
4. After introducing μ₀ and c, apply the hypothesis to get a witness b₁. You now have h_inc: (b₁ • c) ≤ t₂ (liftProb μ₀) and h_wp: b₁ ∈ wp t₁ Q.
5. The main challenge: h_wp is defined over initial states of the form liftProb μ'₀, but you need to reason about running t₁ on the state t₂ (liftProb μ₀). You will likely need a lemma that generalizes the wp property. This lemma might look like:

   lemma wp_generic_state (ht : monotonic t) (a : M) (m : M) (c : M) :
     a ∈ wp t Q → (a • c) ≤ m → ∃ b, (b • c) ≤ t m ∧ Q b := by ...

   You would need to prove this lemma first, possibly assuming monotonicity of the transformers t.
6. Apply this hypothetical lemma with the state m := t₂ (liftProb μ₀), the resource b₁, and the frame c. The condition (b₁ • c) ≤ m is exactly your hypothesis h_inc.
7. The lemma will yield the existence of the final resource b that satisfies the goal.

Part 2: (wp (t₁ ∘ t₂) Q) ⊢ (wp t₂ (wp t₁ Q)) (Backward direction)

1. Unfold definitions again. Your hypothesis h_a will be a ∈ wp (t₁ ∘ t₂) Q. Your goal is a ∈ wp t₂ (wp t₁ Q).
2. After introducing μ₀ and c, your goal is to find a witness b₂ such that (b₂ • c) ≤ t₂(liftProb μ₀) and b₂ ∈ wp t₁ Q.
3. b₂ ∈ wp t₁ Q means ∀ μ'₀ c', (b₂ • c') ≤ liftProb μ'₀ → ∃ b', (b' • c') ≤ t₁(liftProb μ'₀) ∧ Q b'.
4. This direction is often more challenging because you have to construct the intermediate resource b₂.
5. Let m₁ := t₂(liftProb μ₀). The hypothesis h_a tells you that if you run t₁ on m₁, you can get a resource b satisfying Q. That is, ∃ b, (b • c) ≤ t₁ m₁ ∧ Q b.
6. You need to construct a b₂ that "owns" enough resources to guarantee Q after running t₁ from any compatible state liftProb μ'₀.
7. A possible approach is to define b₂ as the weakest precondition for t₁ and Q itself. However, since wp t₁ Q is a set of resources (HyperAssertion), you cannot simply use it as a witness. The construction is subtle and depends on the properties of your resource model (CMRA). This direction might require a deeper dive into the algebraic properties of IndexedPSpPm.

Goal: Replace the sorry with a complete proof.

Link to the sorry on GitHub

Code Snippet:

theorem wp_comp : (wp t₁ (wp t₂ Q)) ⊣⊢ (wp (t₁ ∘ t₂) Q) := by sorry

[pirapira]

The Bluebell paper has only one direction "Part 1: (wp t₂ (wp t₁ Q)) ⊢ (wp (t₁ ∘ t₂) Q)". The other direction might not be provable.

[edit: maybe it should be called wp_seq because it's WP-SEQ in the paper.]