Public RAM input/output ABI for the sparse TM simulator

The public RAM input occupies the unbounded prefix R₁, …, Rₙ, so no fixed scratch register is initially disjoint from every input. The marshaller first captures the six registers it must clobber in finite control flow. Each leaf then copies the raw input backward into the sparse input tape while clearing the old prefix, repairs those six statically remembered bits, and initializes the state, heads, and left-end markers.

def Complexity.RAM.TMConfig.Sparse.captureRegs (n : ℕ) : List ℕ

Fixed registers clobbered before the backward input-copy loop reaches them.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.RAM.TMConfig.Sparse.marshalConstants (n : ℕ) : List Structured.Basic

Constants needed by each backward-copy iteration. They are restored inside the loop because clearing the raw prefix eventually visits these registers.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.RAM.TMConfig.Sparse.marshalLoopOps (n : ℕ) : List Structured.Basic

Copy and clear the raw input cell selected by the cursor in R₀, convert its public-ABI Boolean code 0/1 to the sparse tape-symbol code 1/2, write it to the sparse input-tape address, and decrement the cursor.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.RAM.TMConfig.Sparse.marshalLoop (n : ℕ) : Structured.Cmd

Backward raw-input copy.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.RAM.TMConfig.Sparse.marshalLoopSteps (n inputLength : ℕ) : ℕ

Exact source/compiled instruction count of the backward-copy loop.

Equations

• Complexity.RAM.TMConfig.Sparse.marshalLoopSteps n inputLength = inputLength * ((Complexity.RAM.TMConfig.Sparse.marshalLoopOps n).length + 2) + 1

def Complexity.RAM.TMConfig.Sparse.marshalBaseBound (n inputLength : ℕ) : ℕ

Initial numeric allowance for public-input marshalling. It contains every raw input register and every sparse destination address used by the copy.

Equations

• Complexity.RAM.TMConfig.Sparse.marshalBaseBound n inputLength = Complexity.RAM.TMConfig.Sparse.registerBound n (inputLength + 1)

def Complexity.RAM.TMConfig.Sparse.marshalBound (n inputLength : ℕ) : ℕ

Common sparse position/resource bound used after marshalling. The additive input-length slack absorbs the one-unit value growth of every loop body.

Equations

• Complexity.RAM.TMConfig.Sparse.marshalBound n inputLength = Complexity.RAM.TMConfig.Sparse.marshalBaseBound n inputLength + inputLength

def Complexity.RAM.TMConfig.Sparse.marshalWidth (n inputLength : ℕ) : ℕ

Logarithmic-cost width used by the public-input marshaller.

Equations

• Complexity.RAM.TMConfig.Sparse.marshalWidth n inputLength = Complexity.RAM.bitlen (Complexity.RAM.TMConfig.Sparse.marshalBound n inputLength) + 1

def Complexity.RAM.TMConfig.Sparse.marshalBaseWidth (n inputLength : ℕ) : ℕ

Width of the smaller envelope used before the copy loop starts.

Equations

• Complexity.RAM.TMConfig.Sparse.marshalBaseWidth n inputLength = Complexity.RAM.bitlen (Complexity.RAM.TMConfig.Sparse.marshalBaseBound n inputLength) + 1

def Complexity.RAM.TMConfig.Sparse.marshalSpaceBound (n inputLength : ℕ) : ℕ

Sparse-store space envelope used throughout public-input marshalling.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.RAM.TMConfig.Sparse.marshalLoopTimeBound (n inputLength : ℕ) : ℕ

Concrete logarithmic-cost bound for the backward-copy loop.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.RAM.TMConfig.Sparse.repairBit (n : ℕ) (captured : ℕ × ℕ) : Structured.Cmd

Restore one input bit remembered in the capture tree, but only when the copy loop actually visited that position. A visited destination is necessarily positive because the loop writes rawBit + 1; an absent position remains the initial zero beyond the raw input prefix.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.RAM.TMConfig.Sparse.repairCaptured (n : ℕ) (captured : List (ℕ × ℕ)) : Structured.Cmd

Restore all visited scratch-position input bits remembered by a capture-tree leaf.

