reprint Montgomery output (order of additions in Rows.flatten changed)

1 files changed, 21 insertions, 18 deletions

diff --git a/src/Experiments/SimplyTypedArithmetic.v b/src/Experiments/SimplyTypedArithmetic.v
index 1deab9dda..da53fcf6c 100644
--- a/src/Experiments/SimplyTypedArithmetic.v
+++ b/src/Experiments/SimplyTypedArithmetic.v
@@ -923,6 +923,7 @@ Module Columns.
         induction p; [ autorewrite with push_eval; congruence |].
         cbv [from_associational Positional.from_associational]; autorewrite with push_fold_right.
         fold (from_associational n p); fold (Positional.from_associational weight n p).
+        cbv [Let_In].
         match goal with |- context [Positional.place _ ?x ?n] =>
                         pose proof (Positional.place_in_range weight x n) end.
         repeat match goal with
@@ -8154,10 +8155,10 @@ montred256 = fun var : type -> Type => λ x : var (type.type_primitive type.Z *
              expr_let x3 := ((uint128)(x2) & 340282366920938463463374607431768211455) in
              expr_let x4 := 340282366841710300986003757985643364352 *₂₅₆ x1 in
              expr_let x5 := ((uint128)(x4) & 340282366920938463463374607431768211455) in
-             expr_let x6 := (uint256)(x3 << 128) in
+             expr_let x6 := (uint256)(x5 << 128) in
              expr_let x7 := 79228162514264337593543950337 *₂₅₆ x1 in
              expr_let x8 := ADD_256 (x6, x7) in
-             expr_let x9 := (uint256)(x5 << 128) in
+             expr_let x9 := (uint256)(x3 << 128) in
              expr_let x10 := ADD_256 (x9, x8₁) in
              expr_let x11 := (uint128)(x10₁ >> 128) in
              expr_let x12 := ((uint128)(x10₁) & 340282366920938463463374607431768211455) in
@@ -8167,19 +8168,20 @@ montred256 = fun var : type -> Type => λ x : var (type.type_primitive type.Z *
              expr_let x16 := 340282366841710300967557013911933812736 *₂₅₆ x12 in
              expr_let x17 := (uint128)(x16 >> 128) in
              expr_let x18 := ((uint128)(x16) & 340282366920938463463374607431768211455) in
-             expr_let x19 := (uint256)(x15 << 128) in
+             expr_let x19 := (uint256)(x18 << 128) in
              expr_let x20 := 79228162514264337593543950335 *₂₅₆ x12 in
              expr_let x21 := ADD_256 (x19, x20) in
-             expr_let x22 := 340282366841710300967557013911933812736 *₂₅₆ x11 in
-             expr_let x23 := ADDC_256 (x21₂, x22, x17) in
-             expr_let x24 := (uint256)(x18 << 128) in
-             expr_let x25 := ADD_256 (x24, x21₁) in
-             expr_let x26 := ADDC_256 (x25₂, x14, x23₁) in
-             expr_let x27 := ADD_256 (x₁, x25₁) in
+             expr_let x22 := ADDC_256 (x21₂, x14, x17) in
+             expr_let x23 := (uint256)(x15 << 128) in
+             expr_let x24 := ADD_256 (x23, x21₁) in
+             expr_let x25 := 340282366841710300967557013911933812736 *₂₅₆ x11 in
+             expr_let x26 := ADDC_256 (x24₂, x25, x22₁) in
+             expr_let x27 := ADD_256 (x₁, x24₁) in
              expr_let x28 := ADDC_256 (x27₂, x₂, x26₁) in
              expr_let x29 := SELC (x28₂, 0, 115792089210356248762697446949407573530086143415290314195533631308867097853951) in
              expr_let x30 := Z.cast uint256 @@ (fst @@ SUB_256 (x28₁, x29)) in
              ADDM (x30, 0, 115792089210356248762697446949407573530086143415290314195533631308867097853951)
+     : Expr (type.type_primitive type.Z * type.type_primitive type.Z -> type.type_primitive type.Z)
    *)
 End Montgomery256.
 
@@ -8289,16 +8291,17 @@ Local Open Scope expr_scope.
 
 Print Montgomery256.montred256.
 (*
+<<<<<<< HEAD
 c.ShiftR($x0, $x_lo, 128);
 c.Lower128($x1, $x_lo);
 c.Mul128x128($x2, Lower128{RegPinv}, $x0);
 c.Lower128($x3, $x2);
 c.Mul128x128($x4, RegPinv >> 128, $x1);
 c.Lower128($x5, $x4);
-c.ShiftL($x6, $x3, 128);
+c.ShiftL($x6, $x5, 128);
 c.Mul128x128($x7, Lower128{RegPinv}, $x1);
 c.Add256($x8, $x6, $x7);
-c.ShiftL($x9, $x5, 128);
+c.ShiftL($x9, $x3, 128);
 c.Add256($x10, $x9, $x8_lo);
 c.ShiftR($x11, $x10_lo, 128);
 c.Lower128($x12, $x10_lo);
@@ -8308,15 +8311,15 @@ c.Lower128($x15, $x13);
 c.Mul128x128($x16, RegMod << 128, $x12);
 c.ShiftR($x17, $x16, 128);
 c.Lower128($x18, $x16);
-c.ShiftL($x19, $x15, 128);
+c.ShiftL($x19, $x18, 128);
 c.Mul128x128($x20, Lower128{RegMod}, $x12);
 c.Add256($x21, $x19, $x20);
-c.Mul128x128($x22, RegMod << 128, $x11);
-c.Addc($x23, $x22, $x17);
-c.ShiftL($x24, $x18, 128);
-c.Add256($x25, $x24, $x21_lo);
-c.Addc($x26, $x14, $x23_lo);
-c.Add256($x27, $x_lo, $x25_lo);
+c.Addc($x22, $x14, $x17);
+c.ShiftL($x23, $x15, 128);
+c.Add256($x24, $x23, $x21_lo);
+c.Mul128x128($x25, RegMod << 128, $x11);
+c.Addc($x26, $x25, $x22_lo);
+c.Add256($x27, $x_lo, $x24_lo);
 c.Addc($x28, $x_hi, $x26_lo);
 c.Selc($x29,RegZero, RegMod);
 c.Sub($x30, $x28_lo, $x29);