Fixed-program sparse RAM dispatch

The dispatch machine copies the canonical PC, walks a fixed decrementing branch tree, and runs the selected instruction with a uniform next-store work buffer. This surface currently exposes its structural transducer and coarse all-prefix space certificates; semantic selection is proved in the internal execution layer.

theorem Complexity.RAM.RegisterStore.Machine.selectedInstruction_eq_getElem?_getD (program : Program) (selector : ℕ) : selectedInstruction program selector = program[selector]?.getD Instr.halt

Pure branch-tree selection agrees with list lookup and the RAM model's out-of-range halt convention.

theorem Complexity.RAM.RegisterStore.Machine.dispatchProgramTM_hoareTime_of_execute {n : ℕ} (tapes : ControlInstructionTapes n) (program : Program) (store : Store) (pcValue selector : ℕ) (cleanWork work₀ : Fin (n + 1) → Tape) (inp₀ out₀ : Tape) (hready : DispatchReady tapes store pcValue selector cleanWork work₀) (hinput : TM.Parked inp₀) (houtput : TM.Parked out₀) (hexecute : ∀ (instruction : Instr), (executeInstructionTM tapes instruction).HoareTime (fun (inp : Tape) (work : Fin (n + 1) → Tape) (out : Tape) => inp = inp₀ ∧ work = cleanWork ∧ out = out₀) (fun (inp : Tape) (work : Fin (n + 1) → Tape) (out : Tape) => inp = inp₀ ∧ InstructionExecutionResult tapes instruction pcValue store work ∧ out = out₀) (executeInstructionTime tapes instruction pcValue store)) : (dispatchProgramTM tapes program).HoareTime (fun (inp : Tape) (work : Fin (n + 1) → Tape) (out : Tape) => inp = inp₀ ∧ work = work₀ ∧ out = out₀) (fun (inp : Tape) (work : Fin (n + 1) → Tape) (out : Tape) => inp = inp₀ ∧ InstructionExecutionResult tapes (selectedInstruction program selector) pcValue store work ∧ out = out₀) (dispatchProgramTime tapes store pcValue program selector)

Public generic correctness rule for the finite decrementing dispatch tree.

theorem Complexity.RAM.RegisterStore.Machine.executeInstructionTM_hoareTime_frame {n : ℕ} (tapes : ControlInstructionTapes n) (instruction : Instr) (store : Store) (pcValue : ℕ) (initialWork : Fin (n + 1) → Tape) (inp₀ : Tape) (hready : InstructionExecutionReady tapes store pcValue initialWork) (hinput : TM.Parked inp₀) : (executeInstructionTM tapes instruction).HoareTime (fun (inp : Tape) (work : Fin (n + 1) → Tape) (out : Tape) => inp = inp₀ ∧ work = initialWork ∧ out = (Tape.init []).move Dir3.right) (fun (inp : Tape) (work : Fin (n + 1) → Tape) (out : Tape) => inp = inp₀ ∧ InstructionExecutionResult tapes instruction pcValue store work ∧ out = (Tape.init []).move Dir3.right) (executeInstructionTime tapes instruction pcValue store)

Every statically selected RAM instruction realizes the common buffered snapshot-step contract.

theorem Complexity.RAM.RegisterStore.Machine.programInstructionTM_hoareTime_frame {n : ℕ} (tapes : ControlInstructionTapes n) (program : Program) (store : Store) (pcValue : ℕ) (initialWork : Fin (n + 1) → Tape) (inp₀ : Tape) (hready : InstructionExecutionReady tapes store pcValue initialWork) (hinput : TM.Parked inp₀) : (programInstructionTM tapes program).HoareTime (fun (inp : Tape) (work : Fin (n + 1) → Tape) (out : Tape) => inp = inp₀ ∧ work = initialWork ∧ out = (Tape.init []).move Dir3.right) (fun (inp : Tape) (work : Fin (n + 1) → Tape) (out : Tape) => inp = inp₀ ∧ InstructionExecutionResult tapes (selectedInstruction program pcValue) pcValue store work ∧ out = (Tape.init []).move Dir3.right) (programInstructionTime tapes program pcValue store)

Copy the canonical PC into dispatch scratch, select the fixed program instruction, and realize one exact sparse snapshot step.

