wdadd change

eclib/JModel_m4.ec

@@ -183,8 +183,9 @@ op UMULL (x y: W32.t) : W32.t * W32.t =
 op UMULLcc x y g o h = if g then UMULL x y else (o, h).
 
 op UMLAL (u v x y: W32.t) : W32.t * W32.t =
-  let (hi, lo) = mulu x y in
-  (lo + u, hi + v + of_int (b2i (carry_add lo u false)))%W32.
+  let n = wdwordu (mulhi x y) (x*y) in
+  let m = wdwordu v u in
+  (of_int (n + m), of_int (IntDiv.(%/) (n + m) modulus))%W32.
 op UMLALcc u v x y g o h= if g then UMLAL u v x y else (o, h).
 
 op SMULL (x y: W32.t) : W32.t * W32.t =
@@ -194,9 +195,9 @@ op SMULL (x y: W32.t) : W32.t * W32.t =
 op SMULLcc x y g o h = if g then SMULL x y else (o, h).
 
 op SMLAL (u v x y: W32.t) : W32.t * W32.t =
-  let lo = x * y in
-  let hi = wmulhs x y in
-  (lo + u, hi + v + of_int (b2i (carry_add lo u false)))%W32.
+  let n = wdwords (wmulhs x y) (x*y) in
+  let m = wdwords v u in
+  (of_int (n + m), of_int (IntDiv.(%/) (n + m) modulus))%W32.
 op SMLALcc u v x y g o h= if g then SMLAL u v x y else (o, h).
 
 op SMMUL (x y: W32.t) : W32.t =

proofs/lang/word.v

@@ -633,14 +633,12 @@ Definition waddcarry sz (x y: word sz) (c: bool) :=
   (wbase sz <=? n, wrepr sz n).
 
 Definition wdaddu sz (hi_1 lo_1 hi_2 lo_2: word sz) :=
-  let (c, lo) := waddcarry lo_1 lo_2 false in
-  let hi := wunsigned hi_1 + wunsigned hi_2 + Z.b2z c in
-  (lo, wrepr sz hi).
+  let n := (wdwordu hi_1 lo_1) + (wdwordu hi_2 lo_2) in
+  (wrepr sz n, wrepr sz (Z.quot n (wbase sz))).
 
 Definition wdadds sz (hi_1 lo_1 hi_2 lo_2: word sz) :=
-  let (c, lo) := waddcarry lo_1 lo_2 false in
-  let hi := wsigned hi_1 + wsigned hi_2 + Z.b2z c in
-  (lo, wrepr sz hi).
+  let n := (wdwords hi_1 lo_1) + (wdwords hi_2 lo_2) in
+  (wrepr sz n, wrepr sz (Z.quot n (wbase sz))).
 
 Definition wsubcarry sz (x y: word sz) (c: bool) :=
   let n := wunsigned x - wunsigned y - Z.b2z c in