External query bounds from the machine clock

Each instruction makes at most one external request and writes at most one symbol per query buffer. Starting from empty channels, a run of fuel instructions therefore makes at most fuel external calls, each with a request length at most fuel. Private coins are sampled independently and do not count as external requests. The bound permits arbitrarily long replies and arbitrary state shared by the external handlers.

Moreover, because each channel's answer head starts at position 0 on query reception and moves by at most one cell per instruction, a fuel-step run from initialConfig never inspects reply indices at or beyond fuel. Replacing every reply by reply.take fuel in finiteRunFrom therefore yields the exact same OracleComp program as machine.run.

Main results

• Turing.MultiTapePTM.query_bounds_runFrom: bounds from a partial run and its initial buffers.
• Turing.MultiTapePTM.query_bounds_runOracle: the clock bounds calls and request lengths.
• Turing.MultiTapePTM.finiteRunFrom_take_init: truncating replies to the clock preserves the exact typed program.

References

Adapted from Computability/Machines/Turing/MultiTape/Oracle/QueryBounds.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8, using the common machine.

theorem Turing.MultiTapePTM.query_bounds_runFrom {k : ℕ} {Symbol Control Operation Query State : Type} [DecidableEq Operation] {input : List Symbol} (machine : MultiTapePTM k Symbol Control Operation) (request : Operation → List Symbol → Query) (size : Query → ℕ) (hrequest : ∀ (op : Operation) (word : List Symbol), size (request op word) ≤ word.length) (oracle : Query → StateT State PMF (List Symbol)) (fuel : ℕ) (cfg : MultiTapeMachine.Config k Symbol Control Operation input) (bound : ℕ) (hbuffers : ∀ (op : Operation), (cfg.channels op).queryBuffer.length ≤ bound) (s s' : State) (transcript transcript' : Cslib.OracleComp.Transcript fun (x : Query) => List Symbol) (output : List Symbol) (htranscript : ∀ entry ∈ transcript, size entry.fst ≤ bound) (h : (output, s', transcript') ∈ ((Cslib.OracleComp.interpret (Cslib.ProbOracleComp.handler (fun (n : ℕ) => StateT.lift (Cslib.ProbComp.unifOracle n)) (Cslib.OracleComp.withTranscript oracle)) (machine.runFrom (Cslib.ProbOracleComp.sample (Cslib.ProbComp.uniform Bool)) (fun (op : Operation) (word : List Symbol) => Cslib.ProbOracleComp.query (request op word)) fuel cfg)).run (s, transcript)).support) : List.length transcript' ≤ List.length transcript + fuel ∧ ∀ entry ∈ transcript', size entry.fst ≤ bound + fuel

A partial run adds at most one external call per instruction. Requests fit within the initial buffer bound plus elapsed time, regardless of the oracle's reply sizes.

theorem Turing.MultiTapePTM.query_bounds_runOracle {k : ℕ} {Symbol Control Operation : Type} [DecidableEq Operation] (machine : MultiTapePTM k Symbol Control Operation) (fuel : ℕ) (input : List Symbol) : (machine.runOracle fuel input).IsQueryBounded fuel ∧ Cslib.ProbOracleComp.QueriesSatisfy (fun (request : Operation × List Symbol) => request.2.length ≤ fuel) (machine.runOracle fuel input)

From blank channels, the same clock bounds external calls and every request length.

structure Turing.MultiTapeMachine.FiniteConfig.RepresentsTake {k : ℕ} {Symbol Control Operation : Type} (limit : ℕ) (finite : FiniteConfig k Symbol Control Operation) (cfg : Config k Symbol Control Operation finite.tapes.input) : Prop

Agreement with a native configuration up to truncating each channel's reply to limit symbols.

• tapes : finite.tapes.Represents cfg.tapes

  Ordinary configurations correspond.

• queries (op : Operation) : (finite.channels op).1 = (cfg.channels op).queryBuffer

  Pending requests agree.

• answers (op : Operation) : (finite.channels op).2.Represents (fun (position : ℤ) => if 0 ≤ position then (List.take limit (cfg.channels op).answer)[position.toNat]? else none) (cfg.channels op).answerPos

  Answer tapes agree with the limit-prefix of each channel's reply.

theorem Turing.MultiTapeMachine.FiniteConfig.representsTake_init {k : ℕ} {Symbol Control Operation : Type} (limit : ℕ) (state : Control) (input : List Symbol) : RepresentsTake limit (init state input) { tapes := Cfg.init state input }

Initial finite storage represents the native initial configuration at any reply truncation limit.

