Reusable sparse-register operand lookup -- definitions

One RAM instruction may need several direct or indirect register reads. This module gives lookup a reusable phase boundary: it loads a query from a canonical source, scans the encoded store, copies out the decoded value, resets all scanner scratch, rewinds the source, and restores the runtime entry count.

structure Complexity.RAM.RegisterStore.Machine.EntryLookupRestoreTapes (n : ℕ) : Type

Fourteen pairwise-distinct tapes for a reusable sparse operand lookup. Slots 0..9 are the bounded scanner; the final four slots preserve the entry count, supply the query, receive the value, and provide zero copy scratch.

• idx : Fin 14 → Fin n

  Physical work tape assigned to each logical lookup role.

• injective : Function.Injective self.idx

  Distinct logical lookup roles occupy distinct physical tapes.

def Complexity.RAM.RegisterStore.Machine.EntryLookupRestoreTapes.scan {n : ℕ} (tapes : EntryLookupRestoreTapes n) : EntryScanTapes n

Bounded scanner view of the reusable lookup assignment.

Equations

• tapes.scan = { entry := { idx := fun (i : Fin 9) => tapes.idx ⟨↑i, ⋯⟩, injective := ⋯ }, count := tapes.idx 9, count_ne := ⋯ }

@[simp]

theorem Complexity.RAM.RegisterStore.Machine.EntryLookupRestoreTapes.scan_entry_idx {n : ℕ} (tapes : EntryLookupRestoreTapes n) (slot : Fin 9) : tapes.scan.entry.idx slot = tapes.idx ⟨↑slot, ⋯⟩

@[simp]

theorem Complexity.RAM.RegisterStore.Machine.EntryLookupRestoreTapes.scan_count {n : ℕ} (tapes : EntryLookupRestoreTapes n) : tapes.scan.count = tapes.idx 9

def Complexity.RAM.RegisterStore.Machine.EntryLookupRestoreTapes.countSource {n : ℕ} (tapes : EntryLookupRestoreTapes n) : Fin n

Preserved canonical copy of the store cardinality.

Equations

• tapes.countSource = tapes.idx 10

def Complexity.RAM.RegisterStore.Machine.EntryLookupRestoreTapes.querySource {n : ℕ} (tapes : EntryLookupRestoreTapes n) : Fin n

Canonical address supplied to this lookup.

Equations

• tapes.querySource = tapes.idx 11

def Complexity.RAM.RegisterStore.Machine.EntryLookupRestoreTapes.destination {n : ℕ} (tapes : EntryLookupRestoreTapes n) : Fin n

Canonical destination receiving the looked-up register value.

Equations

• tapes.destination = tapes.idx 12

def Complexity.RAM.RegisterStore.Machine.EntryLookupRestoreTapes.copyScratch {n : ℕ} (tapes : EntryLookupRestoreTapes n) : Fin n

Preserved zero tape used by width-linear binary copying.

Equations

• tapes.copyScratch = tapes.idx 13

theorem Complexity.RAM.RegisterStore.Machine.EntryLookupRestoreTapes.ne {n : ℕ} (tapes : EntryLookupRestoreTapes n) {i j : Fin 14} (hne : i ≠ j) : tapes.idx i ≠ tapes.idx j

Inequality of logical slots gives inequality of physical tapes.

theorem Complexity.RAM.RegisterStore.Machine.EntryLookupRestoreTapes.scan_ne_external {n : ℕ} (tapes : EntryLookupRestoreTapes n) (slot : Fin 10) (external : Fin 4) : tapes.idx ⟨↑slot, ⋯⟩ ≠ tapes.idx ⟨↑external + 10, ⋯⟩

Every scanner tape is distinct from an external reusable-lookup role.

theorem Complexity.RAM.RegisterStore.Machine.EntryLookupRestoreTapes.countSource_ne_querySource {n : ℕ} (tapes : EntryLookupRestoreTapes n) : tapes.countSource ≠ tapes.querySource

theorem Complexity.RAM.RegisterStore.Machine.EntryLookupRestoreTapes.countSource_ne_destination {n : ℕ} (tapes : EntryLookupRestoreTapes n) : tapes.countSource ≠ tapes.destination

theorem Complexity.RAM.RegisterStore.Machine.EntryLookupRestoreTapes.countSource_ne_copyScratch {n : ℕ} (tapes : EntryLookupRestoreTapes n) : tapes.countSource ≠ tapes.copyScratch

theorem Complexity.RAM.RegisterStore.Machine.EntryLookupRestoreTapes.querySource_ne_destination {n : ℕ} (tapes : EntryLookupRestoreTapes n) : tapes.querySource ≠ tapes.destination

