Dense public input with a sparse mutable overlay

This module exposes the semantic representation used by the optimized RAM-to-Turing simulation. The immutable public input is not duplicated in the mutable snapshot; positive tags make explicit writes of zero distinguishable from an absent overlay entry.

theorem Complexity.RAM.RegisterStore.DenseOverlay.read_empty (input : List Bool) (address : ℕ) : read input [] address = initRegs input address

With no mutable entries, reads agree exactly with the public RAM input ABI.

theorem Complexity.RAM.RegisterStore.DenseOverlay.read_write (input : List Bool) (overlay : Store) (hcanonical : Canonical overlay) (address value : ℕ) : read input (write overlay address value) = Function.update (read input overlay) address value

A positive-tag overlay write implements functional update, including an explicit write of zero over a nonzero public-input bit.

theorem Complexity.RAM.RegisterStore.DenseOverlay.write_canonical (overlay : Store) (hcanonical : Canonical overlay) (address value : ℕ) : Canonical (write overlay address value)

Every overlay write preserves unique addresses and positive tags.

theorem Complexity.RAM.RegisterStore.DenseOverlay.write_coversZero (overlay : Store) (hcanonical : Canonical overlay) (hcovers : CoversZero overlay) (address value : ℕ) : CoversZero (write overlay address value)

Materializing a positive tag preserves the invariant that register zero never falls through to the dense input bank.

theorem Complexity.RAM.RegisterStore.DenseOverlay.Snapshot.initial_decode (input : List Bool) : decode input (initial input) = initCfg input

The empty mutable overlay already decodes to the complete public RAM input configuration.

theorem Complexity.RAM.RegisterStore.DenseOverlay.Snapshot.initial_canonical (input : List Bool) : Canonical (initial input).overlay

The initial one-entry overlay is canonical.

theorem Complexity.RAM.RegisterStore.DenseOverlay.Snapshot.initial_coversZero (input : List Bool) : CoversZero (initial input).overlay

The initial overlay materializes register zero.

theorem Complexity.RAM.RegisterStore.DenseOverlay.Snapshot.initial_valid (input : List Bool) : Valid (initial input).overlay

The initial overlay satisfies the full representation invariant.

theorem Complexity.RAM.RegisterStore.DenseOverlay.Snapshot.decode_stepInstr (input : List Bool) (instruction : Instr) (snapshot : Snapshot) (hcanonical : Canonical snapshot.overlay) : decode input (stepInstr input instruction snapshot) = RAM.stepInstr instruction (decode input snapshot)

Decoding commutes exactly with one selected instruction.

theorem Complexity.RAM.RegisterStore.DenseOverlay.Snapshot.stepInstr_canonical (input : List Bool) (instruction : Instr) (snapshot : Snapshot) (hcanonical : Canonical snapshot.overlay) : Canonical (stepInstr input instruction snapshot).overlay

One selected instruction preserves overlay canonicality.

theorem Complexity.RAM.RegisterStore.DenseOverlay.Snapshot.stepInstr_coversZero (input : List Bool) (instruction : Instr) (snapshot : Snapshot) (hvalid : Valid snapshot.overlay) : CoversZero (stepInstr input instruction snapshot).overlay

One selected instruction preserves materialization of register zero.

theorem Complexity.RAM.RegisterStore.DenseOverlay.Snapshot.stepInstr_valid (input : List Bool) (instruction : Instr) (snapshot : Snapshot) (hvalid : Valid snapshot.overlay) : Valid (stepInstr input instruction snapshot).overlay

One selected instruction preserves the full overlay invariant.

theorem Complexity.RAM.RegisterStore.DenseOverlay.Snapshot.decode_step (program : Program) (input : List Bool) (snapshot : Snapshot) (hcanonical : Canonical snapshot.overlay) : decode input (step program input snapshot) = RAM.step program (decode input snapshot)

Decoding commutes exactly with one program-selected RAM step.

theorem Complexity.RAM.RegisterStore.DenseOverlay.Snapshot.step_canonical (program : Program) (input : List Bool) (snapshot : Snapshot) (hcanonical : Canonical snapshot.overlay) : Canonical (step program input snapshot).overlay

Every program-selected step preserves overlay canonicality.

theorem Complexity.RAM.RegisterStore.DenseOverlay.Snapshot.step_valid (program : Program) (input : List Bool) (snapshot : Snapshot) (hvalid : Valid snapshot.overlay) : Valid (step program input snapshot).overlay

One program-selected step preserves the full overlay invariant.

theorem Complexity.RAM.RegisterStore.DenseOverlay.Snapshot.decode_run (program : Program) (input : List Bool) (fuel : ℕ) (snapshot : Snapshot) (hcanonical : Canonical snapshot.overlay) : decode input (run program input fuel snapshot) = RAM.run program fuel (decode input snapshot)

A complete fuel-bounded dense-overlay execution decodes to the ordinary RAM run.

