Dense-overlay RAM instruction kernels -- definitions

These kernels retain the checked sparse scanner/update ABI while interpreting the immutable public input in place. Reads use the dense-overlay lookup and writes successor-tag their actual value before sparse update.

def Complexity.RAM.RegisterStore.Machine.denseBinaryInstructionUpdateTM {n : ℕ} (tapes : BinaryInstructionTapes n) (op : BinaryInstrOp) : TM n

Arithmetic followed by positive tagging and sparse overlay update.

Equations

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

def Complexity.RAM.RegisterStore.Machine.denseDirectBinaryInstructionTM {n : ℕ} (tapes : BinaryInstructionTapes n) (op : BinaryInstrOp) (destination source₀ source₁ : ℕ) : TM n

Two direct dense-overlay reads, arithmetic, and a tagged destination write.

Equations

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

def Complexity.RAM.RegisterStore.Machine.denseIndirectLoadInstructionTM {n : ℕ} (tapes : BinaryInstructionTapes n) (destination addressRegister : ℕ) : TM n

Dense-overlay indirect read followed by a tagged direct destination write.

Equations

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

def Complexity.RAM.RegisterStore.Machine.denseImmediateInstructionTM {n : ℕ} (tapes : BinaryInstructionTapes n) (destination value : ℕ) : TM n

Immediate assignment with its value converted to a positive overlay tag.

Equations

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

def Complexity.RAM.RegisterStore.Machine.denseIndirectStoreInstructionTM {n : ℕ} (tapes : BinaryInstructionTapes n) (addressRegister source : ℕ) : TM n

Dense-overlay indirect destination/source reads followed by a tagged write.

Equations

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

def Complexity.RAM.RegisterStore.Machine.denseZeroJumpInstructionTM {n : ℕ} (tapes : ControlInstructionTapes n) (source target : ℕ) : TM n

Conditional jump whose tested register is read through the dense overlay.

Equations

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

def Complexity.RAM.RegisterStore.Machine.DenseBinaryInstructionUpdateResult {n : ℕ} (tapes : BinaryInstructionTapes n) (op : BinaryInstrOp) (overlay : Store) (address lhs rhs : ℕ) (initialWork finalWork : Fin n → Tape) : Prop

Semantic endpoint of arithmetic and one tagged overlay update.

Equations

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

def Complexity.RAM.RegisterStore.Machine.DenseDirectBinaryOperandsResult {n : ℕ} (tapes : BinaryInstructionTapes n) (input : List Bool) (overlay : Store) (source₀ source₁ : ℕ) (initialWork finalWork : Fin n → Tape) : Prop

Boundary after two fixed-address dense-overlay reads.

Equations

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

def Complexity.RAM.RegisterStore.Machine.DenseDirectBinaryAddressResult {n : ℕ} (tapes : BinaryInstructionTapes n) (input : List Bool) (overlay : Store) (destination source₀ source₁ : ℕ) (initialWork finalWork : Fin n → Tape) : Prop

Boundary after dense operands and direct destination synthesis.

Equations

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

def Complexity.RAM.RegisterStore.Machine.DenseDirectBinaryInstructionResult {n : ℕ} (tapes : BinaryInstructionTapes n) (op : BinaryInstrOp) (input : List Bool) (overlay : Store) (destination source₀ source₁ : ℕ) (initialWork finalWork : Fin n → Tape) : Prop

Semantic endpoint of a complete dense direct arithmetic instruction.

Equations

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

def Complexity.RAM.RegisterStore.Machine.DenseImmediateInstructionResult {n : ℕ} (tapes : BinaryInstructionTapes n) (overlay : Store) (destination value : ℕ) (initialWork finalWork : Fin n → Tape) : Prop

Semantic endpoint of one dense immediate assignment.

Equations

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

def Complexity.RAM.RegisterStore.Machine.DenseIndirectLoadInstructionResult {n : ℕ} (tapes : BinaryInstructionTapes n) (input : List Bool) (overlay : Store) (destination addressRegister : ℕ) (initialWork finalWork : Fin n → Tape) : Prop

Semantic endpoint of a complete dense indirect load.

Equations

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

def Complexity.RAM.RegisterStore.Machine.DenseIndirectStoreInstructionResult {n : ℕ} (tapes : BinaryInstructionTapes n) (input : List Bool) (overlay : Store) (addressRegister source : ℕ) (initialWork finalWork : Fin n → Tape) : Prop

Semantic endpoint of a complete dense indirect store.

Equations

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

def Complexity.RAM.RegisterStore.Machine.denseBinaryInstructionUpdateTime {n : ℕ} (tapes : BinaryInstructionTapes n) (op : BinaryInstrOp) (overlay : Store) (address lhs rhs : ℕ) : ℕ

Runtime of arithmetic followed by positive tagging and overlay update.

Equations

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

def Complexity.RAM.RegisterStore.Machine.denseDirectBinaryInstructionTime {n : ℕ} (tapes : BinaryInstructionTapes n) (op : BinaryInstrOp) (input : List Bool) (overlay : Store) (destination source₀ source₁ : ℕ) : ℕ

Complete direct dense arithmetic-instruction budget.

Equations

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

def Complexity.RAM.RegisterStore.Machine.denseImmediateInstructionTime {n : ℕ} (tapes : BinaryInstructionTapes n) (overlay : Store) (destination value : ℕ) : ℕ

Complete immediate dense assignment budget.

Equations

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

def Complexity.RAM.RegisterStore.Machine.denseIndirectLoadInstructionTime {n : ℕ} (tapes : BinaryInstructionTapes n) (input : List Bool) (overlay : Store) (destination addressRegister : ℕ) : ℕ

Complete dense indirect-load instruction budget.

Equations

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

def Complexity.RAM.RegisterStore.Machine.denseIndirectStoreInstructionTime {n : ℕ} (tapes : BinaryInstructionTapes n) (input : List Bool) (overlay : Store) (addressRegister source : ℕ) : ℕ

Complete dense indirect-store instruction budget.

Equations

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

def Complexity.RAM.RegisterStore.Machine.denseZeroJumpInstructionTime {n : ℕ} (tapes : ControlInstructionTapes n) (input : List Bool) (overlay : Store) (pcValue source target : ℕ) : ℕ

Runtime for a conditional jump using one dense-overlay register read.

Equations

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