Fixed-program sparse RAM instruction dispatch -- definitions

One fresh last work tape is the next-store buffer. Data instructions redirect their encoded output there; control instructions copy the unchanged read-only store there. A binary copy of the program counter is then decremented through a fixed finite branch tree, so the resulting TM depends only on the RAM program.

def Complexity.RAM.RegisterStore.Machine.ControlInstructionTapes.lifted {n : ℕ} (tapes : ControlInstructionTapes n) : ControlInstructionTapes (n + 1)

Embed every control/data role into the initial n tapes of the one-buffer layout.

Equations

• tapes.lifted = { data := { idx := fun (slot : Fin 18) => (tapes.data.idx slot).castSucc, injective := ⋯ }, pc := tapes.pc.castSucc, pc_ne := ⋯ }

def Complexity.RAM.RegisterStore.Machine.ControlInstructionTapes.liftedPC {n : ℕ} (tapes : ControlInstructionTapes n) : Fin (n + 1)

Program counter in the one-buffer execution layout.

Equations

• tapes.liftedPC = tapes.lifted.pc

def Complexity.RAM.RegisterStore.Machine.ControlInstructionTapes.liftedLhs {n : ℕ} (tapes : ControlInstructionTapes n) : Fin (n + 1)

First temporary operand in the one-buffer execution layout.

Equations

• tapes.liftedLhs = tapes.lifted.data.lhs

def Complexity.RAM.RegisterStore.Machine.ControlInstructionTapes.liftedFound {n : ℕ} (tapes : ControlInstructionTapes n) : Fin (n + 1)

Zero scratch used while copying the dispatch selector.

Equations

• tapes.liftedFound = tapes.lifted.data.update.found

def Complexity.RAM.RegisterStore.Machine.ControlInstructionTapes.liftedSource {n : ℕ} (tapes : ControlInstructionTapes n) : Fin (n + 1)

Read-only encoded-store source in the one-buffer execution layout.

Equations

• tapes.liftedSource = tapes.lifted.data.update.entry.source

def Complexity.RAM.RegisterStore.Machine.ControlInstructionTapes.buffer {n : ℕ} (_tapes : ControlInstructionTapes n) : Fin (n + 1)

Fresh last work tape receiving the next encoded store.

Equations

• _tapes.buffer = Fin.last n

theorem Complexity.RAM.RegisterStore.Machine.ControlInstructionTapes.liftedSource_ne_buffer {n : ℕ} (tapes : ControlInstructionTapes n) : tapes.liftedSource ≠ tapes.buffer

theorem Complexity.RAM.RegisterStore.Machine.ControlInstructionTapes.liftedPC_ne_buffer {n : ℕ} (tapes : ControlInstructionTapes n) : tapes.liftedPC ≠ tapes.buffer

theorem Complexity.RAM.RegisterStore.Machine.ControlInstructionTapes.liftedPC_ne_source {n : ℕ} (tapes : ControlInstructionTapes n) : tapes.liftedPC ≠ tapes.liftedSource

The lifted program counter is disjoint from the encoded-store source.

theorem Complexity.RAM.RegisterStore.Machine.ControlInstructionTapes.liftedData_ne_buffer {n : ℕ} (tapes : ControlInstructionTapes n) (slot : Fin 18) : tapes.lifted.data.idx slot ≠ tapes.buffer

def Complexity.RAM.RegisterStore.Machine.finishControlInstructionTM {n : ℕ} (tapes : ControlInstructionTapes n) (control : TM (n + 1)) : TM (n + 1)

Emit the unchanged store from the read-only source into the fresh buffer after executing a control-only instruction.

Equations

• Complexity.RAM.RegisterStore.Machine.finishControlInstructionTM tapes control = control.seqTM (Complexity.TM.copyWorkToWorkTM tapes.liftedSource tapes.buffer)

def Complexity.RAM.RegisterStore.Machine.executeInstructionTM {n : ℕ} (tapes : ControlInstructionTapes n) : Instr → TM (n + 1)

Execute one statically selected RAM instruction. Every case writes the next encoded store to the fresh last work tape and leaves real output blank.

Equations

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

def Complexity.RAM.RegisterStore.Machine.dispatchWithTM {n : ℕ} (tapes : ControlInstructionTapes n) (execute : Instr → TM (n + 1)) : Program → TM (n + 1)

