pRHL Proof Rules #
This file contains the core proof rules for probabilistic relational Hoare logic.
Structural Rules #
Consequence rule: strengthen precondition, weaken postcondition
Symmetry rule
Symmetry specialized to the equality pre/postconditions: swap the two programs.
Return Rules #
Bind Rule #
Bind rule: sequential composition of judgments
Reflexivity and Transitivity #
Reflexivity: same code with equal heaps gives equal results
Transitivity for equal-heap coupling.
When composing through an intermediate computation, if:
- c₁ and c₂ produce equal results with equal heaps
- c₂ and c₃ produce equal results with equal heaps Then c₁ and c₃ also produce equal results with equal heaps.
This is used in hybrid argument proofs where we compose through intermediate games.
Sampling Rules #
Same distribution, diagonal coupling
One-sided sample on the left.
Key idea: Use averaging coupling.
- For each sampled value a, we have a coupling from
h a - Rewrite right side as (uniform σ).bind (fun _ => c₂ h₂) using uniform_bind_const
- Apply liftR_bind with the diagonal coupling on σ
One-sided sample on the right.
Key idea: Use averaging coupling (symmetric to sample_l).
State Rules #
Synchronized get: same location, synchronized values
Synchronized set: same location and value
One-sided get on the left. Note: β is constrained to Type (universe 0) since l.ty : Type.
One-sided get on the right. Note: β is constrained to Type (universe 0) since l.ty : Type.
One-sided put on the left
One-sided put on the right
Failure and Assertion Rules #
Failure on both sides: when both programs fail, any postcondition holds vacuously. Note: With coupling-based semantics, failure on one side requires failure on the other for a valid coupling to exist (since marginals must match).
Assertion: if precondition implies P, assertion succeeds
Conditional Rules #
Synchronized conditional: when both sides branch on the same Bool value,
prove each branch separately.
This is the standard pRHL if rule. After a synchronized get, both
sides evaluate the same condition, so we case-split on the shared value.
Synchronized conditional with different conditions: when conditions agree (provable from equality or other means), prove each branch separately.
Synchronized decidable conditional: both sides branch on the same
decidable proposition P. The branch proofs may depend on P or ¬P.
Swap Rules #
These rules allow reordering independent operations in a computation. This is useful when the order of operations on the left and right sides differ.
Swap on left: if two SPComp programs are equal (as functions from Heap), we can replace one with the other on the left side of a relational judgment.
Swap on right: symmetric to swap_lhs
Swap two consecutive samples. The order of two independent sampling operations can be exchanged because sampling from independent distributions commutes.
Uses the Fubini property for finite distributions.
Swap sample followed by get on the left. Sample and get from a location commute because sampling doesn't affect the heap and get doesn't affect the distribution.
Swap get followed by sample on the left. Get and sample commute because get is deterministic and doesn't affect the distribution of sample.
Swap two consecutive gets from different locations. Get operations from independent locations can be reordered.
Swap set followed by sample. Set and sample commute because set is deterministic and sample doesn't depend on heap.
Swap sample followed by set. Sample and set commute because sample doesn't affect the heap value being set.
Swap set followed by get from a different location. Set and get from independent locations can be reordered.
Swap get followed by set to a different location. Get and set to independent locations can be reordered.
Swap two consecutive sets to different locations. Set operations to independent locations can be reordered.
Post-Processing and Factorization #
These rules establish key inequalities for security reductions. The post-processing lemma states that applying the same function to two distributions cannot increase the advantage of distinguishing them.
Factorization: rewriting advantage in terms of intermediate computations.
If two games can be written as the same function f applied to different
base computations, the advantage equals the advantage on the base
computations with the composed distinguisher fun x => (f x).bind A.
This is an equality, not just an inequality, because bind is
associative — post-composing both games with the same f neither increases
nor decreases distinguishing advantage (it merely moves f into the
distinguisher). The one-directional "post-processing cannot increase
advantage" bound is the immediate le_of_eq consequence.
Advantage is symmetric: swapping the games doesn't change the advantage. This follows from the symmetric definition using max of both directions.
Contract Rules #
These rules establish equality between SPComp programs by eliminating redundant operations. They are used by contract tactics to simplify code before relational reasoning.
Contract duplicate gets: getting the same location twice in sequence is equivalent to getting once and using the value twice.
x ← get l; y ← get l; f x y = x ← get l; f x x
Note: α is constrained to Type (universe 0) since l.ty : Type.
Contract duplicate puts: putting to the same location twice in sequence is equivalent to just putting the second value.
put l v; put l v'; k = put l v'; k
Note: α is constrained to Type (universe 0) since l.ty : Type.
Contract put-get: getting a location immediately after putting to it returns the value that was put.
put l v; x ← get l; f x = put l v; f v
Note: α is constrained to Type (universe 0) since l.ty : Type.
Dead Code Elimination Rules #
These rules eliminate unused computations from SPComp programs. They are used by the ProofFrog-inspired dead code elimination tactics.
Const sample: sampling and ignoring the result is equivalent to identity.
This lemma is used by dead_sample to eliminate unused samples.
Dead sample: if a sample result is not used, the sample can be eliminated.
let _ ← sample α; k = k
Note: This is sound because sampling from a uniform distribution and discarding the result is equivalent to doing nothing (lossless sampling).
Dead get: if a get result is not used, the get can be eliminated.
let _ ← get l; k = k
Note: This is sound because get is a pure read with no side effects.
Dead pure: if a pure result is not used, the pure can be eliminated.
let _ ← pure v; k = k
Copy Propagation Rules #
These rules help with copy propagation by providing lemmas for substituting known values.
Get followed by using the value: the continuation sees the heap value.
After x ← get l, we know x = h.get l. This lemma is used for
copy propagation where we substitute the known value.
After set, the location has the set value.
(set l v; get l) returns v.
Unreachable Code Rules #
These rules help identify and eliminate unreachable code paths.
If the precondition is False, any relational judgment holds trivially.
If we have an assertion #assert false, the code is unreachable.
Rewriting on LHS is sound for rHoare when the codes are equal.
Rewriting on RHS is sound for rHoare when the codes are equal.
Combined Coupling Steps #
These lemmas combine rHoare_bind + rHoare_sample_bij/rHoare_sample_same
into a single step, eliminating the need for explicit intermediate postconditions.
Combined bijection coupling step.
Combines rHoare_bind + rHoare_sample_bij + precondition adjustment in one step.
When both sides sample and you have a bijection f, this reduces to proving
the continuation for each sampled value a with the right side receiving f a.
Replaces the common 4-8 line pattern:
apply rHoare_bind (Ψ := fun a _ b _ => Φ h₁ h₂ ∧ f a = b)
· exact rHoare_sample_bij α β f
· intro a b
apply rHoare_conseq ...
with a single application.
Bijection step with bare sample on the right side.
Bijection step with bare sample on the left side.
Combined same-distribution coupling step.
Combines rHoare_bind + rHoare_sample_same in one step.
When both sides sample from the same distribution, this reduces to proving
the continuation for each sampled value a shared by both sides.
Replaces the common pattern:
apply liftR_bind liftR_uniform_same
intro a a' haa'; subst haa'
with a single application.
Canonicalization Lemmas #
These lemmas help put SPComp programs into a canonical form for easier comparison and simplification.
Bind of bind can be reassociated (left-to-right).
Pure on the left of bind simplifies.
Bind with pure on the right is identity.
FoldM Rule #
Relational Hoare rule for foldM: if each step preserves the invariant, then foldM preserves it.
Inv a₁ a₂ is the loop invariant parameterized by the accumulators on both sides.
The precondition establishes Inv a₁ a₂, and each step must preserve it.