Bounded encoded sparse-store update

This module exposes the complete fixed-controller implementation of one canonical sparse-store write. The machine scans a runtime-counted old store, copies misses, replaces or deletes the unique hit, and appends a fresh nonzero entry exactly when the address was absent.

theorem Complexity.RAM.RegisterStore.Machine.entryUpdateTM_source_readOnly {n : ℕ} (tapes : EntryUpdateTapes n) : (entryUpdateTM tapes).WorkReadOnly tapes.entry.source

The encoded source cursor may move during an update, but its complete cell contents are read-only.

theorem Complexity.RAM.RegisterStore.Machine.entryUpdateTM_hoareTime_frame {n : ℕ} (tapes : EntryUpdateTapes n) (store : Store) (address newValue : ℕ) (emittedBits : List Bool) (initialWork : Fin n → Tape) (inp₀ out₀ : Tape) (hcanonical : Canonical store) (hready : EntryScanReady tapes.entry (List.flatMap Entry.encode store) address.bits initialWork initialWork) (hreplacement : (initialWork tapes.replacement).HasBinaryNat newValue) (hremaining : (initialWork tapes.remaining).HasBinaryNat (List.length store)) (hfound : (initialWork tapes.found).HasBinaryNat 0) (hresultCount : (initialWork tapes.resultCount).HasBinaryNat (List.length store)) (hinput : TM.Parked inp₀) (houtput : out₀.HasBinaryPrefix emittedBits) : (entryUpdateTM tapes).HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = initialWork ∧ out = out₀) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ EntryUpdateOutcome tapes store address newValue initialWork work ∧ out.HasBinaryPrefix (emittedBits ++ List.flatMap Entry.encode (write store address newValue)) ∧ (work tapes.entry.source).cells = (initialWork tapes.entry.source).cells) (entryUpdateTime tapes store address newValue)

Update one runtime-sized canonical sparse store. The output appends exactly the encoding of RegisterStore.write; input, the replacement source, and every work tape outside the thirteen-tape assignment retain their checked frames.

theorem Complexity.RAM.RegisterStore.Machine.entryUpdateTM_retargetOutput_hoareTime_frame {n : ℕ} (tapes : EntryUpdateTapes n) (store : Store) (address newValue : ℕ) (emittedBits : List Bool) (initialWork : Fin (n + 1) → Tape) (inp₀ : Tape) (hcanonical : Canonical store) (hready : EntryScanReady tapes.entry (List.flatMap Entry.encode store) address.bits (fun (i : Fin n) => initialWork i.castSucc) fun (i : Fin n) => initialWork i.castSucc) (hreplacement : (initialWork tapes.replacement.castSucc).HasBinaryNat newValue) (hremaining : (initialWork tapes.remaining.castSucc).HasBinaryNat (List.length store)) (hfound : (initialWork tapes.found.castSucc).HasBinaryNat 0) (hresultCount : (initialWork tapes.resultCount.castSucc).HasBinaryNat (List.length store)) (hinput : TM.Parked inp₀) (hbuffer : (initialWork (Fin.last n)).HasBinaryPrefix emittedBits) : (entryUpdateTM tapes).retargetOutput.HoareTime (fun (inp : Tape) (work : Fin (n + 1) → Tape) (out : Tape) => inp = inp₀ ∧ work = initialWork ∧ out = (Tape.init []).move Dir3.right) (fun (inp : Tape) (work : Fin (n + 1) → Tape) (out : Tape) => inp = inp₀ ∧ (EntryUpdateOutcome tapes store address newValue (fun (i : Fin n) => initialWork i.castSucc) fun (i : Fin n) => work i.castSucc) ∧ (work (Fin.last n)).HasBinaryPrefix (emittedBits ++ List.flatMap Entry.encode (write store address newValue)) ∧ (work tapes.entry.source.castSucc).cells = (initialWork tapes.entry.source.castSucc).cells ∧ out = (Tape.init []).move Dir3.right) (entryUpdateTime tapes store address newValue)

Redirect an encoded sparse-store update into a fresh last work tape. This is the stable seam used by the multi-step RAM interpreter: the real output is left blank while the updated store becomes an ordinary work-tape buffer.

theorem Complexity.RAM.RegisterStore.Machine.entryUpdateTM_isTransducer {n : ℕ} (tapes : EntryUpdateTapes n) : (entryUpdateTM tapes).IsTransducer

The sparse-store update controller is append-only on its output tape.

theorem Complexity.RAM.RegisterStore.Machine.entryUpdateTM_prefix_withinAuxSpace {n : ℕ} (tapes : EntryUpdateTapes n) (store : Store) (address newValue inputLength initialSpace time : ℕ) (start current : Complexity.Cfg n (entryUpdateTM tapes).Q) (hinitial : start.WithinAuxSpace inputLength initialSpace) (hreach : (entryUpdateTM tapes).reachesIn time start current) (htime : time ≤ entryUpdateTime tapes store address newValue) : current.WithinAuxSpace inputLength (initialSpace + entryUpdateTime tapes store address newValue)

Coarse all-prefix auxiliary-space envelope for one complete update.

theorem Complexity.RAM.RegisterStore.Machine.entryUpdateTime_le_encoded {n : ℕ} (tapes : EntryUpdateTapes n) (store : Store) (address newValue : ℕ) : entryUpdateTime tapes store address newValue ≤ 1000 * (encodedStoreLength store + (List.length store + 1) * (bitlen address + bitlen newValue + bitlen (List.length store) + 1) + 1)

A complete sparse update is charged by the entries actually traversed and the query, replacement, and remaining-count widths reserved at each iteration. This avoids the former product of entry count with a squared run-wide width.