Sparse RAM register stores on Turing tapes: definitions

This file defines the auditable representation boundary for simulating a RAM with a Turing machine. A finite register file is represented by a list of address/value pairs. Zero-valued registers are omitted. Words use a self-delimiting binary code consisting of a unary width, a zero separator, and exactly that many binary payload bits. Thus a word of bit-width w occupies 2 * w + 1 tape cells.

Snapshot adds the program counter to a finite store. Its bit encoding begins with the program counter and entry count, followed by the address and value of each entry. The corresponding decoders are total Option-valued functions.

Proofs that the store operations implement functional register reads/writes and that every codec round-trips live in the internal module.

def Complexity.RAM.RegisterStore.Instr.staticWidth : Instr → ℕ

Maximum bit-width of an instruction's hardwired register indices, immediate, and jump target. These literals are fixed with the program and are therefore not charged as runtime indirect addresses by Instr.logCost.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.RAM.RegisterStore.Instr.staticWidth (Complexity.RAM.Instr.imm destination value) = max (Complexity.RAM.bitlen destination) (Complexity.RAM.bitlen value)
• Complexity.RAM.RegisterStore.Instr.staticWidth (Complexity.RAM.Instr.load destination addressRegister) = max (Complexity.RAM.bitlen destination) (Complexity.RAM.bitlen addressRegister)
• Complexity.RAM.RegisterStore.Instr.staticWidth (Complexity.RAM.Instr.store destination addressRegister) = max (Complexity.RAM.bitlen destination) (Complexity.RAM.bitlen addressRegister)
• Complexity.RAM.RegisterStore.Instr.staticWidth (Complexity.RAM.Instr.jz source target) = max (Complexity.RAM.bitlen source) (Complexity.RAM.bitlen target)
• Complexity.RAM.RegisterStore.Instr.staticWidth (Complexity.RAM.Instr.jmp target) = Complexity.RAM.bitlen target
• Complexity.RAM.RegisterStore.Instr.staticWidth Complexity.RAM.Instr.halt = 0

def Complexity.RAM.RegisterStore.programStaticWidth : Program → ℕ

Maximum hardwired literal width appearing in a fixed RAM program.

Equations

• Complexity.RAM.RegisterStore.programStaticWidth [] = 0
• Complexity.RAM.RegisterStore.programStaticWidth (instruction :: rest) = max (Complexity.RAM.RegisterStore.Instr.staticWidth instruction) (Complexity.RAM.RegisterStore.programStaticWidth rest)

@[reducible, inline]

abbrev Complexity.RAM.RegisterStore.Entry : Type

One sparse register entry: an address paired with its nonzero value.

Equations

• Complexity.RAM.RegisterStore.Entry = (ℕ × ℕ)

@[reducible, inline]

abbrev Complexity.RAM.RegisterStore.Store : Type

A finite sparse register file.

Equations

• Complexity.RAM.RegisterStore.Store = List Complexity.RAM.RegisterStore.Entry

def Complexity.RAM.RegisterStore.read : Store → ℕ → ℕ

Read an address from a sparse store, defaulting to zero.

Equations

• Complexity.RAM.RegisterStore.read [] x✝ = 0
• Complexity.RAM.RegisterStore.read ((storedAddress, value) :: rest) x✝ = if x✝ = storedAddress then value else Complexity.RAM.RegisterStore.read rest x✝

def Complexity.RAM.RegisterStore.write : Store → ℕ → ℕ → Store

Write one address in a sparse store. Writing zero removes the entry; writing a nonzero value replaces the first matching entry or appends a fresh entry when the address is absent.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.RAM.RegisterStore.write [] x✝¹ x✝ = if x✝ = 0 then [] else [(x✝¹, x✝)]

def Complexity.RAM.RegisterStore.AddressesNodup (store : Store) : Prop

No address occurs twice in a sparse store.

Equations

