Quantitative Hoare triples for `OracleComp` #

The construction is based on a Loom-style ordered monad algebra (MAlgOrdered) instantiated for OracleComp spec with carrier ℝ≥0∞.

API contract #

This unary quantitative interface is instantiated for OracleComp spec.
Probability/evaluation assumptions are [spec.Fintype] and [spec.Inhabited].
The quantitative codomain is fixed to ℝ≥0∞.

source

noncomputable def OracleComp.ProgramLogic.μ {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] (oa : OracleComp spec ENNReal) :

ENNReal

Expectation-style algebra for oracle computations returning ℝ≥0∞.

Equations

Instances For

source

noncomputable instance OracleComp.ProgramLogic.instMAlgOrdered {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] :

MAlgOrdered (OracleComp spec) ENNReal

Equations

source

@[reducible, inline]

noncomputable abbrev OracleComp.ProgramLogic.wp {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α : Type} (oa : OracleComp spec α) (post : α → ENNReal) :

ENNReal

Quantitative weakest precondition for OracleComp.

Equations

Instances For

source

@[reducible, inline]

noncomputable abbrev OracleComp.ProgramLogic.Triple {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α : Type} (pre : ENNReal) (oa : OracleComp spec α) (post : α → ENNReal) :

Prop

Quantitative Hoare-style triple for OracleComp.

Equations

Instances For

source

@[simp]

theorem OracleComp.ProgramLogic.wp_pure {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α : Type} (x : α) (post : α → ENNReal) :

wp (pure x) post = post x

source

@[simp]

theorem OracleComp.ProgramLogic.wp_ite {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α : Type} (c : Prop) [Decidable c] (oa ob : OracleComp spec α) (post : α → ENNReal) :

wp (if c then oa else ob) post = if c then wp oa post else wp ob post

source

@[simp]

theorem OracleComp.ProgramLogic.wp_dite {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α : Type} (c : Prop) [Decidable c] (oa : c → OracleComp spec α) (ob : ¬c → OracleComp spec α) (post : α → ENNReal) :

wp (dite c oa ob) post = if h : c then wp (oa h) post else wp (ob h) post

source

theorem OracleComp.ProgramLogic.wp_bind {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α β : Type} (oa : OracleComp spec α) (ob : α → OracleComp spec β) (post : β → ENNReal) :

wp (oa >>= ob) post = wp oa fun (x : α) => wp (ob x) post

source

theorem OracleComp.ProgramLogic.wp_replicate_zero {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α : Type} (oa : OracleComp spec α) (post : List α → ENNReal) :

wp (replicate 0 oa) post = post []

source

theorem OracleComp.ProgramLogic.wp_replicate_succ {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α : Type} (oa : OracleComp spec α) (n : ℕ) (post : List α → ENNReal) :

wp (replicate (n + 1) oa) post = wp oa fun (x : α) => wp (replicate n oa) fun (xs : List α) => post (x :: xs)

source

theorem OracleComp.ProgramLogic.wp_list_mapM_nil {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α β : Type} (f : α → OracleComp spec β) (post : List β → ENNReal) :

wp (List.mapM f []) post = post []

source

theorem OracleComp.ProgramLogic.wp_list_mapM_cons {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α β : Type} (x : α) (xs : List α) (f : α → OracleComp spec β) (post : List β → ENNReal) :

wp (List.mapM f (x :: xs)) post = wp (f x) fun (y : β) => wp (List.mapM f xs) fun (ys : List β) => post (y :: ys)

source

theorem OracleComp.ProgramLogic.wp_list_foldlM_nil {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α σ : Type} (f : σ → α → OracleComp spec σ) (init : σ) (post : σ → ENNReal) :

wp (List.foldlM f init []) post = post init

source

theorem OracleComp.ProgramLogic.wp_list_foldlM_cons {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α σ : Type} (x : α) (xs : List α) (f : σ → α → OracleComp spec σ) (init : σ) (post : σ → ENNReal) :

