Dense public input with a sparse mutable overlay -- definitions

The ordinary sparse snapshot eagerly materializes every nonzero public-input register. That representation is convenient but occupies Theta(n log n) cells before the RAM executes a step. This module separates the immutable input bank from the mutable register overlay.

An overlay entry (address, tag) represents the actual value tag - 1. Because every stored tag is positive, an absent address is distinguishable from an explicit write of zero (tag = 1). Absent reads fall through to the dense public-input ABI RAM.initRegs input.

@[reducible, inline]

abbrev Complexity.RAM.RegisterStore.DenseOverlay.Store : Type

Mutable tagged entries layered over the immutable public-input bank.

Equations

• Complexity.RAM.RegisterStore.DenseOverlay.Store = Complexity.RAM.RegisterStore.Store

def Complexity.RAM.RegisterStore.DenseOverlay.read (input : List Bool) (overlay : Store) (address : ℕ) : ℕ

Read through the sparse tagged overlay, falling back to the public input.

Equations

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

def Complexity.RAM.RegisterStore.DenseOverlay.write (overlay : Store) (address value : ℕ) : Store

Record an explicit mutable value. The positive tag preserves written zero.

Equations

• Complexity.RAM.RegisterStore.DenseOverlay.write overlay address value = Complexity.RAM.RegisterStore.write overlay address (value + 1)

@[reducible, inline]

abbrev Complexity.RAM.RegisterStore.DenseOverlay.Canonical (overlay : Store) : Prop

A valid overlay has unique addresses and positive tags.

Equations

• Complexity.RAM.RegisterStore.DenseOverlay.Canonical overlay = Complexity.RAM.RegisterStore.Canonical overlay

def Complexity.RAM.RegisterStore.DenseOverlay.CoversZero (overlay : Store) : Prop

Register zero is materialized in every concrete overlay. This lets the dense-input lookup specialize its fallback path to positive input addresses.

Equations

• Complexity.RAM.RegisterStore.DenseOverlay.CoversZero overlay = (Complexity.RAM.RegisterStore.read overlay 0 ≠ 0)

def Complexity.RAM.RegisterStore.DenseOverlay.Valid (overlay : Store) : Prop

Full representation invariant for the mutable overlay.

Equations

• Complexity.RAM.RegisterStore.DenseOverlay.Valid overlay = (Complexity.RAM.RegisterStore.DenseOverlay.Canonical overlay ∧ Complexity.RAM.RegisterStore.DenseOverlay.CoversZero overlay)

def Complexity.RAM.RegisterStore.DenseOverlay.decode (input : List Bool) (overlay : Store) : ℕ → ℕ

Decode the dense-input/overlay pair to a total RAM register file.

Equations

• Complexity.RAM.RegisterStore.DenseOverlay.decode input overlay = Complexity.RAM.RegisterStore.DenseOverlay.read input overlay

structure Complexity.RAM.RegisterStore.DenseOverlay.Snapshot : Type

A finite mutable overlay plus program counter. The immutable input remains on the Turing input tape and is not duplicated in this snapshot.

• pc : ℕ

  Current RAM program counter.

• overlay : Store

  Sparse positive-tag overlay.

@[implicit_reducible]

instance Complexity.RAM.RegisterStore.DenseOverlay.instDecidableEqSnapshot : DecidableEq Snapshot

Equations

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

def Complexity.RAM.RegisterStore.DenseOverlay.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.DenseOverlay.Snapshot.decode (input : List Bool) (snapshot : Snapshot) : Cfg

Decode one dense-overlay snapshot against its immutable public input.

Equations

• Complexity.RAM.RegisterStore.DenseOverlay.Snapshot.decode input snapshot = { pc := snapshot.pc, regs := Complexity.RAM.RegisterStore.DenseOverlay.decode input snapshot.overlay }

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

Reuse the checked sparse snapshot codec for the tagged mutable overlay.

Equations

• snapshot.encode = { pc := snapshot.pc, store := snapshot.overlay }.encode

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

The initial mutable overlay materializes only R₀ = input.length; all input bits remain in the read-only dense bank. The stored positive tag is input.length + 1.

Equations

• Complexity.RAM.RegisterStore.DenseOverlay.Snapshot.initial input = { pc := 0, overlay := Complexity.RAM.RegisterStore.DenseOverlay.write [] 0 input.length }

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

Instruction selected by the current program counter.

Equations

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

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

Whether the selected instruction is halt.

Equations

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

@[implicit_reducible]

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

Equations

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

def Complexity.RAM.RegisterStore.DenseOverlay.Snapshot.stepInstr (input : List Bool) : Instr → Snapshot → Snapshot

Execute one RAM instruction against the decoded input/overlay register file, recording the result as a positive tag.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.RAM.RegisterStore.DenseOverlay.Snapshot.stepInstr input (Complexity.RAM.Instr.jmp target) x✝ = { pc := target, overlay := x✝.overlay }
• Complexity.RAM.RegisterStore.DenseOverlay.Snapshot.stepInstr input Complexity.RAM.Instr.halt x✝ = x✝

def Complexity.RAM.RegisterStore.DenseOverlay.Snapshot.step (program : Program) (input : List Bool) (snapshot : Snapshot) : Snapshot

Execute the instruction selected by the current program counter.

Equations

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

def Complexity.RAM.RegisterStore.DenseOverlay.Snapshot.run (program : Program) (input : List Bool) : ℕ → Snapshot → Snapshot

Fuel-bounded dense-overlay execution, stopping once halted.

Equations

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