RAM sparse-entry matching — definitions

entryMatchTM is the concrete unit consumed by a bounded sparse-store scan. It decodes one address/value entry and compares the decoded address with a preserved canonical query. The result is appended to a dedicated work tape.

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

Nine pairwise-distinct work tapes used to decode and match one sparse register-store entry.

• idx : Fin 9 → Fin n

  Tape assignment in the order source, address, value, address counter, address width, value counter, value width, query, and result.

• injective : Function.Injective self.idx

def Complexity.RAM.RegisterStore.Machine.EntryMatchTapes.decode {n : ℕ} (tapes : EntryMatchTapes n) : EntryDecodeTapes n

The seven decoder tapes contained in an entry-matching assignment.

Equations

• tapes.decode = { idx := fun (i : Fin 7) => tapes.idx ⟨↑i, ⋯⟩, injective := ⋯ }

def Complexity.RAM.RegisterStore.Machine.EntryMatchTapes.source {n : ℕ} (tapes : EntryMatchTapes n) : Fin n

Encoded entry-stream source tape.

Equations

• tapes.source = tapes.idx 0

def Complexity.RAM.RegisterStore.Machine.EntryMatchTapes.address {n : ℕ} (tapes : EntryMatchTapes n) : Fin n

Decoded address scratch tape.

Equations

• tapes.address = tapes.idx 1

def Complexity.RAM.RegisterStore.Machine.EntryMatchTapes.value {n : ℕ} (tapes : EntryMatchTapes n) : Fin n

Decoded value scratch tape.

Equations

• tapes.value = tapes.idx 2

def Complexity.RAM.RegisterStore.Machine.EntryMatchTapes.addressCounter {n : ℕ} (tapes : EntryMatchTapes n) : Fin n

Binary loop counter used while decoding the address.

Equations

• tapes.addressCounter = tapes.idx 3

def Complexity.RAM.RegisterStore.Machine.EntryMatchTapes.addressWidth {n : ℕ} (tapes : EntryMatchTapes n) : Fin n

Preserved address payload-width tape.

Equations

• tapes.addressWidth = tapes.idx 4

def Complexity.RAM.RegisterStore.Machine.EntryMatchTapes.valueCounter {n : ℕ} (tapes : EntryMatchTapes n) : Fin n

Binary loop counter used while decoding the value.

Equations

• tapes.valueCounter = tapes.idx 5

def Complexity.RAM.RegisterStore.Machine.EntryMatchTapes.valueWidth {n : ℕ} (tapes : EntryMatchTapes n) : Fin n

Preserved value payload-width tape.

Equations

• tapes.valueWidth = tapes.idx 6

def Complexity.RAM.RegisterStore.Machine.EntryMatchTapes.query {n : ℕ} (tapes : EntryMatchTapes n) : Fin n

Canonical query-address tape.

Equations

• tapes.query = tapes.idx 7

def Complexity.RAM.RegisterStore.Machine.EntryMatchTapes.result {n : ℕ} (tapes : EntryMatchTapes n) : Fin n

Boolean match-result tape.

Equations

• tapes.result = tapes.idx 8

theorem Complexity.RAM.RegisterStore.Machine.EntryMatchTapes.ne {n : ℕ} (tapes : EntryMatchTapes n) {i j : Fin 9} (h : i ≠ j) : tapes.idx i ≠ tapes.idx j

theorem Complexity.RAM.RegisterStore.Machine.EntryMatchTapes.binaryEqDistinct {n : ℕ} (tapes : EntryMatchTapes n) : TM.BinaryEqDistinct tapes.address tapes.query tapes.result

@[simp]

theorem Complexity.RAM.RegisterStore.Machine.EntryMatchTapes.decode_source {n : ℕ} (tapes : EntryMatchTapes n) : tapes.decode.source = tapes.source

@[simp]

theorem Complexity.RAM.RegisterStore.Machine.EntryMatchTapes.decode_address {n : ℕ} (tapes : EntryMatchTapes n) : tapes.decode.address = tapes.address

@[simp]

theorem Complexity.RAM.RegisterStore.Machine.EntryMatchTapes.decode_value {n : ℕ} (tapes : EntryMatchTapes n) : tapes.decode.value = tapes.value

@[simp]

theorem Complexity.RAM.RegisterStore.Machine.EntryMatchTapes.decode_addressCounter {n : ℕ} (tapes : EntryMatchTapes n) : tapes.decode.addressCounter = tapes.addressCounter