theorem Complexity.RAM.RegisterStore.Machine.EntryLookupRestoreTapes.querySource_ne_copyScratch {n : ℕ} (tapes : EntryLookupRestoreTapes n) : tapes.querySource ≠ tapes.copyScratch

theorem Complexity.RAM.RegisterStore.Machine.EntryLookupRestoreTapes.destination_ne_copyScratch {n : ℕ} (tapes : EntryLookupRestoreTapes n) : tapes.destination ≠ tapes.copyScratch

def Complexity.RAM.RegisterStore.Machine.EntryLookupRestoreTapes.resetSlot (slot : Fin 9) : Fin 14

Logical parent slots reset after one lookup.

Equations

• Complexity.RAM.RegisterStore.Machine.EntryLookupRestoreTapes.resetSlot slot = match ↑slot with | 0 => 1 | 1 => 2 | 2 => 3 | 3 => 4 | 4 => 5 | 5 => 6 | 6 => 8 | 7 => 7 | x => 9

def Complexity.RAM.RegisterStore.Machine.EntryLookupRestoreTapes.resetIdx {n : ℕ} (tapes : EntryLookupRestoreTapes n) (slot : Fin 9) : Fin n

Physical reset target selected by a finite logical slot.

Equations

• tapes.resetIdx slot = tapes.idx (Complexity.RAM.RegisterStore.Machine.EntryLookupRestoreTapes.resetSlot slot)

theorem Complexity.RAM.RegisterStore.Machine.EntryLookupRestoreTapes.resetIdx_injective {n : ℕ} (tapes : EntryLookupRestoreTapes n) : Function.Injective tapes.resetIdx

@[simp]

theorem Complexity.RAM.RegisterStore.Machine.EntryLookupRestoreTapes.resetIdx_zero {n : ℕ} (tapes : EntryLookupRestoreTapes n) : tapes.resetIdx 0 = tapes.scan.entry.address

@[simp]

theorem Complexity.RAM.RegisterStore.Machine.EntryLookupRestoreTapes.resetIdx_one {n : ℕ} (tapes : EntryLookupRestoreTapes n) : tapes.resetIdx 1 = tapes.scan.entry.value

@[simp]

theorem Complexity.RAM.RegisterStore.Machine.EntryLookupRestoreTapes.resetIdx_two {n : ℕ} (tapes : EntryLookupRestoreTapes n) : tapes.resetIdx 2 = tapes.scan.entry.addressCounter

@[simp]

theorem Complexity.RAM.RegisterStore.Machine.EntryLookupRestoreTapes.resetIdx_three {n : ℕ} (tapes : EntryLookupRestoreTapes n) : tapes.resetIdx 3 = tapes.scan.entry.addressWidth

@[simp]

theorem Complexity.RAM.RegisterStore.Machine.EntryLookupRestoreTapes.resetIdx_four {n : ℕ} (tapes : EntryLookupRestoreTapes n) : tapes.resetIdx 4 = tapes.scan.entry.valueCounter

@[simp]

theorem Complexity.RAM.RegisterStore.Machine.EntryLookupRestoreTapes.resetIdx_five {n : ℕ} (tapes : EntryLookupRestoreTapes n) : tapes.resetIdx 5 = tapes.scan.entry.valueWidth

@[simp]

theorem Complexity.RAM.RegisterStore.Machine.EntryLookupRestoreTapes.resetIdx_six {n : ℕ} (tapes : EntryLookupRestoreTapes n) : tapes.resetIdx 6 = tapes.scan.entry.result

@[simp]

theorem Complexity.RAM.RegisterStore.Machine.EntryLookupRestoreTapes.resetIdx_seven {n : ℕ} (tapes : EntryLookupRestoreTapes n) : tapes.resetIdx 7 = tapes.scan.entry.query

@[simp]

theorem Complexity.RAM.RegisterStore.Machine.EntryLookupRestoreTapes.resetIdx_eight {n : ℕ} (tapes : EntryLookupRestoreTapes n) : tapes.resetIdx 8 = tapes.scan.count

def Complexity.RAM.RegisterStore.Machine.entryLookupResetTargets {n : ℕ} (tapes : EntryLookupRestoreTapes n) : List (Fin n)

Scanner-owned tapes reset after copying out a lookup result. The encoded source is deliberately excluded because it is read-only and merely rewound.

Equations

• Complexity.RAM.RegisterStore.Machine.entryLookupResetTargets tapes = List.ofFn tapes.resetIdx