Representation-independent finite branch tree for any family of static instruction executors sharing the standard decrementing selector tape.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.RAM.RegisterStore.Machine.dispatchWithTM tapes execute [] = (Complexity.TM.resetBinaryWorkTM tapes.liftedLhs).seqTM (execute Complexity.RAM.Instr.halt)

def Complexity.RAM.RegisterStore.Machine.dispatchProgramTM {n : ℕ} (tapes : ControlInstructionTapes n) : Program → TM (n + 1)

Finite branch tree selected by a decrementing canonical PC copy.

Equations

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

def Complexity.RAM.RegisterStore.Machine.selectedInstruction : Program → ℕ → Instr

Pure instruction selected by the same finite branch-tree recursion.

Equations

• Complexity.RAM.RegisterStore.Machine.selectedInstruction [] x✝ = Complexity.RAM.Instr.halt
• Complexity.RAM.RegisterStore.Machine.selectedInstruction (instruction :: tail) 0 = instruction
• Complexity.RAM.RegisterStore.Machine.selectedInstruction (head :: program) selector.succ = Complexity.RAM.RegisterStore.Machine.selectedInstruction program selector

def Complexity.RAM.RegisterStore.Machine.programInstructionTM {n : ℕ} (tapes : ControlInstructionTapes n) (program : Program) : TM (n + 1)

Copy the preserved PC into zero scratch and enter the fixed branch tree.

Equations

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

def Complexity.RAM.RegisterStore.Machine.instructionStore (instruction : Instr) (pcValue : ℕ) (store : Store) : Store

Pure next store selected by one RAM instruction.

Equations

• Complexity.RAM.RegisterStore.Machine.instructionStore instruction pcValue store = (Complexity.RAM.RegisterStore.Snapshot.stepInstr instruction { pc := pcValue, store := store }).store

def Complexity.RAM.RegisterStore.Machine.instructionPC (instruction : Instr) (pcValue : ℕ) (store : Store) : ℕ

Pure next program counter selected by one RAM instruction.

Equations

• Complexity.RAM.RegisterStore.Machine.instructionPC instruction pcValue store = (Complexity.RAM.RegisterStore.Snapshot.stepInstr instruction { pc := pcValue, store := store }).pc

def Complexity.RAM.RegisterStore.Machine.instructionCleanupParentSlot : Fin 5 → Fin 18

Parent data slots cleared between simulated RAM instructions.

Equations

• Complexity.RAM.RegisterStore.Machine.instructionCleanupParentSlot 0 = 7
• Complexity.RAM.RegisterStore.Machine.instructionCleanupParentSlot 1 = 10
• Complexity.RAM.RegisterStore.Machine.instructionCleanupParentSlot 2 = 11
• Complexity.RAM.RegisterStore.Machine.instructionCleanupParentSlot 3 = 13
• Complexity.RAM.RegisterStore.Machine.instructionCleanupParentSlot x✝ = 14

def Complexity.RAM.RegisterStore.Machine.instructionCleanupTape {n : ℕ} (tapes : ControlInstructionTapes n) (slot : Fin 5) : Fin (n + 1)

Five canonical data roles that must be cleared between simulated RAM instructions: update query, replacement, found flag, and the two operands.

Equations

• Complexity.RAM.RegisterStore.Machine.instructionCleanupTape tapes slot = tapes.lifted.data.idx (Complexity.RAM.RegisterStore.Machine.instructionCleanupParentSlot slot)

theorem Complexity.RAM.RegisterStore.Machine.instructionCleanupTape_ne_source {n : ℕ} (tapes : ControlInstructionTapes n) (slot : Fin 5) : instructionCleanupTape tapes slot ≠ tapes.liftedSource

theorem Complexity.RAM.RegisterStore.Machine.instructionCleanupTape_ne_buffer {n : ℕ} (tapes : ControlInstructionTapes n) (slot : Fin 5) : instructionCleanupTape tapes slot ≠ tapes.buffer

def Complexity.RAM.RegisterStore.Machine.instructionCleanupValue (instruction : Instr) (store : Store) : Fin 5 → ℕ

