RAM sparse-entry decoder — definitions

One sparse register entry contains two consecutive self-delimiting words: its address and value. entryDecodeTM gives each word its own target, counter, and width tapes so the two checked word decoders compose without a clearing phase.

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

Seven pairwise-distinct work tapes used by one sparse-entry decoder.

• idx : Fin 7 → Fin n

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

• injective : Function.Injective self.idx

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

Encoded entry-stream source tape.

Equations

• tapes.source = tapes.idx 0

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

Decoded address target tape.

Equations

• tapes.address = tapes.idx 1

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

Decoded value target tape.

Equations

• tapes.value = tapes.idx 2

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

Binary loop counter used while decoding the address.

Equations

• tapes.addressCounter = tapes.idx 3

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

Preserved address payload-width tape.

Equations

• tapes.addressWidth = tapes.idx 4

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

Binary loop counter used while decoding the value.

Equations

• tapes.valueCounter = tapes.idx 5

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

Preserved value payload-width tape.

Equations

• tapes.valueWidth = tapes.idx 6

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

theorem Complexity.RAM.RegisterStore.Machine.EntryDecodeTapes.addressDistinct {n : ℕ} (tapes : EntryDecodeTapes n) : PayloadLoopDistinct tapes.source tapes.address tapes.addressCounter tapes.addressWidth

theorem Complexity.RAM.RegisterStore.Machine.EntryDecodeTapes.valueDistinct {n : ℕ} (tapes : EntryDecodeTapes n) : PayloadLoopDistinct tapes.source tapes.value tapes.valueCounter tapes.valueWidth

theorem Complexity.RAM.RegisterStore.Machine.EntryDecodeTapes.addressLinearDistinct {n : ℕ} (tapes : EntryDecodeTapes n) : LinearWordDistinct tapes.source tapes.address tapes.addressCounter

Source, address target, and address marker are pairwise distinct.

theorem Complexity.RAM.RegisterStore.Machine.EntryDecodeTapes.valueLinearDistinct {n : ℕ} (tapes : EntryDecodeTapes n) : LinearWordDistinct tapes.source tapes.value tapes.valueCounter

Source, value target, and value marker are pairwise distinct.

def Complexity.RAM.RegisterStore.Machine.entryDecodeTM {n : ℕ} (tapes : EntryDecodeTapes n) : TM n

Decode the address word and then the value word of one sparse entry.

Equations

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

def Complexity.RAM.RegisterStore.Machine.entryDecodeTime (address value : ℕ) : ℕ

Exact runtime for decoding both words, including the composition seam.

Equations

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

def Complexity.RAM.RegisterStore.Machine.entryDecodeLinearTM {n : ℕ} (tapes : EntryDecodeTapes n) : TM n

Decode both entry words with unary markers. The former counter tapes serve as address and value markers; the two width tapes are left untouched so this machine can replace entryDecodeTM inside the established seven-tape ABI.

Equations

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

def Complexity.RAM.RegisterStore.Machine.entryDecodeLinearTime (address value : ℕ) : ℕ

Exact runtime of the optimized two-word decoder, including its composition seam.

Equations

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