Structured RAM Hamming-weight program — definitions

The benchmark uses a small reserved-register ABI: registers R₀ through R₄ hold loop state and input bits start at R₅. This avoids the existing raw RAM input convention's overlap between an unbounded input and fixed scratch registers.

def Complexity.RAM.Structured.Hamming.lengthReg : ℕ

Remaining input length and final-result register.

Equations

• Complexity.RAM.Structured.Hamming.lengthReg = 0

def Complexity.RAM.Structured.Hamming.countReg : ℕ

Hamming-weight accumulator register.

Equations

• Complexity.RAM.Structured.Hamming.countReg = 1

def Complexity.RAM.Structured.Hamming.pointerReg : ℕ

Address of the next input bit.

Equations

• Complexity.RAM.Structured.Hamming.pointerReg = 2

def Complexity.RAM.Structured.Hamming.oneReg : ℕ

Constant-one register used for increments and decrements.

Equations

• Complexity.RAM.Structured.Hamming.oneReg = 3

def Complexity.RAM.Structured.Hamming.scratchReg : ℕ

Temporary register receiving the current input bit.

Equations

• Complexity.RAM.Structured.Hamming.scratchReg = 4

def Complexity.RAM.Structured.Hamming.inputBase : ℕ

First register occupied by input data under the reserved-register ABI.

Equations

• Complexity.RAM.Structured.Hamming.inputBase = 5

def Complexity.RAM.Structured.Hamming.bitValue (bit : Bool) : ℕ

Natural-number representation of one input bit.

Equations

• Complexity.RAM.Structured.Hamming.bitValue bit = Complexity.RAM.Structured.Input.bitValue bit

def Complexity.RAM.Structured.Hamming.weight : List Bool → ℕ

Mathematical Hamming weight of a Boolean list.

Equations

• Complexity.RAM.Structured.Hamming.weight [] = 0
• Complexity.RAM.Structured.Hamming.weight (bit :: rest) = Complexity.RAM.Structured.Hamming.bitValue bit + Complexity.RAM.Structured.Hamming.weight rest

def Complexity.RAM.Structured.Hamming.inputStore (bits : List Bool) : Store

Reserved-register input layout for the structured benchmark.

Equations

• Complexity.RAM.Structured.Hamming.inputStore bits = Complexity.RAM.Structured.Input.bitStore Complexity.RAM.Structured.Hamming.lengthReg Complexity.RAM.Structured.Hamming.inputBase bits

def Complexity.RAM.Structured.Hamming.setupOps : List Basic

Basic instructions that initialize the accumulator, input pointer, and constant-one register.

Equations

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

def Complexity.RAM.Structured.Hamming.setup : Cmd

Initialize the Hamming loop registers.

Equations

• Complexity.RAM.Structured.Hamming.setup = Complexity.RAM.Structured.Cmd.basics Complexity.RAM.Structured.Hamming.setupOps

def Complexity.RAM.Structured.Hamming.body : Cmd

One Hamming-weight loop iteration.

Equations

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

def Complexity.RAM.Structured.Hamming.mainLoop : Cmd

Process input bits until the remaining-length register reaches zero.

Equations

• Complexity.RAM.Structured.Hamming.mainLoop = Complexity.RAM.Structured.Cmd.whileNonzero Complexity.RAM.Structured.Hamming.lengthReg Complexity.RAM.Structured.Hamming.body

def Complexity.RAM.Structured.Hamming.finalize : Cmd

Copy the accumulator to the result register R₀.

Equations

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

def Complexity.RAM.Structured.Hamming.program : Cmd

Complete structured Hamming-weight program.

Equations

• Complexity.RAM.Structured.Hamming.program = Complexity.RAM.Structured.Hamming.setup.seq (Complexity.RAM.Structured.Hamming.mainLoop.seq Complexity.RAM.Structured.Hamming.finalize)

def Complexity.RAM.Structured.Hamming.compiled : Program

Concrete compiled RAM program for Hamming weight.

Equations

• Complexity.RAM.Structured.Hamming.compiled = Complexity.RAM.Structured.Hamming.program.compile

def Complexity.RAM.Structured.Hamming.stepCount (bits : List Bool) : ℕ

Exact number of target RAM transitions needed to reach the compiled halt instruction. A zero bit uses six loop transitions and a one bit uses eight.

Equations

• Complexity.RAM.Structured.Hamming.stepCount bits = 6 + 6 * bits.length + 2 * Complexity.RAM.Structured.Hamming.weight bits

def Complexity.RAM.Structured.Hamming.timeBound (inputLength : ℕ) : ℕ

Explicit logarithmic-cost time budget as a function of input length. The constant is deliberately simple: the important content is the linear number of operations, each on values of O(bitlen n) bits.

Equations

• Complexity.RAM.Structured.Hamming.timeBound inputLength = 64 * (inputLength + 1) * (Complexity.RAM.bitlen (inputLength + 5) + 1)

def Complexity.RAM.Structured.Hamming.spaceBound (inputLength : ℕ) : ℕ

Explicit peak-space budget for the reserved-register input representation. There are at most inputLength + 5 nonzero registers, and both an occupied register index and its value have at most bitlen (inputLength + 5) bits.

Equations

• Complexity.RAM.Structured.Hamming.spaceBound inputLength = (inputLength + 5) * (2 * Complexity.RAM.bitlen (inputLength + 5))

def Complexity.RAM.Structured.Hamming.quasilinearBound (inputLength : ℕ) : ℕ

A shifted n · bitlen n comparison function used to state the benchmark's quasilinear time and space bounds without hiding small-input behavior.

Equations

• Complexity.RAM.Structured.Hamming.quasilinearBound inputLength = (inputLength + 5) * (Complexity.RAM.bitlen (inputLength + 5) + 1)