Sparse RAM register stores on Turing tapes: proof internals

This module proves the finite-store semantics and codec round trips exposed by the surface module. It is not part of the human-audited definitions layer.

theorem Complexity.RAM.RegisterStore.read_write_internal (store : Store) (hstore : AddressesNodup store) (address value target : ℕ) : read (write store address value) target = Function.update (read store) address value target

theorem Complexity.RAM.RegisterStore.write_addressesNodup_internal (store : Store) (hstore : AddressesNodup store) (address value : ℕ) : AddressesNodup (write store address value)

theorem Complexity.RAM.RegisterStore.write_valuesNonzero_internal (store : Store) (hstore : ValuesNonzero store) (address value : ℕ) : ValuesNonzero (write store address value)

theorem Complexity.RAM.RegisterStore.write_canonical_internal (store : Store) (hstore : Canonical store) (address value : ℕ) : Canonical (write store address value)

theorem Complexity.RAM.RegisterStore.decode_write_internal (store : Store) (hstore : AddressesNodup store) (address value : ℕ) : decode (write store address value) = Function.update (decode store) address value

theorem Complexity.RAM.RegisterStore.ofRegs_canonical_internal (regs : ℕ → ℕ) (hfinite : (Function.support regs).Finite) : Canonical (ofRegs regs hfinite)

theorem Complexity.RAM.RegisterStore.decode_ofRegs_internal (regs : ℕ → ℕ) (hfinite : (Function.support regs).Finite) : decode (ofRegs regs hfinite) = regs

theorem Complexity.RAM.RegisterStore.ofRegs_represents_internal (regs : ℕ → ℕ) (hfinite : (Function.support regs).Finite) : Represents (ofRegs regs hfinite) regs

theorem Complexity.RAM.RegisterStore.initialStore_canonical_internal (input : List Bool) : Canonical (initialStore input)

theorem Complexity.RAM.RegisterStore.decode_initialStore_internal (input : List Bool) : decode (initialStore input) = initRegs input

theorem Complexity.RAM.RegisterStore.Snapshot.initial_represents_internal (input : List Bool) : (initial input).Represents (initCfg input)

theorem Complexity.RAM.RegisterStore.initialStore_length_le_internal (input : List Bool) : List.length (initialStore input) ≤ input.length + 1

theorem Complexity.RAM.RegisterStore.Snapshot.initial_width_le_internal (input : List Bool) : (initial input).width ≤ bitlen (input.length + 1)

theorem Complexity.RAM.RegisterStore.Snapshot.ofCfg_represents_internal (cfg : Cfg) (hfinite : (Function.support cfg.regs).Finite) : (ofCfg cfg hfinite).Represents cfg

theorem Complexity.RAM.RegisterStore.Snapshot.stepInstr_canonical_internal (instruction : Instr) (snapshot : Snapshot) (hcanonical : Canonical snapshot.store) : Canonical (stepInstr instruction snapshot).store

theorem Complexity.RAM.RegisterStore.Snapshot.decode_stepInstr_internal (instruction : Instr) (snapshot : Snapshot) (hcanonical : Canonical snapshot.store) : (stepInstr instruction snapshot).decode = RAM.stepInstr instruction snapshot.decode

theorem Complexity.RAM.RegisterStore.Snapshot.curInstr_decode_internal (program : Program) (snapshot : Snapshot) : RAM.curInstr program snapshot.decode = curInstr program snapshot

theorem Complexity.RAM.RegisterStore.Snapshot.halted_decode_iff_internal (program : Program) (snapshot : Snapshot) : RAM.Halted program snapshot.decode ↔ Halted program snapshot

theorem Complexity.RAM.RegisterStore.Snapshot.step_canonical_internal (program : Program) (snapshot : Snapshot) (hcanonical : Canonical snapshot.store) : Canonical (step program snapshot).store

theorem Complexity.RAM.RegisterStore.Snapshot.decode_step_internal (program : Program) (snapshot : Snapshot) (hcanonical : Canonical snapshot.store) : (step program snapshot).decode = RAM.step program snapshot.decode

