Sparse register lookup — definitions

The bounded scanner is already the concrete lookup machine. This module names its semantic endpoint in terms of the pure sparse-store read operation.

structure Complexity.RAM.RegisterStore.Machine.EntryLookupResult {n : ℕ} (tapes : EntryScanTapes n) (store : Store) (address : ℕ) (initialWork finalWork : Fin n → Tape) : Prop

A completed lookup leaves the pure sparse-store value on the decoded-value tape and preserves the scanner's complete external frame.

• value : (finalWork tapes.entry.value).HasBinaryPrefix (read store address).bits
• valueStart : (finalWork tapes.entry.value).cells 0 = Γ.start
• count : ∃ remaining ≤ List.length store, (finalWork tapes.count).HasBinaryNat remaining

  The runtime counter records the unscanned suffix beginning at a hit, or zero after an unsuccessful scan.

• parked (i : Fin n) : TM.Parked (finalWork i)
• frame : EntryScanFrame tapes initialWork finalWork
• outcome : EntryScanOutcome tapes store address.bits initialWork finalWork

  The complete scanner endpoint is retained so a caller can restore every owned cursor and scratch tape without re-proving the scan decomposition.

@[reducible, inline]

abbrev Complexity.RAM.RegisterStore.Machine.entryLookupTM {n : ℕ} (tapes : EntryScanTapes n) : TM n

The concrete sparse lookup is the fixed runtime-count entry scanner.

Equations

• Complexity.RAM.RegisterStore.Machine.entryLookupTM tapes = Complexity.RAM.RegisterStore.Machine.entryScanTM tapes

@[reducible, inline]

abbrev Complexity.RAM.RegisterStore.Machine.entryLookupTime {n : ℕ} (tapes : EntryScanTapes n) (address : ℕ) (store : Store) : ℕ

Lookup inherits the scanner's explicit runtime bound.

Equations

• Complexity.RAM.RegisterStore.Machine.entryLookupTime tapes address store = Complexity.RAM.RegisterStore.Machine.entryScanTime tapes address.bits store