Complete sparse RAM decision machine #
theorem
Complexity.RAM.RegisterStore.Machine.programDecisionTM_hoareTime_run
{n : ℕ}
(tapes : ControlInstructionTapes n)
(program : Program)
(input : List Bool)
(fuel : ℕ)
(hhalted : Snapshot.Halted program (Snapshot.run program fuel (programInitialSnapshot input)))
:
(programDecisionTM 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 := Snapshot.run program fuel (programInitialSnapshot input);
out = registerVerdictOutput (read final.store 0))
(programDecisionTime tapes program input fuel)
The complete concrete machine realizes one halted pure sparse RAM run and
emits its R₀ verdict.
theorem
Complexity.RAM.RegisterStore.Machine.programDecisionTM_hoareTime_ramRun
{n : ℕ}
(tapes : ControlInstructionTapes n)
(program : Program)
(input : List Bool)
(fuel : ℕ)
(hhalted : Halted program (run program fuel (initCfg input)))
:
(programDecisionTM 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)
(programDecisionTime tapes program input fuel)
The complete machine realizes a halted executable RAM run and emits its
public R₀ verdict.