Add some assembly tests from BoringSSL p256

[JasonGross]

Towards better equivalence checking

cc @davidben @andres-erbsen

We don't support these instructions yet:

$ src/ExtractionOCaml/word_by_word_montgomery p256 64 '2^256 - 2^224 + 2^192 + 2^96 - 1' mul --no-wide-int --shiftr-avoid-uint1 --hints-file fiat-amd64/boringssl_intel_manual_mul_p256.asm
[...]
In parsing:
Error while parsing assembly:
mul    r9
mul    r10
mul    r11
mul    r12
mul    r15
mov    rax,QWORD PTR [rbx+0x8]
mul    QWORD PTR [rsi]
mul    QWORD PTR [rsi+0x8]
mul    QWORD PTR [rsi+0x10]
mul    QWORD PTR [rsi+0x18]
mul    r15
mov    rax,QWORD PTR [rbx+0x10]
mul    QWORD PTR [rsi]
mul    QWORD PTR [rsi+0x8]
mul    QWORD PTR [rsi+0x10]
mul    QWORD PTR [rsi+0x18]
mul    r15
mov    rax,QWORD PTR [rbx+0x18]
mul    QWORD PTR [rsi]
mul    QWORD PTR [rsi+0x8]
mul    QWORD PTR [rsi+0x10]
mul    QWORD PTR [rsi+0x18]
mul    r15
cmovb  r12,rcx
cmovb  r13,rbp
mov    QWORD PTR [rdi],r12
cmovb  r8,rbx
mov    QWORD PTR [rdi+0x8],r13
cmovb  r9,rdx
mov    QWORD PTR [rdi+0x10],r8
mov    QWORD PTR [rdi+0x18],r9
repz ret

Fatal error: exception Failure("Synthesis failed")

[JasonGross]