wp (List.foldlM f init (x :: xs)) post = wp (f init x) fun (s : σ) => wp (List.foldlM f s xs) post

source

theorem OracleComp.ProgramLogic.wp_mono {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α : Type} (oa : OracleComp spec α) {post post' : α → ENNReal} (hpost : ∀ (x : α), post x ≤ post' x) :

wp oa post ≤ wp oa post'

source

theorem OracleComp.ProgramLogic.wp_map {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α β : Type} (f : α → β) (oa : OracleComp spec α) (post : β → ENNReal) :

wp (f <$> oa) post = wp oa (post ∘ f)

source

theorem OracleComp.ProgramLogic.wp_eq_tsum {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α : Type} (oa : OracleComp spec α) (post : α → ENNReal) :

wp oa post = ∑' (x : α), Pr[=x | oa] * post x

General unfolding: wp as weighted sum over output probabilities.

source

@[simp]

theorem OracleComp.ProgramLogic.wp_const {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α : Type} (oa : OracleComp spec α) (c : ENNReal) :

(wp oa fun (x : α) => c) = c

source

theorem OracleComp.ProgramLogic.wp_add {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α : Type} (oa : OracleComp spec α) (f g : α → ENNReal) :

(wp oa fun (x : α) => f x + g x) = wp oa f + wp oa g

source

theorem OracleComp.ProgramLogic.wp_mul_const {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α : Type} (oa : OracleComp spec α) (c : ENNReal) (f : α → ENNReal) :

(wp oa fun (x : α) => c * f x) = c * wp oa f

source

theorem OracleComp.ProgramLogic.wp_const_mul {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α : Type} (oa : OracleComp spec α) (f : α → ENNReal) (c : ENNReal) :

(wp oa fun (x : α) => f x * c) = wp oa f * c

source

theorem OracleComp.ProgramLogic.triple_conseq {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α : Type} {pre pre' : ENNReal} {oa : OracleComp spec α} {post post' : α → ENNReal} (hpre : pre' ≤ pre) (hpost : ∀ (x : α), post x ≤ post' x) :

Triple pre oa post → Triple pre' oa post'

source

theorem OracleComp.ProgramLogic.triple_bind {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α β : Type} {pre : ENNReal} {oa : OracleComp spec α} {cut : α → ENNReal} {ob : α → OracleComp spec β} {post : β → ENNReal} (hoa : Triple pre oa cut) (hob : ∀ (x : α), Triple (cut x) (ob x) post) :

Triple pre (oa >>= ob) post

source

theorem OracleComp.ProgramLogic.triple_bind_wp {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α β : Type} {pre : ENNReal} {oa : OracleComp spec α} {ob : α → OracleComp spec β} {post : β → ENNReal} (h : Triple pre oa fun (x : α) => wp (ob x) post) :

Triple pre (oa >>= ob) post

source

theorem OracleComp.ProgramLogic.triple_pure {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α : Type} (x : α) (post : α → ENNReal) :

Triple (post x) (pure x) post

source

theorem OracleComp.ProgramLogic.triple_zero {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α : Type} (oa : OracleComp spec α) (post : α → ENNReal) :

Triple 0 oa post

A quantitative triple with precondition 0 is always true.

source

theorem OracleComp.ProgramLogic.triple_ite {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α : Type} {c : Prop} [Decidable c] {pre : ENNReal} {oa ob : OracleComp spec α} {post : α → ENNReal} (ht : c → Triple pre oa post) (hf : ¬c → Triple pre ob post) :

Triple pre (if c then oa else ob) post

source

theorem OracleComp.ProgramLogic.triple_dite {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α : Type} {c : Prop} [Decidable c] {pre : ENNReal} {oa : c → OracleComp spec α} {ob : ¬c → OracleComp spec α} {post : α → ENNReal} (ht : ∀ (h : c), Triple pre (oa h) post) (hf : ∀ (h : ¬c), Triple pre (ob h) post) :

