Bounded encoded sparse-store update — progress invariant internals

This file isolates the pure list semantics of the entry-update loop. The invariant relates the processed and remaining portions of the old store to the entries already emitted by the machine, independently of the tape-level simulation proof.

structure Complexity.RAM.RegisterStore.Machine.EntryUpdateProgress (store : Store) (address newValue : ℕ) (processed remaining emitted : Store) (found : Bool) (resultCount : ℕ) : Prop

Pure semantic progress of a left-to-right sparse-store update.

The output equation is deliberately phrased as a completion equation. Before the target address is found, completing the emitted prefix requires updating the remaining suffix. Afterwards, the untouched remaining suffix is copied verbatim.

• store_eq : store = processed ++ remaining

  The scan decomposition still covers the original store.

• found_iff : found = true ↔ address ∈ List.map Prod.fst processed

  The flag records exactly whether the processed prefix contains the requested address.

• output_eq : (emitted ++ if found = true then remaining else write remaining address newValue) = write store address newValue

  Completing the emitted prefix produces the abstract sparse-store write.

• resultCount_eq : resultCount = List.length emitted + List.length remaining

  Until the optional final append, the runtime result count equals emitted entries plus old entries still remaining.

theorem Complexity.RAM.RegisterStore.Machine.entryUpdateProgress_initial_internal (store : Store) (address newValue : ℕ) : EntryUpdateProgress store address newValue [] store [] false (List.length store)

Before scanning any entries, the empty emitted prefix satisfies the progress invariant.

theorem Complexity.RAM.RegisterStore.Machine.EntryUpdateProgress.miss_internal {store : Store} {address newValue : ℕ} {processed remaining emitted : Store} {entry : Entry} {found : Bool} {resultCount : ℕ} (h : EntryUpdateProgress store address newValue processed (entry :: remaining) emitted found resultCount) (hne : entry.1 ≠ address) : EntryUpdateProgress store address newValue (processed ++ [entry]) remaining (emitted ++ [entry]) found resultCount

Copying a nonmatching entry advances all three list frontiers without changing either the found flag or the result count.

theorem Complexity.RAM.RegisterStore.Machine.EntryUpdateProgress.replace_internal {store : Store} {address newValue : ℕ} {processed remaining emitted : Store} {entry : Entry} {resultCount : ℕ} (h : EntryUpdateProgress store address newValue processed (entry :: remaining) emitted false resultCount) (haddress : address = entry.1) (hvalue : newValue ≠ 0) : EntryUpdateProgress store address newValue (processed ++ [entry]) remaining (emitted ++ [(address, newValue)]) true resultCount

Replacing the first matching entry emits the new nonzero pair and records that the target address has been found.

theorem Complexity.RAM.RegisterStore.Machine.EntryUpdateProgress.delete_internal {store : Store} {address : ℕ} {processed remaining emitted : Store} {entry : Entry} {resultCount : ℕ} (h : EntryUpdateProgress store address 0 processed (entry :: remaining) emitted false resultCount) (haddress : address = entry.1) : EntryUpdateProgress store address 0 (processed ++ [entry]) remaining emitted true (resultCount - 1)

Deleting the first matching entry emits nothing for it, records the hit, and decrements the result count.

theorem Complexity.RAM.RegisterStore.Machine.EntryUpdateProgress.terminal_found_internal {store : Store} {address newValue : ℕ} {processed emitted : Store} {resultCount : ℕ} (h : EntryUpdateProgress store address newValue processed [] emitted true resultCount) : emitted = write store address newValue ∧ resultCount = List.length (write store address newValue)

Once the scan is exhausted after a hit, the emitted store and result count are already the abstract write result.

theorem Complexity.RAM.RegisterStore.Machine.EntryUpdateProgress.terminal_zero_internal {store : Store} {address : ℕ} {processed emitted : Store} {resultCount : ℕ} (h : EntryUpdateProgress store address 0 processed [] emitted false resultCount) : emitted = write store address 0 ∧ resultCount = List.length (write store address 0)

An absent address written with zero requires no append; exhaustion already produces the abstract empty write contribution.

theorem Complexity.RAM.RegisterStore.Machine.EntryUpdateProgress.terminal_append_internal {store : Store} {address newValue : ℕ} {processed emitted : Store} {resultCount : ℕ} (h : EntryUpdateProgress store address newValue processed [] emitted false resultCount) (hvalue : newValue ≠ 0) : emitted ++ [(address, newValue)] = write store address newValue ∧ resultCount + 1 = List.length (write store address newValue)

An absent address written with a nonzero value is completed by one final append and one result-count increment.

theorem Complexity.RAM.RegisterStore.Machine.EntryUpdateProgress.not_mem_remaining_of_found_internal {store : Store} {address newValue : ℕ} {processed remaining emitted : Store} {found : Bool} {resultCount : ℕ} (h : EntryUpdateProgress store address newValue processed remaining emitted found resultCount) (hnodup : AddressesNodup store) (hfound : found = true) : address ∉ List.map Prod.fst remaining

In a store with unique addresses, finding the target in the processed prefix excludes it from the unprocessed suffix.