Exact values left on the five cleanup roles by one instruction kernel.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.RAM.RegisterStore.Machine.instructionCleanupValue (Complexity.RAM.Instr.imm destination value) store 0 = destination
• Complexity.RAM.RegisterStore.Machine.instructionCleanupValue (Complexity.RAM.Instr.add destination source₀ source₁) store 0 = destination
• Complexity.RAM.RegisterStore.Machine.instructionCleanupValue (Complexity.RAM.Instr.sub destination source₀ source₁) store 0 = destination
• Complexity.RAM.RegisterStore.Machine.instructionCleanupValue (Complexity.RAM.Instr.mul destination source₀ source₁) store 0 = destination
• Complexity.RAM.RegisterStore.Machine.instructionCleanupValue (Complexity.RAM.Instr.load destination addressRegister) store 0 = destination
• Complexity.RAM.RegisterStore.Machine.instructionCleanupValue (Complexity.RAM.Instr.store addressRegister source) store 0 = Complexity.RAM.RegisterStore.read store addressRegister
• Complexity.RAM.RegisterStore.Machine.instructionCleanupValue (Complexity.RAM.Instr.jz source target) store 0 = 0
• Complexity.RAM.RegisterStore.Machine.instructionCleanupValue (Complexity.RAM.Instr.jmp target) store 0 = 0
• Complexity.RAM.RegisterStore.Machine.instructionCleanupValue Complexity.RAM.Instr.halt store 0 = 0
• Complexity.RAM.RegisterStore.Machine.instructionCleanupValue (Complexity.RAM.Instr.imm destination value) store 1 = value
• Complexity.RAM.RegisterStore.Machine.instructionCleanupValue (Complexity.RAM.Instr.store addressRegister source) store 1 = Complexity.RAM.RegisterStore.read store source
• Complexity.RAM.RegisterStore.Machine.instructionCleanupValue (Complexity.RAM.Instr.jz source target) store 1 = 0
• Complexity.RAM.RegisterStore.Machine.instructionCleanupValue (Complexity.RAM.Instr.jmp target) store 1 = 0
• Complexity.RAM.RegisterStore.Machine.instructionCleanupValue Complexity.RAM.Instr.halt store 1 = 0
• Complexity.RAM.RegisterStore.Machine.instructionCleanupValue (Complexity.RAM.Instr.imm destination value) store 2 = if destination ∈ List.map Prod.fst store then 1 else 0
• Complexity.RAM.RegisterStore.Machine.instructionCleanupValue (Complexity.RAM.Instr.add destination source₀ source₁) store 2 = if destination ∈ List.map Prod.fst store then 1 else 0
• Complexity.RAM.RegisterStore.Machine.instructionCleanupValue (Complexity.RAM.Instr.sub destination source₀ source₁) store 2 = if destination ∈ List.map Prod.fst store then 1 else 0
• Complexity.RAM.RegisterStore.Machine.instructionCleanupValue (Complexity.RAM.Instr.mul destination source₀ source₁) store 2 = if destination ∈ List.map Prod.fst store then 1 else 0
• Complexity.RAM.RegisterStore.Machine.instructionCleanupValue (Complexity.RAM.Instr.load destination addressRegister) store 2 = if destination ∈ List.map Prod.fst store then 1 else 0
• Complexity.RAM.RegisterStore.Machine.instructionCleanupValue (Complexity.RAM.Instr.jz source target) store 2 = 0
• Complexity.RAM.RegisterStore.Machine.instructionCleanupValue (Complexity.RAM.Instr.jmp target) store 2 = 0
• Complexity.RAM.RegisterStore.Machine.instructionCleanupValue Complexity.RAM.Instr.halt store 2 = 0
• Complexity.RAM.RegisterStore.Machine.instructionCleanupValue (Complexity.RAM.Instr.add d source₀ t) store 3 = Complexity.RAM.RegisterStore.read store source₀
• Complexity.RAM.RegisterStore.Machine.instructionCleanupValue (Complexity.RAM.Instr.sub d source₀ t) store 3 = Complexity.RAM.RegisterStore.read store source₀
• Complexity.RAM.RegisterStore.Machine.instructionCleanupValue (Complexity.RAM.Instr.mul d source₀ t) store 3 = Complexity.RAM.RegisterStore.read store source₀
• Complexity.RAM.RegisterStore.Machine.instructionCleanupValue (Complexity.RAM.Instr.load d addressRegister) store 3 = Complexity.RAM.RegisterStore.read store addressRegister
• Complexity.RAM.RegisterStore.Machine.instructionCleanupValue (Complexity.RAM.Instr.store addressRegister s) store 3 = Complexity.RAM.RegisterStore.read store addressRegister
• Complexity.RAM.RegisterStore.Machine.instructionCleanupValue (Complexity.RAM.Instr.imm d v) store 3 = 0
• Complexity.RAM.RegisterStore.Machine.instructionCleanupValue (Complexity.RAM.Instr.jz s tgt) store 3 = 0
• Complexity.RAM.RegisterStore.Machine.instructionCleanupValue (Complexity.RAM.Instr.jmp tgt) store 3 = 0
• Complexity.RAM.RegisterStore.Machine.instructionCleanupValue Complexity.RAM.Instr.halt store 3 = 0
• Complexity.RAM.RegisterStore.Machine.instructionCleanupValue (Complexity.RAM.Instr.add d s source₁) store x✝ = Complexity.RAM.RegisterStore.read store source₁
• Complexity.RAM.RegisterStore.Machine.instructionCleanupValue (Complexity.RAM.Instr.sub d s source₁) store x✝ = Complexity.RAM.RegisterStore.read store source₁
• Complexity.RAM.RegisterStore.Machine.instructionCleanupValue (Complexity.RAM.Instr.mul d s source₁) store x✝ = Complexity.RAM.RegisterStore.read store source₁
• Complexity.RAM.RegisterStore.Machine.instructionCleanupValue (Complexity.RAM.Instr.store a source) store x✝ = Complexity.RAM.RegisterStore.read store source
• Complexity.RAM.RegisterStore.Machine.instructionCleanupValue (Complexity.RAM.Instr.imm d v) store x✝ = 0
• Complexity.RAM.RegisterStore.Machine.instructionCleanupValue (Complexity.RAM.Instr.load d a) store x✝ = 0
• Complexity.RAM.RegisterStore.Machine.instructionCleanupValue (Complexity.RAM.Instr.jz s tgt) store x✝ = 0
• Complexity.RAM.RegisterStore.Machine.instructionCleanupValue (Complexity.RAM.Instr.jmp tgt) store x✝ = 0
• Complexity.RAM.RegisterStore.Machine.instructionCleanupValue Complexity.RAM.Instr.halt store x✝ = 0

