Width-driven binary shift-and-add multiplication -- composed semantics

This file composes the width-linear copy and ripple-add primitives through a bit-driven work-tape loop. The multiplier cursor is preserved by every body phase and advanced only by the loopback seam.

def Complexity.TM.binaryShiftMulPost {n : ℕ} (abi : BinaryShiftMulABI n) (lhs rhs : ℕ) (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) : TapePred n

Postcondition for completed shift-and-add binary multiplication.

Equations

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

theorem Complexity.TM.binaryShiftMulTM_hoareTime_frame_internal {n : ℕ} (abi : BinaryShiftMulABI n) (lhs rhs : ℕ) (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) (hlhs : (work₀ abi.lhs).HasBinaryNat lhs) (hrhs : (work₀ abi.rhs).HasBinaryNat rhs) (hacc : (work₀ abi.acc).HasBinaryNat 0) (hshift : (work₀ abi.shift).HasBinaryNat 0) (htmp : (work₀ abi.tmp).HasBinaryNat 0) (hdbl : (work₀ abi.dbl).HasBinaryNat 0) (hinput : Parked inp₀) (hwork : ∀ (i : Fin n), Parked (work₀ i)) (houtput : Parked out₀) : (binaryShiftMulTM abi).HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = work₀ ∧ out = out₀) (binaryShiftMulPost abi lhs rhs inp₀ work₀ out₀) (binaryShiftMulTime lhs rhs)

The concrete shift-and-add multiplier preserves both operands, writes their product to the accumulator, clears all three scratch tapes, and preserves the complete external frame.

theorem Complexity.TM.binaryShiftMulTM_hoareTimeSpace_frame_internal {n : ℕ} (abi : BinaryShiftMulABI n) (lhs rhs inputLength initialSpace : ℕ) (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) (hlhs : (work₀ abi.lhs).HasBinaryNat lhs) (hrhs : (work₀ abi.rhs).HasBinaryNat rhs) (hacc : (work₀ abi.acc).HasBinaryNat 0) (hshift : (work₀ abi.shift).HasBinaryNat 0) (htmp : (work₀ abi.tmp).HasBinaryNat 0) (hdbl : (work₀ abi.dbl).HasBinaryNat 0) (hinput : Parked inp₀) (hwork : ∀ (i : Fin n), Parked (work₀ i)) (houtput : Parked out₀) (hinitial : { state := (binaryShiftMulTM abi).qstart, input := inp₀, work := work₀, output := out₀ }.WithinAuxSpace inputLength initialSpace) : (binaryShiftMulTM abi).HoareTimeSpace (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = work₀ ∧ out = out₀) (binaryShiftMulPost abi lhs rhs inp₀ work₀ out₀) (binaryShiftMulTime lhs rhs) inputLength (initialSpace + binaryShiftMulTime lhs rhs)

Coarse all-prefix auxiliary-space contract inherited from the concrete quadratic time envelope.