insert a reduce step in the correct place of the carry chain

2 files changed, 38 insertions, 19 deletions

diff --git a/src/NewBaseSystem.v b/src/NewBaseSystem.v
index 6b80a99c9..44f6a7fe6 100644
--- a/src/NewBaseSystem.v
+++ b/src/NewBaseSystem.v
@@ -614,27 +614,27 @@ Module B.
         Context {modulo div : Z->Z->Z}.
         Context {div_mod : forall a b:Z, b <> 0 ->
                                        a = b * (div a b) + modulo a b}.
-        Definition carry_cps {n} (index:nat) (p:tuple Z n)
-                   {T} (f:tuple Z n->T) :=
+        Definition carry_cps {n m} (index:nat) (p:tuple Z n)
+                   {T} (f:tuple Z m->T) :=
           to_associational_cps p
             (fun P =>  @Associational.carry_cps
                          modulo div
                          (weight index)
                          (weight (S index) / weight index)
                          P T
-             (fun R => from_associational_cps n R f)).
+             (fun R => from_associational_cps m R f)).
 
-      Definition carry {n} i p := @carry_cps n i p _ id.
-      Lemma carry_cps_id {n} i p {T} f:
-        @carry_cps n i p T f = f (carry i p).
+      Definition carry {n m} i p := @carry_cps n m i p _ id.
+      Lemma carry_cps_id {n m} i p {T} f:
+        @carry_cps n m i p T f = f (carry i p).
       Proof.
         cbv [carry_cps carry]; prove_id; rewrite carry_cps_id; reflexivity.
       Qed.
       Hint Opaque carry : uncps. Hint Rewrite @carry_cps_id : uncps.
 
-      Lemma eval_carry {n} i p: (n <> 0%nat) ->
+      Lemma eval_carry {n m} i p: (n <> 0%nat) -> (m <> 0%nat) ->
                                 weight (S i) / weight i <> 0 ->
-        eval (carry (n := n) i p) = eval p.
+        eval (carry (n:=n) (m:=m) i p) = eval p.
       Proof.
         cbv [carry_cps carry]; intros. prove_eval.
         rewrite @eval_carry by eauto.
@@ -705,6 +705,12 @@ Module B.
             (fun P => Associational.reduce_cps s c P
                (fun R => from_associational_cps n R f)).
 
+        Definition carry_reduce_cps {n div modulo}
+                   (s:Z) (c:list limb) (p : tuple Z n)
+                   {T} (f: tuple Z n ->T) :=
+          carry_cps (div:=div) (modulo:=modulo) (n:=n) (m:=S n) (pred n) p
+            (fun r => reduce_cps (m:=S n) (n:=n) s c r f).
+
         Definition negate_snd_cps {n} (p : tuple Z n)
                    {T} (f:tuple Z n->T) :=
           to_associational_cps p
@@ -716,6 +722,7 @@ Module B.
            Positional.add_cps 
            Positional.mul_cps
            Positional.reduce_cps
+           Positional.carry_reduce_cps
            Positional.negate_snd_cps
       .
 
@@ -811,6 +818,7 @@ Module B.
       Positional.add_cps 
       Positional.mul_cps
       Positional.reduce_cps
+      Positional.carry_reduce_cps
       Positional.negate_snd_cps
       Positional.opp_cps
   .
@@ -913,7 +921,7 @@ Ltac F_mod_eq :=
   apply mod_eq_Z2F_iff.
 
 Ltac solve_op_mod_eq wt x :=
-  transitivity (Positional.eval wt x); autounfold;
+  transitivity (Positional.eval wt x); repeat autounfold;
   [|autorewrite with uncps push_id push_basesystem_eval;
     reflexivity];
   cbv [mod_eq]; apply f_equal2; [|reflexivity];
diff --git a/src/Specific/NewBaseSystemTest.v b/src/Specific/NewBaseSystemTest.v
index 595e4baea..2271db4e4 100644
--- a/src/Specific/NewBaseSystemTest.v
+++ b/src/Specific/NewBaseSystemTest.v
@@ -24,7 +24,8 @@ Section Ops25p5.
   Definition s : Z := 2^255.
   Definition c : list B.limb := [(1, 19)].
   Definition coef_div_modulus := 2. (* add 2*modulus before subtracting *)