• Complexity.RAM.RegisterStore.AddressesNodup store = (List.map Prod.fst store).Nodup

def Complexity.RAM.RegisterStore.ValuesNonzero (store : Store) : Prop

Every materialized entry carries a nonzero value.

Equations

• Complexity.RAM.RegisterStore.ValuesNonzero store = ∀ entry ∈ store, entry.2 ≠ 0

def Complexity.RAM.RegisterStore.Canonical (store : Store) : Prop

A canonical sparse store has unique addresses and omits zero values.

Equations

• Complexity.RAM.RegisterStore.Canonical store = (Complexity.RAM.RegisterStore.AddressesNodup store ∧ Complexity.RAM.RegisterStore.ValuesNonzero store)

def Complexity.RAM.RegisterStore.decode (store : Store) : ℕ → ℕ

Decode a sparse store into the RAM model's total register file.

Equations

• Complexity.RAM.RegisterStore.decode store = Complexity.RAM.RegisterStore.read store

def Complexity.RAM.RegisterStore.Represents (store : Store) (regs : ℕ → ℕ) : Prop

A finite sparse store represents a total RAM register file exactly.

Equations

• Complexity.RAM.RegisterStore.Represents store regs = (Complexity.RAM.RegisterStore.Canonical store ∧ Complexity.RAM.RegisterStore.decode store = regs)

def Complexity.RAM.RegisterStore.maxWidth : Store → ℕ

Maximum address/value bit-width materialized in a sparse store.

Equations

• Complexity.RAM.RegisterStore.maxWidth [] = 0
• Complexity.RAM.RegisterStore.maxWidth (entry :: rest) = max (Complexity.RAM.bitlen entry.1) (max (Complexity.RAM.bitlen entry.2) (Complexity.RAM.RegisterStore.maxWidth rest))

noncomputable def Complexity.RAM.RegisterStore.ofRegs (regs : ℕ → ℕ) (hfinite : (Function.support regs).Finite) : Store

Materialize the finite support of a total register file as a sparse store.

Equations

• Complexity.RAM.RegisterStore.ofRegs regs hfinite = List.map (fun (address : ℕ) => (address, regs address)) hfinite.toFinset.toList

def Complexity.RAM.RegisterStore.initialAddresses (input : List Bool) : Finset ℕ

Nonzero public-input registers, selected from the known finite input range.

Equations

• Complexity.RAM.RegisterStore.initialAddresses input = {address ∈ Finset.range (input.length + 1) | Complexity.RAM.initRegs input address ≠ 0}

def Complexity.RAM.RegisterStore.initialStore (input : List Bool) : Store

Canonical sparse materialization of the RAM public-input register file.

Equations

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

Self-delimiting binary words

def Complexity.RAM.RegisterStore.WordCode.encode (value : ℕ) : List Bool

Encode a natural as unary bit-width, a zero separator, and fixed-width little-endian payload bits. The payload convention matches the library's canonical binary-arithmetic work tapes.

Equations

• Complexity.RAM.RegisterStore.WordCode.encode value = List.replicate (Complexity.RAM.bitlen value) true ++ false :: (Complexity.RAM.bitlen value).toBitsLE value

def Complexity.RAM.RegisterStore.WordCode.decodeAux? : List Bool → ℕ → Option (ℕ × List Bool)

Parse the unary-width prefix, then consume exactly that many payload bits.

Equations

• Complexity.RAM.RegisterStore.WordCode.decodeAux? [] x✝ = none
• Complexity.RAM.RegisterStore.WordCode.decodeAux? (true :: rest) x✝ = Complexity.RAM.RegisterStore.WordCode.decodeAux? rest (x✝ + 1)
• Complexity.RAM.RegisterStore.WordCode.decodeAux? (false :: rest) x✝ = if x✝ ≤ rest.length then some (Nat.fromBitsLE (List.take x✝ rest), List.drop x✝ rest) else none