def Complexity.RAM.RegisterStore.Machine.entryLookupEntryWidth (entry : Entry) (address : ℕ) : ℕ

Width envelope for every binary scratch value at a successful hit on one entry.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.RAM.RegisterStore.Machine.entryLookupStoreWidth (address : ℕ) : Store → ℕ

Width envelope contributed by possible hit entries in a complete store.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.RAM.RegisterStore.Machine.entryLookupStoreWidth address [] = address.bits.length

def Complexity.RAM.RegisterStore.Machine.entryLookupResetWidth (store : Store) (address : ℕ) : ℕ

Width envelope for every hit or miss reset target in a complete store.

Equations

• Complexity.RAM.RegisterStore.Machine.entryLookupResetWidth store address = max (List.length store).bits.length (Complexity.RAM.RegisterStore.Machine.entryLookupStoreWidth address store)

def Complexity.RAM.RegisterStore.Machine.entryLookupFoundBits {n : ℕ} (tapes : EntryLookupRestoreTapes n) (entry : Entry) (remaining address : ℕ) (i : Fin n) : List Bool

Exact reset contents at a successful lookup endpoint.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.RAM.RegisterStore.Machine.entryLookupMissBits {n : ℕ} (tapes : EntryLookupRestoreTapes n) (address : ℕ) (i : Fin n) : List Bool

Exact reset contents at an unsuccessful lookup endpoint.

Equations

• Complexity.RAM.RegisterStore.Machine.entryLookupMissBits tapes address i = if i = tapes.scan.entry.query then address.bits else []

@[simp]

theorem Complexity.RAM.RegisterStore.Machine.entryLookupFoundBits_zero {n : ℕ} (tapes : EntryLookupRestoreTapes n) (entry : Entry) (remaining address : ℕ) : entryLookupFoundBits tapes entry remaining address tapes.scan.entry.address = entry.1.bits

@[simp]

theorem Complexity.RAM.RegisterStore.Machine.entryLookupFoundBits_one {n : ℕ} (tapes : EntryLookupRestoreTapes n) (entry : Entry) (remaining address : ℕ) : entryLookupFoundBits tapes entry remaining address tapes.scan.entry.value = entry.2.bits

@[simp]

theorem Complexity.RAM.RegisterStore.Machine.entryLookupFoundBits_two {n : ℕ} (tapes : EntryLookupRestoreTapes n) (entry : Entry) (remaining address : ℕ) : entryLookupFoundBits tapes entry remaining address tapes.scan.entry.addressCounter = List.replicate (bitlen entry.1) true

@[simp]

theorem Complexity.RAM.RegisterStore.Machine.entryLookupFoundBits_three {n : ℕ} (tapes : EntryLookupRestoreTapes n) (entry : Entry) (remaining address : ℕ) : entryLookupFoundBits tapes entry remaining address tapes.scan.entry.addressWidth = []

@[simp]

theorem Complexity.RAM.RegisterStore.Machine.entryLookupFoundBits_four {n : ℕ} (tapes : EntryLookupRestoreTapes n) (entry : Entry) (remaining address : ℕ) : entryLookupFoundBits tapes entry remaining address tapes.scan.entry.valueCounter = List.replicate (bitlen entry.2) true

@[simp]

theorem Complexity.RAM.RegisterStore.Machine.entryLookupFoundBits_five {n : ℕ} (tapes : EntryLookupRestoreTapes n) (entry : Entry) (remaining address : ℕ) : entryLookupFoundBits tapes entry remaining address tapes.scan.entry.valueWidth = []

@[simp]

theorem Complexity.RAM.RegisterStore.Machine.entryLookupFoundBits_six {n : ℕ} (tapes : EntryLookupRestoreTapes n) (entry : Entry) (remaining address : ℕ) : entryLookupFoundBits tapes entry remaining address tapes.scan.entry.result = [decide (entry.1.bits = address.bits)]

@[simp]

theorem Complexity.RAM.RegisterStore.Machine.entryLookupFoundBits_seven {n : ℕ} (tapes : EntryLookupRestoreTapes n) (entry : Entry) (remaining address : ℕ) : entryLookupFoundBits tapes entry remaining address tapes.scan.entry.query = address.bits

@[simp]

theorem Complexity.RAM.RegisterStore.Machine.entryLookupFoundBits_eight {n : ℕ} (tapes : EntryLookupRestoreTapes n) (entry : Entry) (remaining address : ℕ) : entryLookupFoundBits tapes entry remaining address (tapes.idx 9) = remaining.bits

