Tidy realizations of oracle PPT programs

IsTidyOraclePPTOn strengthens IsOraclePPTOn by requiring one finite machine that halts within a polynomial clock as a clean phase: it starts with blank work tapes and empty query buffers, works for arbitrary retained answer tapes, and finishes with blank work tapes, empty query buffers and its input head restored. Its output is appended to the output tape, and the complete joint law of that output and every external oracle state is exact.

Clean phases compose. This module gives the shared core of the open calculus: deterministic programs, the bounded-prefix query, fair bits, captured data, monadic composition and branching. Only the selected branch of a conditional is executed, so unselected branches make no external call. An unbounded oracle reply is never copied for free: query_take charges its prefix length.

Main definitions

• Cslib.Probability.IsTidyOraclePPTOn: a uniform polynomial-time clean-phase realization.

Main results

• Cslib.Probability.IsTidyOraclePPTOn.isOraclePPTOn: clean realizations are oracle PPT.
• Cslib.Probability.IsTidyOraclePPTOn.query_take: one external call returning a reply prefix.
• Cslib.Probability.IsTidyOraclePPTOn.bind, .bind_with, .pair, .map, .preprocess: composition, charging every intermediate word.
• Cslib.Probability.IsTidyOraclePPTOn.cond, .finite_cases: dispatch executing only the selected branch.

References

The clean-phase combinators adapt the tidy deterministic calculus of cslib (Christian Reitwiessner) to the probabilistic oracle machines of the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8.

def Cslib.Probability.IsTidyOraclePPTOn {Operation α β : Type} [DecidableEq Operation] (input : α ↪ List Bool) (output : β ↪ List Bool) (program : α → WordOracleComp Operation β) : Prop

One finite machine computes the encoded program as a clean phase within a uniform polynomial clock, preserving the joint law of the output and every shared stateful oracle.

theorem Cslib.Probability.IsTidyOraclePPTOn.of_polyBounded {Operation α γ : Type} [DecidableEq Operation] {input : α ↪ List Bool} {output : γ ↪ List Bool} [Finite Operation] {k : ℕ} {Control : Type} [Finite Control] {program : α → WordOracleComp Operation γ} (machine : Turing.MultiTapePTM k Bool Control Operation) {time : α → ℕ} (htime : Turing.MultiTapeTM.PolyBounded (fun (a : α) => (input a).length) time) (h : ∀ (a : α), machine.ComputesTidily (input a) (time a) (⇑output <$> program a)) : IsTidyOraclePPTOn input output program

A fixed finite machine with a polynomially bounded clean-phase clock is a certificate.

theorem Cslib.Probability.IsTidyOraclePPTOn.isOraclePPTOn {Operation α γ : Type} [DecidableEq Operation] {input : α ↪ List Bool} {output : γ ↪ List Bool} {program : α → WordOracleComp Operation γ} (h : IsTidyOraclePPTOn input output program) : IsOraclePPTOn input output program

A clean realization is in particular a strict oracle PPT certificate.

theorem Cslib.Probability.IsTidyOraclePPTOn.congr {Operation α γ : Type} [DecidableEq Operation] {input : α ↪ List Bool} {output : γ ↪ List Bool} {program program' : α → WordOracleComp Operation γ} (h : IsTidyOraclePPTOn input output program) (heq : ∀ (a : α) (State : Type) (oracle : Operation × List Bool → StateT State PMF (List Bool)) (s : State), (OracleComp.interpret (ProbOracleComp.handler (fun (n : ℕ) => StateT.lift (ProbComp.unifOracle n)) oracle) (program a)).run s = (OracleComp.interpret (ProbOracleComp.handler (fun (n : ℕ) => StateT.lift (ProbComp.unifOracle n)) oracle) (program' a)).run s) : IsTidyOraclePPTOn input output program'

Equality of the complete stateful semantics preserves a clean realization.

theorem Cslib.Probability.IsTidyOraclePPTOn.iff_encoded {Operation α γ : Type} [DecidableEq Operation] {input : α ↪ List Bool} {output : γ ↪ List Bool} {program : α → WordOracleComp Operation γ} : IsTidyOraclePPTOn input output program ↔ IsTidyOraclePPTOn input Turing.MultiTapeTM.encBits fun (a : α) => ⇑output <$> program a

