Fix scmul bounds issue

1 files changed, 10 insertions, 3 deletions

diff --git a/src/Arithmetic/Saturated.v b/src/Arithmetic/Saturated.v
index d5b23f8b2..529a6877a 100644
--- a/src/Arithmetic/Saturated.v
+++ b/src/Arithmetic/Saturated.v
@@ -733,9 +733,16 @@ Section API.
   Definition drop_high {n} p : T n := @drop_high_cps n p _ id.
 
   Definition scmul_cps {n} (c : Z) (p : T n) {R} (f:T (S n)->R) :=
-    Columns.mul_cps (n1:=1) (n3:=n) (uweight bound) bound c p
-      (fun carry_result => Tuple.left_append_cps (fst carry_result) (snd carry_result)
-      f).
+    Columns.mul_cps (n1:=1) (n3:=S n) (uweight bound) bound c p
+      (fun carry_result =>
+         Tuple.left_append_cps (fst carry_result) (snd carry_result)
+      (* The carry that comes out of Columns.mul_cps will be 0, since
+      (S n) limbs is enough to hold the result of the
+      multiplication. To make this extra limb disappear, we convert to
+      and from associational, simply indicating that we only need to
+      have (S n) limbs when converting back. *)
+      (fun R => B.Positional.to_associational_cps (uweight bound) R
+      (fun r => B.Positional.from_associational_cps (uweight bound) (S n) r f))).
   Definition scmul {n} c p : T (S n) := @scmul_cps n c p _ id.
 
   Definition add_cps {n m pred_nm} (p : T n) (q : T m) {R} (f:T (S pred_nm)->R) :=