Uniform oracle PPT with a security parameter

The unary security parameter and auxiliary word use the same pair encoding as closed IsPPT. IsOraclePPT is a specialization of the existing joint-state contract, with the same named word channels. No second machine model or interpreter is introduced. A single Unit channel suffices for cryptographic random-function experiments.

Main definitions

• Cslib.Probability.IsOraclePPT: strict uniform oracle PPT with a unary security parameter.

Main results

• Cslib.Probability.IsOraclePPT.query_bounds: polynomial external call and request budgets.
• Cslib.Probability.IsOraclePPT.run_interpret_preprocess: efficient closed stateful substitution.
• Cslib.Probability.IsOraclePPT.run_interpret_preprocess_open: efficient open stateful substitution, whose handler may call an external oracle.

References

Adapts the security-parameter interface in Computability/Probabilistic/Oracle.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8, using the existing word channels.

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

One uniform oracle machine on a unary security parameter and an auxiliary word.

theorem Cslib.Probability.IsOraclePPT.on {Operation β : Type} [DecidableEq Operation] {output : β ↪ List Bool} {program : ℕ → List Bool → WordOracleComp Operation β} (h : IsOraclePPT output program) : IsOraclePPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits) output fun (input : ℕ × List Bool) => program input.1 input.2

Expose the existing encoded-input contract.

theorem Cslib.Probability.IsOraclePPTOn.isOraclePPT {Operation β : Type} [DecidableEq Operation] {output : β ↪ List Bool} {program : ℕ → List Bool → WordOracleComp Operation β} (h : IsOraclePPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits) output fun (input : ℕ × List Bool) => program input.1 input.2) : IsOraclePPT output program

An encoded certificate for the unary parameter and word is uniform oracle PPT.

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

Equality of the joint output/state semantics preserves the parameterized certificate.

theorem Cslib.Probability.IsOraclePPT.query_bounds {Operation β : Type} [DecidableEq Operation] {output : β ↪ List Bool} {program : ℕ → List Bool → WordOracleComp Operation β} (h : IsOraclePPT output program) : ∃ (c : ℕ) (d : ℕ), ∀ (n : ℕ) (input : List Bool), ProbOracleComp.IsQueryBounded (program n input) (c * (n + input.length + 2) ^ d) ∧ ProbOracleComp.QueriesSatisfy (fun (request : Operation × List Bool) => request.2.length ≤ c * (n + input.length + 2) ^ d) (program n input)

The same polynomial bounds external calls and request lengths, independently of replies.

theorem Cslib.Probability.IsOraclePPT.run_interpret_preprocess {Operation β : Type} [DecidableEq Operation] {output : β ↪ List Bool} {program : ℕ → List Bool → WordOracleComp Operation β} {Caller State : Type} [Finite Operation] {input : Caller ↪ List Bool} {stateEncoding : State ↪ List Bool} {handler : Caller → Operation × List Bool → State → ProbComp (List Bool × State)} {prepare : Caller → ℕ × List Bool} {initial : Caller → State} {resources : Caller → List Bool → ℕ} (hprogram : IsOraclePPT output program) (hprepare : Turing.MultiTapeTM.ComputableTidilyInPolyTime prepare input (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits)) (hhandler : IsPPTOn (Turing.MultiTapeTM.encPair input (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encFinite Operation) Turing.MultiTapeTM.encBits) stateEncoding)) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits stateEncoding) fun (pair : Caller × (Operation × List Bool) × State) => handler pair.1 pair.2.1 pair.2.2) (hinitial : Turing.MultiTapeTM.ComputableTidilyInPolyTime initial input stateEncoding) (invariant : Caller → State → Prop) (hinit : ∀ (a : Caller), invariant a (initial a)) (hresources : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (pair : Caller × List Bool) => resources pair.1 pair.2) (Turing.MultiTapeTM.encPair input Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encUnary) (hpreserve : ∀ (a : Caller) (request : Operation × List Bool) (state : State), invariant a state → ∀ result ∈ (handler a request state).eval.support, invariant a result.2 ∧ result.1.length ≤ resources a request.2 ∧ (stateEncoding result.2).length ≤ (stateEncoding state).length + resources a request.2) : IsPPTOn input (Turing.MultiTapeTM.encPair output stateEncoding) fun (a : Caller) => (OracleComp.interpret (ProbOracleComp.handler (fun (n : ℕ) => StateT.lift (ProbComp.unifFin n)) (handler a)) (program (prepare a).1 (prepare a).2)).run (initial a)

Supply a closed stateful handler to a parameterized oracle program. The result retains the final private state, and a local invariant charges reply length and all added encoded storage.

theorem Cslib.Probability.IsOraclePPT.run_interpret_preprocess_open {Operation β : Type} [DecidableEq Operation] {output : β ↪ List Bool} {program : ℕ → List Bool → WordOracleComp Operation β} {External Caller State : Type} [DecidableEq External] [Finite External] {input : Caller ↪ List Bool} {operationEncoding : Operation ↪ List Bool} {stateEncoding : State ↪ List Bool} {handler : Caller → Operation × List Bool → State → WordOracleComp External (List Bool × State)} {prepare : Caller → ℕ × List Bool} {initial : Caller → State} {resources : Caller → List Bool → ℕ} (hprogram : IsOraclePPT output program) (hprepare : Turing.MultiTapeTM.ComputableTidilyInPolyTime prepare input (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits)) (hhandler : IsOraclePPTOn (Turing.MultiTapeTM.encPair input (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair operationEncoding Turing.MultiTapeTM.encBits) stateEncoding)) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits stateEncoding) fun (pair : Caller × (Operation × List Bool) × State) => handler pair.1 pair.2.1 pair.2.2) (hinitial : Turing.MultiTapeTM.ComputableTidilyInPolyTime initial input stateEncoding) (invariant : Caller → State → Prop) (hinit : ∀ (a : Caller), invariant a (initial a)) (hresources : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (pair : Caller × List Bool) => resources pair.1 pair.2) (Turing.MultiTapeTM.encPair input Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encUnary) (hpreserve : ∀ (a : Caller) (request : Operation × List Bool) (state : State), invariant a state → ∀ result ∈ ProbOracleComp.support (handler a request state), invariant a result.2 ∧ result.1.length ≤ resources a request.2 ∧ (stateEncoding result.2).length ≤ (stateEncoding state).length + resources a request.2) : IsOraclePPTOn input (Turing.MultiTapeTM.encPair output stateEncoding) fun (a : Caller) => (OracleComp.interpret (ProbOracleComp.handler (fun (n : ℕ) => StateT.lift (ProbOracleComp.sample (ProbComp.unifFin n))) (handler a)) (program (prepare a).1 (prepare a).2)).run (initial a)

Supply a stateful handler with its own external calls to a parameterized oracle program. The result retains the handler's final state and every external oracle's state, and a local invariant charges reply length and all added encoded storage.