@davidben @andres-erbsen I'm staring at the equation that we want to hold:
(addcarry₆₄, [(#24 >>₆₄ 32), (addcarry₆₄, [#27, (#24 *₆₄ 2^32)])])
=?
(addcarry₆₄, [((#24 *ℤ 2^32-1) >>₆₄ 64), (addcarry₆₄, [(#24 *₆₄ 2^32-1), ((#24 *ℤ 2^64-1) >>₆₄ 64)]), (addcarry₆₄, [#27, ((#24 *₆₄ 2^32-1) +₆₄ ((#24 *ℤ 2^64-1) >>₆₄ 64)), (addcarry₆₄, [#24, (#24 *₆₄ 2^64-1)])])])

(Note that the parentheses are a bit off; we're multiplying by 2^k-1, not multiplying by 2^k and then subtracting 1)

I guess we need a rule for (addcarry₆₄, [#24, (#24 *₆₄ 2^64-1)]) = 0

What's up with (x * (2^32-1)) >> 64? It seems like this is almost but not quite computing x >> 32? And what does (x * (2^64-1)) >> 64 compute?

[davidben]

Where in the assembly does that correspond to?

[JasonGross]

I guess in this case the assembly is the simpler one (the LHS). The outermost * 2^32 is the shl on the last line of

ecp_nistz256_mul_mont:
push rbp
push rbx
push r12
push r13
push r14
push r15
xchg rdx, rsi                  ; hack: swap args
mov rbx, rdx
mov rax, QWORD PTR [rbx]
mov r9, QWORD PTR [rsi]
mov r10, QWORD PTR [rsi + 0x08 * 1]
mov r11, QWORD PTR [rsi + 0x08 * 2]
mov r12, QWORD PTR [rsi + 0x08 * 3]
mov rbp, rax
mul r9
mov r14, 4294967295
mov r8, rax
mov rax, rbp
mov r9, rdx
mul r10
mov r15, 18446744069414584321
add r9, rax	; #549
mov rax, rbp
adc rdx, 0	; #550, #551
mov r10, rdx
mul r11
add r10, rax	; #552
mov rax, rbp
adc rdx, 0	; #553, #554
mov r11, rdx
mul r12
add r11, rax	; #555
mov rax, r8
adc rdx, 0	; #556
xor r13, r13	; #557
mov r12, rdx
mov rbp, r8
shl r8, 32	; #558, #559, #560

The PHOAS fragment corresponding to the "multiply by 2^32-1 then shift right by 64" is, I believe,

  x1 = (arg1[1]);
  x2 = (arg1[2]);
  x3 = (arg1[3]);
  x4 = (arg1[0]);
  mulx_u64(&x5, &x6, x4, (arg2[3]));
  mulx_u64(&x7, &x8, x4, (arg2[2]));
  mulx_u64(&x9, &x10, x4, (arg2[1]));
  mulx_u64(&x11, &x12, x4, (arg2[0]));
  addcarryx_u64(&x13, &x14, 0x0, x12, x9);
  addcarryx_u64(&x15, &x16, x14, x10, x7);
  addcarryx_u64(&x17, &x18, x16, x8, x5);
  x19 = (x18 + x6);
  mulx_u64(&x20, &x21, x11, UINT64_C(0xffffffff00000001));
  mulx_u64(&x22, &x23, x11, UINT32_C(0xffffffff));
  mulx_u64(&x24, &x25, x11, UINT64_C(0xffffffffffffffff));
  addcarryx_u64(&x26, &x27, 0x0, x25, x22);

where "shift right by 64" is how the PHOAS/the equivalence checker is interpreting the upper-half of double-wide multiplication.

Some more details

The full error trace is:

Unable to unify: [inr [762, 763, 764, 765]] == [inr [322, 323, 324, 325]]
Could not unify the values at index 0: [#762, #763, #764, #765] ≠ [#322, #323, #324, #325]
index 0: #762 ≠ #322
(selectznz, [#761, #748, #735]) ≠ (selectznz, [#321, #303, #288])
index 0: #761 ≠ #321
(subborrow 64, [#747, #758]) ≠ (subborrow 64, [#301, #317])
index 0: #747 ≠ #301
(add 64, [#727, #745]) ≠ (add 64, [#267, #299])
index 0: #727 ≠ #267
(addcarry 64, [#229, #669, #687, #719, #724]) ≠ (addcarry 64, [#191, #223, #229, #250, #264])
index 1: #669 ≠ #191
(addcarry 64, [#153, #611, #629, #661, #666]) ≠ (addcarry 64, [#115, #147, #153, #174, #188])
index 1: #611 ≠ #115
(addcarry 64, [#77, #572, #603, #608]) ≠ (addcarry 64, [#73, #77, #98, #112])
index 1: #572 ≠ #73
(addcarry 64, [#14, #35, #42, #569]) ≠ (addcarry 64, [#14, #35, #42, #70])
index 3: #569 ≠ #70
(addcarry 64, [#33, #40, #566]) ≠ (addcarry 64, [#33, #40, #67])
index 2: #566 ≠ #67
(addcarry 64, [#30, #561, #563]) ≠ (addcarry 64, [#30, #47, #55, #64])
(addcarry 64, [#561, #563]) ≠ (addcarry 64, [#47, #55, #64])
(addcarry 64, [(shr 64, [#24, #418]), (addcarry 64, [#27, #560])]) ≠ (addcarry 64, [(shr 64, [#44, #10]), (addcarry 64, [#45, #52]), (addcarry 64, [#27, #53, #61])])
(addcarry 64, [(shr 64, [#24, (const 32, [])]), (addcarry 64, [#27, (mul 64, [#3, #7, #559])])]) ≠ (addcarry 64, [(shr 64, [(mulZ, [#24, #43]), #10]), (addcarry 64, [(mul 64, [#3, #7, #43]), (shr 64, [#49, #10])]), (addcarry 64, [#27, (add 64, [#45, #52]), (addcarry 64, [#24, #50])])])
(addcarry 64, [(shr 64, [#24, (const 32, [])]), (addcarry 64, [#27, (mul 64, [#3, #7, (const 4294967296, [])])])]) ≠ (addcarry 64, [(shr 64, [(mulZ, [#24, (const 4294967295, [])]), #10]), (addcarry 64, [(mul 64, [#3, #7, (const 4294967295, [])]), (shr 64, [(mulZ, [#24, #48]), #10])]), (addcarry 64, [#27, (add 64, [(mul 64, [#3, #7, #43]), (shr 64, [#49, #10])]), (addcarry 64, [#24, (mul 64, [#3, #7, #48])])])])
(addcarry 64, [(shr 64, [#24, (const 32, [])]), (addcarry 64, [#27, (mul 64, [#3, #7, (const 4294967296, [])])])]) ≠ (addcarry 64, [(shr 64, [(mulZ, [#24, (const 4294967295, [])]), #10]), (addcarry 64, [(mul 64, [#3, #7, (const 4294967295, [])]), (shr 64, [(mulZ, [#24, (const 18446744073709551615, [])]), #10])]), (addcarry 64, [#27, (add 64, [(mul 64, [#3, #7, (const 4294967295, [])]), (shr 64, [(mulZ, [#24, #48]), #10])]), (addcarry 64, [#24, (mul 64, [#3, #7, (const 18446744073709551615, [])])])])])
(addcarry 64, [(shr 64, [#24, (const 32, [])]), (addcarry 64, [#27, (mul 64, [#3, #7, (const 4294967296, [])])])]) ≠ (addcarry 64, [(shr 64, [(mulZ, [#24, (const 4294967295, [])]), #10]), (addcarry 64, [(mul 64, [#3, #7, (const 4294967295, [])]), (shr 64, [(mulZ, [#24, (const 18446744073709551615, [])]), #10])]), (addcarry 64, [#27, (add 64, [(mul 64, [#3, #7, (const 4294967295, [])]), (shr 64, [(mulZ, [#24, (const 18446744073709551615, [])]), #10])]), (addcarry 64, [#24, (mul 64, [#3, #7, (const 18446744073709551615, [])])])])])
(addcarry 64, [(shr 64, [(mul 64, [#3, #7]), (const 32, [])]), (addcarry 64, [(add 64, [#20, #26]), (mul 64, [(old 64 3, []), (old 64 7, []), (const 4294967296, [])])])]) ≠ (addcarry 64, [(shr 64, [(mulZ, [(mul 64, [#3, #7]), (const 4294967295, [])]), (const 64, [])]), (addcarry 64, [(mul 64, [(old 64 3, []), (old 64 7, []), (const 4294967295, [])]), (shr 64, [(mulZ, [(mul 64, [#3, #7]), (const 18446744073709551615, [])]), (const 64, [])])]), (addcarry 64, [(add 64, [#20, #26]), (add 64, [(mul 64, [(old 64 3, []), (old 64 7, []), (const 4294967295, [])]), (shr 64, [(mulZ, [(mul 64, [#3, #7]), (const 18446744073709551615, [])]), (const 64, [])])]), (addcarry 64, [(mul 64, [#3, #7]), (mul 64, [(old 64 3, []), (old 64 7, []), (const 18446744073709551615, [])])])])])
(addcarry₆₄, [((#3 *₆₄ #7) >>₆₄ 32), (addcarry₆₄, [(#20 +₆₄ #26), (old₆₄ 3 *₆₄ old₆₄ 7 *₆₄ 2^32)])]) ≠ (addcarry₆₄, [(((#3 *₆₄ #7) *ℤ 2^32-1) >>₆₄ 64), (addcarry₆₄, [(old₆₄ 3 *₆₄ old₆₄ 7 *₆₄ 2^32-1), (((#3 *₆₄ #7) *ℤ 2^64-1) >>₆₄ 64)]), (addcarry₆₄, [(#20 +₆₄ #26), ((old₆₄ 3 *₆₄ old₆₄ 7 *₆₄ 2^32-1) +₆₄ (((#3 *₆₄ #7) *ℤ 2^64-1) >>₆₄ 64)), (addcarry₆₄, [(#3 *₆₄ #7), (old₆₄ 3 *₆₄ old₆₄ 7 *₆₄ 2^64-1)])])])
3 is a special value no longer present in the symbolic machine state at the end of execution.
7 is a special value no longer present in the symbolic machine state at the end of execution.

We're mostly interested in things under #560, which shows up by

Assembly (in fiat-amd64/boringssl_intel_manual_mul_p256.asm):
ecp_nistz256_mul_mont:
push rbp
push rbx
push r12
push r13
push r14
push r15
xchg rdx, rsi                  ; hack: swap args
mov rbx, rdx
mov rax, QWORD PTR [rbx]
mov r9, QWORD PTR [rsi]
mov r10, QWORD PTR [rsi + 0x08 * 1]
mov r11, QWORD PTR [rsi + 0x08 * 2]
mov r12, QWORD PTR [rsi + 0x08 * 3]
mov rbp, rax
mul r9
mov r14, 4294967295
mov r8, rax
mov rax, rbp
mov r9, rdx
mul r10
mov r15, 18446744069414584321
add r9, rax	; #549
mov rax, rbp
adc rdx, 0	; #550, #551
mov r10, rdx
mul r11
add r10, rax	; #552
mov rax, rbp
adc rdx, 0	; #553, #554
mov r11, rdx
mul r12
add r11, rax	; #555
mov rax, r8
adc rdx, 0	; #556
xor r13, r13	; #557
mov r12, rdx
mov rbp, r8
shl r8, 32	; #558, #559, #560