def Complexity.RAM.RegisterStore.Machine.instructionRemainingValue (instruction : Instr) (store : Store) : ℕ

The old-entry counter is exhausted by data updates and untouched by control instructions. Cleanup resets either canonical value uniformly.

Equations

• Complexity.RAM.RegisterStore.Machine.instructionRemainingValue (Complexity.RAM.Instr.imm destination value) store = 0
• Complexity.RAM.RegisterStore.Machine.instructionRemainingValue (Complexity.RAM.Instr.add destination source₀ source₁) store = 0
• Complexity.RAM.RegisterStore.Machine.instructionRemainingValue (Complexity.RAM.Instr.sub destination source₀ source₁) store = 0
• Complexity.RAM.RegisterStore.Machine.instructionRemainingValue (Complexity.RAM.Instr.mul destination source₀ source₁) store = 0
• Complexity.RAM.RegisterStore.Machine.instructionRemainingValue (Complexity.RAM.Instr.load destination addressRegister) store = 0
• Complexity.RAM.RegisterStore.Machine.instructionRemainingValue (Complexity.RAM.Instr.store addressRegister source) store = 0
• Complexity.RAM.RegisterStore.Machine.instructionRemainingValue (Complexity.RAM.Instr.jz source target) store = List.length store
• Complexity.RAM.RegisterStore.Machine.instructionRemainingValue (Complexity.RAM.Instr.jmp target) store = List.length store
• Complexity.RAM.RegisterStore.Machine.instructionRemainingValue Complexity.RAM.Instr.halt store = List.length store

structure Complexity.RAM.RegisterStore.Machine.InstructionExecutionReady {n : ℕ} (tapes : ControlInstructionTapes n) (store : Store) (pcValue : ℕ) (work : Fin (n + 1) → Tape) : Prop

Clean one-buffer entry boundary shared by every selected instruction.

• canonical : Canonical store

  The sparse representation contains one nonzero entry per address.

• control : ControlInstructionReady tapes.lifted store pcValue work

  The lifted control/lookup ABI is ready.

• sourceContent : (work tapes.liftedSource).HasBinaryContent (List.flatMap Entry.encode store)

  The read-only source has the complete canonical sparse-store image.

• rhs : (work tapes.lifted.data.rhs).HasBinaryNat 0

  The second direct operand starts at zero.