theorem Turing.MultiTapeMachine.FiniteConfig.RepresentsTake.answerSymbols {k : ℕ} {Symbol Control Operation : Type} {limit : ℕ} {finite : FiniteConfig k Symbol Control Operation} {cfg : Config k Symbol Control Operation finite.tapes.input} (h : RepresentsTake limit finite cfg) (hpos : ∀ (op : Operation), (cfg.channels op).answerPos < ↑limit) : finite.answerSymbols = cfg.answerSymbols

When every answer head lies strictly before limit, the truncated finite configuration sees the exact same answer symbols as the native configuration.

theorem Turing.MultiTapeMachine.FiniteConfig.RepresentsTake.step {k : ℕ} {Symbol Control Operation : Type} {limit : ℕ} {finite : FiniteConfig k Symbol Control Operation} {cfg : Config k Symbol Control Operation finite.tapes.input} (h : RepresentsTake limit finite cfg) (action : Turing.Action k Symbol Control) (symbol : Operation → Option Symbol) (move : Operation → SignType) : RepresentsTake limit (finite.step action symbol move) (cfg.step action symbol move)

An ordinary transition preserves truncated representation.

theorem Turing.MultiTapeMachine.FiniteConfig.RepresentsTake.receive {k : ℕ} {Symbol Control Operation : Type} [DecidableEq Operation] {limit : ℕ} {finite : FiniteConfig k Symbol Control Operation} {cfg : Config k Symbol Control Operation finite.tapes.input} (h : RepresentsTake limit finite cfg) (op : Operation) (next : Control) (answer : List Symbol) : RepresentsTake limit (finite.receive op next (List.take limit answer)) (cfg.receive op next answer)

Installing a truncated reply in finite storage represents installing the full reply in native storage.

theorem Turing.MultiTapePTM.finiteRunFrom_take_eq {k : ℕ} {Symbol Control Operation Query : Type} [DecidableEq Operation] {spec : Cslib.OracleSpec Query} (machine : MultiTapePTM k Symbol Control Operation) (coin : Cslib.OracleComp spec Bool) (query : Operation → List Symbol → Cslib.OracleComp spec (List Symbol)) (fuel limit : ℕ) (finite : MultiTapeMachine.FiniteConfig k Symbol Control Operation) (cfg : MultiTapeMachine.Config k Symbol Control Operation finite.tapes.input) (h : MultiTapeMachine.FiniteConfig.RepresentsTake limit finite cfg) (hfuel : fuel ≤ limit) (hpos : ∀ (op : Operation), (cfg.channels op).answerPos + ↑fuel ≤ ↑limit) : MultiTapeMachine.finiteRunFrom machine (fun (choices : ReaderT Bool Id (MultiTapeMachine.Action k Symbol Control Operation)) => choices <$> coin) (fun (op : Operation) (word : List Symbol) => List.take limit <$> query op word) fuel finite = machine.runFrom coin query fuel cfg

Truncating every reply to limit symbols in finiteRunFrom produces the exact same typed program as runFrom whenever the remaining fuel keeps every answer head below limit.

theorem Turing.MultiTapePTM.finiteRunFrom_take_init {k : ℕ} {Symbol Control Operation Query : Type} [DecidableEq Operation] {spec : Cslib.OracleSpec Query} (machine : MultiTapePTM k Symbol Control Operation) (coin : Cslib.OracleComp spec Bool) (query : Operation → List Symbol → Cslib.OracleComp spec (List Symbol)) (fuel : ℕ) (input : List Symbol) : MultiTapeMachine.finiteRunFrom machine (fun (choices : ReaderT Bool Id (MultiTapeMachine.Action k Symbol Control Operation)) => choices <$> coin) (fun (op : Operation) (word : List Symbol) => List.take fuel <$> query op word) fuel (MultiTapeMachine.FiniteConfig.init machine.initial input) = machine.run coin query fuel input

Over fuel steps from blank initial storage, truncating every oracle reply to fuel symbols preserves the exact typed OracleComp program.

theorem Turing.MultiTapePTM.finiteRunFrom_take_runOracle {k : ℕ} {Symbol Control Operation : Type} [DecidableEq Operation] (machine : MultiTapePTM k Symbol Control Operation) (fuel : ℕ) (input : List Symbol) : MultiTapeMachine.finiteRunFrom machine (fun (choices : ReaderT Bool Id (MultiTapeMachine.Action k Symbol Control Operation)) => choices <$> Cslib.ProbOracleComp.sample (Cslib.ProbComp.uniform Bool)) (fun (op : Operation) (word : List Symbol) => List.take fuel <$> Cslib.ProbOracleComp.query (op, word)) fuel (MultiTapeMachine.FiniteConfig.init machine.initial input) = machine.runOracle fuel input

Specializing finiteRunFrom_take_init to runOracle: truncating every external reply to fuel symbols preserves the exact ProbOracleComp program.