Fair-bit and bounded-prefix oracle query machines

coinMachine emits a single fair bit in one step. queryTakePTM op realizes the primitive bounded-prefix oracle call on an encoded pair encPair encBits encUnary (q, limit): it unframes q into channel op's query buffer, submits the query once, copies at most limit reply bits while scanning the unary limit, and rewinds the input head.

Main definitions

• Turing.MultiTapePTM.coinMachine: one-step fair-bit emitter.
• Turing.MultiTapePTM.queryTakePTM: tidy machine for List.take limit <$> query (op, q).

Main results

• Turing.MultiTapePTM.computesTidily_coinMachine: tidy specification of coinMachine.
• Turing.MultiTapePTM.computesTidily_queryTakePTM: tidy specification of queryTakePTM.

References

Adapts the probabilistic oracle machines of the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8 to the tidy-machine conventions of crei:crei/tidy-universal @7f7c0696.

Fair-bit machine

def Turing.MultiTapePTM.coinMachine {Operation : Type} : MultiTapePTM 0 Bool Unit Operation

One-state machine that emits a single fair bit and halts without moving any head.

theorem Turing.MultiTapePTM.computesTidily_coinMachine {Operation : Type} [DecidableEq Operation] (x : List Bool) : coinMachine.ComputesTidily x 1 (⇑MultiTapeTM.encBool <$> Cslib.ProbOracleComp.sample (Cslib.ProbComp.uniform Bool))

coinMachine tidily computes encBool <$> sample (uniform Bool) in 1 step.

Bounded-prefix query machine

inductive Turing.MultiTapePTM.QueryTakeState : Type

Control states of queryTakeCore: read frame marker, read framed query bit, submit query, and copy reply bits while scanning the unary limit.

• marker : QueryTakeState
• bit : QueryTakeState
• submit : QueryTakeState
• copyReply : QueryTakeState

@[instance_reducible]

instance Turing.MultiTapePTM.instDecidableEqQueryTakeState : DecidableEq QueryTakeState

instance Turing.MultiTapePTM.instFiniteQueryTakeState : Finite QueryTakeState

def Turing.MultiTapePTM.queryTakeCore {Operation : Type} [DecidableEq Operation] (op : Operation) : MultiTapePTM 0 Bool QueryTakeState Operation

Unframe the query word from the input into channel op, submit the query, and copy at most limit reply bits while scanning the unary suffix.

noncomputable def Turing.MultiTapePTM.queryTakePTM {Operation : Type} [DecidableEq Operation] (op : Operation) : MultiTapePTM 0 Bool (QueryTakeState ⊕ MultiTapeTM.RewindState) Operation

Run queryTakeCore op and then rewind the input head to position 1.

def Turing.MultiTapePTM.QueryTakeCore.config {Operation : Type} (x : List Bool) (state : Option QueryTakeState) (idx : ℕ) (hidx : idx ≤ x.length) (out : List Bool) (ch : Operation → MultiTapeMachine.Channel Bool) : MultiTapeMachine.Config 0 Bool QueryTakeState Operation x

Configuration of queryTakeCore at 0-based input index idx ≤ x.length.

theorem Turing.MultiTapePTM.QueryTakeCore.run_copyReply {Operation OracleState : Type} [DecidableEq Operation] (op : Operation) (x : List Bool) (oracle : Operation × List Bool → StateT OracleState PMF (List Bool)) (remLimit : ℕ) (pre : List Bool) (h : x = pre ++ List.replicate remLimit true) (pos : ℕ) (answer out : List Bool) (ch : Operation → MultiTapeMachine.Channel Bool) (_hch : ch op = { answer := answer, answerPos := ↑pos }) (s : OracleState) : (Cslib.OracleComp.interpret (Cslib.ProbOracleComp.handler (fun (n : ℕ) => StateT.lift (Cslib.ProbComp.unifOracle n)) oracle) ((queryTakeCore op).runOracleConfigFrom (remLimit + 1) (config x (some QueryTakeState.copyReply) pre.length ⋯ out ch))).run s = PMF.pure (config x none x.length ⋯ (out ++ List.take remLimit (List.drop pos answer)) (Function.update ch op { answer := answer, answerPos := ↑pos + ↑remLimit }), s)

Scanning List.replicate remLimit true in state .copyReply appends (answer.drop pos).take remLimit to out and halts at the right boundary in remLimit + 1 steps.

theorem Turing.MultiTapePTM.QueryTakeCore.run_frame {Operation OracleState : Type} [DecidableEq Operation] (op : Operation) (x : List Bool) (oracle : Operation × List Bool → StateT OracleState PMF (List Bool)) (rem pre suf : List Bool) (h : x = pre ++ MultiTapeTM.frame rem ++ suf) (out : List Bool) (ch : Operation → MultiTapeMachine.Channel Bool) (s : OracleState) : (Cslib.OracleComp.interpret (Cslib.ProbOracleComp.handler (fun (n : ℕ) => StateT.lift (Cslib.ProbComp.unifOracle n)) oracle) ((queryTakeCore op).runOracleConfigFrom (2 * rem.length + 2) (config x (some QueryTakeState.marker) pre.length ⋯ out ch))).run s = PMF.map (fun (x_1 : List Bool × OracleState) => match x_1 with | (answer, s') => (config x (some QueryTakeState.copyReply) (pre.length + (MultiTapeTM.frame rem).length) ⋯ out (Function.update ch op { answer := answer }), s')) (oracle (op, (ch op).queryBuffer ++ rem) s)

Scanning frame rem in state .marker appends rem to channel op's query buffer and submits the accumulated query in 2 * rem.length + 2 steps, entering .copyReply.

theorem Turing.MultiTapePTM.computesTidily_queryTakePTM {Operation : Type} [DecidableEq Operation] (op : Operation) (q : List Bool) (limit : ℕ) : (queryTakePTM op).ComputesTidily ((MultiTapeTM.encPair MultiTapeTM.encBits MultiTapeTM.encUnary) (q, limit)) (4 * q.length + 2 * limit + 6) (List.take limit <$> Cslib.ProbOracleComp.query (op, q))

queryTakePTM op tidily computes List.take limit <$> query (op, q) on encPair encBits encUnary (q, limit) in 4 * q.length + 2 * limit + 6 steps.