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

[alexanderlhicks]

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

🤖 AI Analysis:

Statement Explanation

This theorem, C_wp_swap, states a relationship between the weakest precondition wp and the joint conditioning modality 𝑪_. It asserts that if a resource satisfies the joint condition for a family of weakest preconditions, then it also satisfies the weakest precondition for the joint condition of the postconditions.

• Hypotheses: The main hypothesis is 𝑪_ μ (fun v => wp t (K v)). This means the current resource can be decomposed according to the probability distribution μ. For each outcome v from the support of μ, the corresponding component of the resource satisfies wp t (K v), which is the weakest precondition for the program t to achieve the postcondition K v. The sorry on the left-hand side likely represents a missing side-condition, possibly related to the behavior of the program t (e.g., that it doesn't interfere with the probabilistic structure).
• Goal: The goal is to prove wp t (𝑪_ μ K). This means the original resource satisfies the weakest precondition for the program t to achieve the joint postcondition 𝑪_ μ K. The postcondition 𝑪_ μ K itself asserts that the final resource can be decomposed according to μ, with each component satisfying K v.

In essence, this theorem allows "swapping" the wp and 𝑪_ operators, moving the wp from inside the modality to the outside. This is a powerful property for compositional verification of probabilistic programs.

Context

This theorem is a key component of the Bluebell program logic, specifically for reasoning about programs that involve probabilistic sampling. It connects the weakest precondition calculus (a standard tool for program verification) with the jointCondition modality (𝑪_), which is the logic's way of specifying properties of probability distributions.

This rule is analogous to other rules that describe how wp interacts with logical connectives. For instance, wp distributes over ∧, but its interaction with separating conjunction ∗ is more complex, as shown by the wp_frame theorem. C_wp_swap clarifies this interaction for the 𝑪_ modality, which is central to expressing hyperproperties about probabilistic behavior.

Proving this theorem is essential for verifying programs that first sample a value v from a distribution μ and then execute code that depends on v. This rule allows reasoning about the whole program by analyzing the weakest precondition for each possible outcome v separately. The sorry placeholder is critical; such "swap" rules in program logic often require side-conditions about non-interference or linearity of the program transformer t.

Proof Suggestion

The proof will involve carefully unfolding the definitions of wp and 𝑪_ and constructing a suitable witness for the final existential quantifier.

1. Unfold Definitions: Start by applying intro a ha to assume you have a resource a that satisfies the left-hand side. Unfold the definition of entailment (⊢). Then, unfold the definition of wp in the goal. This will require you to prove a statement of the form ∀ μ₀ c, (a • c) ≤ ... → ∃ b, .... So, introduce μ₀, c, and the inclusion hypothesis h_inc.

2. Deconstruct the Hypothesis: The main hypothesis is a ∈ 𝑪_ μ (fun v => wp t (K v)). Unfold jointCondition (𝑪_) on this hypothesis. This will give you existential witnesses:

   • P: An indexed family of probability spaces.
   • p: An indexed family of permissions.
   • h_compat: A compatibility proof.
   • κ: An indexed family of Markov kernels.
     And several properties, including:
   • An inclusion a_k ≤ a, where a_k is the resource (fun i => ⟨⟨WithTop.some (P i), p i⟩, h_compat i⟩).
   • A factorization of measures: ∀ i, (P i).μ = μ.toMeasure.bind (κ i).
   • The core property: ∀ v ∈ μ.support, b_v ∈ wp t (K v), where b_v is the resource corresponding to the outcome v.

3. Use the Inner wp: For each v ∈ μ.support, you have a hypothesis b_v ∈ wp t (K v). The definition of wp is universally quantified over initial distributions and frames. The main challenge is to connect the single global execution starting from IndexedPSpPm.liftProb μ₀ (from the goal) with these individual wp hypotheses. This step will likely rely on a key property of the program transformer t, for example, that it is "linear" or preserves the kernel decomposition in some way. This might be what the sorry hypothesis is intended to capture.

4. Construct the Witness b: Your goal is to provide a resource b that satisfies b ∈ 𝑪_ μ K and (b • c) ≤ t (IndexedPSpPm.liftProb μ₀). You will need to construct b by defining its own decomposition (P', p', κ'). This construction will likely use the results of applying the wp property for each v.

   • For each v ∈ μ.support, the hypothesis b_v ∈ wp t (K v) gives you the existence of a final resource b'_v satisfying K v.
   • You need a way to "stitch together" these individual b'_v resources to form the final global resource b. The structure of b should mirror the structure of a, using a new set of kernels that represent the state after the program t has run.

5. Show Inclusion and Postcondition: Once you have constructed b, you must prove the two required properties:

   • b ∈ 𝑪_ μ K: This should follow from your construction of b, as its components b'_v were chosen to satisfy K v.
   • (b • c) ≤ t (IndexedPSpPm.liftProb μ₀): This is the most difficult part. It requires relating the global final state t (IndexedPSpPm.liftProb μ₀) to the components b'_v you obtained. Again, this relies on the properties of t.

A useful tactic throughout this proof will be unfold to manage the complex definitions. You may need to use rcases or cases to deconstruct the existential hypotheses from 𝑪_. The key insight will likely involve identifying and applying a linearity or decomposition property of t. Consider investigating what properties are assumed for a program transformer of type IndexedPSpPm I α V F → IndexedPSpPm I α V F, as this might be where the justification for the swap lies.

Goal: Replace the sorry with a complete proof.

Link to the sorry on GitHub

Code Snippet:

theorem C_wp_swap {β : Type*} [MeasurableSpace β] {μ : PMF β}
    {K : β → HyperAssertion (IndexedPSpPm I α V F)} :
    𝑪_ μ (fun v => wp t (K v)) ∧ sorry ⊢ wp t (𝑪_ μ K) := by sorry