Composing strict oracle PPT programs

Strict oracle PPT certificates compose like closed ones: by monadic bind, with captured input, deterministic pre- and postprocessing, conditionals and bounded adaptive loops. Every rule quantifies over all shared stateful oracles and arbitrarily long replies, and preserves the complete joint law of the result and the external oracle state.

Each rule first replaces its premises by clean realizations (Cslib.Probability.IsOraclePPTOn.isTidyOraclePPTOn), so a later phase never sees partial requests or stale storage left by an earlier one, and then composes those. Conditionals execute only the selected branch: an unselected branch makes no external call. The only primitive external operation is query_take, which returns a charged prefix of one reply; returning a full unbounded reply is not oracle PPT (ComplexityTests.OraclePPT).

Main results

• Cslib.Probability.IsOraclePPTOn.query_take: one external call returning a reply prefix.
• Cslib.Probability.IsPPTOn.isOraclePPTOn: closed PPT programs are oracle PPT via sample.
• Cslib.Probability.IsOraclePPTOn.isPPTOn: conversely, a sampled closed program certified without external channels is closed PPT.
• Cslib.Probability.IsOraclePPTOn.bind, .bind_with, .pair, .keep_input, .map, .map_with, .preprocess: composition with charged intermediate data.
• Cslib.Probability.IsOraclePPTOn.cond, .ite, .finite_cases: dispatch to one branch.
• Cslib.Probability.IsOraclePPTOn.iterate_spec, .iterateWith_spec, .iterateWith_of_bounded_growth, .iterate_of_bounded_growth: bounded adaptive loops.

References

Adapts the closed composition rules of Computability/Probabilistic/Composition.lean and Computability/Probabilistic/Adaptive.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8 to strict oracle PPT.

theorem Cslib.Probability.IsOraclePPTOn.query_take {Operation α : Type} [DecidableEq Operation] {input : α ↪ List Bool} [Finite Operation] (op : Operation) {request : α → List Bool} {limit : α → ℕ} (hrequest : Turing.MultiTapeTM.ComputableTidilyInPolyTime request input Turing.MultiTapeTM.encBits) (hlimit : Turing.MultiTapeTM.ComputableTidilyInPolyTime limit input Turing.MultiTapeTM.encUnary) : IsOraclePPTOn input Turing.MultiTapeTM.encBits fun (a : α) => List.take (limit a) <$> ProbOracleComp.query (op, request a)

One external call on channel op with an efficiently computed request, returning at most an efficiently computed number of reply bits. Building the request and reading the prefix are charged; the remainder of an arbitrarily long reply is never read.

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

Sequence two strict oracle PPT programs. The intermediate output length bounds the continuation's clock, and every effect of both phases on the shared oracle is retained.

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

Retain efficiently computed input data beside an oracle result.

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

Keep the original argument available to a later computation, charging its encoded copy.

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

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

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

Efficiently prepare the argument of a strict oracle PPT program.

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

Efficient deterministic postprocessing of every result preserves strict oracle PPT.

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

A deterministic callback may capture the original argument.

theorem Cslib.Probability.IsOraclePPTOn.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 : IsOraclePPTOn input output yes) (hno : IsOraclePPTOn input output no) : IsOraclePPTOn 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: the other branch makes no external call and cannot change the oracle state.

theorem Cslib.Probability.IsOraclePPTOn.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 : IsOraclePPTOn input output yes) (hno : IsOraclePPTOn input output no) : IsOraclePPTOn 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.IsOraclePPTOn.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), IsOraclePPTOn input output (branch choice)) : IsOraclePPTOn input output fun (a : α) => branch (tag a) a

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

theorem Cslib.Probability.IsOraclePPTOn.iterate_spec {Operation α σ : Type} [DecidableEq Operation] {input : α ↪ List Bool} {stateEncoding : σ ↪ List Bool} {initial : α → σ} {count : α → ℕ} {step : σ → WordOracleComp Operation σ} (hcount : Turing.MultiTapeTM.ComputableTidilyInPolyTime count input Turing.MultiTapeTM.encUnary) (hinitial : Turing.MultiTapeTM.ComputableTidilyInPolyTime initial input stateEncoding) (hstep : IsOraclePPTOn stateEncoding stateEncoding step) (invariant : α → ℕ → σ → Prop) (hbase : ∀ (a : α), invariant a 0 (initial a)) (hpreserve : ∀ (a : α) (i : ℕ) (state : σ), i < count a → invariant a i state → ∀ next ∈ ProbOracleComp.support (step state), invariant a (i + 1) next) {size : α → ℕ} (hsize : Turing.MultiTapeTM.PolyBounded (fun (a : α) => (input a).length) size) (hbound : ∀ (a : α) (i : ℕ) (state : σ), i ≤ count a → invariant a i state → (stateEncoding state).length ≤ size a) : (IsOraclePPTOn input stateEncoding fun (a : α) => OracleComp.iterate (count a) step (initial a)) ∧ ∀ (a : α), ∀ state ∈ ProbOracleComp.support (OracleComp.iterate (count a) step (initial a)), invariant a (count a) state

