Public RAM ABI for the fixed sparse TM simulator

The public RAM convention stores the input length in R₀ and its raw bits in R₁, …, Rₙ. The fixed marshaller relocates that unbounded prefix into the sparse TM layout without assuming a length bound, despite its scratch registers potentially overlapping the raw input. The complete decision program then runs the fixed sparse simulator to a halted TM configuration and returns a public Boolean verdict in R₀.

theorem Complexity.RAM.TMConfig.Sparse.marshalInput_correct {n : ℕ} (tm : TM n) (x : List Bool) : ∃ (final : Structured.Store) (steps : ℕ) (cost : ℕ) (space : ℕ), Structured.Exec (marshalInput tm) (initRegs x) final steps cost space ∧ Represents tm (tm.initCfg x) final

The fixed marshaller converts the public RAM input store into a complete sparse representation of the TM's initial configuration.

theorem Complexity.RAM.TMConfig.Sparse.decisionProgram_correct {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

The complete fixed source program follows any exact halting TM run and returns its output bit using the public RAM verdict convention 0/1.

theorem Complexity.RAM.TMConfig.Sparse.compiledDecision_correct {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 concrete-RAM transfer for the complete public-ABI simulator. Source and target agree on final registers, logarithmic cost, and peak space.

theorem Complexity.RAM.TMConfig.Sparse.compiledDecision_resourceBound {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 ∧ cost ≤ decisionTimeBound tm x.length steps ∧ space ≤ spaceBound tm (marshalBound n x.length + steps) ∧ 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

Concrete end-to-end resource transfer from the public RAM input ABI. The program depends only on tm; a steps-step halting TM run determines bounded RAM fuel, logarithmic cost, sparse-store space, and the same verdict.

theorem Complexity.RAM.TMConfig.Sparse.decisionTimeBound_mono_steps {n : ℕ} (tm : TM n) (inputLength : ℕ) {steps larger : ℕ} (hle : steps ≤ larger) : decisionTimeBound tm inputLength steps ≤ decisionTimeBound tm inputLength larger

Increasing the simulated TM step budget only increases the advertised end-to-end public-ABI cost bound.