2 files changed, 53 insertions, 4 deletions

diff --git a/src/ModularArithmetic/ModularBaseSystemInterface.v b/src/ModularArithmetic/ModularBaseSystemInterface.v
index 40ad3f3ec..f92245bd7 100644
--- a/src/ModularArithmetic/ModularBaseSystemInterface.v
+++ b/src/ModularArithmetic/ModularBaseSystemInterface.v
@@ -5,16 +5,19 @@ Require Import Crypto.ModularArithmetic.ModularBaseSystemProofs.
 Require Import Crypto.BaseSystemProofs.
 Require Import Crypto.Util.Tuple Crypto.Util.CaseUtil.
 Require Import ZArith.
+Require Import Crypto.Algebra.
+Import Group.
 Import PseudoMersenneBaseParams PseudoMersenneBaseParamProofs.
 
 Generalizable All Variables.
 Section s.
   Context `{prm:PseudoMersenneBaseParams m} {sc : SubtractionCoefficient m prm}.
+  Context {k_ c_} (pfk : k = k_) (pfc:c = c_).
 
   Definition fe := tuple Z (length PseudoMersenneBaseParamProofs.base).
 
-  Definition mul {k_ c_} (pfk : k = k_) (pfc:c = c_) (x y:fe) : fe :=
-    carry_mul_opt_cps k_ c_ (fun xs : digits => from_list_default 0%Z (length base) xs)
+  Definition mul  (x y:fe) : fe :=
+    carry_mul_opt_cps k_ c_ (from_list_default 0%Z (length base))
       (to_list _ x) (to_list _ y).
 
   Definition add : fe -> fe -> fe.
@@ -27,4 +30,50 @@ Section s.
     abstract (intros; rewrite sub_opt_correct; apply length_sub; rewrite ?coeff_length; auto).
   Defined.
 
+  Arguments to_list {_ _} _.
+  Definition phi (a : fe) : ModularArithmetic.F m := decode (to_list a).
+  Definition phi_inv (a : ModularArithmetic.F m) : fe :=
+    from_list_default 0%Z _ (encode a).
+
+  Lemma phi_inv_spec : forall a, phi (phi_inv a) = a.
+  Proof.
+    intros; cbv [phi_inv phi].
+    erewrite from_list_default_eq.
+    rewrite to_list_from_list.
+    apply ModularBaseSystemProofs.encode_rep.
+    Grab Existential Variables.
+    apply ModularBaseSystemProofs.encode_rep.
+  Qed.
+
+  Definition eq (x y : fe) : Prop := phi x = phi y.
+
+  Definition zero : fe := phi_inv (ModularArithmetic.ZToField 0).
+
+  Definition opp (x : fe) : fe := phi_inv (ModularArithmetic.opp (phi x)).
+
+  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.
+  Admitted.
+
+  Lemma mul_correct : forall a b,
+    to_list (mul a b) = carry_mul (to_list a) (to_list b).
+  Proof.
+    intros; cbv [mul].
+    rewrite carry_mul_opt_cps_correct by assumption.
+    erewrite from_list_default_eq.
+    apply to_list_from_list.
+    Grab Existential Variables.
+    apply carry_mul_length; apply length_to_list.
+  Qed.
+
+  Lemma mul_phi : forall a b : fe,
+    phi (mul a b) = ModularArithmetic.mul (phi a) (phi b).
+  Proof.
+    intros; cbv beta delta [phi].
+    rewrite mul_correct.
+    apply carry_mul_rep; auto using decode_rep, length_to_list.
+  Qed.
+
 End s.
\ No newline at end of file
diff --git a/src/Specific/GF1305.v b/src/Specific/GF1305.v
index edb122ac2..057676ee2 100644
--- a/src/Specific/GF1305.v
+++ b/src/Specific/GF1305.v
@@ -48,11 +48,11 @@ Definition fe1305 : Type := Eval cbv in fe.
 
 Local Opaque Z.shiftr Z.shiftl Z.land Z.mul Z.add Z.sub Let_In.
 
-Definition mul (f g:fe1305) : { fg | fg = ModularBaseSystemInterface.mul k_subst c_subst f g }.
+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 *)
   cbv [fe1305] in *.
   repeat match goal with [p : (_*Z)%type |- _ ] => destruct p end.
-  eexists. 
+  eexists.
   cbv.
   autorewrite with zsimplify.
   reflexivity.