Dense-overlay RAM program controller -- proof internals

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

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

Final dense lookup overwrites the loop's halt-test bit with the decoded RAM verdict.

theorem Complexity.RAM.RegisterStore.Machine.denseProgramLoopTM_iteration_internal {n : ℕ} (tapes : ControlInstructionTapes n) (program : Program) (input : List Bool) (snapshot : DenseOverlay.Snapshot) (initialWork : Fin (n + 1) → Tape) (hvalid : DenseOverlay.Valid snapshot.overlay) (hready : InstructionExecutionReady tapes snapshot.overlay snapshot.pc initialWork) : have next := DenseOverlay.Snapshot.step program input snapshot; ∃ (nextWork : Fin (n + 1) → Tape), ∃ time ≤ denseProgramLoopIterationTime tapes program input snapshot, InstructionExecutionReady tapes next.overlay next.pc nextWork ∧ (DenseOverlay.Snapshot.Halted program next ∧ (denseProgramLoopTM tapes program).reachesIn time { state := (denseProgramLoopTM tapes program).qstart, input := (Tape.init (List.map Γ.ofBool input)).move Dir3.right, work := initialWork, output := (Tape.init []).move Dir3.right } { state := Sum.inr (Sum.inl TM.LoopPhase.done), input := (Tape.init (List.map Γ.ofBool input)).move Dir3.right, work := nextWork, output := instructionHaltOutput (DenseOverlay.Snapshot.curInstr program next) } ∨ ¬DenseOverlay.Snapshot.Halted program next ∧ (denseProgramLoopTM tapes program).reachesIn time { state := (denseProgramLoopTM tapes program).qstart, input := (Tape.init (List.map Γ.ofBool input)).move Dir3.right, work := initialWork, output := (Tape.init []).move Dir3.right } { state := (denseProgramLoopTM tapes program).qstart, input := (Tape.init (List.map Γ.ofBool input)).move Dir3.right, work := nextWork, output := (Tape.init []).move Dir3.right })

One dense loop iteration realizes one overlay step and either halts on the successor's selected instruction or returns to the body start.

theorem Complexity.RAM.RegisterStore.Machine.denseSnapshot_step_eq_self_of_halted_internal (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 selected step.

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

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

theorem Complexity.RAM.RegisterStore.Machine.denseProgramLoopTM_hoareTime_run_internal {n : ℕ} (tapes : ControlInstructionTapes n) (program : Program) (input : List Bool) (fuel : ℕ) (snapshot : DenseOverlay.Snapshot) (initialWork : Fin (n + 1) → Tape) : DenseOverlay.Valid snapshot.overlay → InstructionExecutionReady tapes snapshot.overlay snapshot.pc initialWork → 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)

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