theorem Complexity.RAM.RegisterStore.Snapshot.run_canonical_internal (program : Program) (fuel : ℕ) (snapshot : Snapshot) (hcanonical : Canonical snapshot.store) : Canonical (run program fuel snapshot).store

theorem Complexity.RAM.RegisterStore.Snapshot.decode_run_internal (program : Program) (fuel : ℕ) (snapshot : Snapshot) (hcanonical : Canonical snapshot.store) : (run program fuel snapshot).decode = RAM.run program fuel snapshot.decode

theorem Complexity.RAM.RegisterStore.Snapshot.width_stepInstr_le_internal (instruction : Instr) (snapshot : Snapshot) : (stepInstr instruction snapshot).width ≤ stepWidthBound instruction snapshot

theorem Complexity.RAM.RegisterStore.Snapshot.width_step_le_internal (program : Program) (snapshot : Snapshot) : (step program snapshot).width ≤ max (snapshot.width + 1) (max (programStaticWidth program) (stepLogCost program snapshot.decode))

theorem Complexity.RAM.RegisterStore.Snapshot.length_stepInstr_le_internal (instruction : Instr) (snapshot : Snapshot) : List.length (stepInstr instruction snapshot).store ≤ List.length snapshot.store + 1

theorem Complexity.RAM.RegisterStore.Snapshot.length_run_le_internal (program : Program) (fuel : ℕ) (snapshot : Snapshot) (hcanonical : Canonical snapshot.store) : List.length (run program fuel snapshot).store ≤ List.length snapshot.store + unitTimeUpto program fuel snapshot.decode

theorem Complexity.RAM.RegisterStore.Snapshot.width_run_le_internal (program : Program) (fuel : ℕ) (snapshot : Snapshot) (hcanonical : Canonical snapshot.store) : (run program fuel snapshot).width ≤ snapshot.width + unitTimeUpto program fuel snapshot.decode * (programStaticWidth program + 1) + logTimeUpto program fuel snapshot.decode

theorem Complexity.RAM.RegisterStore.WordCode.decodePrefix?_encode_append_internal (value : ℕ) (suffix : List Bool) : decodePrefix? (encode value ++ suffix) = some (value, suffix)

theorem Complexity.RAM.RegisterStore.WordCode.decodePrefix?_encode_internal (value : ℕ) : decodePrefix? (encode value) = some (value, [])

theorem Complexity.RAM.RegisterStore.WordCode.encode_length_internal (value : ℕ) : (encode value).length = 2 * bitlen value + 1

theorem Complexity.RAM.RegisterStore.Entry.decodePrefix?_encode_append_internal (entry : Entry) (suffix : List Bool) : decodePrefix? (entry.encode ++ suffix) = some (entry, suffix)

theorem Complexity.RAM.RegisterStore.Entry.encode_length_internal (entry : Entry) : entry.encode.length = 2 * bitlen entry.1 + 2 * bitlen entry.2 + 2

theorem Complexity.RAM.RegisterStore.encodedStoreLength_write_le_internal (store : Store) (address value : ℕ) : encodedStoreLength (write store address value) ≤ encodedStoreLength store + (Entry.encode (address, value)).length

theorem Complexity.RAM.RegisterStore.Snapshot.encodedStoreLength_run_le_internal (program : Program) (fuel : ℕ) (snapshot : Snapshot) (hcanonical : Canonical snapshot.store) : encodedStoreLength (run program fuel snapshot).store ≤ encodedStoreLength snapshot.store + 4 * (unitTimeUpto program fuel snapshot.decode * (programStaticWidth program + 1) + logTimeUpto program fuel snapshot.decode)

theorem Complexity.RAM.RegisterStore.decodeEntries?_encode_append_internal (store : Store) (suffix : List Bool) : decodeEntries? (List.length store) (List.flatMap Entry.encode store ++ suffix) = some (store, suffix)

theorem Complexity.RAM.RegisterStore.Snapshot.decodePrefix?_encode_append_internal (snapshot : Snapshot) (suffix : List Bool) : decodePrefix? (snapshot.encode ++ suffix) = some (snapshot, suffix)

