ed448 mul: use two carry chains to fix bounds (still silly otherwise)

2 files changed, 24 insertions, 15 deletions

diff --git a/src/Specific/IntegrationTestKaratsubaMul.v b/src/Specific/IntegrationTestKaratsubaMul.v
index 444c0746b..ca25596ec 100644
--- a/src/Specific/IntegrationTestKaratsubaMul.v
+++ b/src/Specific/IntegrationTestKaratsubaMul.v
@@ -87,17 +87,16 @@ Section BoundedField25p5.
     Unshelve.
     all:shelve_unifiable.
     cbv [Interpretation.Bounds.is_tighter_thanb Relations.interp_flat_type_relb_pointwise Relations.interp_flat_type_rel_pointwise_gen_Prop Syntax.tuple Syntax.tuple' fst snd codomain bounds Interpretation.Bounds.is_tighter_thanb'].
-    Show.
-    (*
-    assert (((r[0 ~> 72057594037927935] <=? r[0 ~> 81064793292668928])%zrange &&
-   (r[0 ~> 72057594037927935] <=? r[0 ~> 81064793292668928])%zrange &&
-   (r[0 ~> 72057594037927935] <=? r[0 ~> 81064793292668928])%zrange &&
-   (r[0 ~> 1166432303488958480] <=? r[0 ~> 81064793292668928])%zrange &&
-   (r[0 ~> 72057594037927935] <=? r[0 ~> 81064793292668928])%zrange &&
-   (r[0 ~> 72057594037927936] <=? r[0 ~> 81064793292668928])%zrange &&
-   (r[0 ~> 72057594037927935] <=? r[0 ~> 81064793292668928])%zrange &&
-   (r[0 ~> 72057594037927935] <=? r[0 ~> 81064793292668928])%zrange)%bool = true). *)
-    (*Show Ltac Profile.*)
+  (*((r[0 ~> 72057594037927935] <=? r[0 ~> 81064793292668928])%zrange &&
+     (r[0 ~> 72057594037927935] <=? r[0 ~> 81064793292668928])%zrange &&
+     (r[0 ~> 72057594037927936] <=? r[0 ~> 81064793292668928])%zrange &&
+     (r[0 ~> 72057594037927935] <=? r[0 ~> 81064793292668928])%zrange &&
+     (r[0 ~> 72057594037927935] <=? r[0 ~> 81064793292668928])%zrange &&
+     (r[0 ~> 72057594037927935] <=? r[0 ~> 81064793292668928])%zrange &&
+     (r[0 ~> 72057594037927936] <=? r[0 ~> 81064793292668928])%zrange &&
+     (r[0 ~> 72057594037927935] <=? r[0 ~> 81064793292668928])%zrange)%bool =
+    true *)
+    Decidable.vm_decide.
   Time Admitted.
 
 End BoundedField25p5.
diff --git a/src/Specific/Karatsuba.v b/src/Specific/Karatsuba.v
index 410e17548..f0800212b 100644
--- a/src/Specific/Karatsuba.v
+++ b/src/Specific/Karatsuba.v
@@ -26,8 +26,9 @@ Section Ops51.
   Definition s : Z := 2^448.
   Definition c : list B.limb := [(1, 1); (2^224, 1)].
   Definition coef_div_modulus : nat := 2. (* add 2*modulus before subtracting *)
-  Definition carry_chain1 := Eval vm_compute in (seq 0 (pred sz)).
-  Definition carry_chain2 := ([0;1])%nat.
+  Definition carry_chain1 := [3;7]%nat.
+  Definition carry_chain2 := [0;4;1;5;2;6;3;7]%nat.
+  Definition carry_chain3 := [4;0]%nat.
   Definition a24 := 121665%Z.
 
   (* These definitions are inferred from those above *)
@@ -65,6 +66,12 @@ Section Ops51.
     repeat match goal with H : _ \/ _ |- _ => destruct H end;
       try (exfalso; assumption); subst; try vm_decide.
   Qed.
+  Lemma wt_divides_chain3 i (H:In i carry_chain3) : wt (S i) / wt i <> 0.
+  Proof.
+    cbv [In carry_chain3] in H.
+    repeat match goal with H : _ \/ _ |- _ => destruct H end;
+      try (exfalso; assumption); subst; try vm_decide.
+  Qed.
   Lemma wt_divides_full i : wt (S i) / wt i <> 0.
   Proof.
     cbv [wt].
@@ -273,11 +280,14 @@ Ltac basesystem_partial_evaluation_RHS :=
     eexists; cbv beta zeta; intros.
     pose proof wt_nonzero. pose proof wt_divides_chain1.
     pose proof div_mod. pose proof wt_divides_chain2.
+    pose proof wt_divides_chain3.
     let x := constr:(
                Positional.chained_carries_cps (n:=sz) (div:=div)(modulo:=modulo) wt a carry_chain1
                   (fun r => Positional.carry_reduce_cps (n:=sz) (div:=div) (modulo:=modulo) wt s c r
-                  (fun rrr => Positional.chained_carries_cps (n:=sz) (div:=div) (modulo:=modulo) wt rrr carry_chain2 id
-             ))) in
+                  (fun r => Positional.chained_carries_cps (n:=sz) (div:=div) (modulo:=modulo) wt r carry_chain2
+                  (fun r => Positional.carry_reduce_cps (n:=sz) (div:=div) (modulo:=modulo) wt s c r
+                  (fun r => Positional.chained_carries_cps (n:=sz) (div:=div) (modulo:=modulo) wt r carry_chain3 id
+             ))))) in
     solve_op_F wt x. reflexivity.
   Defined.