Width-driven binary shift-and-add multiplication -- definitions

This module defines a six-work-tape multiplication ABI and a concrete least-significant-bit-first shift-and-add machine. The multiplicands are preserved, the accumulator receives their product, and three scratch tapes are returned to canonical zero.

def Complexity.BinaryShiftMul.step (bit : Bool) (acc shift : ℕ) : ℕ × ℕ

One pure shift-and-add iteration. The first component is the partial accumulator and the second is the current shifted multiplicand.

Equations

• Complexity.BinaryShiftMul.step bit acc shift = (if bit = true then acc + shift else acc, 2 * shift)

def Complexity.BinaryShiftMul.fold : List Bool → ℕ → ℕ → ℕ × ℕ

Fold little-endian multiplier bits through generalized initial accumulator and shift values.

Equations

• Complexity.BinaryShiftMul.fold [] x✝¹ x✝ = (x✝¹, x✝)
• Complexity.BinaryShiftMul.fold (bit :: bits) x✝¹ x✝ = Complexity.BinaryShiftMul.fold bits (Complexity.BinaryShiftMul.step bit x✝¹ x✝).1 (Complexity.BinaryShiftMul.step bit x✝¹ x✝).2

def Complexity.BinaryShiftMul.partialAcc (lhs rhs i : ℕ) : ℕ

Accumulator value after the first i little-endian multiplier bits.

Equations

• Complexity.BinaryShiftMul.partialAcc lhs rhs i = lhs * Nat.fromBitsLE (List.take i rhs.bits)

def Complexity.BinaryShiftMul.partialShift (lhs i : ℕ) : ℕ

Shifted multiplicand after i iterations.

Equations

• Complexity.BinaryShiftMul.partialShift lhs i = lhs * 2 ^ i

structure Complexity.TM.BinaryShiftMulABI (n : ℕ) : Type

Compact injective assignment of the six multiplication roles to work tapes. Injectivity makes every pair of roles structurally distinct.

• tape : Fin 6 ↪ Fin n

  Injective map from semantic roles to physical work tapes.

def Complexity.TM.BinaryShiftMulABI.lhs {n : ℕ} (abi : BinaryShiftMulABI n) : Fin n

Preserved multiplicand tape.

Equations

• abi.lhs = abi.tape 0

def Complexity.TM.BinaryShiftMulABI.rhs {n : ℕ} (abi : BinaryShiftMulABI n) : Fin n

Preserved multiplier and loop-driver tape.

Equations

• abi.rhs = abi.tape 1

def Complexity.TM.BinaryShiftMulABI.acc {n : ℕ} (abi : BinaryShiftMulABI n) : Fin n

Initially-zero output accumulator tape.

Equations

• abi.acc = abi.tape 2

def Complexity.TM.BinaryShiftMulABI.shift {n : ℕ} (abi : BinaryShiftMulABI n) : Fin n

Current shifted multiplicand tape.

Equations

• abi.shift = abi.tape 3

def Complexity.TM.BinaryShiftMulABI.tmp {n : ℕ} (abi : BinaryShiftMulABI n) : Fin n

First alternating zero scratch tape.

Equations

• abi.tmp = abi.tape 4

def Complexity.TM.BinaryShiftMulABI.dbl {n : ℕ} (abi : BinaryShiftMulABI n) : Fin n

Second alternating zero scratch tape.

Equations

• abi.dbl = abi.tape 5

theorem Complexity.TM.BinaryShiftMulABI.tape_ne {n : ℕ} (abi : BinaryShiftMulABI n) {first second : Fin 6} (hne : first ≠ second) : abi.tape first ≠ abi.tape second

Distinct ABI slots map to distinct work tapes.

@[simp]

theorem Complexity.TM.BinaryShiftMulABI.lhs_ne_rhs {n : ℕ} (abi : BinaryShiftMulABI n) : abi.lhs ≠ abi.rhs

@[simp]

theorem Complexity.TM.BinaryShiftMulABI.lhs_ne_acc {n : ℕ} (abi : BinaryShiftMulABI n) : abi.lhs ≠ abi.acc

@[simp]

theorem Complexity.TM.BinaryShiftMulABI.lhs_ne_shift {n : ℕ} (abi : BinaryShiftMulABI n) : abi.lhs ≠ abi.shift

@[simp]

theorem Complexity.TM.BinaryShiftMulABI.lhs_ne_tmp {n : ℕ} (abi : BinaryShiftMulABI n) : abi.lhs ≠ abi.tmp

@[simp]

theorem Complexity.TM.BinaryShiftMulABI.lhs_ne_dbl {n : ℕ} (abi : BinaryShiftMulABI n) : abi.lhs ≠ abi.dbl

@[simp]

theorem Complexity.TM.BinaryShiftMulABI.rhs_ne_acc {n : ℕ} (abi : BinaryShiftMulABI n) : abi.rhs ≠ abi.acc

@[simp]

theorem Complexity.TM.BinaryShiftMulABI.rhs_ne_shift {n : ℕ} (abi : BinaryShiftMulABI n) : abi.rhs ≠ abi.shift

@[simp]

theorem Complexity.TM.BinaryShiftMulABI.rhs_ne_tmp {n : ℕ} (abi : BinaryShiftMulABI n) : abi.rhs ≠ abi.tmp

@[simp]