@[simp]

theorem Complexity.RAM.RegisterStore.Machine.entryLookupMissBits_seven {n : ℕ} (tapes : EntryLookupRestoreTapes n) (address : ℕ) : entryLookupMissBits tapes address tapes.scan.entry.query = address.bits

@[simp]

theorem Complexity.RAM.RegisterStore.Machine.entryLookupMissBits_zero {n : ℕ} (tapes : EntryLookupRestoreTapes n) (address : ℕ) : entryLookupMissBits tapes address tapes.scan.entry.address = []

@[simp]

theorem Complexity.RAM.RegisterStore.Machine.entryLookupMissBits_one {n : ℕ} (tapes : EntryLookupRestoreTapes n) (address : ℕ) : entryLookupMissBits tapes address tapes.scan.entry.value = []

@[simp]

theorem Complexity.RAM.RegisterStore.Machine.entryLookupMissBits_two {n : ℕ} (tapes : EntryLookupRestoreTapes n) (address : ℕ) : entryLookupMissBits tapes address tapes.scan.entry.addressCounter = []

@[simp]

theorem Complexity.RAM.RegisterStore.Machine.entryLookupMissBits_three {n : ℕ} (tapes : EntryLookupRestoreTapes n) (address : ℕ) : entryLookupMissBits tapes address tapes.scan.entry.addressWidth = []

@[simp]

theorem Complexity.RAM.RegisterStore.Machine.entryLookupMissBits_four {n : ℕ} (tapes : EntryLookupRestoreTapes n) (address : ℕ) : entryLookupMissBits tapes address tapes.scan.entry.valueCounter = []

@[simp]

theorem Complexity.RAM.RegisterStore.Machine.entryLookupMissBits_five {n : ℕ} (tapes : EntryLookupRestoreTapes n) (address : ℕ) : entryLookupMissBits tapes address tapes.scan.entry.valueWidth = []

@[simp]

theorem Complexity.RAM.RegisterStore.Machine.entryLookupMissBits_six {n : ℕ} (tapes : EntryLookupRestoreTapes n) (address : ℕ) : entryLookupMissBits tapes address tapes.scan.entry.result = []

@[simp]

theorem Complexity.RAM.RegisterStore.Machine.entryLookupMissBits_eight {n : ℕ} (tapes : EntryLookupRestoreTapes n) (address : ℕ) : entryLookupMissBits tapes address (tapes.idx 9) = []

@[simp]

theorem Complexity.RAM.RegisterStore.Machine.entryLookupMissBits_other {n : ℕ} (tapes : EntryLookupRestoreTapes n) (address : ℕ) (slot : Fin 9) (hslot : slot ≠ 7) : entryLookupMissBits tapes address (tapes.resetIdx slot) = []

def Complexity.RAM.RegisterStore.Machine.entryLookupRestoreHeadBound {n : ℕ} (tapes : EntryLookupRestoreTapes n) (store : Store) (address : ℕ) : ℕ

Uniform scanner-head bound from a canonical cell-one start.

Equations

• Complexity.RAM.RegisterStore.Machine.entryLookupRestoreHeadBound tapes store address = 1 + Complexity.RAM.RegisterStore.Machine.entryLookupTime tapes.scan address store

def Complexity.RAM.RegisterStore.Machine.entryLookupResetTime {n : ℕ} (tapes : EntryLookupRestoreTapes n) (store : Store) (address : ℕ) : ℕ

Reset budget obtained from the nine fixed owned targets and the common head/width envelopes.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.RAM.RegisterStore.Machine.entryLookupRestoreTailTM {n : ℕ} (tapes : EntryLookupRestoreTapes n) : TM n

Restore scanner scratch, source cursor, and runtime count after a completed lookup whose value has already been copied out.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.RAM.RegisterStore.Machine.entryLookupCopyRestoreTM {n : ℕ} (tapes : EntryLookupRestoreTapes n) : TM n

Copy out a lookup result, then restore the complete reusable scanner ABI.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.RAM.RegisterStore.Machine.entryLookupLoadedTM {n : ℕ} (tapes : EntryLookupRestoreTapes n) : TM n

Load the supplied query, perform one sparse lookup, copy out its value, and return to the same reusable blank-query scanner boundary.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.RAM.RegisterStore.Machine.entryLookupRestoreTailTime {n : ℕ} (tapes : EntryLookupRestoreTapes n) (store : Store) (address : ℕ) : ℕ

Time bound for scanner reset, source rewind, and count restoration.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.RAM.RegisterStore.Machine.entryLookupCopyRestoreTime {n : ℕ} (tapes : EntryLookupRestoreTapes n) (store : Store) (address : ℕ) : ℕ

