Canonical binary multiply-add — proof internals

The outer canonical count-up loop invokes verified binary addition once per right-operand value. Since the public addition contract is a time upper bound, the loop certificate chooses its actual deterministic body runtime privately and proves that the resulting exact loop runtime is bounded by the public formula. Space is proved compositionally for each repeated-addition iteration, so it depends on binary widths rather than on the number of loop steps.

def Complexity.TM.binaryMulAddNatTape (value : ℕ) : Tape

Canonical parked tape encoding of a natural for multiply-add.

Equations

• Complexity.TM.binaryMulAddNatTape value = (Complexity.Tape.init (List.map Complexity.Γ.ofBool value.bits)).move Complexity.Dir3.right

@[reducible, inline]

abbrev Complexity.TM.binaryMulAddFramePred {n : ℕ} (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) : TapePred n

Predicate fixing the tapes framing a binary multiply-add execution.

Equations

• Complexity.TM.binaryMulAddFramePred inp₀ work₀ out₀ inp work out = (inp = inp₀ ∧ work = work₀ ∧ out = out₀)

theorem Complexity.TM.binaryMulAddIntoTM_hoareTime_frame_internal {n : ℕ} (leftIdx rightIdx accIdx mulCounterIdx addCounterIdx : Fin n) (hdistinct : BinaryMulAddDistinct leftIdx rightIdx accIdx mulCounterIdx addCounterIdx) (leftValue rightValue accValue : ℕ) (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) (hleft : (work₀ leftIdx).HasBinaryNat leftValue) (hright : (work₀ rightIdx).HasBinaryNat rightValue) (hacc : (work₀ accIdx).HasBinaryNat accValue) (hmulCounter : (work₀ mulCounterIdx).HasBinaryNat 0) (haddCounter : (work₀ addCounterIdx).HasBinaryNat 0) (hinp : Parked inp₀) (hother : ∀ (i : Fin n), i ≠ leftIdx → i ≠ rightIdx → i ≠ accIdx → i ≠ mulCounterIdx → i ≠ addCounterIdx → Parked (work₀ i)) (hout : Parked out₀) : (binaryMulAddIntoTM leftIdx rightIdx accIdx mulCounterIdx addCounterIdx).HoareTime (binaryMulAddFramePred inp₀ work₀ out₀) (binaryMulAddFramePred inp₀ (Function.update work₀ accIdx (binaryMulAddNatTape (accValue + leftValue * rightValue))) out₀) (binaryMulAddTime leftValue rightValue accValue)

Multiply-add restores both counters and preserves the literal frame.

theorem Complexity.TM.binaryMulAddIntoTM_hoareTimeSpace_frame_internal {n : ℕ} (leftIdx rightIdx accIdx mulCounterIdx addCounterIdx : Fin n) (hdistinct : BinaryMulAddDistinct leftIdx rightIdx accIdx mulCounterIdx addCounterIdx) (leftValue rightValue accValue inputLength initialSpace : ℕ) (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) (hleft : (work₀ leftIdx).HasBinaryNat leftValue) (hright : (work₀ rightIdx).HasBinaryNat rightValue) (hacc : (work₀ accIdx).HasBinaryNat accValue) (hmulCounter : (work₀ mulCounterIdx).HasBinaryNat 0) (haddCounter : (work₀ addCounterIdx).HasBinaryNat 0) (hinp : Parked inp₀) (hother : ∀ (i : Fin n), i ≠ leftIdx → i ≠ rightIdx → i ≠ accIdx → i ≠ mulCounterIdx → i ≠ addCounterIdx → Parked (work₀ i)) (hout : Parked out₀) (hworkSpace : ∀ (i : Fin n), (work₀ i).head ≤ initialSpace) (hinputSpace : inp₀.head ≤ inputLength + initialSpace + 1) : (binaryMulAddIntoTM leftIdx rightIdx accIdx mulCounterIdx addCounterIdx).HoareTimeSpace (binaryMulAddFramePred inp₀ work₀ out₀) (binaryMulAddFramePred inp₀ (Function.update work₀ accIdx (binaryMulAddNatTape (accValue + leftValue * rightValue))) out₀) (binaryMulAddTime leftValue rightValue accValue) inputLength (binaryMulAddSpace initialSpace leftValue rightValue accValue)

Multiply-add has an honest all-prefix width-based space bound.

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

Binary multiply-add never moves its output head left.