theorem Complexity.TM.BinaryShiftMulABI.rhs_ne_dbl {n : ℕ} (abi : BinaryShiftMulABI n) : abi.rhs ≠ abi.dbl

@[simp]

theorem Complexity.TM.BinaryShiftMulABI.acc_ne_shift {n : ℕ} (abi : BinaryShiftMulABI n) : abi.acc ≠ abi.shift

@[simp]

theorem Complexity.TM.BinaryShiftMulABI.acc_ne_tmp {n : ℕ} (abi : BinaryShiftMulABI n) : abi.acc ≠ abi.tmp

@[simp]

theorem Complexity.TM.BinaryShiftMulABI.acc_ne_dbl {n : ℕ} (abi : BinaryShiftMulABI n) : abi.acc ≠ abi.dbl

@[simp]

theorem Complexity.TM.BinaryShiftMulABI.shift_ne_tmp {n : ℕ} (abi : BinaryShiftMulABI n) : abi.shift ≠ abi.tmp

@[simp]

theorem Complexity.TM.BinaryShiftMulABI.shift_ne_dbl {n : ℕ} (abi : BinaryShiftMulABI n) : abi.shift ≠ abi.dbl

@[simp]

theorem Complexity.TM.BinaryShiftMulABI.tmp_ne_dbl {n : ℕ} (abi : BinaryShiftMulABI n) : abi.tmp ≠ abi.dbl

def Complexity.TM.binaryShiftMulInitTM {n : ℕ} (abi : BinaryShiftMulABI n) : TM n

Initialize the shifted multiplicand from lhs, using the zero accumulator as the copy routine's preserved zero scratch.

Equations

• Complexity.TM.binaryShiftMulInitTM abi = Complexity.TM.binaryCopyIntoTM abi.lhs abi.shift abi.acc

def Complexity.TM.binaryShiftMulUpdateTM {n : ℕ} (abi : BinaryShiftMulABI n) : TM n

Add the current shift into the accumulator. The sum is formed on tmp, copied back through zero scratch dbl, and tmp is reset.

Equations

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

def Complexity.TM.binaryShiftMulDoubleTM {n : ℕ} (abi : BinaryShiftMulABI n) : TM n

Double shift. A copy on tmp is added back into dbl; after alternating copy-back and resets, shift contains twice its old value and both scratch tapes are zero.

Equations

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

def Complexity.TM.binaryShiftMulOneTM {n : ℕ} (abi : BinaryShiftMulABI n) : TM n

Execute the conditional add and then the unconditional doubling step.

Equations

• Complexity.TM.binaryShiftMulOneTM abi = (Complexity.TM.binaryShiftMulUpdateTM abi).seqTM (Complexity.TM.binaryShiftMulDoubleTM abi)

def Complexity.TM.binaryShiftMulBitBodyTM {n : ℕ} (abi : BinaryShiftMulABI n) : TM n

Branch on the current multiplier bit. A one performs update-and-double; every other dispatched Boolean symbol performs only the doubling step.

Equations

• Complexity.TM.binaryShiftMulBitBodyTM abi = Complexity.TM.branchWorkSymbolTM abi.rhs Complexity.Γ.one (Complexity.TM.binaryShiftMulOneTM abi) (Complexity.TM.binaryShiftMulDoubleTM abi)

def Complexity.TM.binaryShiftMulLoopTM {n : ℕ} (abi : BinaryShiftMulABI n) : TM n

Iterate once per canonical bit on the preserved multiplier tape.

Equations

• Complexity.TM.binaryShiftMulLoopTM abi = Complexity.TM.forBinaryWorkTM abi.rhs (Complexity.TM.binaryShiftMulBitBodyTM abi)

def Complexity.TM.binaryShiftMulCleanupTM {n : ℕ} (abi : BinaryShiftMulABI n) : TM n

Restore the multiplier head and reset every non-output scratch tape.

Equations

• Complexity.TM.binaryShiftMulCleanupTM abi = (Complexity.TM.rewindWorkTM abi.rhs).seqTM (Complexity.TM.resetBinaryWorkManyTM [abi.shift, abi.tmp, abi.dbl])

def Complexity.TM.binaryShiftMulTM {n : ℕ} (abi : BinaryShiftMulABI n) : TM n

Initialize, scan the multiplier, and clean up the six-tape shift-and-add implementation.

Equations

• Complexity.TM.binaryShiftMulTM abi = (Complexity.TM.binaryShiftMulInitTM abi).seqTM ((Complexity.TM.binaryShiftMulLoopTM abi).seqTM (Complexity.TM.binaryShiftMulCleanupTM abi))

def Complexity.TM.binaryShiftMulWidth (lhs rhs : ℕ) : ℕ

Combined input width used by the conservative multiplication budget.

Equations

• Complexity.TM.binaryShiftMulWidth lhs rhs = lhs.size + rhs.size

def Complexity.TM.binaryShiftMulTime (lhs rhs : ℕ) : ℕ

Audited conservative quadratic budget for initialization, all multiplier iterations, cleanup, and composition seams.

Equations

• Complexity.TM.binaryShiftMulTime lhs rhs = 33 * Complexity.TM.binaryShiftMulWidth lhs rhs ^ 2 + 170 * Complexity.TM.binaryShiftMulWidth lhs rhs + 58