• replacement : (work tapes.lifted.data.update.replacement).HasBinaryNat 0

  Sparse-update replacement starts at zero.

• tmp : (work tapes.lifted.data.tmp).HasBinaryNat 0

  First multiplication alternating scratch starts at zero.

• dbl : (work tapes.lifted.data.dbl).HasBinaryNat 0

  Second multiplication alternating scratch starts at zero.

• buffer : work tapes.buffer = (Tape.init []).move Dir3.right

  The next-store buffer is fresh.

def Complexity.RAM.RegisterStore.Machine.DispatchReady {n : ℕ} (tapes : ControlInstructionTapes n) (store : Store) (pcValue selector : ℕ) (cleanWork work : Fin (n + 1) → Tape) : Prop

Dispatch boundary obtained by replacing the clean zero lhs tape by a canonical decrementing selector.

Equations

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

structure Complexity.RAM.RegisterStore.Machine.InstructionExecutionResult {n : ℕ} (tapes : ControlInstructionTapes n) (instruction : Instr) (pcValue : ℕ) (store : Store) (work : Fin (n + 1) → Tape) : Prop

Common semantic endpoint of every selected instruction before cleanup.

• buffer : (work tapes.buffer).HasBinaryPrefix (List.flatMap Entry.encode (instructionStore instruction pcValue store))

  The fresh buffer contains exactly the pure next sparse store.

• pc : (work tapes.liftedPC).HasBinaryNat (instructionPC instruction pcValue store)

  The canonical PC equals the pure instruction successor.

• resultCount : (work tapes.lifted.data.update.resultCount).HasBinaryNat (List.length (instructionStore instruction pcValue store))

  The preserved output-entry count equals the next store cardinality.

• sourceContent : (work tapes.liftedSource).HasBinaryContent (List.flatMap Entry.encode store)

  The old encoded source remains available for bounded clearing.

• cleanup (slot : Fin 5) : (work (instructionCleanupTape tapes slot)).HasBinaryNat (instructionCleanupValue instruction store slot)

  Every instruction leaves the cleanup roles as canonical binary naturals.

• remaining : (work tapes.lifted.data.update.remaining).HasBinaryNat (instructionRemainingValue instruction store)

  The runtime old-entry counter has a canonical value before reset.

• scanner : EntryScanReady tapes.lifted.data.update.entry [] (instructionCleanupValue instruction store 0).bits work work

  Decode/match scratch is clean; only the update query remains loaded.

• shift : (work tapes.lifted.data.shift).HasBinaryNat 0

  Lookup query-source scratch is restored.

• tmp : (work tapes.lifted.data.tmp).HasBinaryNat 0

  First multiplication scratch is restored.

• dbl : (work tapes.lifted.data.dbl).HasBinaryNat 0

  Second multiplication scratch is restored.

• parked (i : Fin (n + 1)) : TM.Parked (work i)

  Every work head is parked at the instruction/cleanup boundary.

structure Complexity.RAM.RegisterStore.Machine.BufferedInstructionResult {n : ℕ} (tapes : ControlInstructionTapes n) (oldStore nextStore : Store) (nextPC : ℕ) (cleanupValues : Fin 5 → ℕ) (remainingValue : ℕ) (work : Fin (n + 1) → Tape) : Prop

Instruction-independent buffered endpoint. This is the semantic interface needed by physical cleanup; sparse and dense register representations provide their own next-store, next-PC, and scratch-value witnesses.

• buffer : (work tapes.buffer).HasBinaryPrefix (List.flatMap Entry.encode nextStore)
• pc : (work tapes.liftedPC).HasBinaryNat nextPC
• resultCount : (work tapes.lifted.data.update.resultCount).HasBinaryNat (List.length nextStore)
• sourceContent : (work tapes.liftedSource).HasBinaryContent (List.flatMap Entry.encode oldStore)
• cleanup (slot : Fin 5) : (work (instructionCleanupTape tapes slot)).HasBinaryNat (cleanupValues slot)
• remaining : (work tapes.lifted.data.update.remaining).HasBinaryNat remainingValue
• scanner : EntryScanReady tapes.lifted.data.update.entry [] (cleanupValues 0).bits work work
• shift : (work tapes.lifted.data.shift).HasBinaryNat 0
• tmp : (work tapes.lifted.data.tmp).HasBinaryNat 0
• dbl : (work tapes.lifted.data.dbl).HasBinaryNat 0
• parked (i : Fin (n + 1)) : TM.Parked (work i)

