Dense-overlay RAM program controller

theorem Complexity.RAM.RegisterStore.Machine.denseProgramOutputTM_hoareTime {n : ℕ} (tapes : ControlInstructionTapes n) (input : List Bool) (overlay : Store) (pcValue : ℕ) (initialWork : Fin (n + 1) → Tape) (hvalid : DenseOverlay.Valid overlay) (hready : InstructionExecutionReady tapes overlay pcValue initialWork) : (denseProgramOutputTM tapes).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 ∧ out = registerVerdictOutput (DenseOverlay.read input overlay 0)) (denseProgramOutputTime tapes input overlay)

Final overlay-aware lookup recovers decoded R₀ and emits its Boolean verdict.

theorem Complexity.RAM.RegisterStore.Machine.denseProgramOutputTM_hoareTime_haltOutput {n : ℕ} (tapes : ControlInstructionTapes n) (input : List Bool) (overlay : Store) (pcValue : ℕ) (initialWork : Fin (n + 1) → Tape) (hvalid : DenseOverlay.Valid overlay) (hready : InstructionExecutionReady tapes overlay pcValue initialWork) : (denseProgramOutputTM tapes).HoareTime (fun (inp : Tape) (work : Fin (n + 1) → Tape) (out : Tape) => inp = (Tape.init (List.map Γ.ofBool input)).move Dir3.right ∧ work = initialWork ∧ out = instructionHaltOutput Instr.halt) (fun (inp : Tape) (_work : Fin (n + 1) → Tape) (out : Tape) => inp = (Tape.init (List.map Γ.ofBool input)).move Dir3.right ∧ out = registerVerdictOutput (DenseOverlay.read input overlay 0)) (denseProgramOutputTime tapes input overlay)

The dense verdict extractor can overwrite the loop's halt-test bit directly.

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

A halted dense snapshot is stationary under one program step.

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

A halted dense snapshot remains fixed for all additional fuel.

theorem Complexity.RAM.RegisterStore.Machine.denseProgramLoopTM_hoareTime_run {n : ℕ} (tapes : ControlInstructionTapes n) (program : Program) (input : List Bool) (fuel : ℕ) (snapshot : DenseOverlay.Snapshot) (initialWork : Fin (n + 1) → Tape) (hvalid : DenseOverlay.Valid snapshot.overlay) (hready : InstructionExecutionReady tapes snapshot.overlay snapshot.pc initialWork) (hhalted : DenseOverlay.Snapshot.Halted program (DenseOverlay.Snapshot.run program input fuel snapshot)) : (denseProgramLoopTM 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) => have final := DenseOverlay.Snapshot.run program input fuel snapshot; inp = (Tape.init (List.map Γ.ofBool input)).move Dir3.right ∧ InstructionExecutionReady tapes final.overlay final.pc work ∧ out = instructionHaltOutput (DenseOverlay.Snapshot.curInstr program final)) (denseProgramLoopTime tapes program input (fuel + 1) snapshot)

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