def Complexity.RAM.RegisterStore.WordCode.decodePrefix? (bits : List Bool) : Option (ℕ × List Bool)

Parse one self-delimiting binary word and return the unconsumed suffix.

Equations

• Complexity.RAM.RegisterStore.WordCode.decodePrefix? bits = Complexity.RAM.RegisterStore.WordCode.decodeAux? bits 0

def Complexity.RAM.RegisterStore.Entry.encode (entry : Entry) : List Bool

Serialize an address/value entry as two self-delimiting words.

Equations

• entry.encode = Complexity.RAM.RegisterStore.WordCode.encode entry.1 ++ Complexity.RAM.RegisterStore.WordCode.encode entry.2

def Complexity.RAM.RegisterStore.Entry.decodePrefix? (bits : List Bool) : Option (Entry × List Bool)

Parse one address/value entry and return the unconsumed suffix.

Equations

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

def Complexity.RAM.RegisterStore.encodedStoreLength (store : Store) : ℕ

Number of tape cells occupied by the concatenated self-delimiting codes of the live sparse-store entries. Unlike Snapshot.sizeBound, this charges the actual width of every entry instead of multiplying the entry count by one run-wide maximum width.

Equations

• Complexity.RAM.RegisterStore.encodedStoreLength store = (List.flatMap Complexity.RAM.RegisterStore.Entry.encode store).length

def Complexity.RAM.RegisterStore.decodeEntries? : ℕ → List Bool → Option (Store × List Bool)

Parse exactly count sparse entries and return the unconsumed suffix.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.RAM.RegisterStore.decodeEntries? 0 x✝ = some ([], x✝)

structure Complexity.RAM.RegisterStore.Snapshot : Type

A finite RAM snapshot: program counter plus sparse register store.

• pc : ℕ

  Program counter of the represented RAM configuration.

• store : Store

  Materialized nonzero register entries.

@[implicit_reducible]

instance Complexity.RAM.RegisterStore.instDecidableEqSnapshot : DecidableEq Snapshot

Equations

• Complexity.RAM.RegisterStore.instDecidableEqSnapshot = Complexity.RAM.RegisterStore.instDecidableEqSnapshot.decEq

def Complexity.RAM.RegisterStore.instDecidableEqSnapshot.decEq (x✝ x✝¹ : Snapshot) : Decidable (x✝ = x✝¹)

Equations

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

def Complexity.RAM.RegisterStore.Snapshot.decode (snapshot : Snapshot) : Cfg

Decode a finite snapshot to a RAM configuration.

Equations

• snapshot.decode = { pc := snapshot.pc, regs := Complexity.RAM.RegisterStore.decode snapshot.store }

def Complexity.RAM.RegisterStore.Snapshot.encode (snapshot : Snapshot) : List Bool

Serialize a snapshot as program counter, entry count, and entries.

Equations

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

def Complexity.RAM.RegisterStore.Snapshot.decodePrefix? (bits : List Bool) : Option (Snapshot × List Bool)

Parse one snapshot prefix and return the unconsumed suffix.

Equations

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

def Complexity.RAM.RegisterStore.Snapshot.decode? (bits : List Bool) : Option Snapshot

Decode an exact snapshot code, rejecting trailing bits.

Equations

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

def Complexity.RAM.RegisterStore.Snapshot.Represents (snapshot : Snapshot) (cfg : Cfg) : Prop

A canonical snapshot represents a RAM configuration exactly.

Equations

• snapshot.Represents cfg = (Complexity.RAM.RegisterStore.Canonical snapshot.store ∧ snapshot.decode = cfg)

def Complexity.RAM.RegisterStore.Snapshot.width (snapshot : Snapshot) : ℕ

One width envelope for the program counter, entry count, addresses, and values of a finite snapshot.

Equations

• snapshot.width = max (Complexity.RAM.bitlen snapshot.pc) (max (Complexity.RAM.bitlen (List.length snapshot.store)) (Complexity.RAM.RegisterStore.maxWidth snapshot.store))