Time bound after the query has been prepared.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.RAM.RegisterStore.Machine.entryLookupLoadedTime {n : ℕ} (tapes : EntryLookupRestoreTapes n) (store : Store) (address : ℕ) : ℕ

Complete reusable loaded-lookup time bound.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.RAM.RegisterStore.Machine.denseOverlayLookupTM {n : ℕ} (tapes : EntryLookupRestoreTapes n) : TM n

Read a positive-tag sparse overlay and either decode the tag or fall back to the immutable public-input bank on a sparse miss.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.RAM.RegisterStore.Machine.denseOverlayLookupTime {n : ℕ} (tapes : EntryLookupRestoreTapes n) (inputLength : ℕ) (overlay : Store) (address : ℕ) : ℕ

Complete reusable dense-overlay lookup budget.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.RAM.RegisterStore.Machine.denseOverlayLookupStaticTM {n : ℕ} (tapes : EntryLookupRestoreTapes n) (address : ℕ) : TM n

Load one fixed address from canonical zero, read through the dense input and sparse overlay, then clear the fixed-address source back to zero.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.RAM.RegisterStore.Machine.denseOverlayLookupStaticTime {n : ℕ} (tapes : EntryLookupRestoreTapes n) (inputLength : ℕ) (overlay : Store) (address : ℕ) : ℕ

Complete fixed-address dense-overlay lookup budget.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.RAM.RegisterStore.Machine.entryLookupStaticTM {n : ℕ} (tapes : EntryLookupRestoreTapes n) (address : ℕ) : TM n

Load one fixed address from canonical zero, run a reusable lookup, then clear the fixed-address source back to zero.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.RAM.RegisterStore.Machine.entryLookupStaticTime {n : ℕ} (tapes : EntryLookupRestoreTapes n) (store : Store) (address : ℕ) : ℕ

Complete fixed-address lookup budget.

Equations

• One or more equations did not get rendered due to their size.

structure Complexity.RAM.RegisterStore.Machine.EntryLookupRestoreReady {n : ℕ} (tapes : EntryLookupRestoreTapes n) (store : Store) (address : ℕ) (work : Fin n → Tape) : Prop

Canonical precondition for one reusable loaded lookup.

• scanner : EntryScanReady tapes.scan.entry (List.flatMap Entry.encode store) [] work work
• sourceStart : (work tapes.scan.entry.source).cells 0 = Γ.start
• sourceHead : (work tapes.scan.entry.source).head = 1
• count : (work tapes.scan.count).HasBinaryNat (List.length store)
• countSource : (work tapes.countSource).HasBinaryNat (List.length store)
• querySource : (work tapes.querySource).HasBinaryNat address
• destination : (work tapes.destination).HasBinaryNat 0
• copyScratch : (work tapes.copyScratch).HasBinaryNat 0

structure Complexity.RAM.RegisterStore.Machine.EntryLookupStaticReady {n : ℕ} (tapes : EntryLookupRestoreTapes n) (store : Store) (work : Fin n → Tape) : Prop

Canonical precondition for a fixed-address lookup whose query source starts at zero and is restored to zero.

• scanner : EntryScanReady tapes.scan.entry (List.flatMap Entry.encode store) [] work work
• sourceStart : (work tapes.scan.entry.source).cells 0 = Γ.start
• sourceHead : (work tapes.scan.entry.source).head = 1
• count : (work tapes.scan.count).HasBinaryNat (List.length store)
• countSource : (work tapes.countSource).HasBinaryNat (List.length store)
• querySource : (work tapes.querySource).HasBinaryNat 0
• destination : (work tapes.destination).HasBinaryNat 0
• copyScratch : (work tapes.copyScratch).HasBinaryNat 0

structure Complexity.RAM.RegisterStore.Machine.EntryLookupPrepared {n : ℕ} (tapes : EntryLookupRestoreTapes n) (store : Store) (address : ℕ) (initialWork work : Fin n → Tape) : Prop

Boundary after the external query has been copied into scanner storage.