A bounded adaptive loop is strict oracle PPT when one invariant bounds every reachable state. The invariant holds for every possible result under every stateful oracle, and it is also established for the final state. Every iteration may query the shared oracle.

theorem Cslib.Probability.IsOraclePPTOn.iterateWith_spec {Operation α σ : Type} [DecidableEq Operation] {input : α ↪ List Bool} {stateEncoding : σ ↪ List Bool} {initial : α → σ} {count : α → ℕ} {step : α → σ → WordOracleComp Operation σ} (hcount : Turing.MultiTapeTM.ComputableTidilyInPolyTime count input Turing.MultiTapeTM.encUnary) (hinitial : Turing.MultiTapeTM.ComputableTidilyInPolyTime initial input stateEncoding) (hstep : IsOraclePPTOn (Turing.MultiTapeTM.encPair input stateEncoding) stateEncoding fun (pair : α × σ) => step pair.1 pair.2) (invariant : α → ℕ → σ → Prop) (hbase : ∀ (a : α), invariant a 0 (initial a)) (hpreserve : ∀ (a : α) (i : ℕ) (state : σ), i < count a → invariant a i state → ∀ next ∈ ProbOracleComp.support (step a state), invariant a (i + 1) next) {size : α → ℕ} (hsize : Turing.MultiTapeTM.PolyBounded (fun (a : α) => (input a).length) size) (hbound : ∀ (a : α) (i : ℕ) (state : σ), i ≤ count a → invariant a i state → (stateEncoding state).length ≤ size a) : (IsOraclePPTOn input stateEncoding fun (a : α) => OracleComp.iterate (count a) (step a) (initial a)) ∧ ∀ (a : α), ∀ state ∈ ProbOracleComp.support (OracleComp.iterate (count a) (step a) (initial a)), invariant a (count a) state

The loop body may capture the original input; the invariant describes the changing state.

theorem Cslib.Probability.IsOraclePPTOn.iterateWith_of_bounded_growth {Operation α σ : Type} [DecidableEq Operation] {input : α ↪ List Bool} {stateEncoding : σ ↪ List Bool} {initial : α → σ} {count : α → ℕ} {step : α → σ → WordOracleComp Operation σ} (hcount : Turing.MultiTapeTM.ComputableTidilyInPolyTime count input Turing.MultiTapeTM.encUnary) (hinitial : Turing.MultiTapeTM.ComputableTidilyInPolyTime initial input stateEncoding) (hstep : IsOraclePPTOn (Turing.MultiTapeTM.encPair input stateEncoding) stateEncoding fun (pair : α × σ) => step pair.1 pair.2) {growth : α → ℕ} (hpoly : Turing.MultiTapeTM.PolyBounded (fun (a : α) => (input a).length) growth) (hgrowth : ∀ (a : α) (state next : σ), next ∈ ProbOracleComp.support (step a state) → (stateEncoding next).length ≤ (stateEncoding state).length + growth a) : IsOraclePPTOn input stateEncoding fun (a : α) => OracleComp.iterate (count a) (step a) (initial a)

Captured-input steps may grow by a polynomially bounded amount depending on that input, for every possible next state under every stateful oracle.

theorem Cslib.Probability.IsOraclePPTOn.iterate_of_bounded_growth {Operation α σ : Type} [DecidableEq Operation] {input : α ↪ List Bool} {stateEncoding : σ ↪ List Bool} {initial : α → σ} {count : α → ℕ} {step : σ → WordOracleComp Operation σ} (hcount : Turing.MultiTapeTM.ComputableTidilyInPolyTime count input Turing.MultiTapeTM.encUnary) (hinitial : Turing.MultiTapeTM.ComputableTidilyInPolyTime initial input stateEncoding) (hstep : IsOraclePPTOn stateEncoding stateEncoding step) {growth : ℕ} (hgrowth : ∀ (state next : σ), next ∈ ProbOracleComp.support (step state) → (stateEncoding next).length ≤ (stateEncoding state).length + growth) : IsOraclePPTOn input stateEncoding fun (a : α) => OracleComp.iterate (count a) step (initial a)

A strict oracle PPT step with constant growth can be repeated a polynomial number of times.

theorem Cslib.Probability.IsPPTOn.isOraclePPTOn {Operation α γ : Type} [DecidableEq Operation] {input : α ↪ List Bool} {output : γ ↪ List Bool} [Finite Operation] {program : α → ProbComp γ} (h : IsPPTOn input output program) : IsOraclePPTOn input output fun (a : α) => ProbOracleComp.sample (program a)

A closed strict PPT program is strict oracle PPT when sampled privately: its machine never uses an external channel, so every external oracle state is preserved.

theorem Cslib.Probability.IsOraclePPTOn.isPPTOn {α γ : Type} {input : α ↪ List Bool} {output : γ ↪ List Bool} {program : α → ProbComp γ} (h : IsOraclePPTOn input output fun (a : α) => ProbOracleComp.sample (program a)) : IsPPTOn input output program

A sampled closed program certified without external channels is closed strict PPT: the realizing machine has no channels, so it is a closed machine with the same output law.