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
    def OracleComp.ProgramLogic.Relational.eRelTriple {ι₁ ι₂ : Type u} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} [spec₁.Fintype] [spec₁.Inhabited] [spec₂.Fintype] [spec₂.Inhabited] {α β : Type} (pre : ENNReal) (oa : OracleComp spec₁ α) (ob : OracleComp spec₂ β) (post : α → β → ENNReal) :
    Prop

    eRHL triple: pre ≤ eRelWP oa ob post.

    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 eRHL with 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 eRHL: "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.