Fixed-program dispatch -- proof internals

theorem Complexity.RAM.RegisterStore.Machine.dispatchProgramTM_hoareTime_of_execute_internal {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)

The finite decrementing branch tree selects the corresponding static instruction, assuming the individual instruction kernels satisfy their common semantic contract.

theorem Complexity.RAM.RegisterStore.Machine.bufferedCleanupTM_hoareTime_frame_internal {n : ℕ} (tapes : ControlInstructionTapes n) (oldStore nextStore : Store) (nextPC : ℕ) (cleanupValues : Fin 5 → ℕ) (remainingValue sourceHeadBound : ℕ) (initialWork : Fin (n + 1) → Tape) (inp₀ out₀ : Tape) (hready : BufferedCleanupReady tapes oldStore nextStore nextPC cleanupValues remainingValue 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 nextStore nextPC work ∧ out = out₀) (bufferedCleanupTime tapes oldStore nextStore cleanupValues remainingValue sourceHeadBound)

Any buffered representation endpoint is restored to the reusable clean ABI.

theorem Complexity.RAM.RegisterStore.Machine.instructionCleanupTM_hoareTime_frame_internal {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)

The ordinary sparse instruction endpoint is an instance of generic buffered cleanup.

theorem Complexity.RAM.RegisterStore.Machine.programStepTM_hoareTime_frame_internal {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₀) (hprogram : (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)) : (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) => inp = inp₀ ∧ InstructionExecutionReady tapes (instructionStore (selectedInstruction program pcValue) pcValue store) (instructionPC (selectedInstruction program pcValue) pcValue store) work ∧ out = (Tape.init []).move Dir3.right) (programStepTime tapes program pcValue store)

One selected instruction followed by cleanup realizes the next reusable sparse-snapshot boundary.