Sparse RAM program controller -- proof internals

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

The exact snapshot work image satisfies the complete reusable instruction ABI whenever its sparse store is canonical.

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

theorem Complexity.RAM.RegisterStore.Machine.registerVerdictTM_hoareTime_frame_internal {n : ℕ} (idx : Fin n) (value : ℕ) (inp₀ : Tape) (work₀ : Fin n → Tape) (hvalue : (work₀ idx).HasBinaryNat value) (hinput : TM.Parked inp₀) (hwork : ∀ (i : Fin n), TM.Parked (work₀ i)) : (registerVerdictTM idx).HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = work₀ ∧ out = (Tape.init []).move Dir3.right) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = work₀ ∧ out = registerVerdictOutput value) 1

theorem Complexity.RAM.RegisterStore.Machine.programOutputTM_hoareTime_internal {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 and Boolean emission recover the RAM verdict register.

theorem Complexity.RAM.RegisterStore.Machine.registerVerdictTM_hoareTime_haltOutput_internal {n : ℕ} (idx : Fin n) (value : ℕ) (inp₀ : Tape) (work₀ : Fin n → Tape) (hvalue : (work₀ idx).HasBinaryNat value) (hinput : TM.Parked inp₀) (hwork : ∀ (i : Fin n), TM.Parked (work₀ i)) : (registerVerdictTM idx).HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = work₀ ∧ out = instructionHaltOutput Instr.halt) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = work₀ ∧ out = registerVerdictOutput value) 1

theorem Complexity.RAM.RegisterStore.Machine.programOutputTM_hoareTime_haltOutput_internal {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, so the controller and extractor compose without an output reset.

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

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

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

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

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

theorem Complexity.RAM.RegisterStore.Machine.programLoop_rewind_check_internal {n : ℕ} (tmBody tmTest : TM n) (c : Complexity.Cfg n (TM.LoopQ tmBody.Q tmTest.Q)) (hstate : c.state = Sum.inr (Sum.inl TM.LoopPhase.rewindOut)) (hin : c.input.read ≠ Γ.start) (hwork : ∀ (i : Fin n), (c.work i).read ≠ Γ.start) (hhead : c.output.head = 1) (hstart : c.output.cells 0 = Γ.start) (hnoStart : ∀ (j : ℕ), 1 ≤ j → c.output.cells j ≠ Γ.start) : ∃ (c' : Complexity.Cfg n (tmBody.loopTM tmTest).Q), (tmBody.loopTM tmTest).reachesIn 3 c c' ∧ (c'.state = if c.output.cells 1 = Γ.one then Sum.inr (Sum.inl TM.LoopPhase.done) else Sum.inl tmBody.qstart) ∧ c'.input = c.input ∧ c'.work = c.work ∧ c'.output = c.output

The loop's fixed three-step rewind/check tail preserves every tape exactly.

theorem Complexity.RAM.RegisterStore.Machine.instructionHaltVerdictTM_hoareTime_frame_internal {n : ℕ} (instruction : Instr) (inp₀ : Tape) (work₀ : Fin n → Tape) (hinput : TM.Parked inp₀) (hwork : ∀ (i : Fin n), TM.Parked (work₀ i)) : (instructionHaltVerdictTM instruction).HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = work₀ ∧ out = (Tape.init []).move Dir3.right) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = work₀ ∧ out = instructionHaltOutput instruction) 1

The verdict leaf has a literal one-step frame.

theorem Complexity.RAM.RegisterStore.Machine.dispatchHaltTM_hoareTime_frame_internal {n : ℕ} (tapes : ControlInstructionTapes n) (program : Program) (store : Store) (pcValue selector : ℕ) (cleanWork work₀ : Fin (n + 1) → Tape) (inp₀ : Tape) (hready : DispatchReady tapes store pcValue selector cleanWork work₀) (hinput : TM.Parked inp₀) : (dispatchHaltTM tapes program).HoareTime (fun (inp : Tape) (work : Fin (n + 1) → Tape) (out : Tape) => inp = inp₀ ∧ work = work₀ ∧ out = (Tape.init []).move Dir3.right) (fun (inp : Tape) (work : Fin (n + 1) → Tape) (out : Tape) => inp = inp₀ ∧ work = cleanWork ∧ out = instructionHaltOutput (selectedInstruction program selector)) (dispatchHaltTime tapes program selector)

The decrementing selector emits the verdict of the selected instruction and restores its scratch tape to the clean ABI.

theorem Complexity.RAM.RegisterStore.Machine.programHaltTM_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₀) : (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) => inp = inp₀ ∧ work = initialWork ∧ out = instructionHaltOutput (selectedInstruction program pcValue)) (programHaltTime tapes program pcValue)

Copy the canonical PC, select its fixed-program instruction, and emit its halt verdict while restoring the complete instruction ABI.

theorem Complexity.RAM.RegisterStore.Machine.programLoopTM_iteration_internal {n : ℕ} (tapes : ControlInstructionTapes n) (program : Program) (snapshot : Snapshot) (initialWork : Fin (n + 1) → Tape) (inp₀ : Tape) (hready : InstructionExecutionReady tapes snapshot.store snapshot.pc initialWork) (hinput : TM.Parked inp₀) : have next := Snapshot.step program snapshot; ∃ (nextWork : Fin (n + 1) → Tape), ∃ time ≤ programLoopIterationTime tapes program snapshot, InstructionExecutionReady tapes next.store next.pc nextWork ∧ (Snapshot.Halted program next ∧ (programLoopTM tapes program).reachesIn time { state := (programLoopTM tapes program).qstart, input := inp₀, work := initialWork, output := (Tape.init []).move Dir3.right } { state := Sum.inr (Sum.inl TM.LoopPhase.done), input := inp₀, work := nextWork, output := instructionHaltOutput (Snapshot.curInstr program next) } ∨ ¬Snapshot.Halted program next ∧ (programLoopTM tapes program).reachesIn time { state := (programLoopTM tapes program).qstart, input := inp₀, work := initialWork, output := (Tape.init []).move Dir3.right } { state := (programLoopTM tapes program).qstart, input := inp₀, work := nextWork, output := (Tape.init []).move Dir3.right })

One loop iteration realizes one pure sparse step and either halts on the successor's halt instruction or returns to the body start with blank output.

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

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

theorem Complexity.RAM.RegisterStore.Machine.programLoopTM_hoareTime_run_internal {n : ℕ} (tapes : ControlInstructionTapes n) (program : Program) (fuel : ℕ) (snapshot : Snapshot) (initialWork : Fin (n + 1) → Tape) (inp₀ : Tape) : InstructionExecutionReady tapes snapshot.store snapshot.pc initialWork → TM.Parked inp₀ → 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)

A halted fuel-bounded sparse run is realized by the fixed controller loop. The extra iteration handles a snapshot that is already halted at fuel zero.