theorem Complexity.RAM.RegisterStore.Snapshot.decodePrefix?_encode_internal (snapshot : Snapshot) : decodePrefix? snapshot.encode = some (snapshot, [])

theorem Complexity.RAM.RegisterStore.Snapshot.decode?_encode_internal (snapshot : Snapshot) : decode? snapshot.encode = some snapshot

theorem Complexity.RAM.RegisterStore.Snapshot.encode_length_le_internal (snapshot : Snapshot) (width : ℕ) (hpc : bitlen snapshot.pc ≤ width) (hcount : bitlen (List.length snapshot.store) ≤ width) (hstore : ∀ entry ∈ snapshot.store, bitlen entry.1 ≤ width ∧ bitlen entry.2 ≤ width) : snapshot.encode.length ≤ (List.length snapshot.store + 1) * (4 * width + 2)

theorem Complexity.RAM.RegisterStore.encodedStoreLength_initial_le_internal (input : List Bool) : encodedStoreLength (initialStore input) ≤ (input.length + 1) * (4 * bitlen (input.length + 1) + 2)

theorem Complexity.RAM.RegisterStore.Snapshot.encode_length_le_sizeBound_internal (snapshot : Snapshot) : snapshot.encode.length ≤ snapshot.sizeBound

theorem Complexity.RAM.RegisterStore.Snapshot.encode_length_le_encodedStore_internal (snapshot : Snapshot) : snapshot.encode.length ≤ encodedStoreLength snapshot.store + 4 * snapshot.width + 2

theorem Complexity.RAM.RegisterStore.Snapshot.encode_run_length_le_amortized_internal (program : Program) (fuel : ℕ) (snapshot : Snapshot) (hcanonical : Canonical snapshot.store) : (run program fuel snapshot).encode.length ≤ encodedStoreLength snapshot.store + 4 * snapshot.width + 8 * (unitTimeUpto program fuel snapshot.decode * (programStaticWidth program + 1) + logTimeUpto program fuel snapshot.decode) + 2

theorem Complexity.RAM.RegisterStore.Snapshot.encode_initial_run_length_le_amortized_internal (program : Program) (fuel : ℕ) (input : List Bool) : (run program fuel (initial input)).encode.length ≤ (input.length + 1) * (4 * bitlen (input.length + 1) + 2) + 4 * bitlen (input.length + 1) + 8 * (logTimeUpto program fuel (initCfg input) * (programStaticWidth program + 2)) + 2

theorem Complexity.RAM.RegisterStore.Snapshot.encode_run_length_le_internal (program : Program) (fuel : ℕ) (snapshot : Snapshot) (hcanonical : Canonical snapshot.store) : (run program fuel snapshot).encode.length ≤ (List.length snapshot.store + unitTimeUpto program fuel snapshot.decode + 1) * (4 * (snapshot.width + unitTimeUpto program fuel snapshot.decode * (programStaticWidth program + 1) + logTimeUpto program fuel snapshot.decode) + 2)

theorem Complexity.RAM.RegisterStore.Snapshot.encode_run_length_le_logTime_internal (program : Program) (fuel : ℕ) (snapshot : Snapshot) (hcanonical : Canonical snapshot.store) : (run program fuel snapshot).encode.length ≤ (List.length snapshot.store + logTimeUpto program fuel snapshot.decode + 1) * (4 * (snapshot.width + logTimeUpto program fuel snapshot.decode * (programStaticWidth program + 1) + logTimeUpto program fuel snapshot.decode) + 2)

theorem Complexity.RAM.RegisterStore.Snapshot.encode_initial_run_length_le_logTime_internal (program : Program) (fuel : ℕ) (input : List Bool) : (run program fuel (initial input)).encode.length ≤ (input.length + 1 + logTimeUpto program fuel (initCfg input) + 1) * (4 * (bitlen (input.length + 1) + logTimeUpto program fuel (initCfg input) * (programStaticWidth program + 1) + logTimeUpto program fuel (initCfg input)) + 2)