Public-input marshalling correctness -- proof internals

This file lifts the pointwise backward-copy facts to a loop invariant, repairs the finitely many captured scratch positions, and establishes the complete sparse representation of the Turing machine's initial configuration.

def Complexity.RAM.TMConfig.Sparse.marshalStart (n : ℕ) (x : List Bool) : Structured.Store

Store after installing the constants used by the backward-copy loop.

Equations

• Complexity.RAM.TMConfig.Sparse.marshalStart n x = Complexity.RAM.Structured.Basic.execList (Complexity.RAM.TMConfig.Sparse.marshalConstants n) (Complexity.RAM.initRegs x)

def Complexity.RAM.TMConfig.Sparse.MarshalInvariant (n : ℕ) (x : List Bool) (cursor : ℕ) (store : Structured.Store) : Prop

Semantic invariant after relocating positions |x|, …, cursor + 1. Uncaptured destinations are exact, captured destinations are at least marked positive, future uncaptured raw sources retain their public-ABI value, and all other data registers have their expected raw-or-zero contents.

Equations

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

theorem Complexity.RAM.TMConfig.Sparse.marshalStart_invariant_internal (n : ℕ) (x : List Bool) : MarshalInvariant n x x.length (marshalStart n x)

Installing loop constants establishes the invariant before any input position has been relocated.

theorem Complexity.RAM.TMConfig.Sparse.marshalLoopOps_invariant_internal (n : ℕ) (x : List Bool) (cursor : ℕ) (store : Structured.Store) (hcursor : 0 < cursor) (hinvariant : MarshalInvariant n x cursor store) : MarshalInvariant n x (cursor - 1) (Structured.Basic.execList (marshalLoopOps n) store)

One positive-cursor body advances the complete relocation invariant by one position, including an exact value for ordinary sources and a positive visited marker for captured scratch sources.

theorem Complexity.RAM.TMConfig.Sparse.marshalLoop_invariant_exec_internal (n : ℕ) (x : List Bool) (cursor : ℕ) (store : Structured.Store) (hinvariant : MarshalInvariant n x cursor store) : ∃ (final : Structured.Store) (cost : ℕ) (space : ℕ), Structured.Exec (marshalLoop n) store final (marshalLoopSteps n cursor) cost space ∧ MarshalInvariant n x 0 final

The complete backward loop executes once per input position and leaves the relocation invariant at cursor zero.

def Complexity.RAM.TMConfig.Sparse.repairBitStore (n : ℕ) (entry : ℕ × ℕ) (store : Structured.Store) : Structured.Store

Exact store selected by one captured-position repair command.

Equations

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

def Complexity.RAM.TMConfig.Sparse.repairStore (n : ℕ) : List (ℕ × ℕ) → Structured.Store → Structured.Store

Exact store selected by the recursive captured-position repair pass.

Equations

• Complexity.RAM.TMConfig.Sparse.repairStore n [] x✝ = x✝
• Complexity.RAM.TMConfig.Sparse.repairStore n (entry :: rest) x✝ = Complexity.RAM.TMConfig.Sparse.repairStore n rest (Complexity.RAM.TMConfig.Sparse.repairBitStore n entry x✝)

theorem Complexity.RAM.TMConfig.Sparse.repairCaptured_exec_internal (n : ℕ) (captured : List (ℕ × ℕ)) (store : Structured.Store) : ∃ (steps : ℕ) (cost : ℕ) (space : ℕ), Structured.Exec (repairCaptured n captured) store (repairStore n captured store) steps cost space

The recursive repair command has an exact structured execution.

theorem Complexity.RAM.TMConfig.Sparse.repairBitStore_data_internal (n : ℕ) (entry : ℕ × ℕ) (store : Structured.Store) (reg : ℕ) (hdata : cellBase n ≤ reg) : repairBitStore n entry store reg = if store (cellReg n (inputTape n) entry.1) = 0 then store reg else Function.update store (cellReg n (inputTape n) entry.1) (entry.2 + 1) reg

