Open stateful oracle substitution

A certified oracle program can be interpreted against a stateful handler that is itself a certified oracle program: the handler may draw private coins and call an arbitrary external stateful oracle, whose replies may be arbitrarily long. The result is again strict oracle PPT, returning the original result and the handler's final state, and it preserves the complete joint law of the result, the handler's state and the external oracle's state.

A local invariant and an efficiently computed additive allowance bound each reply given to the program and the encoded private storage added per call. Individually efficient calls alone do not suffice: repeatedly doubling the handler's state is efficient per call but not overall. Closed substitution (Cslib.Probability.IsOraclePPTOn.run_interpret_preprocess) is the special case of a sampled closed handler without external channels.

Main results

• Cslib.Probability.IsOraclePPTOn.run_interpret_preprocess_open: open substitution with captured caller data, a local state invariant and an efficiently computed resource allowance.
• Cslib.Probability.IsOraclePPTOn.interpret_bitQueries: replace each deterministic word query by a polynomial-time transformed request, keeping only one answer bit.

References

Extends Computability/Probabilistic/OracleSimulation.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8 from closed to open handlers.

theorem Cslib.Probability.IsOraclePPTOn.run_interpret_preprocess_open {Operation External α β Caller State : Type} [DecidableEq Operation] [DecidableEq External] [Finite External] {source : α ↪ List Bool} {input : Caller ↪ List Bool} {output : β ↪ List Bool} {operationEncoding : Operation ↪ List Bool} {stateEncoding : State ↪ List Bool} {program : α → WordOracleComp Operation β} {handler : Caller → Operation × List Bool → State → WordOracleComp External (List Bool × State)} {prepare : Caller → α} {initial : Caller → State} {resources : Caller → List Bool → ℕ} (hprogram : IsOraclePPTOn source output program) (hprepare : Turing.MultiTapeTM.ComputableTidilyInPolyTime prepare input source) (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))).run (initial a)

Substitute a stateful handler with its own external calls into an oracle program. The substituted program is strict oracle PPT and preserves the joint law of the result, the handler's final state and every external oracle's state. The efficiently computed allowance bounds each reply and the added encoded state; one invariant must hold for every possible handler result under every external oracle. External replies to the handler need no length bound.

theorem Cslib.Probability.IsOraclePPTOn.interpret_bitQueries {α β : Type} {input : α ↪ List Bool} {output : β ↪ List Bool} {program : α → OracleComp (fun (x : Unit × List Bool) => List Bool) β} {request : List Bool → List Bool} (hprogram : IsOraclePPTOn input output fun (a : α) => OracleComp.interpret ProbOracleComp.query (program a)) (hrequest : Turing.MultiTapeTM.ComputableTidilyInPolyTime request Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) : IsOraclePPTOn input output fun (a : α) => OracleComp.interpret ProbOracleComp.query (OracleComp.interpret (fun (q : Unit × List Bool) => List.take 1 <$> OracleComp.query ((), request q.2)) (program a))

Replacing every request by a polynomial-time computed word and reading at most one reply bit preserves strict oracle polynomial time. The certificate holds uniformly for every external stateful oracle, including oracles with arbitrarily long answers.