def Complexity.RAM.RegisterStore.Machine.instructionCleanupResetParentSlot : Fin 7 → Fin 18

Parent roles reset before the buffered successor store is installed. The first five are instruction-specific data, followed by the old remaining count and the old encoded source.

Equations

• Complexity.RAM.RegisterStore.Machine.instructionCleanupResetParentSlot 0 = 7
• Complexity.RAM.RegisterStore.Machine.instructionCleanupResetParentSlot 1 = 10
• Complexity.RAM.RegisterStore.Machine.instructionCleanupResetParentSlot 2 = 11
• Complexity.RAM.RegisterStore.Machine.instructionCleanupResetParentSlot 3 = 13
• Complexity.RAM.RegisterStore.Machine.instructionCleanupResetParentSlot 4 = 14
• Complexity.RAM.RegisterStore.Machine.instructionCleanupResetParentSlot 5 = 9
• Complexity.RAM.RegisterStore.Machine.instructionCleanupResetParentSlot x✝ = 0

def Complexity.RAM.RegisterStore.Machine.instructionCleanupResetTape {n : ℕ} (tapes : ControlInstructionTapes n) (slot : Fin 7) : Fin (n + 1)

Physical reset target in the one-buffer instruction layout.

Equations

• Complexity.RAM.RegisterStore.Machine.instructionCleanupResetTape tapes slot = tapes.lifted.data.idx (Complexity.RAM.RegisterStore.Machine.instructionCleanupResetParentSlot slot)

theorem Complexity.RAM.RegisterStore.Machine.instructionCleanupResetTape_injective {n : ℕ} (tapes : ControlInstructionTapes n) : Function.Injective (instructionCleanupResetTape tapes)

def Complexity.RAM.RegisterStore.Machine.instructionCleanupResetTargets {n : ℕ} (tapes : ControlInstructionTapes n) : List (Fin (n + 1))

Fixed distinct list consumed by the bulk binary reset.

Equations

• Complexity.RAM.RegisterStore.Machine.instructionCleanupResetTargets tapes = List.ofFn (Complexity.RAM.RegisterStore.Machine.instructionCleanupResetTape tapes)

def Complexity.RAM.RegisterStore.Machine.instructionCleanupResetBits (instruction : Instr) (store : Store) : Fin 7 → List Bool

Binary contents advertised at each reset target.

Equations

• Complexity.RAM.RegisterStore.Machine.instructionCleanupResetBits instruction store 0 = (Complexity.RAM.RegisterStore.Machine.instructionCleanupValue instruction store 0).bits
• Complexity.RAM.RegisterStore.Machine.instructionCleanupResetBits instruction store 1 = (Complexity.RAM.RegisterStore.Machine.instructionCleanupValue instruction store 1).bits
• Complexity.RAM.RegisterStore.Machine.instructionCleanupResetBits instruction store 2 = (Complexity.RAM.RegisterStore.Machine.instructionCleanupValue instruction store 2).bits
• Complexity.RAM.RegisterStore.Machine.instructionCleanupResetBits instruction store 3 = (Complexity.RAM.RegisterStore.Machine.instructionCleanupValue instruction store 3).bits
• Complexity.RAM.RegisterStore.Machine.instructionCleanupResetBits instruction store 4 = (Complexity.RAM.RegisterStore.Machine.instructionCleanupValue instruction store 4).bits
• Complexity.RAM.RegisterStore.Machine.instructionCleanupResetBits instruction store 5 = (Complexity.RAM.RegisterStore.Machine.instructionRemainingValue instruction store).bits
• Complexity.RAM.RegisterStore.Machine.instructionCleanupResetBits instruction store x✝ = List.flatMap Complexity.RAM.RegisterStore.Entry.encode store

def Complexity.RAM.RegisterStore.Machine.instructionCleanupResetHeadBound (sourceHeadBound : ℕ) : Fin 7 → ℕ

Head bounds at the seven bulk-reset targets. Canonical natural tapes are at cell one; only the scanned old source needs an external bound.

Equations

