Probabilistic RelWP carrier for OracleComp (Prob, scoped) #
Installs the probabilistic Std.Do'.RelWP (OracleComp spec₁) (OracleComp spec₂) Prob EPost.nil EPost.nil instance, where Prob = { x : ℝ≥0∞ // x ≤ 1 } is the unit interval as a subtype of ℝ≥0∞
(see VCVio/ProgramLogic/Unary/Loom/Probabilistic.lean for the
Prob carrier and its Lean.Order.{PartialOrder, CompleteLattice}
instances).
Sitting between the qualitative Prop carrier and the quantitative
ℝ≥0∞ carrier, this tier is the natural home for relational
probability-bounded reasoning: pRHL with quantitative slack, apRHL with
ε-budgets that always live in [0, 1], advantage / negligibility on the
relational side.
The carrier is a noncomputable scoped instance under namespace OracleComp.Rel.Probabilistic. Consumers open the namespace to enable
it. See .ignore/wp-cutover-plan.md §"Three-tier carrier design" for
the broader story (Galois connections, coherence lemmas).
Layout and discipline #
Because Std.Do'.RelWP's Pred, EPred₁, EPred₂ are outParams,
only one carrier can be visible to instance synthesis at a time. The
default quantitative ℝ≥0∞ carrier (in Loom/Quantitative.lean)
remains a normal instance and is always live; this scoped instance
is opt-in via open OracleComp.Rel.Probabilistic.
The keystone alignment lemma rwp_val_eq_eRelWP confirms the
underlying ℝ≥0∞ value of Std.Do'.rwp agrees with eRelWP on the
nose, so quantitative theorems still apply after coercing through
.val.
Bound: eRelWP on a Prob-valued post is always ≤ 1 #
The relational expectation of a Prob-valued postcondition is bounded
by 1: any coupling has total mass ≤ 1, and pointwise the
postcondition is ≤ 1.
Probabilistic Std.Do'.RelWP interpretation of pairs of
OracleComp programs valued in Prob = [0, 1] ⊆ ℝ≥0∞.
The rwpTrans is the existing quantitative eRelWP evaluated on
Prob-valued postconditions and packaged into Prob via the ≤ 1
bound. The two EPost.nil arguments are ignored since neither side of
an OracleComp pair has a first-class exception slot.
This is a scoped instance rather than a normal instance: only one
Std.Do'.RelWP (OracleComp spec₁) (OracleComp spec₂) _ _ _ instance
can be visible at a time (Pred is an outParam), and the default is
the quantitative ℝ≥0∞ carrier. Open OracleComp.Rel.Probabilistic
to switch into the probabilistic carrier.
Instances For
Definitional alignment with eRelWP (Prob) #
The keystone lemma confirms that the underlying ℝ≥0∞ value of
Std.Do'.rwp agrees with the quantitative eRelWP on the nose, so
quantitative theorems still apply after coercing through .val.