Sparse-entry replacement #

theorem Complexity.RAM.RegisterStore.Machine.entryReplaceCleanupTM_hoareTime_frame {n : ℕ} (tapes : EntryReplaceTapes n) (entry : Entry) (newValue : ℕ) (rest queryBits emitted : List Bool) (initialWork matchedWork : Fin n → Tape) (inp₀ out₀ : Tape) (hmatch : ReadableEntryMatch tapes.entry entry rest queryBits initialWork matchedWork) (hreplacement : (matchedWork tapes.replacement).HasBinaryNat newValue) (hinput : TM.Parked inp₀) (houtput : out₀.HasBinaryPrefix emitted) :

(entryReplaceCleanupTM tapes).HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = matchedWork ∧ out = out₀) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ EntryScanReady tapes.entry rest queryBits initialWork work ∧ work tapes.replacement = matchedWork tapes.replacement ∧ out.HasBinaryPrefix (emitted ++ Entry.encode (entry.1, newValue))) (entryReplaceCleanupTime tapes entry newValue queryBits initialWork matchedWork)

Emit a matched address with a canonical replacement value, restore that external value source, and clear all entry scratch for the next iteration.

Replacement emission and cleanup are append-only on the output tape.

theorem Complexity.RAM.RegisterStore.Machine.entryReplaceCleanupTM_prefix_withinAuxSpace {n : ℕ} (tapes : EntryReplaceTapes n) (entry : Entry) (newValue : ℕ) (queryBits : List Bool) (initialWork matchedWork : Fin n → Tape) (inputLength initialSpace time : ℕ) (start current : Complexity.Cfg n (entryReplaceCleanupTM tapes).Q) (hinitial : start.WithinAuxSpace inputLength initialSpace) (hreach : (entryReplaceCleanupTM tapes).reachesIn time start current) (htime : time ≤ entryReplaceCleanupTime tapes entry newValue queryBits initialWork matchedWork) :

current.WithinAuxSpace inputLength (initialSpace + entryReplaceCleanupTime tapes entry newValue queryBits initialWork matchedWork)

Coarse all-prefix auxiliary-space envelope for replacement and cleanup.

Documentation