A program returning its declared encoding has the same clean realizations.

theorem Cslib.Probability.IsTidyOraclePPTOn.length_le {Operation α γ : Type} [DecidableEq Operation] {input : α ↪ List Bool} {output : γ ↪ List Bool} {program : α → WordOracleComp Operation γ} (h : IsTidyOraclePPTOn input output program) : ∃ (c : ℕ) (d : ℕ), ∀ (a : α) (State : Type) (oracle : Operation × List Bool → StateT State PMF (List Bool)) (s s' : State) (result : γ), (result, s') ∈ ((OracleComp.interpret (ProbOracleComp.handler (fun (n : ℕ) => StateT.lift (ProbComp.unifOracle n)) oracle) (program a)).run s).support → (output result).length ≤ c * ((input a).length + 1) ^ d

Every supported encoded output has polynomial length, independently of all oracle replies.

theorem Cslib.Probability.IsTidyOraclePPTOn.query_take {Operation : Type} [DecidableEq Operation] [Finite Operation] (op : Operation) : IsTidyOraclePPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encUnary) Turing.MultiTapeTM.encBits fun (request : List Bool × ℕ) => List.take request.2 <$> ProbOracleComp.query (op, request.1)

One external call submits query on channel op and returns at most limit reply bits. Unframing the request, the call and scanning the unary limit are all charged.

theorem Cslib.Probability.IsTidyOraclePPTOn.uniform_bool {Operation α : Type} [DecidableEq Operation] [Finite Operation] (input : α ↪ List Bool) : IsTidyOraclePPTOn input Turing.MultiTapeTM.encBool fun (x : α) => ProbOracleComp.sample (ProbComp.uniform Bool)

A fair private bit leaves every external oracle state unchanged.

theorem Cslib.Probability.IsTidyOraclePPTOn.pair {Operation α β γ : Type} [DecidableEq Operation] {input : α ↪ List Bool} {middle : β ↪ List Bool} {output : γ ↪ List Bool} {program : α → WordOracleComp Operation γ} {f : α → β} (hprogram : IsTidyOraclePPTOn input output program) (hf : Turing.MultiTapeTM.ComputableTidilyInPolyTime f input middle) : IsTidyOraclePPTOn input (Turing.MultiTapeTM.encPair middle output) fun (a : α) => (fun (b : γ) => (f a, b)) <$> program a

Retain efficiently computed data beside a probabilistic oracle result.

theorem Cslib.Probability.IsTidyOraclePPTOn.bind {Operation α β γ : Type} [DecidableEq Operation] {input : α ↪ List Bool} {middle : β ↪ List Bool} {output : γ ↪ List Bool} {first : α → WordOracleComp Operation β} {second : β → WordOracleComp Operation γ} (hfirst : IsTidyOraclePPTOn input middle first) (hsecond : IsTidyOraclePPTOn middle output second) : IsTidyOraclePPTOn input output fun (a : α) => first a >>= second

Sequence two clean realizations. The first output length bounds the continuation's clock, and transferring the intermediate word is charged.

theorem Cslib.Probability.IsTidyOraclePPTOn.bind_with {Operation α β γ : Type} [DecidableEq Operation] {input : α ↪ List Bool} {middle : β ↪ List Bool} {output : γ ↪ List Bool} {first : α → WordOracleComp Operation β} {second : α → β → WordOracleComp Operation γ} (hfirst : IsTidyOraclePPTOn input middle first) (hsecond : IsTidyOraclePPTOn (Turing.MultiTapeTM.encPair input middle) output fun (pair : α × β) => second pair.1 pair.2) : IsTidyOraclePPTOn input output fun (a : α) => first a >>= second a

A continuation may use both the caller's input and the first result.

theorem Cslib.Probability.IsTidyOraclePPTOn.of_computableTidilyInPolyTime {Operation α γ : Type} [DecidableEq Operation] {input : α ↪ List Bool} {output : γ ↪ List Bool} [Finite Operation] {f : α → γ} (h : Turing.MultiTapeTM.ComputableTidilyInPolyTime f input output) : IsTidyOraclePPTOn input output fun (a : α) => pure (f a)