Equations

• Complexity.RAM.TMConfig.Sparse.repairCaptured n [] = Complexity.RAM.Structured.Cmd.skip
• Complexity.RAM.TMConfig.Sparse.repairCaptured n (entry :: rest) = (Complexity.RAM.TMConfig.Sparse.repairBit n entry).seq (Complexity.RAM.TMConfig.Sparse.repairCaptured n rest)

def Complexity.RAM.TMConfig.Sparse.captureValues (store : Structured.Store) : List ℕ → List (ℕ × ℕ) → List (ℕ × ℕ)

Values accumulated by the capture tree, in the same reverse order used by captureInput.

Equations

• Complexity.RAM.TMConfig.Sparse.captureValues store [] x✝ = x✝
• Complexity.RAM.TMConfig.Sparse.captureValues store (reg :: rest) x✝ = Complexity.RAM.TMConfig.Sparse.captureValues store rest ((reg, store reg) :: x✝)

noncomputable def Complexity.RAM.TMConfig.Sparse.initializeConfigWrites {n : ℕ} (tm : TM n) : List (ℕ × ℕ)

Immediate writes that initialize the semantic fields of tm.initCfg after the raw input prefix has been relocated and cleared.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Complexity.RAM.TMConfig.Sparse.initializeConfigOps {n : ℕ} (tm : TM n) : List Structured.Basic

Straight-line realization of the initial-configuration writes.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Complexity.RAM.TMConfig.Sparse.marshalLeafTimeBound {n : ℕ} (tm : TM n) (inputLength : ℕ) : ℕ

Concrete cost bound for one selected capture-tree leaf.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Complexity.RAM.TMConfig.Sparse.marshalTimeBound {n : ℕ} (tm : TM n) (inputLength : ℕ) : ℕ

Concrete cost bound for the full public-input marshaller, including the fixed capture tree.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Complexity.RAM.TMConfig.Sparse.marshalLeaf {n : ℕ} (tm : TM n) (captured : List (ℕ × ℕ)) : Structured.Cmd

One capture-tree leaf: initialize scratch constants, copy backward, repair captured positions, and establish the sparse initial configuration.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Complexity.RAM.TMConfig.Sparse.captureInput {n : ℕ} (tm : TM n) : List ℕ → List (ℕ × ℕ) → Structured.Cmd

Capture the initial Boolean contents of a finite register list in control flow. The zero/nonzero branches record canonical numeric values 0 and 1.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.RAM.TMConfig.Sparse.captureInput tm [] x✝ = Complexity.RAM.TMConfig.Sparse.marshalLeaf tm x✝

noncomputable def Complexity.RAM.TMConfig.Sparse.marshalInput {n : ℕ} (tm : TM n) : Structured.Cmd

Fixed public-ABI marshaller for tm.

Equations

• Complexity.RAM.TMConfig.Sparse.marshalInput tm = Complexity.RAM.TMConfig.Sparse.captureInput tm (Complexity.RAM.TMConfig.Sparse.captureRegs n) []

def Complexity.RAM.TMConfig.Sparse.extractVerdictOps (n : ℕ) : List Structured.Basic

Copy the halted TM output symbol at cell one into public verdict register R₀ and shift the sparse symbol codes 1/2 back to public verdicts 0/1. This intentionally destroys the final sparse state code.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Complexity.RAM.TMConfig.Sparse.decisionTimeBound {n : ℕ} (tm : TM n) (inputLength steps : ℕ) : ℕ

End-to-end logarithmic-cost bound from the public ABI through verdict extraction for a halting run of the given length.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Complexity.RAM.TMConfig.Sparse.decisionProgram {n : ℕ} (tm : TM n) : Structured.Cmd

Complete fixed source program from the public RAM input ABI to verdict register R₀.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Complexity.RAM.TMConfig.Sparse.compiledDecision {n : ℕ} (tm : TM n) : Program

Concrete compiled public-ABI simulator.

Equations

• Complexity.RAM.TMConfig.Sparse.compiledDecision tm = (Complexity.RAM.TMConfig.Sparse.decisionProgram tm).compile