Dense-overlay RAM decision-machine resource-bound definitions

The optimized accounting keeps the live serialized overlay separate from the width charged by the instruction actually selected at the current program counter. This is the local product that sums quadratically over a run.

def Complexity.RAM.RegisterStore.Machine.denseStepWidth (program : Program) (input : List Bool) (snapshot : DenseOverlay.Snapshot) : ℕ

Width charged by the selected instruction, including the fixed program literals.

Equations

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

def Complexity.RAM.RegisterStore.Machine.denseStepVolume (program : Program) (input : List Bool) (snapshot : DenseOverlay.Snapshot) : ℕ

Local amount of serialized data exposed to one dense simulated step.

Equations

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

def Complexity.RAM.RegisterStore.Machine.denseStepEnvelope (program : Program) (input : List Bool) (snapshot : DenseOverlay.Snapshot) : ℕ

Width-sensitive envelope for one selected dense step. The program magnitude is fixed once the simulated RAM program is fixed.

Equations

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

def Complexity.RAM.RegisterStore.Machine.denseRunScale (program : Program) (input : List Bool) (fuel : ℕ) (snapshot : DenseOverlay.Snapshot) : ℕ

Potential controlling a complete dense run. Its square absorbs both live overlay growth and the sum of selected-instruction widths. The explicit fuel reserve also pays for the conservative loop timer after an early halt, when the semantic RAM costs have become stationary.

Equations

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

def Complexity.RAM.RegisterStore.Machine.denseProgramLoopEnvelope (program : Program) (input : List Bool) (fuel : ℕ) (snapshot : DenseOverlay.Snapshot) : ℕ

Quadratic envelope for a complete dense loop from an arbitrary valid snapshot.

Equations

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

def Complexity.RAM.RegisterStore.Machine.denseProgramDecisionEnvelope (program : Program) (inputLength cost : ℕ) : ℕ

Public-ABI quadratic envelope in input length and charged RAM time.

Equations

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