def Complexity.RAM.RegisterStore.Snapshot.sizeBound (snapshot : Snapshot) : ℕ

Concrete tape-cell envelope for the canonical snapshot encoding.

Equations

• snapshot.sizeBound = (List.length snapshot.store + 1) * (4 * snapshot.width + 2)

def Complexity.RAM.RegisterStore.Snapshot.stepWidthBound (instruction : Instr) (snapshot : Snapshot) : ℕ

One-step width envelope: old width plus one, or a width explicitly exposed by the instruction literal or its logarithmic runtime charge.

Equations

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

noncomputable def Complexity.RAM.RegisterStore.Snapshot.ofCfg (cfg : Cfg) (hfinite : (Function.support cfg.regs).Finite) : Snapshot

Materialize a RAM configuration whose register support is finite.

Equations

• Complexity.RAM.RegisterStore.Snapshot.ofCfg cfg hfinite = { pc := cfg.pc, store := Complexity.RAM.RegisterStore.ofRegs cfg.regs hfinite }

def Complexity.RAM.RegisterStore.Snapshot.initial (input : List Bool) : Snapshot

Canonical finite snapshot of the RAM public-input configuration.

Equations

• Complexity.RAM.RegisterStore.Snapshot.initial input = { pc := 0, store := Complexity.RAM.RegisterStore.initialStore input }

def Complexity.RAM.RegisterStore.Snapshot.curInstr (program : Program) (snapshot : Snapshot) : Instr

The instruction selected by a finite snapshot.

Equations

• Complexity.RAM.RegisterStore.Snapshot.curInstr program snapshot = program[snapshot.pc]?.getD Complexity.RAM.Instr.halt

def Complexity.RAM.RegisterStore.Snapshot.stepInstr : Instr → Snapshot → Snapshot

Execute one RAM instruction directly on the sparse finite store.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.RAM.RegisterStore.Snapshot.stepInstr (Complexity.RAM.Instr.imm destination value) x✝ = { pc := x✝.pc + 1, store := Complexity.RAM.RegisterStore.write x✝.store destination value }
• Complexity.RAM.RegisterStore.Snapshot.stepInstr (Complexity.RAM.Instr.jmp target) x✝ = { pc := target, store := x✝.store }
• Complexity.RAM.RegisterStore.Snapshot.stepInstr Complexity.RAM.Instr.halt x✝ = x✝

def Complexity.RAM.RegisterStore.Snapshot.step (program : Program) (snapshot : Snapshot) : Snapshot

Execute the selected RAM instruction on a sparse snapshot.

Equations

• Complexity.RAM.RegisterStore.Snapshot.step program snapshot = Complexity.RAM.RegisterStore.Snapshot.stepInstr (Complexity.RAM.RegisterStore.Snapshot.curInstr program snapshot) snapshot

def Complexity.RAM.RegisterStore.Snapshot.Halted (program : Program) (snapshot : Snapshot) : Prop

A sparse snapshot is halted exactly when its selected instruction is halt.

Equations

• Complexity.RAM.RegisterStore.Snapshot.Halted program snapshot = (Complexity.RAM.RegisterStore.Snapshot.curInstr program snapshot = Complexity.RAM.Instr.halt)

@[implicit_reducible]

instance Complexity.RAM.RegisterStore.Snapshot.instDecidableHalted (program : Program) (snapshot : Snapshot) : Decidable (Halted program snapshot)

Equations

• Complexity.RAM.RegisterStore.Snapshot.instDecidableHalted program snapshot = id inferInstance

def Complexity.RAM.RegisterStore.Snapshot.run (program : Program) : ℕ → Snapshot → Snapshot

Fuel-bounded sparse execution, stopping at the first halted snapshot.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.RAM.RegisterStore.Snapshot.run program 0 x✝ = x✝