ported Specific files to use ModularBaseSystemInterface

1 files changed, 33 insertions, 80 deletions

diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v
index 6d7e2c38c..b668459bf 100644
--- a/src/Specific/GF25519.v
+++ b/src/Specific/GF25519.v
@@ -2,7 +2,7 @@ Require Import Crypto.ModularArithmetic.ModularBaseSystem.
 Require Import Crypto.ModularArithmetic.ModularBaseSystemOpt.
 Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParams.
 Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParamProofs.
-Require Import Crypto.ModularArithmetic.PseudoMersenneBaseRep.
+Require Import Crypto.ModularArithmetic.ModularBaseSystemInterface.
 Require Import Coq.Lists.List Crypto.Util.ListUtil.
 Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
 Require Import Crypto.Tactics.VerdiTactics.
@@ -38,94 +38,47 @@ Defined.
 (* Precompute k and c *)
 Definition k_ := Eval compute in k.
 Definition c_ := Eval compute in c.
+Definition k_subst : k = k_ := eq_refl k_.
 Definition c_subst : c = c_ := eq_refl c_.
+Definition fe25519 : Type := Eval cbv in fe.
 
-(* Makes Qed not take forever *)
-Opaque Z.shiftr Pos.iter Z.div2 Pos.div2 Pos.div2_up Pos.succ Z.land
-  Z.of_N Pos.land N.ldiff Pos.pred_N Pos.pred_double Z.opp Z.mul Pos.mul
-  Let_In digits Z.add Pos.add Z.pos_sub andb Z.eqb Z.ltb.
+Local Opaque Z.shiftr Z.shiftl Z.land Z.mul Z.add Z.sub Let_In.
 
-Local Open Scope nat_scope.
-Lemma GF25519Base25Point5_mul_reduce_formula :
-  forall f0 f1 f2 f3 f4 f5 f6 f7 f8 f9
-    g0 g1 g2 g3 g4 g5 g6 g7 g8 g9,
-    {ls | forall f g, rep [f0;f1;f2;f3;f4;f5;f6;f7;f8;f9] f
-                      -> rep [g0;g1;g2;g3;g4;g5;g6;g7;g8;g9] g
-                      -> rep ls (f*g)%F}.
-Proof.
-  eexists; intros ? ? Hf Hg.
-  pose proof (carry_mul_opt_rep k_ c_ (eq_refl k_) c_subst _ _ _ _ Hf Hg) as Hfg.
-  compute_formula.
-  exact Hfg.
-(*Time*) Defined.
-
-(* Uncomment this to see a pretty-printed mulmod
-Local Transparent Let_In.
-Infix "<<" := Z.shiftr.
-Infix "&" := Z.land.
-Eval cbv beta iota delta [proj1_sig GF25519Base25Point5_mul_reduce_formula Let_In] in
-  fun f0 f1 f2 f3 f4 f5 f6 f7 f8 f9
-    g0 g1 g2 g3 g4 g5 g6 g7 g8 g9 => 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).
-Local Opaque Let_In.
-*)
-
-
-Extraction "/tmp/test.ml" GF25519Base25Point5_mul_reduce_formula.
-(* It's easy enough to use extraction to get the proper nice-looking formula.
- * More Ltac acrobatics will be needed to get out that formula for further use in Coq.
- * The easiest fix will be to make the proof script above fully automated,
- * using [abstract] to contain the proof part. *)
-
-
-Lemma GF25519Base25Point5_add_formula :
-  forall f0 f1 f2 f3 f4 f5 f6 f7 f8 f9
-    g0 g1 g2 g3 g4 g5 g6 g7 g8 g9,
-    {ls | forall f g, rep [f0;f1;f2;f3;f4;f5;f6;f7;f8;f9] f
-                   -> rep [g0;g1;g2;g3;g4;g5;g6;g7;g8;g9] g
-                   -> rep ls (f + g)%F}.
+Definition add (f g:fe25519) : { fg | phi fg = @ModularArithmetic.add modulus (phi f) (phi g) }.
 Proof.
+  cbv [fe25519] in *.
+  repeat match goal with [p : (_*Z)%type |- _ ] => destruct p end.
   eexists.
-  intros f g Hf Hg.
-  pose proof (add_opt_rep _ _ _ _ Hf Hg) as Hfg.
-  compute_formula.
-  exact Hfg.
-Defined.
+  rewrite <-add_phi.
+  apply f_equal.
+  cbv.
+  reflexivity.
+Qed.
 
-Lemma GF25519Base25Point5_sub_formula :
-  forall f0 f1 f2 f3 f4 f5 f6 f7 f8 f9
-    g0 g1 g2 g3 g4 g5 g6 g7 g8 g9,
-    {ls | forall f g, rep [f0;f1;f2;f3;f4;f5;f6;f7;f8;f9] f
-                   -> rep [g0;g1;g2;g3;g4;g5;g6;g7;g8;g9] g
-                   -> rep ls (f - g)%F}.
+Definition mul (f g:fe25519) : { fg | phi fg = @ModularArithmetic.mul modulus (phi f) (phi g) }.
 Proof.
+  cbv [fe25519] in *.
+  repeat match goal with [p : (_*Z)%type |- _ ] => destruct p end.
   eexists.
-  intros f g Hf Hg.
-  pose proof (sub_opt_rep _ _ _ _ Hf Hg) as Hfg.
-  compute_formula.
-  exact Hfg.
-Defined.
+  rewrite <-(mul_phi (c_ := c_) (k_ := k_)) by auto using k_subst,c_subst.
+  apply f_equal.
+  cbv.
+  autorewrite with zsimplify.
+  reflexivity.
+Qed.
 
-Lemma GF25519Base25Point5_freeze_formula :
-  forall f0 f1 f2 f3 f4 f5 f6 f7 f8 f9,
-    {ls | forall x, rep [f0;f1;f2;f3;f4;f5;f6;f7;f8;f9] x
-                 -> rep ls x}.
-Proof.
-  eexists.
-  intros x Hf.
-  pose proof (freeze_opt_preserves_rep _ c_subst freezePreconditions25519 _ _ Hf) as Hfreeze_rep.
-  compute_formula.
-  exact Hfreeze_rep.
-Defined.
-
-(* Uncomment the below to see pretty-printed freeze function *)
 (*
-Set Printing Depth 1000.
 Local Transparent Let_In.
-Infix "<<" := Z.shiftr.
-Infix "&" := Z.land.
-Eval cbv beta iota delta [proj1_sig GF25519Base25Point5_freeze_formula Let_In] in
-  fun f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 => proj1_sig (
-    GF25519Base25Point5_freeze_formula f0 f1 f2 f3 f4 f5 f6 f7 f8 f9).
+Eval cbv iota beta delta [proj1_sig mul Let_In] in (fun f0 f1 f2 f3 f4  g0 g1 g2 g3 g4 => proj1_sig (mul (f4,f3,f2,f1,f0) (g4,g3,g2,g1,g0))).
 *)
+
+(* TODO: This file should eventually contain the following operations:
+   toBytes
+   fromBytes
+   inv
+   opp
+   sub
+   zero
+   one
+   eq
+*)
\ No newline at end of file