Simulating instructions by bounded blocks

A machine transformation can implement each source instruction with a fixed block of target instructions. The simulation preserves the joint distribution of machine configuration and private interpreter state. Its configuration embedding may change after each block, for example to track a clock head. Source and target may use different alphabets, tapes, channels and choices; their programs use the same typed effect interface.

The one-block hypothesis includes halted configurations, so padding a halted source is simulated correctly. The source need not halt before its external clock expires.

Main results

• Turing.MultiTapeMachine.runConfigFrom_map: one-instruction simulation preserves the entire typed program, before interpretation.
• Turing.MultiTapeMachine.runConfigFrom_mapState: commuting transition tables preserve clocked execution under a possibly noninjective control-state relabelling.
• Turing.MultiTapeMachine.run_interpret_runConfigFrom_mul_indexed: bounded block simulation with a changing configuration embedding.
• Turing.MultiTapeMachine.run_interpret_runConfigFrom_mul: the fixed-embedding specialization.

References

Adapted from MultiTape/Oracle/Simulation.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8 to the common machine and typed program interface.

theorem Turing.MultiTapeMachine.runConfigFrom_map {k k' : ℕ} {Symbol Symbol' State State' Oracle Oracle' : Type} {Query : Type u} {spec : Cslib.OracleSpec Query} {Choose : Type → Type v} {Choose' : Type → Type w} {input : List Symbol} {input' : List Symbol'} [DecidableEq Oracle] [DecidableEq Oracle'] (source : MultiTapeMachine k Symbol State Oracle Choose) (target : MultiTapeMachine k' Symbol' State' Oracle' Choose') (choose : Choose (Action k Symbol State Oracle) → Cslib.OracleComp spec (Action k Symbol State Oracle)) (choose' : Choose' (Action k' Symbol' State' Oracle') → Cslib.OracleComp spec (Action k' Symbol' State' Oracle')) (query : Oracle → List Symbol → Cslib.OracleComp spec (List Symbol)) (query' : Oracle' → List Symbol' → Cslib.OracleComp spec (List Symbol')) (embed : Config k Symbol State Oracle input → Config k' Symbol' State' Oracle' input') (hstep : ∀ (cfg : Config k Symbol State Oracle input), target.runConfigFrom choose' query' 1 (embed cfg) = embed <$> source.runConfigFrom choose query 1 cfg) (fuel : ℕ) (cfg : Config k Symbol State Oracle input) : target.runConfigFrom choose' query' fuel (embed cfg) = embed <$> source.runConfigFrom choose query fuel cfg

A one-instruction program simulation preserves every clocked run. The hypothesis includes halted configurations, and the embedding may change the tape alphabet and input word.

theorem Turing.MultiTapeMachine.runConfigFrom_mapState {k : ℕ} {Symbol State State' Oracle : Type} {Query : Type u} {spec : Cslib.OracleSpec Query} {Choose : Type → Type v} {input : List Symbol} [DecidableEq Oracle] [Functor Choose] (source : MultiTapeMachine k Symbol State Oracle Choose) (target : MultiTapeMachine k Symbol State' Oracle Choose) (choose : {α : Type} → Choose α → Cslib.OracleComp spec α) (hchoose : ∀ {α β : Type} (f : α → β) (choices : Choose α), choose (f <$> choices) = f <$> choose choices) (query : Oracle → List Symbol → Cslib.OracleComp spec (List Symbol)) (f : State → State') (htr : ∀ (state : State) (inp : Option Symbol) (work : Fin k → Option Symbol) (answer : Oracle → Option Symbol), target.tr (f state) inp work answer = Action.mapState f <$> source.tr state inp work answer) (fuel : ℕ) (cfg : Config k Symbol State Oracle input) : target.runConfigFrom choose query fuel (Config.mapState f cfg) = Config.mapState f <$> source.runConfigFrom choose query fuel cfg

Relabelling control preserves the full clocked program when transition tables commute. The map need not be injective: the table equation must hold at every source state, including states identified by the map. Halting is preserved, and the fuel and query handler are unchanged.

theorem Turing.MultiTapeMachine.run_interpret_runConfigFrom_mul_indexed {k k' : ℕ} {Symbol Symbol' State State' Oracle Oracle' OracleState : Type} {Query : Type u} {spec : Cslib.OracleSpec Query} {Choose : Type → Type v} {Choose' : Type → Type w} {input : List Symbol} {input' : List Symbol'} [DecidableEq Oracle] [DecidableEq Oracle'] (source : MultiTapeMachine k Symbol State Oracle Choose) (target : MultiTapeMachine k' Symbol' State' Oracle' Choose') (choose : Choose (Action k Symbol State Oracle) → Cslib.OracleComp spec (Action k Symbol State Oracle)) (choose' : Choose' (Action k' Symbol' State' Oracle') → Cslib.OracleComp spec (Action k' Symbol' State' Oracle')) (query : Oracle → List Symbol → Cslib.OracleComp spec (List Symbol)) (query' : Oracle' → List Symbol' → Cslib.OracleComp spec (List Symbol')) (delay fuel : ℕ) (embed : ℕ → Config k Symbol State Oracle input → Config k' Symbol' State' Oracle' input') (oracle : (q : Query) → StateT OracleState PMF (spec q)) (hstep : ∀ i < fuel, ∀ (cfg : Config k Symbol State Oracle input) (s : OracleState), (Cslib.OracleComp.interpret oracle (target.runConfigFrom choose' query' delay (embed i cfg))).run s = PMF.map (fun (x : Config k Symbol State Oracle input × OracleState) => match x with | (final, s') => (embed (i + 1) final, s')) ((Cslib.OracleComp.interpret oracle (source.runConfigFrom choose query 1 cfg)).run s)) (cfg : Config k Symbol State Oracle input) (s : OracleState) : (Cslib.OracleComp.interpret oracle (target.runConfigFrom choose' query' (delay * fuel) (embed 0 cfg))).run s = PMF.map (fun (x : Config k Symbol State Oracle input × OracleState) => match x with | (final, s') => (embed fuel final, s')) ((Cslib.OracleComp.interpret oracle (source.runConfigFrom choose query fuel cfg)).run s)

A bounded simulation may update its embedding after each source instruction. All private interpreter state is retained, including state shared by coin and oracle programs.

theorem Turing.MultiTapeMachine.run_interpret_runConfigFrom_mul {k k' : ℕ} {Symbol Symbol' State State' Oracle Oracle' OracleState : Type} {Query : Type u} {spec : Cslib.OracleSpec Query} {Choose : Type → Type v} {Choose' : Type → Type w} {input : List Symbol} {input' : List Symbol'} [DecidableEq Oracle] [DecidableEq Oracle'] (source : MultiTapeMachine k Symbol State Oracle Choose) (target : MultiTapeMachine k' Symbol' State' Oracle' Choose') (choose : Choose (Action k Symbol State Oracle) → Cslib.OracleComp spec (Action k Symbol State Oracle)) (choose' : Choose' (Action k' Symbol' State' Oracle') → Cslib.OracleComp spec (Action k' Symbol' State' Oracle')) (query : Oracle → List Symbol → Cslib.OracleComp spec (List Symbol)) (query' : Oracle' → List Symbol' → Cslib.OracleComp spec (List Symbol')) (embed : Config k Symbol State Oracle input → Config k' Symbol' State' Oracle' input') (delay : ℕ) (oracle : (q : Query) → StateT OracleState PMF (spec q)) (hstep : ∀ (cfg : Config k Symbol State Oracle input) (s : OracleState), (Cslib.OracleComp.interpret oracle (target.runConfigFrom choose' query' delay (embed cfg))).run s = PMF.map (fun (x : Config k Symbol State Oracle input × OracleState) => match x with | (final, s') => (embed final, s')) ((Cslib.OracleComp.interpret oracle (source.runConfigFrom choose query 1 cfg)).run s)) (fuel : ℕ) (cfg : Config k Symbol State Oracle input) (s : OracleState) : (Cslib.OracleComp.interpret oracle (target.runConfigFrom choose' query' (delay * fuel) (embed cfg))).run s = PMF.map (fun (x : Config k Symbol State Oracle input × OracleState) => match x with | (final, s') => (embed final, s')) ((Cslib.OracleComp.interpret oracle (source.runConfigFrom choose query fuel cfg)).run s)

Simulating one instruction by a block of delay instructions preserves every bounded run.