Bounded encoded sparse-store update — loop invariant internals

structure Complexity.RAM.RegisterStore.Machine.EntryUpdateLoopInv {n : ℕ} (tapes : EntryUpdateTapes n) (store : Store) (address newValue : ℕ) (processed remaining emitted : Store) (found : Bool) (resultCount : ℕ) (initialWork work : Fin n → Tape) : Prop

Tape and list semantics carried between controller iterations.

• progress : EntryUpdateProgress store address newValue processed remaining emitted found resultCount
• ready : EntryScanReady tapes.entry (List.flatMap Entry.encode remaining) address.bits work work
• replacement : (work tapes.replacement).HasBinaryNat newValue
• replacement_eq : work tapes.replacement = initialWork tapes.replacement
• remainingCount : (work tapes.remaining).HasBinaryNat (List.length remaining)
• foundCount : (work tapes.found).HasBinaryNat (if found = true then 1 else 0)
• resultCountTape : (work tapes.resultCount).HasBinaryNat resultCount
• resultCount_le : resultCount ≤ List.length store
• frame : EntryUpdateFrame tapes initialWork work

theorem Complexity.RAM.RegisterStore.Machine.entryUpdateFrame_refl_internal {n : ℕ} (tapes : EntryUpdateTapes n) (work : Fin n → Tape) : EntryUpdateFrame tapes work work

The controller frame is reflexive.

theorem Complexity.RAM.RegisterStore.Machine.EntryUpdateFrame.trans_internal {n : ℕ} {tapes : EntryUpdateTapes n} {work₀ work₁ work₂ : Fin n → Tape} (h₁ : EntryUpdateFrame tapes work₀ work₁) (h₂ : EntryUpdateFrame tapes work₁ work₂) : EntryUpdateFrame tapes work₀ work₂

Controller frames compose.

theorem Complexity.RAM.RegisterStore.Machine.EntryUpdateFrame.markFound_internal {n : ℕ} {tapes : EntryUpdateTapes n} {initialWork work : Fin n → Tape} (h : EntryUpdateFrame tapes initialWork work) : EntryUpdateFrame tapes initialWork (entryUpdateMarkFoundWork tapes work)

Changing the found flag preserves the frame outside all controller tapes.

theorem Complexity.RAM.RegisterStore.Machine.EntryUpdateFrame.trans_ready_internal {n : ℕ} {tapes : EntryUpdateTapes n} {remaining queryBits : List Bool} {initialWork work finalWork : Fin n → Tape} (hframe : EntryUpdateFrame tapes initialWork work) (hready : EntryScanReady tapes.entry remaining queryBits work finalWork) : EntryUpdateFrame tapes initialWork finalWork

An entry-machine frame extends an existing controller frame.

theorem Complexity.RAM.RegisterStore.Machine.EntryUpdateFrame.trans_single_internal {n : ℕ} {tapes : EntryUpdateTapes n} {initialWork work finalWork : Fin n → Tape} (hframe : EntryUpdateFrame tapes initialWork work) (slot : Fin 13) (hother : ∀ (i : Fin n), i ≠ tapes.idx slot → finalWork i = work i) : EntryUpdateFrame tapes initialWork finalWork

A one-tape arithmetic frame extends an existing controller frame.

theorem Complexity.RAM.RegisterStore.Machine.entryUpdateLoopInv_initial_internal {n : ℕ} (tapes : EntryUpdateTapes n) (store : Store) (address newValue : ℕ) (work : Fin n → Tape) (hready : EntryScanReady tapes.entry (List.flatMap Entry.encode store) address.bits work work) (hreplacement : (work tapes.replacement).HasBinaryNat newValue) (hremaining : (work tapes.remaining).HasBinaryNat (List.length store)) (hfound : (work tapes.found).HasBinaryNat 0) (hresultCount : (work tapes.resultCount).HasBinaryNat (List.length store)) : EntryUpdateLoopInv tapes store address newValue [] store [] false (List.length store) work work

The public initial tape contract establishes the first loop invariant.