Sparse RAM program controller

The fixed-program halt test copies the canonical sparse-snapshot PC, walks a finite decrementing selector, restores its scratch, and writes 1 exactly when the selected instruction is halt.

@[simp]

theorem Complexity.RAM.RegisterStore.Machine.instructionHaltOutput_head (instruction : Instr) : (instructionHaltOutput instruction).head = 1

@[simp]

theorem Complexity.RAM.RegisterStore.Machine.instructionHaltOutput_cells_zero (instruction : Instr) : (instructionHaltOutput instruction).cells 0 = Γ.start

theorem Complexity.RAM.RegisterStore.Machine.instructionHaltOutput_cells_ne_start (instruction : Instr) (j : ℕ) : j ≥ 1 → (instructionHaltOutput instruction).cells j ≠ Γ.start

@[simp]

theorem Complexity.RAM.RegisterStore.Machine.instructionHaltOutput_cell_one_eq_one_iff (instruction : Instr) : (instructionHaltOutput instruction).cells 1 = Γ.one ↔ instruction = Instr.halt

@[simp]

theorem Complexity.RAM.RegisterStore.Machine.instructionHaltOutput_eq_blank_of_ne_halt {instruction : Instr} (h : instruction ≠ Instr.halt) : instructionHaltOutput instruction = (Tape.init []).move Dir3.right

theorem Complexity.RAM.RegisterStore.Machine.programSnapshotWork_ready {n : ℕ} (tapes : ControlInstructionTapes n) (snapshot : Snapshot) (hcanonical : Canonical snapshot.store) : InstructionExecutionReady tapes snapshot.store snapshot.pc (programSnapshotWork tapes snapshot)

The canonical work-tape image of a sparse snapshot satisfies the complete reusable instruction ABI.

@[simp]

theorem Complexity.RAM.RegisterStore.Machine.registerVerdictOutput_cell_one (value : ℕ) : (registerVerdictOutput value).cells 1 = if value = 0 then Γ.zero else Γ.one

theorem Complexity.RAM.RegisterStore.Machine.programOutputTM_hoareTime {n : ℕ} (tapes : ControlInstructionTapes n) (store : Store) (pcValue : ℕ) (initialWork : Fin (n + 1) → Tape) (inp₀ : Tape) (hready : InstructionExecutionReady tapes store pcValue initialWork) (hinput : TM.Parked inp₀) : (programOutputTM tapes).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₀ ∧ out = registerVerdictOutput (read store 0)) (programOutputTime tapes store)

Final sparse lookup recovers R₀ and emits zero exactly for value zero, or one for any nonzero value.

theorem Complexity.RAM.RegisterStore.Machine.programOutputTM_hoareTime_haltOutput {n : ℕ} (tapes : ControlInstructionTapes n) (store : Store) (pcValue : ℕ) (initialWork : Fin (n + 1) → Tape) (inp₀ : Tape) (hready : InstructionExecutionReady tapes store pcValue initialWork) (hinput : TM.Parked inp₀) : (programOutputTM tapes).HoareTime (fun (inp : Tape) (work : Fin (n + 1) → Tape) (out : Tape) => inp = inp₀ ∧ work = initialWork ∧ out = instructionHaltOutput Instr.halt) (fun (inp : Tape) (_work : Fin (n + 1) → Tape) (out : Tape) => inp = inp₀ ∧ out = registerVerdictOutput (read store 0)) (programOutputTime tapes store)

Final sparse lookup overwrites the loop's halt-test bit with the RAM verdict, allowing direct controller/extractor composition.

theorem Complexity.RAM.RegisterStore.Machine.programHaltTM_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₀) : (programHaltTM 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 snapshot := { pc := pcValue, store := store }; inp = inp₀ ∧ work = initialWork ∧ out = instructionHaltOutput (Snapshot.curInstr program snapshot)) (programHaltTime tapes program pcValue)

The fixed-program test preserves the complete clean instruction ABI and emits the exact sparse snapshot's halt status.

theorem Complexity.RAM.RegisterStore.Machine.Snapshot.step_eq_self_of_halted (program : Program) (snapshot : Snapshot) (hhalted : Snapshot.Halted program snapshot) : Snapshot.step program snapshot = snapshot

A halted sparse snapshot is stationary under both one pure step and every fuel-bounded run.

theorem Complexity.RAM.RegisterStore.Machine.Snapshot.run_halted (program : Program) (snapshot : Snapshot) (hhalted : Snapshot.Halted program snapshot) (fuel : ℕ) : Snapshot.run program fuel snapshot = snapshot

Running a halted sparse snapshot for arbitrary additional fuel is a no-op.

theorem Complexity.RAM.RegisterStore.Machine.programLoopTM_hoareTime_run {n : ℕ} (tapes : ControlInstructionTapes n) (program : Program) (fuel : ℕ) (snapshot : Snapshot) (initialWork : Fin (n + 1) → Tape) (inp₀ : Tape) (hready : InstructionExecutionReady tapes snapshot.store snapshot.pc initialWork) (hinput : TM.Parked inp₀) (hhalted : Snapshot.Halted program (Snapshot.run program fuel snapshot)) : (programLoopTM 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 final := Snapshot.run program fuel snapshot; inp = inp₀ ∧ InstructionExecutionReady tapes final.store final.pc work ∧ out = instructionHaltOutput (Snapshot.curInstr program final)) (programLoopTime tapes program (fuel + 1) snapshot)

If the pure fuel-bounded sparse run is halted, the fixed controller loop reaches that exact reusable snapshot and exposes its halt verdict.