Efficient deterministic programs are clean phases that make no external call.

theorem Cslib.Probability.IsTidyOraclePPTOn.preprocess {Operation α β γ : Type} [DecidableEq Operation] {input : α ↪ List Bool} {middle : β ↪ List Bool} {output : γ ↪ List Bool} {program : β → WordOracleComp Operation γ} {prepare : α → β} (hprogram : IsTidyOraclePPTOn middle output program) (hprepare : Turing.MultiTapeTM.ComputableTidilyInPolyTime prepare input middle) : IsTidyOraclePPTOn input output fun (a : α) => program (prepare a)

Efficiently prepare the argument of a clean realization.

theorem Cslib.Probability.IsTidyOraclePPTOn.map {Operation α β γ : Type} [DecidableEq Operation] {input : α ↪ List Bool} {middle : β ↪ List Bool} {output : γ ↪ List Bool} {program : α → WordOracleComp Operation β} {f : β → γ} (hprogram : IsTidyOraclePPTOn input middle program) (hf : Turing.MultiTapeTM.ComputableTidilyInPolyTime f middle output) : IsTidyOraclePPTOn input output fun (a : α) => f <$> program a

Efficient deterministic postprocessing of every result preserves clean realization.

theorem Cslib.Probability.IsTidyOraclePPTOn.map_with {Operation α β γ : Type} [DecidableEq Operation] {input : α ↪ List Bool} {middle : β ↪ List Bool} {output : γ ↪ List Bool} {program : α → WordOracleComp Operation β} {f : α → β → γ} (hprogram : IsTidyOraclePPTOn input middle program) (hf : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (pair : α × β) => f pair.1 pair.2) (Turing.MultiTapeTM.encPair input middle) output) : IsTidyOraclePPTOn input output fun (a : α) => f a <$> program a

A deterministic callback may capture the original argument.

theorem Cslib.Probability.IsTidyOraclePPTOn.cond {Operation α γ : Type} [DecidableEq Operation] {input : α ↪ List Bool} {output : γ ↪ List Bool} {condition : α → Bool} {yes no : α → WordOracleComp Operation γ} (hcondition : Turing.MultiTapeTM.ComputableTidilyInPolyTime condition input Turing.MultiTapeTM.encBool) (hyes : IsTidyOraclePPTOn input output yes) (hno : IsTidyOraclePPTOn input output no) : IsTidyOraclePPTOn input output fun (a : α) => if condition a = true then yes a else no a

Select a branch with an efficient Boolean condition. Only the selected branch runs, so an unselected branch makes no external call and cannot change any oracle state.

theorem Cslib.Probability.IsTidyOraclePPTOn.ite {Operation α γ : Type} [DecidableEq Operation] {input : α ↪ List Bool} {output : γ ↪ List Bool} {condition : α → Prop} [(a : α) → Decidable (condition a)] {yes no : α → WordOracleComp Operation γ} (hcondition : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => decide (condition a)) input Turing.MultiTapeTM.encBool) (hyes : IsTidyOraclePPTOn input output yes) (hno : IsTidyOraclePPTOn input output no) : IsTidyOraclePPTOn input output fun (a : α) => if condition a then yes a else no a

Select a branch with an efficiently decidable condition, executing only that branch.

theorem Cslib.Probability.IsTidyOraclePPTOn.finite_cases {Operation α γ : Type} [DecidableEq Operation] {input : α ↪ List Bool} {output : γ ↪ List Bool} {Tag : Type} [Finite Tag] {tagEncoding : Tag ↪ List Bool} {tag : α → Tag} {branch : Tag → α → WordOracleComp Operation γ} [Finite Operation] (htag : Turing.MultiTapeTM.ComputableTidilyInPolyTime tag input tagEncoding) (hbranch : ∀ (choice : Tag), IsTidyOraclePPTOn input output (branch choice)) : IsTidyOraclePPTOn input output fun (a : α) => branch (tag a) a

A computed finite tag selects one certified branch, which alone is executed.