F,Ed25519: integrate F representation for mul,add,sub. Ed25519 even more broken...

1 files changed, 97 insertions, 1 deletions

diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v
index b01e6280e..8aaf8caf6 100644
--- a/src/Specific/GF25519.v
+++ b/src/Specific/GF25519.v
@@ -7,6 +7,7 @@ Require Import Coq.Lists.List Crypto.Util.ListUtil.
 Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
 Require Import Crypto.Tactics.VerdiTactics.
 Require Import Crypto.BaseSystem.
+Require Import Crypto.Rep.
 Import ListNotations.
 Require Import Coq.ZArith.ZArith Coq.ZArith.Zpower Coq.ZArith.ZArith Coq.ZArith.Znumtheory.
 Local Open Scope Z.
@@ -81,4 +82,99 @@ Proof.
   intros f g Hf Hg.
   pose proof (sub_opt_rep _ _ _ _ Hf Hg) as Hfg.
   compute_formula.
-Defined.
\ No newline at end of file
+Defined.
+
+Definition F25519Rep := (Z * Z * Z * Z * Z  *  Z * Z * Z * Z * Z)%type.
+
+Definition F25519toRep (x:F (2^255 - 19)) : F25519Rep := (0, 0, 0, 0, 0,  0, 0, 0, 0, FieldToZ x)%Z.
+Definition F25519unRep (rx:F25519Rep) :=
+  let '(x9, x8, x7, x6, x5, x4, x3, x2, x1, x0) := rx in
+                ModularBaseSystem.decode [x0;x1;x2;x3;x4;x5;x6;x7;x8;x9].
+
+Global Instance F25519RepConversions : RepConversions (F (2^255 - 19)) F25519Rep :=
+  {
+    toRep := F25519toRep;
+    unRep := F25519unRep
+  }.
+
+Lemma F25519RepConversionsOK : RepConversionsOK F25519RepConversions.
+Proof.
+  unfold F25519RepConversions, RepConversionsOK, unRep, toRep, F25519toRep, F25519unRep; intros.
+  change (ModularBaseSystem.decode (ModularBaseSystem.encode x) = x).
+  eauto using ModularBaseSystemProofs.rep_decode, ModularBaseSystemProofs.encode_rep.
+Qed.
+
+Definition F25519Rep_mul (f g:F25519Rep) : F25519Rep.
+  refine (
+  let '(f9, f8, f7, f6, f5, f4, f3, f2, f1, f0) := f in
+  let '(g9, g8, g7, g6, g5, g4, g3, g2, g1, g0) := g in _).
+  (* FIXME: the r should not be present in generated code *)
+  pose (r := proj1_sig (GF25519Base25Point5_mul_reduce_formula f0 f1 f2 f3 f4 f5 f6 f7 f8 f9
+                                                             g0 g1 g2 g3 g4 g5 g6 g7 g8 g9)).
+  simpl in r.
+  unfold F25519Rep.
+  repeat let t' := (eval cbv beta delta [r] in r) in
+    lazymatch t' with Let_In ?arg ?f =>
+                      let x := fresh "x" in
+                      refine (let x := arg in _);
+                        let t'' := (eval cbv beta in (f x)) in
+                        change (Let_In arg f) with t'' in r
+    end.
+  let t' := (eval cbv beta delta [r] in r) in
+  lazymatch t' with [?r0;?r1;?r2;?r3;?r4;?r5;?r6;?r7;?r8;?r9] =>
+                    clear r;
+                    exact (r9, r8, r7, r6, r5, r4, r3, r2, r1, r0)
+  end.
+Time Defined.
+
+Lemma F25519_mul_OK : RepBinOpOK F25519RepConversions ModularArithmetic.mul F25519Rep_mul.
+  cbv iota beta delta [RepBinOpOK F25519RepConversions F25519Rep_mul toRep unRep F25519toRep F25519unRep].
+  destruct x as [[[[[[[[[x9 x8] x7] x6] x5] x4] x3] x2] x1] x0].
+  destruct y as [[[[[[[[[y9 y8] y7] y6] y5] y4] y3] y2] y1] y0].
+  let E := constr:(GF25519Base25Point5_mul_reduce_formula x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 y0 y1 y2 y3 y4 y5 y6 y7 y8 y9) in
+  transitivity (ModularBaseSystem.decode (proj1_sig E)); [|solve[simpl;f_equal]];
+    destruct E as [? r]; cbv [proj1_sig].
+  cbv [rep ModularBaseSystem.rep PseudoMersenneBase modulus] in r; edestruct r; eauto.
+Qed.
+
+Definition F25519Rep_add (f g:F25519Rep) : F25519Rep.
+  refine (
+  let '(f9, f8, f7, f6, f5, f4, f3, f2, f1, f0) := f in
+  let '(g9, g8, g7, g6, g5, g4, g3, g2, g1, g0) := g in _).
+  let t' := (eval simpl in (proj1_sig (GF25519Base25Point5_add_formula f0 f1 f2 f3 f4 f5 f6 f7 f8 f9
+                                                                       g0 g1 g2 g3 g4 g5 g6 g7 g8 g9))) in
+  lazymatch t' with [?r0;?r1;?r2;?r3;?r4;?r5;?r6;?r7;?r8;?r9] =>
+                    exact (r9, r8, r7, r6, r5, r4, r3, r2, r1, r0)
+  end.
+Defined.
+
+Definition F25519Rep_sub (f g:F25519Rep) : F25519Rep.
+  refine (
+  let '(f9, f8, f7, f6, f5, f4, f3, f2, f1, f0) := f in
+  let '(g9, g8, g7, g6, g5, g4, g3, g2, g1, g0) := g in _).
+  let t' := (eval simpl in (proj1_sig (GF25519Base25Point5_sub_formula f0 f1 f2 f3 f4 f5 f6 f7 f8 f9
+                                                                       g0 g1 g2 g3 g4 g5 g6 g7 g8 g9))) in
+  lazymatch t' with [?r0;?r1;?r2;?r3;?r4;?r5;?r6;?r7;?r8;?r9] =>
+                    exact (r9, r8, r7, r6, r5, r4, r3, r2, r1, r0)
+  end.
+Defined.
+
+Lemma F25519_add_OK : RepBinOpOK F25519RepConversions ModularArithmetic.add F25519Rep_add.
+  cbv iota beta delta [RepBinOpOK F25519RepConversions F25519Rep_add toRep unRep F25519toRep F25519unRep].
+  destruct x as [[[[[[[[[x9 x8] x7] x6] x5] x4] x3] x2] x1] x0].
+  destruct y as [[[[[[[[[y9 y8] y7] y6] y5] y4] y3] y2] y1] y0].
+  let E := constr:(GF25519Base25Point5_add_formula x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 y0 y1 y2 y3 y4 y5 y6 y7 y8 y9) in
+  transitivity (ModularBaseSystem.decode (proj1_sig E)); [|solve[simpl;f_equal]];
+    destruct E as [? r]; cbv [proj1_sig].
+  cbv [rep ModularBaseSystem.rep PseudoMersenneBase modulus] in r; edestruct r; eauto.
+Qed.
+
+Lemma F25519_sub_OK : RepBinOpOK F25519RepConversions ModularArithmetic.sub F25519Rep_sub.
+  cbv iota beta delta [RepBinOpOK F25519RepConversions F25519Rep_sub toRep unRep F25519toRep F25519unRep].
+  destruct x as [[[[[[[[[x9 x8] x7] x6] x5] x4] x3] x2] x1] x0].
+  destruct y as [[[[[[[[[y9 y8] y7] y6] y5] y4] y3] y2] y1] y0].
+  let E := constr:(GF25519Base25Point5_sub_formula x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 y0 y1 y2 y3 y4 y5 y6 y7 y8 y9) in
+  transitivity (ModularBaseSystem.decode (proj1_sig E)); [|solve[simpl;f_equal]];
+    destruct E as [? r]; cbv [proj1_sig].
+  cbv [rep ModularBaseSystem.rep PseudoMersenneBase modulus] in r; edestruct r; eauto.
+Qed.
\ No newline at end of file