Dense-overlay public-input initialization -- definitions

The optimized initializer counts the immutable input in binary but emits only the tagged R₀ overlay entry. It then installs the ordinary sparse scanner ABI and rewinds the real input for dense fallback reads.

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

Phases of the input-length counter.

• scan : DenseInitialLengthPhase
• done : DenseInitialLengthPhase

@[implicit_reducible]

instance Complexity.RAM.RegisterStore.Machine.instDecidableEqDenseInitialLengthPhase : DecidableEq DenseInitialLengthPhase

Equations

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

@[implicit_reducible]

instance Complexity.RAM.RegisterStore.Machine.instFintypeDenseInitialLengthPhase : Fintype DenseInitialLengthPhase

Equations

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

@[reducible, inline]

abbrev Complexity.RAM.RegisterStore.Machine.DenseInitialLengthQ {n : ℕ} (tapes : ControlInstructionTapes n) : Type

State space for input scanning with one binary-successor body.

Equations

• Complexity.RAM.RegisterStore.Machine.DenseInitialLengthQ tapes = (Complexity.RAM.RegisterStore.Machine.DenseInitialLengthPhase ⊕ (Complexity.RAM.RegisterStore.Machine.initialZeroBitTM tapes).Q)

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

Count every input symbol into the existing initialization address tape.

Equations

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

def Complexity.RAM.RegisterStore.Machine.denseInitialLengthLoopTime : ℕ → List Bool → ℕ

Exact recursive time budget for binary input-length counting.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.RAM.RegisterStore.Machine.denseInitialLengthLoopTime x✝ [] = 1

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

The lone positive-tag overlay installed for the public input.

Equations

• Complexity.RAM.RegisterStore.Machine.denseProgramInitialStore input = (Complexity.RAM.RegisterStore.DenseOverlay.Snapshot.initial input).overlay

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

Exact clean work image of a dense-overlay snapshot.

Equations

• Complexity.RAM.RegisterStore.Machine.denseProgramSnapshotWork tapes snapshot = Complexity.RAM.RegisterStore.Machine.programSnapshotWork tapes { pc := snapshot.pc, store := snapshot.overlay }

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

Count the input, emit its positive R₀ tag, install the sparse ABI, and rewind the immutable input bank to cell one.

Equations

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

def Complexity.RAM.RegisterStore.Machine.denseProgramInitTime {n : ℕ} (tapes : ControlInstructionTapes n) (input : List Bool) : ℕ

Exact compositional time budget for dense-overlay initialization.

Equations

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