Improve mulmod_256 specs

Now they talk about F.  Pair-programmed with Andres.

1 files changed, 40 insertions, 1 deletions

diff --git a/src/Specific/MontgomeryP256_128.v b/src/Specific/MontgomeryP256_128.v
index 9f3fb7f52..71df829e6 100644
--- a/src/Specific/MontgomeryP256_128.v
+++ b/src/Specific/MontgomeryP256_128.v
@@ -97,7 +97,7 @@ Z.of_nat *)
   reflexivity.
 Defined.
 
-Definition mulmod_256 : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz
+Definition mulmod_256'' : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz
                         | forall (A B : Tuple.tuple Z sz),
                             Saturated.small (Z.pos r) A -> Saturated.small (Z.pos r) B ->
                             let eval := Saturated.eval (Z.pos r) in
@@ -124,5 +124,44 @@ Proof.
           end
     ).
 Defined.
+Import ModularArithmetic.
+
+(*Definition mulmod_256 : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz
+                        | forall (A : Tuple.tuple Z sz) (_ : Saturated.small (Z.pos r) A)
+                                 (B : Tuple.tuple Z sz) (_ : Saturated.small (Z.pos r) B),
+                            Saturated.small (Z.pos r) (f A B)
+                            /\ (let eval := Saturated.eval (Z.pos r) in
+                                0 <= eval (f A B) < Z.pos r^Z.of_nat sz
+                                /\ (eval (f A B) mod Z.pos m
+                                    = (eval A * eval B * r'^(Z.of_nat sz)) mod Z.pos m))%Z
+                        }.
+Proof.*)
+
+(** TODO: MOVE ME *)
+Definition montgomery_to_F (v : Z) : F m
+  := (F.of_Z m v * F.of_Z m (r'^Z.of_nat sz)%Z)%F.
+
+Definition mulmod_256 : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz
+                        | forall (A : Tuple.tuple Z sz) (_ : Saturated.small (Z.pos r) A)
+                                 (B : Tuple.tuple Z sz) (_ : Saturated.small (Z.pos r) B),
+                            Saturated.small (Z.pos r) (f A B)
+                            /\ (let eval := Saturated.eval (Z.pos r) in
+                                montgomery_to_F (eval (f A B))
+                                = (montgomery_to_F (eval A) * montgomery_to_F (eval B))%F) }.
+Proof.
+  exists (proj1_sig mulmod_256'').
+  abstract (
+      intros A Asm B Bsm;
+      pose proof (proj2_sig mulmod_256'' A B Asm Bsm) as H;
+      cbv zeta in *;
+      split; try solve [ destruct_head'_and; assumption ];
+      rewrite ModularArithmeticTheorems.F.eq_of_Z_iff in H;
+      unfold montgomery_to_F;
+      destruct H as [H1 [H2 H3]];
+      rewrite H3;
+      rewrite <- !ModularArithmeticTheorems.F.of_Z_mul;
+      f_equal; nia
+    ).
+Defined.
 
 Print Assumptions mulmod_256.