Fixed-program dense-overlay dispatch

theorem Complexity.RAM.RegisterStore.Machine.denseDispatchProgramTM_hoareTime_frame {n : ℕ} (tapes : ControlInstructionTapes n) (program : Program) (input : List Bool) (overlay : Store) (pcValue selector : ℕ) (cleanWork work₀ : Fin (n + 1) → Tape) (hvalid : DenseOverlay.Valid overlay) (hready : DispatchReady tapes overlay pcValue selector cleanWork work₀) : (denseDispatchProgramTM tapes program).HoareTime (fun (inp : Tape) (work : Fin (n + 1) → Tape) (out : Tape) => inp = (Tape.init (List.map Γ.ofBool input)).move Dir3.right ∧ work = work₀ ∧ out = (Tape.init []).move Dir3.right) (fun (inp : Tape) (work : Fin (n + 1) → Tape) (out : Tape) => inp = (Tape.init (List.map Γ.ofBool input)).move Dir3.right ∧ DenseInstructionExecutionResult tapes input (selectedInstruction program selector) pcValue overlay work ∧ out = (Tape.init []).move Dir3.right) (denseDispatchProgramTime tapes input overlay pcValue program selector)

The decrementing branch tree selects the corresponding dense instruction, including the out-of-range halt convention.

theorem Complexity.RAM.RegisterStore.Machine.denseProgramInstructionTM_hoareTime_frame {n : ℕ} (tapes : ControlInstructionTapes n) (program : Program) (input : List Bool) (overlay : Store) (pcValue : ℕ) (initialWork : Fin (n + 1) → Tape) (hvalid : DenseOverlay.Valid overlay) (hready : InstructionExecutionReady tapes overlay pcValue initialWork) : (denseProgramInstructionTM tapes program).HoareTime (fun (inp : Tape) (work : Fin (n + 1) → Tape) (out : Tape) => inp = (Tape.init (List.map Γ.ofBool input)).move Dir3.right ∧ work = initialWork ∧ out = (Tape.init []).move Dir3.right) (fun (inp : Tape) (work : Fin (n + 1) → Tape) (out : Tape) => inp = (Tape.init (List.map Γ.ofBool input)).move Dir3.right ∧ DenseInstructionExecutionResult tapes input (selectedInstruction program pcValue) pcValue overlay work ∧ out = (Tape.init []).move Dir3.right) (denseProgramInstructionTime tapes program input pcValue overlay)

Copy the canonical PC into dispatch scratch and execute the selected dense instruction.

theorem Complexity.RAM.RegisterStore.Machine.denseProgramStepTM_hoareTime_frame {n : ℕ} (tapes : ControlInstructionTapes n) (program : Program) (input : List Bool) (overlay : Store) (pcValue : ℕ) (initialWork : Fin (n + 1) → Tape) (hvalid : DenseOverlay.Valid overlay) (hready : InstructionExecutionReady tapes overlay pcValue initialWork) : (denseProgramStepTM tapes program).HoareTime (fun (inp : Tape) (work : Fin (n + 1) → Tape) (out : Tape) => inp = (Tape.init (List.map Γ.ofBool input)).move Dir3.right ∧ work = initialWork ∧ out = (Tape.init []).move Dir3.right) (fun (inp : Tape) (work : Fin (n + 1) → Tape) (out : Tape) => inp = (Tape.init (List.map Γ.ofBool input)).move Dir3.right ∧ InstructionExecutionReady tapes (denseInstructionStore input (selectedInstruction program pcValue) pcValue overlay) (denseInstructionPC input (selectedInstruction program pcValue) pcValue overlay) work ∧ out = (Tape.init []).move Dir3.right) (denseProgramStepTime tapes program input pcValue overlay)

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