End-to-end public-ABI sparse simulation -- proof internals #
theorem
Complexity.RAM.TMConfig.Sparse.extractVerdict_exec_internal
{n : ℕ}
{tm : TM n}
{halted : Complexity.Cfg n tm.Q}
{store : Structured.Store}
(hrepresents : Represents tm halted store)
:
have final := Structured.Basic.execList (extractVerdictOps n) store;
∃ (cost : ℕ) (space : ℕ),
Structured.Exec (Structured.Cmd.basics (extractVerdictOps n)) store final (extractVerdictOps n).length cost space ∧ final stateReg = symbolCode (halted.output.cells 1) - 1
The verdict extractor copies the represented halted output cell one into the public verdict register.
theorem
Complexity.RAM.TMConfig.Sparse.decisionProgram_exec_internal
{n : ℕ}
{tm : TM n}
{steps : ℕ}
{x : List Bool}
{halted : Complexity.Cfg n tm.Q}
(hreach : tm.reachesIn steps (tm.initCfg x) halted)
(hhalted : tm.halted halted)
:
∃ (final : Structured.Store) (sourceSteps : ℕ) (cost : ℕ) (space : ℕ),
Structured.Exec (decisionProgram tm) (initRegs x) final sourceSteps cost space ∧ final stateReg = symbolCode (halted.output.cells 1) - 1
From the public RAM input store, the complete fixed source program follows
any exact halting TM run and returns the halted output symbol in R₀.
theorem
Complexity.RAM.TMConfig.Sparse.compiledDecision_exec_internal
{n : ℕ}
{tm : TM n}
{steps : ℕ}
{x : List Bool}
{halted : Complexity.Cfg n tm.Q}
(hreach : tm.reachesIn steps (tm.initCfg x) halted)
(hhalted : tm.halted halted)
:
∃ (final : Structured.Store) (sourceSteps : ℕ) (cost : ℕ) (space : ℕ),
Structured.Exec (decisionProgram tm) (initRegs x) final sourceSteps cost space ∧ run (compiledDecision tm) sourceSteps (initCfg x) = { pc := (decisionProgram tm).codeSize, regs := final } ∧ Halted (compiledDecision tm) (run (compiledDecision tm) sourceSteps (initCfg x)) ∧ logTimeUpto (compiledDecision tm) sourceSteps (initCfg x) = cost ∧ spaceUpto (compiledDecision tm) sourceSteps (initCfg x) = space ∧ final stateReg = symbolCode (halted.output.cells 1) - 1
Exact transfer of the public-ABI decision program to its concrete compiled RAM, including source/target store agreement, cost, and space.