@[simp]

theorem Complexity.RAM.RegisterStore.Machine.EntryMatchTapes.decode_addressWidth {n : ℕ} (tapes : EntryMatchTapes n) : tapes.decode.addressWidth = tapes.addressWidth

@[simp]

theorem Complexity.RAM.RegisterStore.Machine.EntryMatchTapes.decode_valueCounter {n : ℕ} (tapes : EntryMatchTapes n) : tapes.decode.valueCounter = tapes.valueCounter

@[simp]

theorem Complexity.RAM.RegisterStore.Machine.EntryMatchTapes.decode_valueWidth {n : ℕ} (tapes : EntryMatchTapes n) : tapes.decode.valueWidth = tapes.valueWidth

def Complexity.RAM.RegisterStore.Machine.entryMatchTM {n : ℕ} (tapes : EntryMatchTapes n) : TM n

Decode one sparse entry with unary markers and compare its address with the preserved query.

Equations

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

def Complexity.RAM.RegisterStore.Machine.entryMatchTime (entry : Entry) (queryBits : List Bool) : ℕ

Runtime bound for decoding and matching one sparse entry, including the composition seam.

Equations

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

def Complexity.RAM.RegisterStore.Machine.entryMatchReadTM {n : ℕ} (tapes : EntryMatchTapes n) : TM n

Decode and compare one sparse entry, then rewind the one-bit result to its canonical cell-one read position.

Equations

• Complexity.RAM.RegisterStore.Machine.entryMatchReadTM tapes = (Complexity.RAM.RegisterStore.Machine.entryMatchTM tapes).seqTM (Complexity.TM.rewindWorkTM tapes.result)

def Complexity.RAM.RegisterStore.Machine.entryMatchReadTime (entry : Entry) (queryBits : List Bool) : ℕ

Runtime bound for a readable one-entry match, including both composition seams and the at-most-four-step rewind of the one-bit result.

Equations

• Complexity.RAM.RegisterStore.Machine.entryMatchReadTime entry queryBits = Complexity.RAM.RegisterStore.Machine.entryMatchTime entry queryBits + 1 + 4

structure Complexity.RAM.RegisterStore.Machine.ReadableEntryMatch {n : ℕ} (tapes : EntryMatchTapes n) (entry : Entry) (rest queryBits : List Bool) (initialWork finalWork : Fin n → Tape) : Prop

Auditable endpoint contract for one readable sparse-entry match. The decoded scratch remains available to a hit branch or can be cleared by a miss branch; the result is parked at cell one for direct controller inspection.

• source : (finalWork tapes.source).HasBinarySuffix rest
• address : (finalWork tapes.address).HasBinaryContent entry.1.bits
• addressStart : (finalWork tapes.address).cells 0 = Γ.start
• value : (finalWork tapes.value).HasBinaryPrefix entry.2.bits
• valueStart : (finalWork tapes.value).cells 0 = Γ.start
• addressCounter : (finalWork tapes.addressCounter).HasBinaryPrefix (List.replicate (bitlen entry.1) true)
• addressCounterStart : (finalWork tapes.addressCounter).cells 0 = Γ.start
• addressWidth : (finalWork tapes.addressWidth).HasBinaryNat 0
• valueCounter : (finalWork tapes.valueCounter).HasBinaryPrefix (List.replicate (bitlen entry.2) true)
• valueCounterStart : (finalWork tapes.valueCounter).cells 0 = Γ.start
• valueWidth : (finalWork tapes.valueWidth).HasBinaryNat 0
• query : (finalWork tapes.query).HasBinaryContent queryBits
• queryStart : (finalWork tapes.query).cells 0 = Γ.start
• result : (finalWork tapes.result).HasBinaryString [decide (entry.1.bits = queryBits)]
• resultStart : (finalWork tapes.result).cells 0 = Γ.start
• parked (i : Fin n) : TM.Parked (finalWork i)
• headBound (i : Fin n) : (finalWork i).head ≤ (initialWork i).head + entryMatchReadTime entry queryBits
• frame (i : Fin n) : i ≠ tapes.source → i ≠ tapes.address → i ≠ tapes.value → i ≠ tapes.addressCounter → i ≠ tapes.addressWidth → i ≠ tapes.valueCounter → i ≠ tapes.valueWidth → i ≠ tapes.query → i ≠ tapes.result → finalWork i = initialWork i