• scanner : EntryScanReady tapes.scan.entry (List.flatMap Entry.encode store) address.bits work work
• sourceStart : (work tapes.scan.entry.source).cells 0 = Γ.start
• sourceHead : (work tapes.scan.entry.source).head = 1
• count : (work tapes.scan.count).HasBinaryNat (List.length store)
• countSource : work tapes.countSource = initialWork tapes.countSource
• countSourceNat : (work tapes.countSource).HasBinaryNat (List.length store)
• querySource : work tapes.querySource = initialWork tapes.querySource
• querySourceNat : (work tapes.querySource).HasBinaryNat address
• destination : (work tapes.destination).HasBinaryNat 0
• copyScratch : (work tapes.copyScratch).HasBinaryNat 0
• parked (i : Fin n) : TM.Parked (work i)
• frame (i : Fin n) : i ≠ tapes.scan.entry.query → work i = initialWork i

def Complexity.RAM.RegisterStore.Machine.EntryLookupResetReady {n : ℕ} (tapes : EntryLookupRestoreTapes n) (store : Store) (address : ℕ) (work : Fin n → Tape) : Prop

Uniform cleanup certificate extracted from either scanner outcome.

Equations

• One or more equations did not get rendered due to their size.

structure Complexity.RAM.RegisterStore.Machine.EntryLookupScanned {n : ℕ} (tapes : EntryLookupRestoreTapes n) (store : Store) (address : ℕ) (initialWork preparedWork work : Fin n → Tape) : Prop

Boundary after the bounded scanner has produced a semantic lookup result. It retains the exact cleanup certificate, the read-only source image, a uniform cursor bound, and the complete external frame needed by restoration.

• result : EntryLookupResult tapes.scan store address preparedWork work
• resetReady : EntryLookupResetReady tapes store address work
• sourceCells : (work tapes.scan.entry.source).cells = (initialWork tapes.scan.entry.source).cells
• sourceStart : (work tapes.scan.entry.source).cells 0 = Γ.start
• sourceHeadBound : (work tapes.scan.entry.source).head ≤ entryLookupRestoreHeadBound tapes store address
• resetHeadBound (i : Fin n) : i ∈ entryLookupResetTargets tapes → (work i).head ≤ entryLookupRestoreHeadBound tapes store address
• countSource : work tapes.countSource = initialWork tapes.countSource
• querySource : work tapes.querySource = initialWork tapes.querySource
• destination : work tapes.destination = initialWork tapes.destination
• copyScratch : work tapes.copyScratch = initialWork tapes.copyScratch
• frame (i : Fin n) : (∀ (slot : Fin 14), i ≠ tapes.idx slot) → work i = initialWork i

def Complexity.RAM.RegisterStore.Machine.EntryLookupScannedReady {n : ℕ} (tapes : EntryLookupRestoreTapes n) (store : Store) (address : ℕ) (initialWork work : Fin n → Tape) : Prop

Existentially packages the concrete prepared work family between query copying and scanning, so subsequent phases can use a semantic Hoare boundary.

Equations

• One or more equations did not get rendered due to their size.

structure Complexity.RAM.RegisterStore.Machine.EntryLookupRestoreInvariant {n : ℕ} (tapes : EntryLookupRestoreTapes n) (store : Store) (address : ℕ) (initialWork work : Fin n → Tape) : Prop

Stable semantic state carried through value rewind, value copy, scratch reset, source rewind, and count restoration.

• valueContent : (work tapes.scan.entry.value).HasBinaryContent (read store address).bits
• valueStart : (work tapes.scan.entry.value).cells 0 = Γ.start
• resetReady : EntryLookupResetReady tapes store address work
• sourceCells : (work tapes.scan.entry.source).cells = (initialWork tapes.scan.entry.source).cells
• sourceStart : (work tapes.scan.entry.source).cells 0 = Γ.start
• sourceHeadBound : (work tapes.scan.entry.source).head ≤ entryLookupRestoreHeadBound tapes store address
• resetHeadBound (i : Fin n) : i ∈ entryLookupResetTargets tapes → (work i).head ≤ entryLookupRestoreHeadBound tapes store address
• countSource : work tapes.countSource = initialWork tapes.countSource
• countSourceNat : (work tapes.countSource).HasBinaryNat (List.length store)
• querySource : work tapes.querySource = initialWork tapes.querySource
• querySourceNat : (work tapes.querySource).HasBinaryNat address
• copyScratch : work tapes.copyScratch = initialWork tapes.copyScratch
• copyScratchNat : (work tapes.copyScratch).HasBinaryNat 0
• parked (i : Fin n) : TM.Parked (work i)
• frame (i : Fin n) : (∀ (slot : Fin 14), i ≠ tapes.idx slot) → work i = initialWork i

structure Complexity.RAM.RegisterStore.Machine.EntryLookupValueReady {n : ℕ} (tapes : EntryLookupRestoreTapes n) (store : Store) (address : ℕ) (initialWork work : Fin n → Tape) : Prop

