Resource bounds for the public sparse-simulator ABI -- proof internals

The simulation core uses StepEnvelope. During the backward input copy only the writable value scratch register can temporarily exceed the core word bound; MarshalEnvelope records that exception while retaining the same finite index support. The first captured-position repair reloads that scratch register from the sparse data region, returning to the core envelope before simulation.

structure Complexity.RAM.TMConfig.Sparse.MarshalEnvelope {n : ℕ} (tm : TM n) (bound valueLimit : ℕ) (store : Structured.Store) : Prop

Temporary marshalling envelope. Every register except valueReg already fits the core word bound; the value scratch may use the larger valueLimit.

• index_lt (index : ℕ) : store index ≠ 0 → index < registerBound n (bound + 1)
• value_le (index : ℕ) : store index ≤ valueLimit
• value_le_of_ne (index : ℕ) : index ≠ valueReg n → store index ≤ wordBound tm bound

theorem Complexity.RAM.TMConfig.Sparse.MarshalEnvelope.storeEnvelope {n : ℕ} {tm : TM n} {bound valueLimit : ℕ} {store : Structured.Store} (henvelope : MarshalEnvelope tm bound valueLimit store) : Structured.Internal.StoreEnvelope (registerBound n (bound + 1)) valueLimit store

theorem Complexity.RAM.TMConfig.Sparse.StepEnvelope.toMarshalEnvelope {n : ℕ} {tm : TM n} {bound valueLimit : ℕ} {store : Structured.Store} (henvelope : StepEnvelope tm bound store) (hlimit : wordBound tm bound ≤ valueLimit) : MarshalEnvelope tm bound valueLimit store

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

theorem Complexity.RAM.TMConfig.Sparse.marshalConstants_measured_internal {n : ℕ} (tm : TM n) (x : List Bool) : Structured.Internal.MeasuredRuns (Structured.Cmd.basics (marshalConstants n)) (initRegs x) (marshalStart n x) (marshalConstants n).length (4 * (marshalConstants n).length * Structured.Internal.valueWidth (marshalBaseBound n x.length)) (Structured.Internal.envelopeSpace (registerBound n (marshalBound n x.length + 1)) (marshalBaseBound n x.length)) ∧ MarshalEnvelope tm (marshalBound n x.length) (marshalBaseBound n x.length) (marshalStart n x) ∧ MarshalInvariant n x x.length (marshalStart n x)

Installing the four copy-loop constants has a uniform marshalling envelope and establishes the semantic loop invariant.

theorem Complexity.RAM.TMConfig.Sparse.marshalLoop_measured_internal {n : ℕ} {tm : TM n} (x : List Bool) : ∃ (final : Structured.Store), Structured.Internal.MeasuredRuns (marshalLoop n) (marshalStart n x) final (marshalLoopSteps n x.length) (marshalLoopTimeBound n x.length) (marshalSpaceBound n x.length) ∧ MarshalInvariant n x 0 final ∧ StepEnvelope tm (marshalBound n x.length) final

The backward-copy loop has an exact source-step count, linear logarithmic cost, and a finite sparse-store envelope.

theorem Complexity.RAM.TMConfig.Sparse.extractVerdict_measured_internal {n : ℕ} {tm : TM n} {bound : ℕ} {halted : Complexity.Cfg n tm.Q} {store : Structured.Store} (hrepresents : Represents tm halted store) (henvelope : StepEnvelope tm bound store) : have final := Structured.Basic.execList (extractVerdictOps n) store; Structured.Internal.MeasuredRuns (Structured.Cmd.basics (extractVerdictOps n)) store final (extractVerdictOps n).length (4 * (extractVerdictOps n).length * wordWidth tm bound) (spaceBound tm bound) ∧ StepEnvelope tm bound final ∧ final stateReg = symbolCode (halted.output.cells 1) - 1

The verdict extractor stays in the core envelope and has the standard four-width-per-basic-instruction cost bound.

theorem Complexity.RAM.TMConfig.Sparse.repairCaptured_measured_internal {n : ℕ} {tm : TM n} {bound valueLimit : ℕ} {captured : List (ℕ × ℕ)} {store : Structured.Store} (hentries : ∀ entry ∈ captured, entry.1 ≤ bound + 1 ∧ entry.2 ≤ 1) (hnonempty : captured ≠ []) (henvelope : MarshalEnvelope tm bound valueLimit store) (hwordLimit : wordBound tm bound ≤ valueLimit) : ∃ (final : Structured.Store) (steps : ℕ), Structured.Internal.MeasuredRuns (repairCaptured n captured) store final steps (captured.length * (27 * (bitlen valueLimit + 1))) (Structured.Internal.envelopeSpace (registerBound n (bound + 1)) valueLimit) ∧ final = repairStore n captured store ∧ StepEnvelope tm bound final

theorem Complexity.RAM.TMConfig.Sparse.initializeConfigOps_measured_internal {n : ℕ} {tm : TM n} {bound : ℕ} {store : Structured.Store} (henvelope : StepEnvelope tm bound store) : have final := Structured.Basic.execList (initializeConfigOps tm) store; Structured.Internal.MeasuredRuns (Structured.Cmd.basics (initializeConfigOps tm)) store final (initializeConfigOps tm).length (4 * (initializeConfigOps tm).length * wordWidth tm bound) (spaceBound tm bound) ∧ StepEnvelope tm bound final

theorem Complexity.RAM.TMConfig.Sparse.marshalLeaf_measured_internal {n : ℕ} (tm : TM n) (x : List Bool) : ∃ (final : Structured.Store) (steps : ℕ), Structured.Internal.MeasuredRuns (marshalLeaf tm (capturedInput n x)) (initRegs x) final steps (marshalLeafTimeBound tm x.length) (spaceBound tm (marshalBound n x.length)) ∧ Represents tm (tm.initCfg x) final ∧ StepEnvelope tm (marshalBound n x.length) final

A selected capture-tree leaf carries the public input through copy, repair, and initialization within one concrete resource envelope.

theorem Complexity.RAM.TMConfig.Sparse.marshalInput_measured_internal {n : ℕ} (tm : TM n) (x : List Bool) : ∃ (final : Structured.Store) (steps : ℕ), Structured.Internal.MeasuredRuns (marshalInput tm) (initRegs x) final steps (marshalTimeBound tm x.length) (spaceBound tm (marshalBound n x.length)) ∧ Represents tm (tm.initCfg x) final ∧ StepEnvelope tm (marshalBound n x.length) final

The full public-input marshaller has a concrete resource certificate and hands the simulation core an exact sparse representation.

theorem Complexity.RAM.TMConfig.Sparse.decisionProgram_measured_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 : ℕ), Structured.Internal.MeasuredRuns (decisionProgram tm) (initRegs x) final sourceSteps (decisionTimeBound tm x.length steps) (spaceBound tm (marshalBound n x.length + steps)) ∧ final stateReg = symbolCode (halted.output.cells 1) - 1

End-to-end public-ABI execution with concrete time and space bounds.

theorem Complexity.RAM.TMConfig.Sparse.compiledDecision_resourceBound_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 ∧ 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 compiled-RAM transfer of the end-to-end resource certificate.