-  Definition carry_chain := Eval vm_compute in (seq 0 sz) ++ ([0;1])%nat.
+  Definition carry_chain1 := Eval vm_compute in (seq 0 (pred sz)).
+  Definition carry_chain2 := ([0;1])%nat.
 
   (* These definitions are inferred from those above *)
   Definition m := Eval vm_compute in Z.to_pos (s - Associational.eval c). (* modulus *)
@@ -35,9 +36,15 @@ Section Ops25p5.
   Lemma sz_nonzero : sz <> 0%nat. Proof. vm_decide. Qed.
   Lemma wt_nonzero i : wt i <> 0.
   Proof. apply Z.pow_nonzero; zero_bounds. Qed.
-  Lemma wt_divides i (H:In i carry_chain) : wt (S i) / wt i <> 0.
+  Lemma wt_divides_chain1 i (H:In i carry_chain1) : wt (S i) / wt i <> 0.
   Proof.
-    cbv [In carry_chain] in H.
+    cbv [In carry_chain1] in H.
+    repeat match goal with H : _ \/ _ |- _ => destruct H end;
+      try (exfalso; assumption); subst; try vm_decide.
+  Qed.
+  Lemma wt_divides_chain2 i (H:In i carry_chain2) : wt (S i) / wt i <> 0.
+  Proof.
+    cbv [In carry_chain2] in H.
     repeat match goal with H : _ \/ _ |- _ => destruct H end;
       try (exfalso; assumption); subst; try vm_decide.
   Qed.
@@ -76,7 +83,7 @@ Section Ops25p5.
                  eval (add a b) = (eval a  + eval b)%F }.
   Proof.
     eexists; cbv beta zeta; intros.
-    pose proof wt_nonzero. pose proof wt_divides.
+    pose proof wt_nonzero.
     let x := constr:(
         Positional.add_cps (n := sz) wt a b id) in
     solve_op_F wt x. reflexivity.
@@ -89,7 +96,7 @@ Section Ops25p5.
                  eval (sub a b) = (eval a - eval b)%F}.
   Proof.
     eexists; cbv beta zeta; intros.
-    pose proof wt_nonzero. pose proof wt_divides.
+    pose proof wt_nonzero.
     let x := constr:(
          Positional.sub_cps (n:=sz) (coef := coef) wt a b id) in
     solve_op_F wt x. reflexivity.
@@ -102,7 +109,7 @@ Section Ops25p5.
                  eval (opp a) = F.opp (eval a)}.
   Proof.
     eexists; cbv beta zeta; intros.
-    pose proof wt_nonzero. pose proof wt_divides.
+    pose proof wt_nonzero.
     let x := constr:(
          Positional.opp_cps (n:=sz) (coef := coef) wt a id) in
     solve_op_F wt x. reflexivity.
@@ -115,7 +122,7 @@ Section Ops25p5.
                  eval (mul a b) = (eval a  * eval b)%F}.
   Proof.
     eexists; cbv beta zeta; intros.
-    pose proof wt_nonzero. pose proof wt_divides.
+    pose proof wt_nonzero.
     let x := constr:(
          Positional.mul_cps (n:=sz) (m:=sz2) wt a b
            (fun ab => Positional.reduce_cps (n:=sz) (m:=sz2) wt s c ab id)) in
@@ -137,9 +144,13 @@ Section Ops25p5.
                  eval (carry a) = eval a}.
   Proof.
     eexists; cbv beta zeta; intros.
-    pose proof wt_nonzero. pose proof wt_divides. pose proof div_mod.
+    pose proof wt_nonzero. pose proof wt_divides_chain1.
+    pose proof div_mod. pose proof wt_divides_chain2.
     let x := constr:(
-               Positional.chained_carries_cps (n:=sz) (div:=div)(modulo:=modulo) wt a carry_chain id) in
+               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
     solve_op_F wt x. reflexivity.
   Defined.
   
@@ -176,4 +187,4 @@ Eval cbv [proj1_sig mul_sig] in (proj1_sig mul_sig).
 Eval cbv [proj1_sig carry_sig] in (proj1_sig carry_sig).
 *)
 
-End Ops25p5.
+End Ops25p5.
\ No newline at end of file