Documentation

VCVio.ProgramLogic.Relational.QuantitativeDefs

Core eRHL Definitions #

This file contains the lightweight definitions for the quantitative relational logic layer. It is intentionally separated from the heavier coupling-development file so downstream users that only need the interfaces and notation do not import the full theorem stack.

source
noncomputable def OracleComp.ProgramLogic.Relational.eRelWP {ι₁ ι₂ : Type u} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} [spec₁.Fintype] [spec₁.Inhabited] [spec₂.Fintype] [spec₂.Inhabited] {α β : Type} (oa : OracleComp spec₁ α) (ob : OracleComp spec₂ β) (g : α → β → ENNReal) :
ENNReal

eRHL-style quantitative relational WP for OracleComp. eRelWP oa ob g is the supremum over all couplings c of the expected value of g under c.

Instances For
    source
    noncomputable def OracleComp.ProgramLogic.Relational.RelPost.indicator {α β : Type} (R : RelPost α β) (a : α) (b : β) :
    ENNReal

    Indicator postcondition: lifts a Prop-valued relation to an ℝ≥0∞-valued one.

    Instances For
      source
      def OracleComp.ProgramLogic.Relational.RelTriple' {ι₁ ι₂ : Type u} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} [spec₁.Fintype] [spec₁.Inhabited] [spec₂.Fintype] [spec₂.Inhabited] {α β : Type} (oa : OracleComp spec₁ α) (ob : OracleComp spec₂ β) (R : RelPost α β) :
      Prop

      pRHL-style exact relational triple, defined via quantitative relational WP with an indicator postcondition.

      Instances For
        source
        def OracleComp.ProgramLogic.Relational.ApproxRelTriple {ι₁ ι₂ : Type u} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} [spec₁.Fintype] [spec₁.Inhabited] [spec₂.Fintype] [spec₂.Inhabited] {α β : Type} (ε : ENNReal) (oa : OracleComp spec₁ α) (ob : OracleComp spec₂ β) (R : RelPost α β) :
        Prop

        ε-approximate relational triple via quantitative relational WP: R holds except with probability at most ε.

        Instances For
          source
          theorem OracleComp.ProgramLogic.Relational.relTriple'_eq_approxRelTriple_zero {ι₁ ι₂ : Type u} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} [spec₁.Fintype] [spec₁.Inhabited] [spec₂.Fintype] [spec₂.Inhabited] {α β : Type} {oa : OracleComp spec₁ α} {ob : OracleComp spec₂ β} {R : RelPost α β} :
          RelTriple' oa ob R ↔ ApproxRelTriple 0 oa ob R

          Exact coupling is the zero-error special case of approximate coupling.