Complete dense-overlay RAM decision-machine proof internals #
theorem
Complexity.RAM.RegisterStore.Machine.denseProgramDecisionTM_hoareTime_run_internal
{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_internal
{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 complete dense machine realizes a halted executable RAM run, with its verdict rewritten through the overlay decoding theorem.