Uniform next-store buffering for control instructions

theorem Complexity.RAM.RegisterStore.Machine.finishBufferedControlInstructionTM_hoareTime_frame_internal {n : ℕ} (tapes : ControlInstructionTapes n) (store : Store) (pcValue newPC : ℕ) (initialWork : Fin (n + 1) → Tape) (inp₀ out₀ : Tape) (control : TM (n + 1)) (controlTime : ℕ) (hready : InstructionExecutionReady tapes store pcValue initialWork) (hinput : TM.Parked inp₀) (houtput : TM.Parked out₀) (hcontrol : control.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₀ ∧ ControlInstructionResult tapes.lifted store newPC initialWork work ∧ out = out₀) controlTime) : (finishControlInstructionTM tapes control).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₀ ∧ BufferedInstructionResult tapes store store newPC (fun (x : Fin 5) => 0) (List.length store) work ∧ out = out₀) (controlTime + 1 + (List.flatMap Entry.encode store).length + 1)

Representation-independent form of the control-instruction finisher. Control instructions preserve the encoded store, leave zero on every cleanup role, and retain the old entry count for the generic cleanup pass.

theorem Complexity.RAM.RegisterStore.Machine.executeInstructionTM_jz_hoareTime_frame {n : ℕ} (tapes : ControlInstructionTapes n) (store : Store) (pcValue source target : ℕ) (initialWork : Fin (n + 1) → Tape) (inp₀ out₀ : Tape) (hready : InstructionExecutionReady tapes store pcValue initialWork) (hinput : TM.Parked inp₀) (houtput : TM.Parked out₀) : (executeInstructionTM tapes (Instr.jz source target)).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₀ ∧ InstructionExecutionResult tapes (Instr.jz source target) pcValue store work ∧ out = out₀) (executeInstructionTime tapes (Instr.jz source target) pcValue store)

Conditional-zero execution has the common one-buffer instruction contract.

theorem Complexity.RAM.RegisterStore.Machine.executeInstructionTM_jmp_hoareTime_frame {n : ℕ} (tapes : ControlInstructionTapes n) (store : Store) (pcValue target : ℕ) (initialWork : Fin (n + 1) → Tape) (inp₀ out₀ : Tape) (hready : InstructionExecutionReady tapes store pcValue initialWork) (hinput : TM.Parked inp₀) (houtput : TM.Parked out₀) : (executeInstructionTM tapes (Instr.jmp target)).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₀ ∧ InstructionExecutionResult tapes (Instr.jmp target) pcValue store work ∧ out = out₀) (executeInstructionTime tapes (Instr.jmp target) pcValue store)

Unconditional-jump execution has the common one-buffer instruction contract.

theorem Complexity.RAM.RegisterStore.Machine.executeInstructionTM_halt_hoareTime_frame {n : ℕ} (tapes : ControlInstructionTapes n) (store : Store) (pcValue : ℕ) (initialWork : Fin (n + 1) → Tape) (inp₀ out₀ : Tape) (hready : InstructionExecutionReady tapes store pcValue initialWork) (hinput : TM.Parked inp₀) (houtput : TM.Parked out₀) : (executeInstructionTM tapes Instr.halt).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₀ ∧ InstructionExecutionResult tapes Instr.halt pcValue store work ∧ out = out₀) (executeInstructionTime tapes Instr.halt pcValue store)

Halt execution has the common one-buffer instruction contract.