The decoded value has been rewound to the canonical read boundary.

• restore : EntryLookupRestoreInvariant tapes store address initialWork work
• value : (work tapes.scan.entry.value).HasBinaryNat (read store address)
• destination : (work tapes.destination).HasBinaryNat 0

structure Complexity.RAM.RegisterStore.Machine.EntryLookupCopied {n : ℕ} (tapes : EntryLookupRestoreTapes n) (store : Store) (address : ℕ) (initialWork work : Fin n → Tape) : Prop

The decoded value has been copied to the instruction operand tape while all scanner restoration data remains available.

• restore : EntryLookupRestoreInvariant tapes store address initialWork work
• value : (work tapes.scan.entry.value).HasBinaryNat (read store address)
• destination : (work tapes.destination).HasBinaryNat (read store address)

structure Complexity.RAM.RegisterStore.Machine.EntryLookupResetDone {n : ℕ} (tapes : EntryLookupRestoreTapes n) (store : Store) (address : ℕ) (initialWork copiedWork work : Fin n → Tape) : Prop

Exact boundary after all nine scanner-owned binary tapes have been reset.

• copied : EntryLookupCopied tapes store address initialWork copiedWork
• work_eq : work = TM.resetBinaryWorkManyResult copiedWork (entryLookupResetTargets tapes)

structure Complexity.RAM.RegisterStore.Machine.EntryLookupScratchReset {n : ℕ} (tapes : EntryLookupRestoreTapes n) (store : Store) (address : ℕ) (initialWork work : Fin n → Tape) : Prop

Semantic form of the reset endpoint, stable while the encoded source is rewound.

• sourceCells : (work tapes.scan.entry.source).cells = (initialWork tapes.scan.entry.source).cells
• sourceStart : (work tapes.scan.entry.source).cells 0 = Γ.start
• sourceHeadBound : (work tapes.scan.entry.source).head ≤ entryLookupRestoreHeadBound tapes store address
• targetsBlank (i : Fin n) : i ∈ entryLookupResetTargets tapes → work i = TM.resetBinaryBlank
• countSource : work tapes.countSource = initialWork tapes.countSource
• countSourceNat : (work tapes.countSource).HasBinaryNat (List.length store)
• querySource : work tapes.querySource = initialWork tapes.querySource
• querySourceNat : (work tapes.querySource).HasBinaryNat address
• destination : (work tapes.destination).HasBinaryNat (read store address)
• copyScratch : work tapes.copyScratch = initialWork tapes.copyScratch
• copyScratchNat : (work tapes.copyScratch).HasBinaryNat 0
• parked (i : Fin n) : TM.Parked (work i)
• frame (i : Fin n) : (∀ (slot : Fin 14), i ≠ tapes.idx slot) → work i = initialWork i

structure Complexity.RAM.RegisterStore.Machine.EntryLookupSourceReady {n : ℕ} (tapes : EntryLookupRestoreTapes n) (store : Store) (address : ℕ) (initialWork work : Fin n → Tape) : Prop

Boundary after scanner reset and encoded-source rewind, immediately before the runtime entry count is copied back.

• scanner : EntryScanReady tapes.scan.entry (List.flatMap Entry.encode store) [] work work
• sourceCells : (work tapes.scan.entry.source).cells = (initialWork tapes.scan.entry.source).cells
• sourceStart : (work tapes.scan.entry.source).cells 0 = Γ.start
• sourceHead : (work tapes.scan.entry.source).head = 1
• countZero : (work tapes.scan.count).HasBinaryNat 0
• countSource : work tapes.countSource = initialWork tapes.countSource
• countSourceNat : (work tapes.countSource).HasBinaryNat (List.length store)
• querySource : work tapes.querySource = initialWork tapes.querySource
• destination : (work tapes.destination).HasBinaryNat (read store address)
• copyScratch : work tapes.copyScratch = initialWork tapes.copyScratch
• copyScratchNat : (work tapes.copyScratch).HasBinaryNat 0
• parked (i : Fin n) : TM.Parked (work i)
• frame (i : Fin n) : (∀ (slot : Fin 14), i ≠ tapes.idx slot) → work i = initialWork i

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

Reusable endpoint after one loaded sparse-register read.

