Sparse RAM public-input initialization definitions

This layer constructs the reusable sparse-snapshot ABI from the standard TM input tape. It emits nonzero bit registers in increasing address order, then appends the nonzero length register R₀. The resulting order need not equal initialStore; it is a canonical sparse store representing the same total RAM register file.

def Complexity.RAM.RegisterStore.Machine.inputBitStoreFrom : ℕ → List Bool → Store

Nonzero public-input bit registers, beginning at address.

Equations

• Complexity.RAM.RegisterStore.Machine.inputBitStoreFrom x✝ [] = []
• Complexity.RAM.RegisterStore.Machine.inputBitStoreFrom x✝ (bit :: rest) = (if bit = true then [(x✝, 1)] else []) ++ Complexity.RAM.RegisterStore.Machine.inputBitStoreFrom (x✝ + 1) rest

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

Streaming-friendly public-input store: bit registers first and the nonzero length register last.

Equations

• Complexity.RAM.RegisterStore.Machine.programInitialStore input = Complexity.RAM.RegisterStore.write (Complexity.RAM.RegisterStore.Machine.inputBitStoreFrom 1 input) 0 input.length

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

Sparse initial snapshot used by the concrete initialization machine.

Equations

• Complexity.RAM.RegisterStore.Machine.programInitialSnapshot input = { pc := 0, store := Complexity.RAM.RegisterStore.Machine.programInitialStore input }

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

Number of nonzero entries emitted by the bit-register prefix.

Equations

• Complexity.RAM.RegisterStore.Machine.inputTrueCount [] = 0
• Complexity.RAM.RegisterStore.Machine.inputTrueCount (bit :: rest) = (if bit = true then 1 else 0) + Complexity.RAM.RegisterStore.Machine.inputTrueCount rest

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

Append-positioned binary tape for an emitted store prefix.

Equations

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

def Complexity.RAM.RegisterStore.Machine.initialLoopWork {n : ℕ} (tapes : ControlInstructionTapes n) (address count : ℕ) (entries : Store) : Fin (n + 1) → Tape

Exact work family at a streaming input-loop boundary.

Equations

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

structure Complexity.RAM.RegisterStore.Machine.InitialLoopReady {n : ℕ} (tapes : ControlInstructionTapes n) (address count : ℕ) (entries : Store) (work : Fin (n + 1) → Tape) : Prop

Streaming input-loop invariant. Only the current address, fixed value one, runtime entry count, and append buffer differ from the standard blank frame.

• address : (work tapes.liftedLhs).HasBinaryNat address
• value : (work tapes.lifted.data.rhs).HasBinaryNat 1
• count : (work tapes.lifted.data.update.remaining).HasBinaryNat count
• buffer : (work tapes.buffer).HasBinaryPrefix (List.flatMap Entry.encode entries)
• parked (i : Fin (n + 1)) : TM.Parked (work i)
• frame (i : Fin (n + 1)) : i ≠ tapes.liftedLhs → i ≠ tapes.lifted.data.rhs → i ≠ tapes.lifted.data.update.remaining → i ≠ tapes.buffer → work i = TM.resetBinaryBlank

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

Recursive work-independent streaming-loop bound.

Equations

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

def Complexity.RAM.RegisterStore.Machine.initialBitEntryTapes {n : ℕ} (tapes : ControlInstructionTapes n) : EntryEncodeTapes n

Dynamic address/value assignment for one nonzero input bit.

Equations

• Complexity.RAM.RegisterStore.Machine.initialBitEntryTapes tapes = { address := tapes.data.lhs, value := tapes.data.rhs, ne := ⋯ }

def Complexity.RAM.RegisterStore.Machine.initialLengthEntryTapes {n : ℕ} (tapes : ControlInstructionTapes n) : EntryEncodeTapes n

Address-zero/length assignment for the final R₀ entry.

Equations

• Complexity.RAM.RegisterStore.Machine.initialLengthEntryTapes tapes = { address := tapes.data.update.entry.query, value := tapes.data.lhs, ne := ⋯ }

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

Emit one nonzero bit entry, restore both entry sources to cell one, then increment the runtime entry count and current input address.

Equations

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

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

A zero input bit emits no entry and only advances the current address.

Equations

• Complexity.RAM.RegisterStore.Machine.initialZeroBitTM tapes = Complexity.TM.binarySuccTM tapes.liftedLhs

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

Driver phases for streaming over the real Boolean input.

• scan : InitialInputPhase
• done : InitialInputPhase

@[implicit_reducible]

instance Complexity.RAM.RegisterStore.Machine.instDecidableEqInitialInputPhase : DecidableEq InitialInputPhase

Equations

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

@[implicit_reducible]

instance Complexity.RAM.RegisterStore.Machine.instFintypeInitialInputPhase : Fintype InitialInputPhase

Equations

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

@[reducible, inline]

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

State space of the public-input bit loop.

Equations

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

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

Scan the real input without moving before body entry. Each 1 invokes the entry-emitting body, each 0 invokes the address-only body, and the preserving body seam advances the input by one cell.

Equations

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

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

Emit the nonzero R₀ = |input| entry and increment the entry count.

Equations

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

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

Skip the length entry at zero; otherwise append it to the buffer.

Equations

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

def Complexity.RAM.RegisterStore.Machine.initialLengthTime (length count : ℕ) : ℕ

Selected-branch bound for optional length-register emission.

Equations

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

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

Cleanup targets used after the complete input store has been copied into the read-only source role.

Equations

• Complexity.RAM.RegisterStore.Machine.initialCleanupTargets tapes = [tapes.liftedLhs, tapes.lifted.data.rhs]

def Complexity.RAM.RegisterStore.Machine.initialCleanupBits {n : ℕ} (tapes : ControlInstructionTapes n) (length : ℕ) (i : Fin (n + 1)) : List Bool

Canonical contents reset by the final two-target cleanup.

Equations

• Complexity.RAM.RegisterStore.Machine.initialCleanupBits tapes length i = if i = tapes.liftedLhs then length.bits else if i = tapes.lifted.data.rhs then Nat.bits 1 else []

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

Exact compositional bound for installing a completed store into the program-loop ABI.

Equations

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

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

Park the standard initial tapes and seed the streaming address/value sources with one.

Equations

• Complexity.RAM.RegisterStore.Machine.initialSetupTM tapes = Complexity.TM.skipTM.seqTM ((Complexity.TM.binarySuccTM tapes.liftedLhs).seqTM (Complexity.TM.binarySuccTM tapes.lifted.data.rhs))

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

Restore the address cursor from |input| + 1 to |input|, then append the optional nonzero length register.

Equations

• Complexity.RAM.RegisterStore.Machine.initialLengthInstallTM tapes = (Complexity.TM.binaryPredTM tapes.liftedLhs).seqTM (Complexity.RAM.RegisterStore.Machine.initialLengthTM tapes)

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

Copy the completed buffer into the reusable source/count roles and clear the remaining initialization temporaries.

Equations

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

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

Install the length entry, source/count ABI, and clean loop temporaries.

Equations

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

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

Complete public-input initialization. A leading skip parks every standard initial tape, the streaming loop writes the sparse store into the last buffer, and the tail installs the reusable source/count ABI and clears temporary roles.

Equations

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

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

Exact compositional time bound for complete public-input initialization.

Equations

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