On data registers, one repair either preserves the store or updates exactly the selected input-cell destination.

theorem Complexity.RAM.TMConfig.Sparse.repairStore_data_of_not_mem_internal (n : ℕ) (captured : List (ℕ × ℕ)) (store : Structured.Store) (reg : ℕ) (hdata : cellBase n ≤ reg) (hnot : ∀ entry ∈ captured, reg ≠ cellReg n (inputTape n) entry.1) : repairStore n captured store reg = store reg

A repair list preserves a data register that is not one of its selected input-cell destinations.

theorem Complexity.RAM.TMConfig.Sparse.repairStore_selected_internal (n : ℕ) (captured : List (ℕ × ℕ)) (store : Structured.Store) (position value : ℕ) (hmem : (position, value) ∈ captured) (hnodup : (List.map Prod.fst captured).Nodup) (hpositive : 0 < store (cellReg n (inputTape n) position)) : repairStore n captured store (cellReg n (inputTape n) position) = value + 1

A visited destination selected exactly once by a repair list receives its captured Boolean value shifted to the sparse symbol code.

theorem Complexity.RAM.TMConfig.Sparse.repairStore_data_zero_internal (n : ℕ) (captured : List (ℕ × ℕ)) (store : Structured.Store) (reg : ℕ) (hdata : cellBase n ≤ reg) (hzero : store reg = 0) : repairStore n captured store reg = 0

A zero data register stays zero throughout every conditional repair, including when it is an unvisited captured destination.

def Complexity.RAM.TMConfig.Sparse.capturedInput (n : ℕ) (x : List Bool) : List (ℕ × ℕ)

Captured values selected for a public input.

Equations

• Complexity.RAM.TMConfig.Sparse.capturedInput n x = Complexity.RAM.TMConfig.Sparse.captureValues (Complexity.RAM.initRegs x) (Complexity.RAM.TMConfig.Sparse.captureRegs n) []

theorem Complexity.RAM.TMConfig.Sparse.repairStore_cells_internal (n : ℕ) (x : List Bool) (store : Structured.Store) (hinvariant : MarshalInvariant n x 0 store) : have repaired := repairStore n (capturedInput n x) store; (∀ (position : ℕ), 0 < position → repaired (cellReg n (inputTape n) position) = symbolCode ((Tape.init (List.map Γ.ofBool x)).cells position)) ∧ repaired (cellReg n (inputTape n) 0) = 0 ∧ ∀ (tape : Fin (n + 2)) (position : ℕ), tape ≠ inputTape n → repaired (cellReg n tape position) = 0

After captured-position repair, every positive input cell has its exact TM symbol code, cell zero is still temporarily blank, and all non-input tapes are still blank.

noncomputable def Complexity.RAM.TMConfig.Sparse.initializeStore {n : ℕ} (tm : TM n) (store : Structured.Store) : Structured.Store

Exact store after initializing state, heads, and all cell-zero markers.

Equations

• Complexity.RAM.TMConfig.Sparse.initializeStore tm store = Complexity.RAM.Structured.Basic.execList (Complexity.RAM.TMConfig.Sparse.initializeConfigOps tm) store

theorem Complexity.RAM.TMConfig.Sparse.initializeStore_represents_internal {n : ℕ} (tm : TM n) (x : List Bool) (store : Structured.Store) (hinvariant : MarshalInvariant n x 0 store) : Represents tm (tm.initCfg x) (initializeStore tm (repairStore n (capturedInput n x) store))

State, head, and left-marker initialization turns repaired tape data into the complete sparse representation of tm.initCfg x.

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

The selected capture-tree leaf executes the constant setup, exact backward copy, conditional repair, and semantic initialization, ending in a complete sparse representation of the TM's initial configuration.

theorem Complexity.RAM.TMConfig.Sparse.marshalInput_exec_internal {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 public-ABI marshaller follows the unique capture-tree path for the input and establishes the sparse initial TM configuration.