Efficient stateful oracle substitution

A certified oracle program can be interpreted against a closed stateful PPT handler. A local invariant bounds reply length and the amount of encoded private storage added per call. The result is a closed PPT program returning both the original result and the final handler state. The proof charges the native interpreter, captured inputs, requests, replies and all stored data.

The machine, clock, finite configurations and query bounds remain internal. Individually efficient calls alone do not suffice: repeatedly doubling the state does not satisfy a resource allowance that depends only on the caller and request. The theorem is the closed case of open substitution (Cslib.Probability.IsOraclePPTOn.run_interpret_preprocess_open): a sampled closed handler makes no external call.

Main results

• Cslib.Probability.IsOraclePPTOn.run_interpret_preprocess: efficient substitution with captured caller data, a local state invariant and an efficiently computed resource allowance.

References

Adapts Computability/Probabilistic/OracleSimulation.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8, using the shared OracleComp.interpret interface.

theorem Cslib.Probability.IsOraclePPTOn.run_interpret_preprocess {Operation α β Caller State : Type} [DecidableEq Operation] [Finite Operation] {source : α ↪ List Bool} {input : Caller ↪ List Bool} {output : β ↪ List Bool} {stateEncoding : State ↪ List Bool} {program : α → WordOracleComp Operation β} {handler : Caller → Operation × List Bool → State → ProbComp (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 : 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))).run (initial a)

Substitute a stateful handler into an oracle program, preserving the joint output/state law. The efficiently computed allowance bounds each reply and the added encoded state. One invariant must hold on every supported transition; clocks and storage bounds are derived internally.