theorem Complexity.RAM.RegisterStore.Machine.instructionCleanupTM_hoareTime_frame {n : ℕ} (tapes : ControlInstructionTapes n) (instruction : Instr) (pcValue : ℕ) (store : Store) (sourceHeadBound : ℕ) (initialWork : Fin (n + 1) → Tape) (inp₀ out₀ : Tape) (hready : InstructionCleanupReady tapes instruction pcValue store sourceHeadBound initialWork) (hinput : TM.Parked inp₀) (houtput : TM.Parked out₀) : (instructionCleanupTM tapes).HoareTime (fun (inp : Tape) (work : Fin (n + 1) → Tape) (out : Tape) => inp = inp₀ ∧ work = initialWork ∧ out = out₀) (fun (inp : Tape) (work : Fin (n + 1) → Tape) (out : Tape) => inp = inp₀ ∧ InstructionExecutionReady tapes (instructionStore instruction pcValue store) (instructionPC instruction pcValue store) work ∧ out = out₀) (instructionCleanupTime tapes instruction pcValue store sourceHeadBound)

Restore the clean instruction ABI after a buffered instruction result.

theorem Complexity.RAM.RegisterStore.Machine.programStepTM_hoareTime_frame {n : ℕ} (tapes : ControlInstructionTapes n) (program : Program) (store : Store) (pcValue : ℕ) (initialWork : Fin (n + 1) → Tape) (inp₀ : Tape) (hready : InstructionExecutionReady tapes store pcValue initialWork) (hinput : TM.Parked inp₀) : (programStepTM tapes program).HoareTime (fun (inp : Tape) (work : Fin (n + 1) → Tape) (out : Tape) => inp = inp₀ ∧ work = initialWork ∧ out = (Tape.init []).move Dir3.right) (fun (inp : Tape) (work : Fin (n + 1) → Tape) (out : Tape) => have next := Snapshot.step program { pc := pcValue, store := store }; inp = inp₀ ∧ InstructionExecutionReady tapes next.store next.pc work ∧ out = (Tape.init []).move Dir3.right) (programStepTime tapes program pcValue store)

One fixed-program RAM step returns directly to the reusable clean ABI for the exact successor sparse snapshot.

theorem Complexity.RAM.RegisterStore.Machine.finishControlInstructionTM_isTransducer {n : ℕ} (tapes : ControlInstructionTapes n) (control : TM (n + 1)) (hcontrol : control.IsTransducer) : (finishControlInstructionTM tapes control).IsTransducer

Control execution followed by unchanged-store copying is append-only on the real output tape.

theorem Complexity.RAM.RegisterStore.Machine.executeInstructionTM_isTransducer {n : ℕ} (tapes : ControlInstructionTapes n) (instruction : Instr) : (executeInstructionTM tapes instruction).IsTransducer

Every statically selected RAM instruction is append-only on real output.

theorem Complexity.RAM.RegisterStore.Machine.dispatchProgramTM_isTransducer {n : ℕ} (tapes : ControlInstructionTapes n) (program : Program) : (dispatchProgramTM tapes program).IsTransducer

Every node of the fixed finite dispatch tree preserves one-way output.

theorem Complexity.RAM.RegisterStore.Machine.programInstructionTM_isTransducer {n : ℕ} (tapes : ControlInstructionTapes n) (program : Program) : (programInstructionTM tapes program).IsTransducer

Fixed-program selection followed by selected execution preserves one-way output.

theorem Complexity.RAM.RegisterStore.Machine.programInstructionTM_prefix_withinAuxSpace {n : ℕ} (tapes : ControlInstructionTapes n) (program : Program) (pcValue : ℕ) (store : Store) (inputLength initialSpace time : ℕ) (start current : Complexity.Cfg (n + 1) (programInstructionTM tapes program).Q) (hinitial : start.WithinAuxSpace inputLength initialSpace) (hreach : (programInstructionTM tapes program).reachesIn time start current) (htime : time ≤ programInstructionTime tapes program pcValue store) : current.WithinAuxSpace inputLength (initialSpace + programInstructionTime tapes program pcValue store)

Every prefix of fixed-program selection and execution stays within the initial auxiliary space plus its advertised total running-time bound.