2.4. Multiplication by Constant (Paper Section 4.1)

The paper presents add_mulc, a macro that generates shift-and-add sequences for constant multiplication. Given add_mulcFast EDI EDX #160, it produces:

SHL EDX, 5;;
ADD EDI, EDX;;
LEA EDI, [EDI + EDX * 4 + 0]

Crucially, this macro has a proved specification:

Lemma add_mulcCorrect nbits : forall (r1 r2: Reg) m,
  m < 2^nbits ->
  basic
    (r1 |-> v ** r2 |-> w ** OSZCP_Any)
    (add_mulc nbits r1 r2 m)
    (r1 |-> addB v (mulB w (fromNat m)) ** r2? ** OSZCP_Any).