fix last wide mul in curve25519-51

3 files changed, 10 insertions, 10 deletions

diff --git a/src/Specific/ArithmeticSynthesisTest.v b/src/Specific/ArithmeticSynthesisTest.v
index 9ea1369dd..438f8305e 100644
--- a/src/Specific/ArithmeticSynthesisTest.v
+++ b/src/Specific/ArithmeticSynthesisTest.v
@@ -204,11 +204,11 @@ Section Ops51.
       dlet d2 := r2 * 2 * 19 in
       dlet d419 := r4 * 19 in
       dlet d4 := d419 * 2 in
-      dlet t0 := r0 * r0 + d4 * r1 + d2 * r3      in
-      dlet t1 := d0 * r1 + d4 * r2 + r3 * r3 * 19 in
-      dlet t2 := d0 * r2 + r1 * r1 + d4 * r3      in
-      dlet t3 := d0 * r3 + d1 * r2 + r4 * d419    in
-      dlet t4 := d0 * r4 + d1 * r3 + r2 * r2      in
+      dlet t0 := r0 * r0 + d4 * r1 + d2 * r3        in
+      dlet t1 := d0 * r1 + d4 * r2 + r3 * (r3 * 19) in
+      dlet t2 := d0 * r2 + r1 * r1 + d4 * r3        in
+      dlet t3 := d0 * r3 + d1 * r2 + r4 * d419      in
+      dlet t4 := d0 * r4 + d1 * r3 + r2 * r2        in
       (t4, t3, t2, t1, t0)
     ).
     break_match; cbv [Let_In runtime_mul runtime_add]; repeat apply (f_equal2 pair); ring.
diff --git a/src/Specific/IntegrationTestLadderstepDisplay.log b/src/Specific/IntegrationTestLadderstepDisplay.log
index cb7d11ba4..8f4998081 100644
--- a/src/Specific/IntegrationTestLadderstepDisplay.log
+++ b/src/Specific/IntegrationTestLadderstepDisplay.log
@@ -106,7 +106,7 @@ let (a, b) := Interp-η
  uint64_t x154 = x141 * 0x13;
  uint64_t x155 = x154 * 0x2;
  uint128_t x156 = (uint128_t) x145 * x145 + (uint128_t) x155 * x144 + (uint128_t) x153 * x142;
- uint128_t x157 = (uint128_t) x151 * x144 + (uint128_t) x155 * x143 + (uint128_t) x142 * x142 * 0x13;
+ uint128_t x157 = (uint128_t) x151 * x144 + (uint128_t) x155 * x143 + (uint128_t) x142 * (x142 * 0x13);
  uint128_t x158 = (uint128_t) x151 * x143 + (uint128_t) x144 * x144 + (uint128_t) x155 * x142;
  uint128_t x159 = (uint128_t) x151 * x142 + (uint128_t) x152 * x143 + (uint128_t) x141 * x154;
  uint128_t x160 = (uint128_t) x151 * x141 + (uint128_t) x152 * x142 + (uint128_t) x143 * x143;
@@ -137,7 +137,7 @@ let (a, b) := Interp-η
  uint64_t x185 = x146 * 0x13;
  uint64_t x186 = x185 * 0x2;
  uint128_t x187 = (uint128_t) x150 * x150 + (uint128_t) x186 * x149 + (uint128_t) x184 * x147;
- uint128_t x188 = (uint128_t) x182 * x149 + (uint128_t) x186 * x148 + (uint128_t) x147 * x147 * 0x13;
+ uint128_t x188 = (uint128_t) x182 * x149 + (uint128_t) x186 * x148 + (uint128_t) x147 * (x147 * 0x13);
  uint128_t x189 = (uint128_t) x182 * x148 + (uint128_t) x149 * x149 + (uint128_t) x186 * x147;
  uint128_t x190 = (uint128_t) x182 * x147 + (uint128_t) x183 * x148 + (uint128_t) x146 * x185;
  uint128_t x191 = (uint128_t) x182 * x146 + (uint128_t) x183 * x147 + (uint128_t) x148 * x148;
@@ -202,7 +202,7 @@ let (a, b) := Interp-η
  uint64_t x250 = x53 * 0x13;
  uint64_t x251 = x250 * 0x2;
  uint128_t x252 = (uint128_t) x57 * x57 + (uint128_t) x251 * x56 + (uint128_t) x249 * x54;
- uint128_t x253 = (uint128_t) x247 * x56 + (uint128_t) x251 * x55 + (uint128_t) x54 * x54 * 0x13;
+ uint128_t x253 = (uint128_t) x247 * x56 + (uint128_t) x251 * x55 + (uint128_t) x54 * (x54 * 0x13);
  uint128_t x254 = (uint128_t) x247 * x55 + (uint128_t) x56 * x56 + (uint128_t) x251 * x54;
  uint128_t x255 = (uint128_t) x247 * x54 + (uint128_t) x248 * x55 + (uint128_t) x53 * x250;
  uint128_t x256 = (uint128_t) x247 * x53 + (uint128_t) x248 * x54 + (uint128_t) x55 * x55;
@@ -233,7 +233,7 @@ let (a, b) := Interp-η
  uint64_t x281 = x58 * 0x13;
  uint64_t x282 = x281 * 0x2;
  uint128_t x283 = (uint128_t) x62 * x62 + (uint128_t) x282 * x61 + (uint128_t) x280 * x59;
- uint128_t x284 = (uint128_t) x278 * x61 + (uint128_t) x282 * x60 + (uint128_t) x59 * x59 * 0x13;
+ uint128_t x284 = (uint128_t) x278 * x61 + (uint128_t) x282 * x60 + (uint128_t) x59 * (x59 * 0x13);
  uint128_t x285 = (uint128_t) x278 * x60 + (uint128_t) x61 * x61 + (uint128_t) x282 * x59;
  uint128_t x286 = (uint128_t) x278 * x59 + (uint128_t) x279 * x60 + (uint128_t) x58 * x281;
  uint128_t x287 = (uint128_t) x278 * x58 + (uint128_t) x279 * x59 + (uint128_t) x60 * x60;
diff --git a/src/Specific/IntegrationTestSquareDisplay.log b/src/Specific/IntegrationTestSquareDisplay.log
index fcdaf3635..b2e5092fc 100644
--- a/src/Specific/IntegrationTestSquareDisplay.log
+++ b/src/Specific/IntegrationTestSquareDisplay.log
@@ -8,7 +8,7 @@ Interp-η
  uint64_t x12 = x7 * 0x13;
  uint64_t x13 = x12 * 0x2;
  uint128_t x14 = (uint128_t) x2 * x2 + (uint128_t) x13 * x4 + (uint128_t) x11 * x8;
- uint128_t x15 = (uint128_t) x9 * x4 + (uint128_t) x13 * x6 + (uint128_t) x8 * x8 * 0x13;
+ uint128_t x15 = (uint128_t) x9 * x4 + (uint128_t) x13 * x6 + (uint128_t) x8 * (x8 * 0x13);
  uint128_t x16 = (uint128_t) x9 * x6 + (uint128_t) x4 * x4 + (uint128_t) x13 * x8;
  uint128_t x17 = (uint128_t) x9 * x8 + (uint128_t) x10 * x6 + (uint128_t) x7 * x12;
  uint128_t x18 = (uint128_t) x9 * x7 + (uint128_t) x10 * x8 + (uint128_t) x6 * x6;