• Complexity.RAM.RegisterStore.Machine.instructionCleanupResetHeadBound sourceHeadBound 0 = 1
• Complexity.RAM.RegisterStore.Machine.instructionCleanupResetHeadBound sourceHeadBound 1 = 1
• Complexity.RAM.RegisterStore.Machine.instructionCleanupResetHeadBound sourceHeadBound 2 = 1
• Complexity.RAM.RegisterStore.Machine.instructionCleanupResetHeadBound sourceHeadBound 3 = 1
• Complexity.RAM.RegisterStore.Machine.instructionCleanupResetHeadBound sourceHeadBound 4 = 1
• Complexity.RAM.RegisterStore.Machine.instructionCleanupResetHeadBound sourceHeadBound 5 = 1
• Complexity.RAM.RegisterStore.Machine.instructionCleanupResetHeadBound sourceHeadBound x✝ = sourceHeadBound

noncomputable def Complexity.RAM.RegisterStore.Machine.instructionCleanupResetBitsAt {n : ℕ} (tapes : ControlInstructionTapes n) (instruction : Instr) (store : Store) : Fin (n + 1) → List Bool

Extend the indexed reset contents to the whole physical work family.

Equations

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

noncomputable def Complexity.RAM.RegisterStore.Machine.instructionCleanupResetHeadBoundAt {n : ℕ} (tapes : ControlInstructionTapes n) (sourceHeadBound : ℕ) : Fin (n + 1) → ℕ

Extend the indexed reset head bounds to the whole work family.

Equations

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

def Complexity.RAM.RegisterStore.Machine.bufferedCleanupResetBits (cleanupValues : Fin 5 → ℕ) (remainingValue : ℕ) (oldStore : Store) : Fin 7 → List Bool

Binary contents reset by representation-independent buffered cleanup.

Equations

• Complexity.RAM.RegisterStore.Machine.bufferedCleanupResetBits cleanupValues remainingValue oldStore 0 = (cleanupValues 0).bits
• Complexity.RAM.RegisterStore.Machine.bufferedCleanupResetBits cleanupValues remainingValue oldStore 1 = (cleanupValues 1).bits
• Complexity.RAM.RegisterStore.Machine.bufferedCleanupResetBits cleanupValues remainingValue oldStore 2 = (cleanupValues 2).bits
• Complexity.RAM.RegisterStore.Machine.bufferedCleanupResetBits cleanupValues remainingValue oldStore 3 = (cleanupValues 3).bits
• Complexity.RAM.RegisterStore.Machine.bufferedCleanupResetBits cleanupValues remainingValue oldStore 4 = (cleanupValues 4).bits
• Complexity.RAM.RegisterStore.Machine.bufferedCleanupResetBits cleanupValues remainingValue oldStore 5 = remainingValue.bits
• Complexity.RAM.RegisterStore.Machine.bufferedCleanupResetBits cleanupValues remainingValue oldStore x✝ = List.flatMap Complexity.RAM.RegisterStore.Entry.encode oldStore

noncomputable def Complexity.RAM.RegisterStore.Machine.bufferedCleanupResetBitsAt {n : ℕ} (tapes : ControlInstructionTapes n) (cleanupValues : Fin 5 → ℕ) (remainingValue : ℕ) (oldStore : Store) : Fin (n + 1) → List Bool

Extend generic buffered-cleanup contents to all physical work tapes.

Equations

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

def Complexity.RAM.RegisterStore.Machine.instructionCleanupPrefixTape (bits : List Bool) : Tape

Canonical tape with bits and its head immediately after the payload.

Equations

• Complexity.RAM.RegisterStore.Machine.instructionCleanupPrefixTape bits = { head := bits.length + 1, cells := (Complexity.Tape.init (List.map Complexity.Γ.ofBool bits)).cells }

structure Complexity.RAM.RegisterStore.Machine.InstructionCleanupReady {n : ℕ} (tapes : ControlInstructionTapes n) (instruction : Instr) (pcValue : ℕ) (store : Store) (sourceHeadBound : ℕ) (work : Fin (n + 1) → Tape) : Prop

Buffered post-state plus the two left markers and old-source cursor bound needed by the executable cleanup pass.

• canonical : Canonical store
• result : InstructionExecutionResult tapes instruction pcValue store work
• sourceStart : (work tapes.liftedSource).cells 0 = Γ.start
• bufferStart : (work tapes.buffer).cells 0 = Γ.start
• sourceHead : (work tapes.liftedSource).head ≤ sourceHeadBound

