Probabilistic machines reading a buffered input

The common virtual-input compiler applies directly to Boolean-indexed choices, preserving the whole typed program, including stateful coin and query effects. Preparing the buffer is separate.

Main definitions

• Turing.MultiTapePTM.inputFromTape: read the input from a word and a boundary-marker tape.

Main results

• Turing.MultiTapePTM.runConfigFrom_inputFromTape: preserve the source configuration program.

References

Specializes MultiTape.Machine.InputFromTape, adapted from the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8 and upstream's deterministic input redirection.

@[reducible, inline]

abbrev Turing.MultiTapePTM.inputFromTape {k : ℕ} {Symbol State Oracle : Type} (machine : MultiTapePTM k Symbol State Oracle) : MultiTapePTM (k + 2) Symbol State Oracle

The common virtual-input compiler specialized to Boolean-indexed transitions.

theorem Turing.MultiTapePTM.runConfigFrom_inputFromTape {k : ℕ} {Symbol State Oracle Query : Type} {spec : Cslib.OracleSpec Query} {input : List Symbol} [DecidableEq Oracle] (machine : MultiTapePTM k Symbol State Oracle) (coin : Cslib.OracleComp spec Bool) (query : Oracle → List Symbol → Cslib.OracleComp spec (List Symbol)) (mark : Symbol) (fuel : ℕ) (cfg : MultiTapeMachine.Config k Symbol State Oracle input) (outerInput : List Symbol) (outerPosition : Fin (outerInput.length + 2)) : machine.inputFromTape.runConfigFrom coin query fuel (MultiTapeMachine.InputFromTape.config mark cfg outerInput outerPosition) = (fun (final : MultiTapeMachine.Config k Symbol State Oracle input) => MultiTapeMachine.InputFromTape.config mark final outerInput outerPosition) <$> machine.runConfigFrom coin query fuel cfg

Read a prepared virtual input, preserving the complete clocked program and oracle channels.