Sparse RAM program controller -- definitions

This layer adds the fixed-program halt test needed to iterate the checked single-instruction simulator. The test copies the canonical program counter, walks the same decrementing finite branch tree as instruction dispatch, and writes 1 exactly for a selected halt; every continuing branch writes blank.

inductive Complexity.RAM.RegisterStore.Machine.HaltVerdictPhase : Type

Two-state leaf that writes one halt verdict at the current output head.

• write : HaltVerdictPhase
• done : HaltVerdictPhase

@[implicit_reducible]

instance Complexity.RAM.RegisterStore.Machine.instDecidableEqHaltVerdictPhase : DecidableEq HaltVerdictPhase

Equations

• Complexity.RAM.RegisterStore.Machine.instDecidableEqHaltVerdictPhase x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Complexity.RAM.RegisterStore.Machine.instFintypeHaltVerdictPhase : Fintype HaltVerdictPhase

Equations

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

def Complexity.RAM.RegisterStore.Machine.instructionHaltVerdict : Instr → Γw

Output symbol used by the fixed-program halt test. Continuing instructions write blank so the instruction body regains its blank-output ABI.

Equations

• Complexity.RAM.RegisterStore.Machine.instructionHaltVerdict Complexity.RAM.Instr.halt = Complexity.Γw.one
• Complexity.RAM.RegisterStore.Machine.instructionHaltVerdict x✝ = Complexity.Γw.blank

def Complexity.RAM.RegisterStore.Machine.instructionHaltOutput (instruction : Instr) : Tape

Canonical output tape produced by one halt-verdict leaf.

Equations

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

def Complexity.RAM.RegisterStore.Machine.instructionHaltVerdictTM {n : ℕ} (instruction : Instr) : TM n

Write the selected instruction's halt verdict in one transition while preserving input and work tapes.

Equations

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

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

Decrementing fixed-program branch tree for the halt verdict.

Equations

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

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

Copy the canonical PC and emit whether its fixed-program instruction is halt.

Equations

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

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

Branch-tree bound for a selector represented by selector.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.RAM.RegisterStore.Machine.dispatchHaltTime tapes [] x✝ = Complexity.TM.resetBinaryWorkTime 1 x✝.bits.length + 1 + 1

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

Complete fixed-program halt-test bound.

Equations

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

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

Repeated pure sparse-snapshot stepping without an explicit halt check. Because the selected halt instruction is a no-op, this agrees with Snapshot.run.

Equations

• Complexity.RAM.RegisterStore.Machine.snapshotSteps program 0 x✝ = x✝
• Complexity.RAM.RegisterStore.Machine.snapshotSteps program fuel.succ x✝ = Complexity.RAM.RegisterStore.Machine.snapshotSteps program fuel (Complexity.RAM.RegisterStore.Snapshot.step program x✝)

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

Canonical parked tape containing one Boolean string.

Equations

• Complexity.RAM.RegisterStore.Machine.programBinaryTape bits = (Complexity.Tape.init (List.map Complexity.Γ.ofBool bits)).move Complexity.Dir3.right

def Complexity.RAM.RegisterStore.Machine.programSnapshotWork {n : ℕ} (tapes : ControlInstructionTapes n) (snapshot : Snapshot) : Fin (n + 1) → Tape

Exact clean work-tape image of one sparse RAM snapshot. The store stream, runtime count, preserved count, and program counter occupy their established instruction-ABI roles; every other tape is the standard parked blank tape.

Equations

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

def Complexity.RAM.RegisterStore.Machine.registerVerdictSymbol (value : ℕ) : Γw

Boolean output symbol obtained from the RAM verdict convention.

Equations

• Complexity.RAM.RegisterStore.Machine.registerVerdictSymbol value = if value = 0 then Complexity.Γw.zero else Complexity.Γw.one

def Complexity.RAM.RegisterStore.Machine.registerVerdictOutput (value : ℕ) : Tape

Exact output tape emitted from one RAM register value.

Equations

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

def Complexity.RAM.RegisterStore.Machine.registerVerdictTM {n : ℕ} (idx : Fin n) : TM n

Read a canonical register-value tape and emit zero exactly for value zero, or one for any nonzero value.

Equations

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

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

Recover register R₀ through the reusable sparse lookup and emit its Boolean verdict on the real output tape.

Equations

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

def Complexity.RAM.RegisterStore.Machine.programOutputTime {n : ℕ} (tapes : ControlInstructionTapes n) (store : Store) : ℕ

Complete final-verdict extraction bound.

Equations

• Complexity.RAM.RegisterStore.Machine.programOutputTime tapes store = Complexity.RAM.RegisterStore.Machine.entryLookupStaticTime tapes.lifted.data.lhsLookup store 0 + 1 + 1

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

Fixed halt-aware loop for one concrete RAM program.

Equations

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

noncomputable def Complexity.RAM.RegisterStore.Machine.programLoopIterationTime {n : ℕ} (tapes : ControlInstructionTapes n) (program : Program) (snapshot : Snapshot) : ℕ

Bound for one loop body, body/test seams, halt test, and the three-step rewind/check tail.

Equations

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

noncomputable def Complexity.RAM.RegisterStore.Machine.programLoopTime {n : ℕ} (tapes : ControlInstructionTapes n) (program : Program) : ℕ → Snapshot → ℕ

Sum of the first fuel loop-iteration bounds.

Equations

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