ported Specific files to use ModularBaseSystemInterface

3 files changed, 61 insertions, 146 deletions

diff --git a/src/ModularArithmetic/ModularBaseSystemInterface.v b/src/ModularArithmetic/ModularBaseSystemInterface.v
index 2affd9793..e4192428e 100644
--- a/src/ModularArithmetic/ModularBaseSystemInterface.v
+++ b/src/ModularArithmetic/ModularBaseSystemInterface.v
@@ -51,7 +51,6 @@ Section s.
 
   Definition opp (x : fe) : fe := phi_inv (ModularArithmetic.opp (phi x)).
 
-
   Lemma add_correct : forall a b,
     to_list (add a b) = BaseSystem.add (to_list a) (to_list b).
   Proof.
@@ -68,18 +67,6 @@ Section s.
     apply ModularBaseSystemProofs.add_rep; auto using decode_rep, length_to_list.
   Qed.
 
-  Lemma optimized_group : @group fe eq add zero opp.
-  Proof.
-    eapply @isomorphism_to_subgroup_group; cbv [opp zero eq]; intros;
-      eauto; rewrite ?phi_inv_spec; try reflexivity.
-    + econstructor; eauto. admit.
-    + apply (eq_dec _ _).
-    + admit.
-    + admit.
-    + admit.
-    + apply add_phi.
-  Qed.
-
   Lemma mul_correct : forall a b,
     to_list (mul a b) = carry_mul (to_list a) (to_list b).
   Proof.
diff --git a/src/Specific/GF1305.v b/src/Specific/GF1305.v
index 057676ee2..2b917086b 100644
--- a/src/Specific/GF1305.v
+++ b/src/Specific/GF1305.v
@@ -46,69 +46,44 @@ Definition c_subst : c = c_ := eq_refl c_.
 
 Definition fe1305 : Type := Eval cbv in fe.
 
-Local Opaque Z.shiftr Z.shiftl Z.land Z.mul Z.add Z.sub Let_In.
+Local Opaque Z.shiftr Z.shiftl Z.land Z.mul Z.add Z.sub Let_In phi.
 
-Definition mul (f g:fe1305) : { fg | fg = @ModularBaseSystemInterface.mul _ _ k_ c_ f g }.
-  (* NOTE: beautiful example of reduction slowness: stack overflow if [f] [g] are not destructed first *)
+Definition add (f g:fe1305) : { fg | phi fg = @ModularArithmetic.add modulus (phi f) (phi g) }.
+Proof.
+  cbv [fe1305] in *.
+  repeat match goal with [p : (_*Z)%type |- _ ] => destruct p end.
+  eexists.
+  rewrite <-add_phi.
+  cbv.
+  apply f_equal.
+  reflexivity.
+Qed.
+
+Definition mul (f g:fe1305) : { fg | phi fg = @ModularArithmetic.mul modulus (phi f) (phi g) }.
+Proof.
   cbv [fe1305] in *.
   repeat match goal with [p : (_*Z)%type |- _ ] => destruct p end.
   eexists.
+  rewrite <-(mul_phi (c_ := c_) (k_ := k_)) by auto using k_subst,c_subst.
   cbv.
+  apply f_equal.
   autorewrite with zsimplify.
+  repeat match goal with |- appcontext[?a * 1] => rewrite (Z.mul_1_r a) end.
   reflexivity.
-Defined.
+Qed.
 
 (*
 Local Transparent Let_In.
 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))).
 *)
 
-Local Open Scope nat_scope.
-Lemma GF1305Base26_mul_reduce_formula :
-  forall f0 f1 f2 f3 f4 g0 g1 g2 g3 g4,
-    {ls | forall f g, rep [f0;f1;f2;f3;f4] f
-                      -> rep [g0;g1;g2;g3;g4] 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.
-Defined.
-
-Lemma GF1305Base26_add_formula :
-  forall f0 f1 f2 f3 f4 g0 g1 g2 g3 g4,
-    {ls | forall f g, rep [f0;f1;f2;f3;f4] f
-                   -> rep [g0;g1;g2;g3;g4] g
-                   -> rep ls (f + g)%F}.
-Proof.
-  eexists; intros ? ? Hf Hg.
-  pose proof (add_opt_rep _ _ _ _ Hf Hg) as Hfg.
-  compute_formula.
-  exact Hfg.
-Defined.
-
-Lemma GF1305Base26_sub_formula :
-  forall f0 f1 f2 f3 f4 g0 g1 g2 g3 g4,
-    {ls | forall f g, rep [f0;f1;f2;f3;f4] f
-                   -> rep [g0;g1;g2;g3;g4] g
-                   -> rep ls (f - g)%F}.
-Proof.
-  eexists.
-  intros f g Hf Hg.
-  pose proof (sub_opt_rep _ _ _ _ Hf Hg) as Hfg.
-  compute_formula.
-  exact Hfg.
-Defined.
-
-Lemma GF1305Base26_freeze_formula :
-  forall f0 f1 f2 f3 f4,
-    {ls | forall x, rep [f0;f1;f2;f3;f4] x
-                 -> rep ls x}.
-Proof.
-  eexists.
-  intros x Hf.
-  pose proof (freeze_opt_preserves_rep _ c_subst freezePreconditions1305 _ _ Hf) as Hfreeze_rep.
-  compute_formula.
-  exact Hfreeze_rep.
-Defined.
+(* TODO: This file should eventually contain the following operations:
+   toBytes
+   fromBytes
+   inv
+   opp
+   sub
+   zero
+   one
+   eq
+*)
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