• scanner : EntryScanReady tapes.scan.entry (List.flatMap Entry.encode store) [] finalWork finalWork
• sourceCells : (finalWork tapes.scan.entry.source).cells = (initialWork tapes.scan.entry.source).cells
• sourceStart : (finalWork tapes.scan.entry.source).cells 0 = Γ.start
• sourceHead : (finalWork tapes.scan.entry.source).head = 1
• count : (finalWork tapes.scan.count).HasBinaryNat (List.length store)
• countSource : finalWork tapes.countSource = initialWork tapes.countSource
• querySource : finalWork tapes.querySource = initialWork tapes.querySource
• value : (finalWork tapes.destination).HasBinaryNat (read store address)
• copyScratch : (finalWork tapes.copyScratch).HasBinaryNat 0
• parked (i : Fin n) : TM.Parked (finalWork i)
• frame (i : Fin n) : (∀ (slot : Fin 14), i ≠ tapes.idx slot) → finalWork i = initialWork i

structure Complexity.RAM.RegisterStore.Machine.DenseOverlayLookupResult {n : ℕ} (tapes : EntryLookupRestoreTapes n) (input : List Bool) (overlay : Store) (address : ℕ) (initialWork finalWork : Fin n → Tape) : Prop

Reusable endpoint after reading through a tagged mutable overlay into the immutable public-input bank.

• scanner : EntryScanReady tapes.scan.entry (List.flatMap Entry.encode overlay) [] finalWork finalWork
• sourceCells : (finalWork tapes.scan.entry.source).cells = (initialWork tapes.scan.entry.source).cells
• sourceStart : (finalWork tapes.scan.entry.source).cells 0 = Γ.start
• sourceHead : (finalWork tapes.scan.entry.source).head = 1
• count : (finalWork tapes.scan.count).HasBinaryNat (List.length overlay)
• countSource : finalWork tapes.countSource = initialWork tapes.countSource
• querySource : finalWork tapes.querySource = initialWork tapes.querySource
• value : (finalWork tapes.destination).HasBinaryNat (DenseOverlay.read input overlay address)
• copyScratch : (finalWork tapes.copyScratch).HasBinaryNat 0
• parked (i : Fin n) : TM.Parked (finalWork i)
• frame (i : Fin n) : (∀ (slot : Fin 14), i ≠ tapes.idx slot) → finalWork i = initialWork i

structure Complexity.RAM.RegisterStore.Machine.DenseOverlayLookupStaticResult {n : ℕ} (tapes : EntryLookupRestoreTapes n) (input : List Bool) (overlay : Store) (address : ℕ) (initialWork finalWork : Fin n → Tape) : Prop

Reusable fixed-address dense-overlay endpoint. The destination contains the decoded register value and the temporary query source is zero again.

• scanner : EntryScanReady tapes.scan.entry (List.flatMap Entry.encode overlay) [] finalWork finalWork
• sourceCells : (finalWork tapes.scan.entry.source).cells = (initialWork tapes.scan.entry.source).cells
• sourceStart : (finalWork tapes.scan.entry.source).cells 0 = Γ.start
• sourceHead : (finalWork tapes.scan.entry.source).head = 1
• count : (finalWork tapes.scan.count).HasBinaryNat (List.length overlay)
• countSource : finalWork tapes.countSource = initialWork tapes.countSource
• querySource : (finalWork tapes.querySource).HasBinaryNat 0
• destination : (finalWork tapes.destination).HasBinaryNat (DenseOverlay.read input overlay address)
• copyScratch : (finalWork tapes.copyScratch).HasBinaryNat 0
• parked (i : Fin n) : TM.Parked (finalWork i)
• frame (i : Fin n) : (∀ (slot : Fin 14), i ≠ tapes.idx slot) → finalWork i = initialWork i

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

Reusable fixed-address endpoint. The destination holds the semantic read, the scanner is restored, and the fixed query source is zero again.

• scanner : EntryScanReady tapes.scan.entry (List.flatMap Entry.encode store) [] finalWork finalWork
• sourceCells : (finalWork tapes.scan.entry.source).cells = (initialWork tapes.scan.entry.source).cells
• sourceStart : (finalWork tapes.scan.entry.source).cells 0 = Γ.start
• sourceHead : (finalWork tapes.scan.entry.source).head = 1
• count : (finalWork tapes.scan.count).HasBinaryNat (List.length store)
• countSource : finalWork tapes.countSource = initialWork tapes.countSource
• querySource : (finalWork tapes.querySource).HasBinaryNat 0
• destination : (finalWork tapes.destination).HasBinaryNat (read store address)
• copyScratch : (finalWork tapes.copyScratch).HasBinaryNat 0
• parked (i : Fin n) : TM.Parked (finalWork i)
• frame (i : Fin n) : (∀ (slot : Fin 14), i ≠ tapes.idx slot) → finalWork i = initialWork i