A certified open stateful oracle interpreter

The interpreter of Cslib.Probability.OracleSimulation retains finite machine storage and a handler's private state in one encoded value. Here the handler may itself draw private coins and call an external stateful oracle, so one interpreter step is an oracle program rather than a closed one. A local step uses the original transition table and a handler certified as strict oracle PPT. Each certificate charges captured input, requests, replies, the handler's state and retained configuration storage, for every external oracle and every external reply length.

Main definitions

• Cslib.Probability.OpenOracleSimulation.step: a native step with an open stateful handler.

Main results

• Cslib.Probability.OpenOracleSimulation.step_eq_run_interpret: the exact stateful step law.
• Cslib.Probability.OpenOracleSimulation.isOraclePPTOn_step: the single-step certificate.
• Cslib.Probability.OpenOracleSimulation.isOraclePPTOn_run: a bounded run with a state invariant is strict oracle PPT.

References

Adapts Computability/Probabilistic/Realization/OracleSimulation.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8 to handlers with external calls, using the compositional strict oracle PPT calculus.

noncomputable def Cslib.Probability.OpenOracleSimulation.step {k : ℕ} {Control Operation External α State : Type} [DecidableEq Operation] (machine : Turing.MultiTapePTM k Bool Control Operation) (handler : α → Operation × List Bool → State → WordOracleComp External (List Bool × State)) (a : α) (pair : Turing.MultiTapeMachine.FiniteConfig k Bool Control Operation × State) : WordOracleComp External (Turing.MultiTapeMachine.FiniteConfig k Bool Control Operation × State)

Execute one native step, retaining all machine storage and the handler's state. A query is answered by the handler, which may draw private coins and call the external oracle.

theorem Cslib.Probability.OpenOracleSimulation.step_eq_run_interpret {k : ℕ} {Control Operation External α State : Type} [DecidableEq Operation] (machine : Turing.MultiTapePTM k Bool Control Operation) (handler : α → Operation × List Bool → State → WordOracleComp External (List Bool × State)) (a : α) (pair : Turing.MultiTapeMachine.FiniteConfig k Bool Control Operation × State) : step machine handler a pair = (OracleComp.interpret (ProbOracleComp.handler (fun (n : ℕ) => StateT.lift (ProbOracleComp.sample (ProbComp.unifFin n))) (handler a)) (Turing.MultiTapeMachine.finiteStep machine (fun (choices : ReaderT Bool Id (Turing.MultiTapeMachine.Action k Bool Control Operation)) => choices <$> ProbOracleComp.sample (ProbComp.uniform Bool)) (fun (op : Operation) (word : List Bool) => ProbOracleComp.query (op, word)) pair.1)).run pair.2

One interpreted step retains the full finite configuration and the handler's final state. The equality is one of oracle programs, so it holds for every later external oracle.

theorem Cslib.Probability.OpenOracleSimulation.isOraclePPTOn_step {k : ℕ} {Control Operation External α State : Type} [DecidableEq Operation] [Finite Control] [DecidableEq External] [Finite External] [Fintype Operation] {input : α ↪ List Bool} {operationEncoding : Operation ↪ List Bool} {stateEncoding : State ↪ List Bool} (machine : Turing.MultiTapePTM k Bool Control Operation) {handler : α → Operation × List Bool → State → WordOracleComp External (List Bool × State)} (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 : α × (Operation × List Bool) × State) => handler pair.1 pair.2.1 pair.2.2) : IsOraclePPTOn (Turing.MultiTapeTM.encPair input (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encFiniteConfig stateEncoding)) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encFiniteConfig stateEncoding) fun (pair : α × Turing.MultiTapeMachine.FiniteConfig k Bool Control Operation × State) => step machine handler pair.1 pair.2

A handler certified as strict oracle PPT makes one complete interpreter step strict oracle PPT. Only the selected transition runs, so a non-query step makes no external call.

theorem Cslib.Probability.OpenOracleSimulation.isOraclePPTOn_run {k : ℕ} {Control Operation External α State : Type} [DecidableEq Operation] [Finite Control] [DecidableEq External] [Finite External] [Finite Operation] {input : α ↪ List Bool} {operationEncoding : Operation ↪ List Bool} {stateEncoding : State ↪ List Bool} (machine : Turing.MultiTapePTM k Bool Control Operation) {word : α → List Bool} {count : α → ℕ} {handler : α → Operation × List Bool → State → WordOracleComp External (List Bool × State)} {initial : α → State} (hword : Turing.MultiTapeTM.ComputableTidilyInPolyTime word input Turing.MultiTapeTM.encBits) (hcount : Turing.MultiTapeTM.ComputableTidilyInPolyTime count input Turing.MultiTapeTM.encUnary) (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 : α × (Operation × List Bool) × State) => handler pair.1 pair.2.1 pair.2.2) (hinitial : Turing.MultiTapeTM.ComputableTidilyInPolyTime initial input stateEncoding) (invariant : α → State → Prop) (hinit : ∀ (a : α), invariant a (initial a)) {resources : ℕ → ℕ} (hresources : PolynomiallyBounded resources) (hpreserve : ∀ (a : α) (request : Operation × List Bool) (state : State), invariant a state → ∀ result ∈ ProbOracleComp.support (handler a request state), invariant a result.2 ∧ result.1.length ≤ resources ((input a).length + request.2.length) ∧ (stateEncoding result.2).length ≤ (stateEncoding state).length + resources ((input a).length + request.2.length)) : IsOraclePPTOn input (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits stateEncoding) fun (a : α) => (OracleComp.interpret (ProbOracleComp.handler (fun (n : ℕ) => StateT.lift (ProbOracleComp.sample (ProbComp.unifFin n))) (handler a)) (machine.runOracle (count a) (word a))).run (initial a)

A bounded native run with an open stateful handler is strict oracle PPT. A local invariant, over every possible handler result under every external oracle, bounds reply length and private-state growth; the loop certificate charges all interpreter storage.