Documentation

Complexity.Computability.Probabilistic.Realization.OracleSimulation

A certified stateful oracle interpreter #

The interpreter retains finite machine storage and the handler's state in one encoded value. A local step uses the original transition table and a certified closed handler. Each certificate charges captured input, requests, replies, state and retained configuration storage. The certificates specialize those of the open interpreter Cslib.Probability.OpenOracleSimulation to a sampled closed handler without external channels.

Main definitions #

Main results #

References #

Adapts Computability/Probabilistic/Realization/OracleSimulation.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8 to the shared interpreter and tidy calculus.

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

Execute one native step, retaining all machine storage and the handler's state.

Instances For
    source
    theorem Cslib.Probability.OracleSimulation.step_eq_run_interpret {k : ℕ} {Control Operation α State : Type} [DecidableEq Operation] (machine : Turing.MultiTapePTM k Bool Control Operation) (handler : α → Operation × List Bool → State → ProbComp (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 (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 final handler state.

    source
    theorem Cslib.Probability.OracleSimulation.sample_step {k : ℕ} {Control Operation α State : Type} [DecidableEq Operation] {External : Type} (machine : Turing.MultiTapePTM k Bool Control Operation) (handler : α → Operation × List Bool → State → ProbComp (List Bool × State)) (a : α) (pair : Turing.MultiTapeMachine.FiniteConfig k Bool Control Operation × State) :
    ProbOracleComp.sample (step machine handler a pair) = OpenOracleSimulation.step machine (fun (a : α) (request : Operation × List Bool) (state : State) => ProbOracleComp.sample (handler a request state)) a pair

    A sampled step is the open interpreter's step with the sampled handler.

    source
    theorem Cslib.Probability.OracleSimulation.isPPTOn_step {k : ℕ} {Control Operation α State : Type} [DecidableEq Operation] [Finite Control] [Fintype Operation] {input : α ↪ List Bool} {stateEncoding : State ↪ List Bool} (machine : Turing.MultiTapePTM k Bool Control Operation) {handler : α → Operation × List Bool → State → ProbComp (List Bool × State)} (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 : α × (Operation × List Bool) × State) => handler pair.1 pair.2.1 pair.2.2) :
    IsPPTOn (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 certified stateful handler makes one complete interpreter step PPT.

    source
    theorem Cslib.Probability.OracleSimulation.isPPTOn_run {k : ℕ} {Control Operation α State : Type} [DecidableEq Operation] [Finite Control] [Finite Operation] {input : α ↪ List Bool} {stateEncoding : State ↪ List Bool} (machine : Turing.MultiTapePTM k Bool Control Operation) {word : α → List Bool} {count : α → ℕ} {handler : α → Operation × List Bool → State → ProbComp (List Bool × State)} {initial : α → State} (hword : Turing.MultiTapeTM.ComputableTidilyInPolyTime word input Turing.MultiTapeTM.encBits) (hcount : Turing.MultiTapeTM.ComputableTidilyInPolyTime count input Turing.MultiTapeTM.encUnary) (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 : α × (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 ∈ (handler a request state).eval.support, 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)) :
    IsPPTOn input (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits stateEncoding) fun (a : α) => (OracleComp.interpret (ProbOracleComp.handler (fun (n : ℕ) => StateT.lift (ProbComp.unifFin n)) (handler a)) (machine.runOracle (count a) (word a))).run (initial a)

    A bounded native run with a stateful PPT handler is PPT. A local invariant bounds reply length and private-state growth; the loop certificate charges all interpreter storage.