Triple pre (dite c oa ob) post

source

theorem OracleComp.ProgramLogic.probEvent_eq_wp_indicator {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α : Type} (oa : OracleComp spec α) (p : α → Prop) [DecidablePred p] :

Pr[p | oa] = wp oa fun (x : α) => if p x then 1 else 0

probEvent as a WP of an indicator postcondition.

source

theorem OracleComp.ProgramLogic.probOutput_eq_wp_indicator {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α : Type} (oa : OracleComp spec α) [DecidableEq α] (x : α) :

Pr[=x | oa] = wp oa fun (y : α) => if y = x then 1 else 0

probOutput as a WP of a singleton-indicator postcondition.

source

theorem OracleComp.ProgramLogic.wp_liftM_query {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] (t : spec.Domain) (post : spec.Range t → ENNReal) :

wp (liftM (query t)) post = ∑' (u : spec.Range t), 1 / ↑(Fintype.card (spec.Range t)) * post u

liftM query form of wp_query.

source

theorem OracleComp.ProgramLogic.wp_query {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] (t : spec.Domain) (post : spec.Range t → ENNReal) :

wp (liftM (query t)) post = ∑' (u : spec.Range t), 1 / ↑(Fintype.card (spec.Range t)) * post u

Quantitative WP rule for a uniform oracle query.

source

theorem OracleComp.ProgramLogic.wp_uniformSample {α : Type} [SampleableType α] (post : α → ENNReal) :

wp ($ᵗα) post = ∑' (x : α), Pr[=x | $ᵗα] * post x

source

theorem OracleComp.ProgramLogic.triple_probEvent_indicator {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α : Type} (oa : OracleComp spec α) (p : α → Prop) [DecidablePred p] :

Triple Pr[p | oa] oa fun (x : α) => if p x then 1 else 0

Indicator-event probability as an exact quantitative triple.

source

theorem OracleComp.ProgramLogic.triple_probOutput_indicator {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α : Type} (oa : OracleComp spec α) [DecidableEq α] (x : α) :

Triple Pr[=x | oa] oa fun (y : α) => if y = x then 1 else 0

Singleton-output probability as an exact quantitative triple.

source

@[simp]

theorem OracleComp.ProgramLogic.probEvent_mem_support {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α : Type} (oa : OracleComp spec α) :

Pr[fun (x : α) => x ∈ support oa | oa] = 1

The support event of an OracleComp occurs almost surely.

source

theorem OracleComp.ProgramLogic.triple_probEvent_eq_one {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α : Type} (oa : OracleComp spec α) (p : α → Prop) [DecidablePred p] (h : Pr[p | oa] = 1) :

Triple 1 oa fun (x : α) => if p x then 1 else 0

Exact probability-1 events are exact quantitative triples.

source

theorem OracleComp.ProgramLogic.triple_probOutput_eq_one {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α : Type} (oa : OracleComp spec α) [DecidableEq α] (x : α) (h : Pr[=x | oa] = 1) :

Triple 1 oa fun (y : α) => if y = x then 1 else 0

Exact probability-1 singleton outputs are exact quantitative triples.

source

theorem OracleComp.ProgramLogic.probOutput_eq_one_iff_triple {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α : Type} (oa : OracleComp spec α) [DecidableEq α] (x : α) :

Pr[=x | oa] = 1 ↔ Triple 1 oa fun (y : α) => if y = x then 1 else 0

Pr[= x | oa] = 1 ↔ Triple 1 oa (indicator). Bridge for qvcgen probability lowering.

source

theorem OracleComp.ProgramLogic.triple_support {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α : Type} (oa : OracleComp spec α) [DecidablePred fun (x : α) => x ∈ support oa] :

Triple 1 oa fun (x : α) => if x ∈ support oa then 1 else 0

