Complete dense-overlay RAM decision machine

theorem Complexity.RAM.RegisterStore.Machine.denseProgramDecisionTM_hoareTime_run {n : ℕ} (tapes : ControlInstructionTapes n) (program : Program) (input : List Bool) (fuel : ℕ) (hhalted : DenseOverlay.Snapshot.Halted program (DenseOverlay.Snapshot.run program input fuel (DenseOverlay.Snapshot.initial input))) : (denseProgramDecisionTM tapes program).HoareTime (fun (inp : Tape) (work : Fin (n + 1) → Tape) (out : Tape) => inp = Tape.init (List.map Γ.ofBool input) ∧ (work = fun (x : Fin (n + 1)) => Tape.init []) ∧ out = Tape.init []) (fun (_inp : Tape) (_work : Fin (n + 1) → Tape) (out : Tape) => have final := DenseOverlay.Snapshot.run program input fuel (DenseOverlay.Snapshot.initial input); out = registerVerdictOutput (DenseOverlay.read input final.overlay 0)) (denseProgramDecisionTime tapes program input fuel)

The complete dense machine realizes one halted overlay run and emits its decoded R₀ verdict.

theorem Complexity.RAM.RegisterStore.Machine.denseProgramDecisionTM_hoareTime_ramRun {n : ℕ} (tapes : ControlInstructionTapes n) (program : Program) (input : List Bool) (fuel : ℕ) (hhalted : Halted program (run program fuel (initCfg input))) : (denseProgramDecisionTM tapes program).HoareTime (fun (inp : Tape) (work : Fin (n + 1) → Tape) (out : Tape) => inp = Tape.init (List.map Γ.ofBool input) ∧ (work = fun (x : Fin (n + 1)) => Tape.init []) ∧ out = Tape.init []) (fun (_inp : Tape) (_work : Fin (n + 1) → Tape) (out : Tape) => out = registerVerdictOutput (run program fuel (initCfg input)).verdict) (denseProgramDecisionTime tapes program input fuel)

The fixed dense machine realizes a halted executable RAM run and emits its public R₀ verdict.