Canonical binary multiply-add — definitions

This module defines multiply-add by nesting the canonical binary addition routine inside a canonical binary count-up loop. Five pairwise-distinct work tapes hold a preserved left operand, a preserved right operand, an updated accumulator, an outer multiplication counter, and the addition routine's private counter. Both counters are restored to canonical zero.

structure Complexity.TM.BinaryMulAddDistinct {n : ℕ} (leftIdx rightIdx accIdx mulCounterIdx addCounterIdx : Fin n) : Prop

The five work-tape roles of binary multiply-add are pairwise distinct.

• left_ne_right : leftIdx ≠ rightIdx
• left_ne_acc : leftIdx ≠ accIdx
• left_ne_mulCounter : leftIdx ≠ mulCounterIdx
• left_ne_addCounter : leftIdx ≠ addCounterIdx
• right_ne_acc : rightIdx ≠ accIdx
• right_ne_mulCounter : rightIdx ≠ mulCounterIdx
• right_ne_addCounter : rightIdx ≠ addCounterIdx
• acc_ne_mulCounter : accIdx ≠ mulCounterIdx
• acc_ne_addCounter : accIdx ≠ addCounterIdx
• mulCounter_ne_addCounter : mulCounterIdx ≠ addCounterIdx

def Complexity.TM.binaryMulAddLoopTM {n : ℕ} (leftIdx rightIdx accIdx mulCounterIdx addCounterIdx : Fin n) : TM n

Repeatedly add leftIdx into accIdx, once per value below rightIdx. The addition counter is restored by every body invocation; the multiplication counter equals the right operand when this loop halts.

Equations

• Complexity.TM.binaryMulAddLoopTM leftIdx rightIdx accIdx mulCounterIdx addCounterIdx = (Complexity.TM.binaryAddIntoTM leftIdx accIdx addCounterIdx).binaryForTM mulCounterIdx rightIdx

def Complexity.TM.binaryMulAddIntoTM {n : ℕ} (leftIdx rightIdx accIdx mulCounterIdx addCounterIdx : Fin n) : TM n

Add the product of two preserved canonical binary operands into an accumulator, then restore the outer multiplication counter to zero.

Equations

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

def Complexity.TM.binaryMulAddLoopTime (leftValue rightValue accValue : ℕ) : ℕ

Public upper bound for the nested repeated-addition loop.

Equations

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

def Complexity.TM.binaryMulAddTime (leftValue rightValue accValue : ℕ) : ℕ

Public time bound for multiply-add, including the composition seam and restoration of the outer counter.

Equations

• Complexity.TM.binaryMulAddTime leftValue rightValue accValue = Complexity.TM.binaryMulAddLoopTime leftValue rightValue accValue + 1 + Complexity.TM.clearWorkTimeBound rightValue.size

def Complexity.TM.binaryMulAddLoopSpace (initialSpace leftValue rightValue accValue : ℕ) : ℕ

All-prefix space bound for the repeated-addition loop. The bound uses only binary widths: the largest accumulator value, the left operand, and the right operand.

Equations

• Complexity.TM.binaryMulAddLoopSpace initialSpace leftValue rightValue accValue = Complexity.TM.binaryAddSpace initialSpace leftValue (accValue + leftValue * rightValue) + 2 * rightValue.size + 2

def Complexity.TM.binaryMulAddSpace (initialSpace leftValue rightValue accValue : ℕ) : ℕ

All-prefix space bound for multiply-add followed by counter restoration.

Equations

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