Support membership is a useful default cut function for support-sensitive bind proofs.

Loop stepping rules (Triple-level) #

source

theorem OracleComp.ProgramLogic.triple_replicate_succ {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α : Type} {pre : ENNReal} {oa : OracleComp spec α} {n : ℕ} {post : List α → ENNReal} (h : Triple pre oa fun (x : α) => wp (replicate n oa) fun (xs : List α) => post (x :: xs)) :

Triple pre (replicate (n + 1) oa) post

source

theorem OracleComp.ProgramLogic.triple_list_mapM_cons {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α β : Type} {pre : ENNReal} {x : α} {xs : List α} {f : α → OracleComp spec β} {post : List β → ENNReal} (h : Triple pre (f x) fun (y : β) => wp (List.mapM f xs) fun (ys : List β) => post (y :: ys)) :

Triple pre (List.mapM f (x :: xs)) post

source

theorem OracleComp.ProgramLogic.triple_list_foldlM_cons {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α σ : Type} {pre : ENNReal} {x : α} {xs : List α} {f : σ → α → OracleComp spec σ} {init : σ} {post : σ → ENNReal} (h : Triple pre (f init x) fun (s : σ) => wp (List.foldlM f s xs) post) :

Triple pre (List.foldlM f init (x :: xs)) post

Loop invariant rules #

source

theorem OracleComp.ProgramLogic.triple_replicate_inv {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α : Type} {I : ENNReal} {oa : OracleComp spec α} {n : ℕ} (hstep : Triple I oa fun (x : α) => I) :

Triple I (replicate n oa) fun (x : List α) => I

Constant invariant through bounded iteration via replicate.

source

theorem OracleComp.ProgramLogic.triple_list_foldlM_inv {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α σ : Type} {I : σ → ENNReal} {f : σ → α → OracleComp spec σ} {l : List α} {s₀ : σ} (hstep : ∀ (s : σ), ∀ x ∈ l, Triple (I s) (f s x) I) :

Triple (I s₀) (List.foldlM f s₀ l) I

Indexed invariant through List.foldlM.

source

theorem OracleComp.ProgramLogic.triple_list_mapM_inv {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α β : Type} {I : ENNReal} {f : α → OracleComp spec β} {l : List α} (hstep : ∀ x ∈ l, Triple I (f x) fun (x : β) => I) :

Triple I (List.mapM f l) fun (x : List β) => I

Constant invariant through List.mapM.

source

theorem OracleComp.ProgramLogic.triple_replicate {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α : Type} {I pre : ENNReal} {oa : OracleComp spec α} {n : ℕ} {post : List α → ENNReal} (hpre : pre ≤ I) (hpost : ∀ (xs : List α), I ≤ post xs) (hstep : Triple I oa fun (x : α) => I) :

Triple pre (replicate n oa) post

replicate invariant with consequence: bridges arbitrary pre/post to the invariant.

source

theorem OracleComp.ProgramLogic.triple_list_foldlM {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α σ : Type} {I : σ → ENNReal} {f : σ → α → OracleComp spec σ} {l : List α} {s₀ : σ} {pre : ENNReal} {post : σ → ENNReal} (hpre : pre ≤ I s₀) (hpost : ∀ (s : σ), I s ≤ post s) (hstep : ∀ (s : σ), ∀ x ∈ l, Triple (I s) (f s x) I) :

Triple pre (List.foldlM f s₀ l) post

List.foldlM invariant with consequence.

source

theorem OracleComp.ProgramLogic.triple_list_mapM {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α β : Type} {I : ENNReal} {f : α → OracleComp spec β} {l : List α} {pre : ENNReal} {post : List β → ENNReal} (hpre : pre ≤ I) (hpost : ∀ (ys : List β), I ≤ post ys) (hstep : ∀ x ∈ l, Triple I (f x) fun (x : β) => I) :

Triple pre (List.mapM f l) post

List.mapM invariant with consequence.