theorem Complexity.RAM.RegisterStore.DenseOverlay.Snapshot.run_canonical (program : Program) (input : List Bool) (fuel : ℕ) (snapshot : Snapshot) (hcanonical : Canonical snapshot.overlay) : Canonical (run program input fuel snapshot).overlay

Every fuel-bounded dense-overlay execution remains canonical.

theorem Complexity.RAM.RegisterStore.DenseOverlay.Snapshot.run_valid (program : Program) (input : List Bool) (fuel : ℕ) (snapshot : Snapshot) (hvalid : Valid snapshot.overlay) : Valid (run program input fuel snapshot).overlay

A complete dense-overlay run preserves the full representation invariant.

theorem Complexity.RAM.RegisterStore.DenseOverlay.write_length_le (overlay : Store) (address value : ℕ) : List.length (write overlay address value) ≤ List.length overlay + 1

One tagged write adds at most one mutable overlay entry.

theorem Complexity.RAM.RegisterStore.DenseOverlay.Snapshot.length_stepInstr_le (input : List Bool) (instruction : Instr) (snapshot : Snapshot) : List.length (stepInstr input instruction snapshot).overlay ≤ List.length snapshot.overlay + 1

One selected instruction adds at most one mutable overlay entry.

theorem Complexity.RAM.RegisterStore.DenseOverlay.Snapshot.length_run_le (program : Program) (input : List Bool) (fuel : ℕ) (snapshot : Snapshot) (hcanonical : Canonical snapshot.overlay) : List.length (run program input fuel snapshot).overlay ≤ List.length snapshot.overlay + unitTimeUpto program fuel (decode input snapshot)

A dense-overlay run materializes at most one entry per executed RAM step.

theorem Complexity.RAM.RegisterStore.DenseOverlay.encodedStoreLength_write_le (overlay : Store) (address value : ℕ) : encodedStoreLength (write overlay address value) ≤ encodedStoreLength overlay + (Entry.encode (address, value + 1)).length

A tagged write increases the live overlay code by at most the code of its address and positive value tag.

theorem Complexity.RAM.RegisterStore.DenseOverlay.Snapshot.encodedStoreLength_stepInstr_le (input : List Bool) (instruction : Instr) (snapshot : Snapshot) : encodedStoreLength (stepInstr input instruction snapshot).overlay ≤ encodedStoreLength snapshot.overlay + 2 * (Instr.staticWidth instruction + instruction.logCost (decode input snapshot) + 1)

One selected instruction grows the actual live overlay code linearly in its fixed literal width and its logarithmic RAM charge.

theorem Complexity.RAM.RegisterStore.DenseOverlay.Snapshot.encodedStoreLength_step_le (program : Program) (input : List Bool) (snapshot : Snapshot) : encodedStoreLength (step program input snapshot).overlay ≤ encodedStoreLength snapshot.overlay + 2 * (programStaticWidth program + stepLogCost program (decode input snapshot) + 1)

One program-selected step satisfies the same live-code bound using the fixed program's maximum literal width.

theorem Complexity.RAM.RegisterStore.DenseOverlay.Snapshot.encodedStoreLength_run_le (program : Program) (input : List Bool) (fuel : ℕ) (snapshot : Snapshot) (hcanonical : Canonical snapshot.overlay) : encodedStoreLength (run program input fuel snapshot).overlay ≤ encodedStoreLength snapshot.overlay + 2 * (unitTimeUpto program fuel (decode input snapshot) * (programStaticWidth program + 1) + logTimeUpto program fuel (decode input snapshot))

The live mutable overlay has amortized encoded growth linear in the work actually charged by the RAM run; the immutable public input contributes no repeated sparse-store term.

theorem Complexity.RAM.RegisterStore.DenseOverlay.Snapshot.initial_length_run_le (program : Program) (input : List Bool) (fuel : ℕ) : List.length (run program input fuel (initial input)).overlay ≤ 1 + unitTimeUpto program fuel (initCfg input)

Starting from the public ABI, mutable entry count is bounded solely by the executed step count.

theorem Complexity.RAM.RegisterStore.DenseOverlay.Snapshot.initial_encodedStoreLength_run_le (program : Program) (input : List Bool) (fuel : ℕ) : encodedStoreLength (run program input fuel (initial input)).overlay ≤ 2 * bitlen (input.length + 1) + 2 + 2 * (unitTimeUpto program fuel (initCfg input) * (programStaticWidth program + 1) + logTimeUpto program fuel (initCfg input))

Starting from the public ABI, live mutable code is linear in accumulated RAM cost and carries no eager input.length * bitlen input.length term.

theorem Complexity.RAM.RegisterStore.DenseOverlay.Snapshot.initial_encode_length (input : List Bool) : (initial input).encode.length = 2 * bitlen (input.length + 1) + 6

The initial snapshot contains only the two headers and the tagged R₀ length entry; public input bits remain in the immutable bank.