structure Complexity.RAM.RegisterStore.Machine.BufferedCleanupReady {n : ℕ} (tapes : ControlInstructionTapes n) (oldStore nextStore : Store) (nextPC : ℕ) (cleanupValues : Fin 5 → ℕ) (remainingValue sourceHeadBound : ℕ) (work : Fin (n + 1) → Tape) : Prop

Representation-independent input boundary for the physical cleanup pass.

• nextCanonical : Canonical nextStore
• result : BufferedInstructionResult tapes oldStore nextStore nextPC cleanupValues remainingValue work
• sourceStart : (work tapes.liftedSource).cells 0 = Γ.start
• bufferStart : (work tapes.buffer).cells 0 = Γ.start
• sourceHead : (work tapes.liftedSource).head ≤ sourceHeadBound

def Complexity.RAM.RegisterStore.Machine.instructionCleanupTM {n : ℕ} (tapes : ControlInstructionTapes n) : TM (n + 1)

Restore the clean instruction ABI around the buffered successor store.

Equations

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

noncomputable def Complexity.RAM.RegisterStore.Machine.instructionCleanupTime {n : ℕ} (tapes : ControlInstructionTapes n) (instruction : Instr) (pcValue : ℕ) (store : Store) (sourceHeadBound : ℕ) : ℕ

Exact compositional cleanup bound for one buffered instruction result.

Equations

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

noncomputable def Complexity.RAM.RegisterStore.Machine.bufferedCleanupTime {n : ℕ} (tapes : ControlInstructionTapes n) (oldStore nextStore : Store) (cleanupValues : Fin 5 → ℕ) (remainingValue sourceHeadBound : ℕ) : ℕ

Exact cleanup budget expressed only through the buffered representation boundary, independent of the instruction semantics that produced it.

Equations

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

def Complexity.RAM.RegisterStore.Machine.executeInstructionTime {n : ℕ} (tapes : ControlInstructionTapes n) (instruction : Instr) (pcValue : ℕ) (store : Store) : ℕ

Runtime bound for a statically selected instruction before iteration cleanup.

Equations

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

def Complexity.RAM.RegisterStore.Machine.dispatchWithTime {n : ℕ} (tapes : ControlInstructionTapes n) (executeTime : Instr → ℕ) : Program → ℕ → ℕ

Representation-independent path-sensitive branch-tree time. Unlike the coarse branch combinator bound, this charges only the instruction selected by the represented selector.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.RAM.RegisterStore.Machine.dispatchWithTime tapes executeTime [] x✝ = Complexity.TM.resetBinaryWorkTime 1 x✝.bits.length + 1 + executeTime Complexity.RAM.Instr.halt
• Complexity.RAM.RegisterStore.Machine.dispatchWithTime tapes executeTime (instruction :: tail) 0 = executeTime instruction + 1

def Complexity.RAM.RegisterStore.Machine.dispatchProgramTime {n : ℕ} (tapes : ControlInstructionTapes n) (store : Store) (pcValue : ℕ) : Program → ℕ → ℕ

Branch-tree bound for a selector currently represented by selector.

Equations

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

def Complexity.RAM.RegisterStore.Machine.programInstructionTime {n : ℕ} (tapes : ControlInstructionTapes n) (program : Program) (pcValue : ℕ) (store : Store) : ℕ

Complete fixed-program selection and selected-instruction bound.

Equations

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

def Complexity.RAM.RegisterStore.Machine.programStepTM {n : ℕ} (tapes : ControlInstructionTapes n) (program : Program) : TM (n + 1)

Select and execute one RAM instruction, then restore the clean instruction ABI for the successor snapshot.

Equations

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

def Complexity.RAM.RegisterStore.Machine.programStepSourceHeadBound {n : ℕ} (tapes : ControlInstructionTapes n) (program : Program) (pcValue : ℕ) (store : Store) : ℕ

Source-head bound available after fixed-program selection and execution.

Equations

• Complexity.RAM.RegisterStore.Machine.programStepSourceHeadBound tapes program pcValue store = 1 + Complexity.RAM.RegisterStore.Machine.programInstructionTime tapes program pcValue store

noncomputable def Complexity.RAM.RegisterStore.Machine.programStepTime {n : ℕ} (tapes : ControlInstructionTapes n) (program : Program) (pcValue : ℕ) (store : Store) : ℕ

Exact compositional time bound for one selected and cleaned RAM step.

Equations

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