From 4ea92779f54a7f6a49e334cd6071096be57c40ca Mon Sep 17 00:00:00 2001
From: jadep <jade.philipoom@gmail.com>
Date: Wed, 20 Jul 2016 16:02:27 -0400
Subject: restructured ModularBaseSystem pipeline to put tuple conversion
 before ModularBaseSystem is fully defined, rather than after
 ModularBaseSystemOpt

---
 src/ModularArithmetic/ModularBaseSystem.v          |  23 +++-
 src/ModularArithmetic/ModularBaseSystemInterface.v | 150 ---------------------
 src/ModularArithmetic/ModularBaseSystemList.v      |  69 ++++++++++
 .../ModularBaseSystemListProofs.v                  |  95 +++++++++++++
 src/ModularArithmetic/ModularBaseSystemOpt.v       | 132 +++++++++---------
 src/Specific/GF1305.v                              |  80 +++++++----
 src/Specific/GF25519.v                             |  85 +++++++-----
 7 files changed, 364 insertions(+), 270 deletions(-)
 delete mode 100644 src/ModularArithmetic/ModularBaseSystemInterface.v
 create mode 100644 src/ModularArithmetic/ModularBaseSystemList.v
 create mode 100644 src/ModularArithmetic/ModularBaseSystemListProofs.v

(limited to 'src')

diff --git a/src/ModularArithmetic/ModularBaseSystem.v b/src/ModularArithmetic/ModularBaseSystem.v
index dde021b4c..70c8138da 100644
--- a/src/ModularArithmetic/ModularBaseSystem.v
+++ b/src/ModularArithmetic/ModularBaseSystem.v
@@ -37,6 +37,19 @@ Section ModularBaseSystem.
    from_list (sub [[modulus_multiple]] [[us]] [[vs]])
    (length_sub length_to_list length_to_list length_to_list).
 
+  Definition zero : digits := encode (ZToField 0).
+
+  Definition one : digits := encode (ZToField 1).
+
+  (* Placeholder *)
+  Definition opp (x : digits) : digits := encode (ModularArithmetic.opp (decode x)).
+
+  (* Placeholder *)
+  Definition inv (x : digits) : digits := encode (ModularArithmetic.inv (decode x)).
+
+  (* Placeholder *)
+  Definition div (x y : digits) : digits := encode (ModularArithmetic.div (decode x) (decode y)).
+
   Definition carry i (us : digits) : digits := from_list (carry i [[us]])
     (length_carry length_to_list).
 
@@ -52,7 +65,15 @@ Section ModularBaseSystem.
 
   Definition freeze (us : digits) : digits :=
     let us' := carry_full (carry_full (carry_full us)) in
-     from_list (conditional_subtract_modulus [[us]] (ge_modulus [[us]]))
+     from_list (conditional_subtract_modulus [[us']] (ge_modulus [[us']]))
      (length_conditional_subtract_modulus length_to_list).
 
+  Definition eq (x y : digits) : Prop := decode x = decode y.
+
+  Import Morphisms.
+  Global Instance eq_Equivalence : Equivalence eq.
+  Proof.
+    split; cbv [eq]; repeat intro; congruence.
+  Qed.
+
 End ModularBaseSystem.
\ No newline at end of file
diff --git a/src/ModularArithmetic/ModularBaseSystemInterface.v b/src/ModularArithmetic/ModularBaseSystemInterface.v
deleted file mode 100644
index c79dce1d3..000000000
--- a/src/ModularArithmetic/ModularBaseSystemInterface.v
+++ /dev/null
@@ -1,150 +0,0 @@
-Require Import Crypto.BaseSystem.
-Require Import Crypto.ModularArithmetic.ModularBaseSystem.
-Require Import Crypto.ModularArithmetic.ModularBaseSystemOpt.
-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_).
-  Local Notation base := (Pow2Base.base_from_limb_widths limb_widths).
-
-  Definition fe := tuple Z (length base).
-
-  Arguments to_list {_ _} _.
-
-  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 (x y : fe) : fe :=
-    from_list_default 0%Z (length base) (add_opt (to_list x) (to_list y)).
-
-  Definition sub : fe -> fe -> fe.
-    refine (on_tuple2 sub_opt _).
-    abstract (intros; rewrite sub_opt_correct; apply length_sub; rewrite ?coeff_length; auto).
-  Defined.
-
-  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.
-
-  Import Morphisms.
-  Global Instance eq_Equivalence : Equivalence eq.
-  Proof.
-    split; cbv [eq]; repeat intro; congruence.
-  Qed.
-
-  Lemma phi_inv_spec_reverse : forall a, eq (phi_inv (phi a)) a.
-  Proof.
-    intros. unfold eq. rewrite phi_inv_spec; reflexivity.
-  Qed.
-
-  Definition zero : fe := phi_inv (ModularArithmetic.ZToField 0).
-
-  Definition opp (x : fe) : fe := phi_inv (ModularArithmetic.opp (phi x)).
-
-  Definition one : fe := phi_inv (ModularArithmetic.ZToField 1).
-
-  Definition inv (x : fe) : fe := phi_inv (ModularArithmetic.inv (phi x)).
-
-  Definition div (x y : fe) : fe := phi_inv (ModularArithmetic.div (phi x) (phi y)).
-
-  Lemma add_correct : forall a b,
-    to_list (add a b) = BaseSystem.add (to_list a) (to_list b).
-  Proof.
-    intros; cbv [add].
-    rewrite add_opt_correct.
-    erewrite from_list_default_eq.
-    apply to_list_from_list.
-    Grab Existential Variables.
-    apply add_same_length; auto using length_to_list.
-  Qed.
-
-  Lemma add_phi : forall a b : fe,
-    phi (add a b) = ModularArithmetic.add (phi a) (phi b).
-  Proof.
-    intros; cbv [phi].
-    rewrite add_correct.
-    apply ModularBaseSystemProofs.add_rep; auto using decode_rep, length_to_list.
-  Qed.
-
-  Lemma sub_correct : forall a b,
-    to_list (sub a b) = ModularBaseSystem.sub coeff (to_list a) (to_list b).
-  Proof.
-    intros; cbv [sub on_tuple2].
-    rewrite to_list_from_list.
-    apply sub_opt_correct.
-  Qed.
-
-  Lemma sub_phi : forall a b : fe,
-    phi (sub a b) = ModularArithmetic.sub (phi a) (phi b).
-  Proof.
-    intros; cbv [phi].
-    rewrite sub_correct.
-    apply ModularBaseSystemProofs.sub_rep; auto using decode_rep, length_to_list,
-      coeff_length, coeff_mod.
-  Qed.
-
-  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.
-
-  Lemma modular_base_system_field : @field fe eq zero one opp add sub mul inv div.
-  Proof.
-    eapply (Field.isomorphism_to_subfield_field (phi := phi) (fieldR := PrimeFieldTheorems.field_modulo  (prime_q := prime_modulus))).
-    Grab Existential Variables.
-    + intros; eapply phi_inv_spec.
-    + intros; eapply phi_inv_spec.
-    + intros; eapply phi_inv_spec.
-    + intros; eapply phi_inv_spec.
-    + intros; eapply mul_phi.
-    + intros; eapply sub_phi.
-    + intros; eapply add_phi.
-    + intros; eapply phi_inv_spec.
-    + cbv [eq zero one]. erewrite !phi_inv_spec. intro A.
-      eapply (PrimeFieldTheorems.Fq_1_neq_0 (prime_q := prime_modulus)). congruence.
-    + trivial.
-    + repeat intro. cbv [div]. congruence.
-    + repeat intro. cbv [inv]. congruence.
-    + repeat intro. cbv [eq]. erewrite !mul_phi. congruence.
-    + repeat intro. cbv [eq]. erewrite !sub_phi. congruence.
-    + repeat intro. cbv [eq]. erewrite !add_phi. congruence.
-    + repeat intro. cbv [opp]. congruence.
-    + cbv [eq]. auto using ModularArithmeticTheorems.F_eq_dec.
-  Qed.
-
-End s.
\ No newline at end of file
diff --git a/src/ModularArithmetic/ModularBaseSystemList.v b/src/ModularArithmetic/ModularBaseSystemList.v
new file mode 100644
index 000000000..6a5a30429
--- /dev/null
+++ b/src/ModularArithmetic/ModularBaseSystemList.v
@@ -0,0 +1,69 @@
+Require Import Coq.ZArith.Zpower Coq.ZArith.ZArith.
+Require Import Coq.Lists.List.
+Require Import Crypto.Util.ListUtil Crypto.Util.CaseUtil Crypto.Util.ZUtil.
+Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
+Require Import Crypto.BaseSystem.
+Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParams.
+Require Import Crypto.ModularArithmetic.ExtendedBaseVector.
+Require Import Crypto.Tactics.VerdiTactics.
+Require Import Crypto.Util.Notations.
+Require Import Crypto.ModularArithmetic.Pow2Base.
+Local Open Scope Z_scope.
+
+Section Defs.
+  Context `{prm :PseudoMersenneBaseParams} (modulus_multiple : digits).
+  Local Notation base := (base_from_limb_widths limb_widths).
+  Local Notation "u [ i ]" := (nth_default 0 u i) (at level 40).
+
+  Definition decode (us : digits) : F modulus := ZToField (BaseSystem.decode base us).
+
+  Definition encode (x : F modulus) := encodeZ limb_widths x.
+
+  (* Converts from length of extended base to length of base by reduction modulo M.*)
+  Definition reduce (us : digits) : digits :=
+    let high := skipn (length limb_widths) us in
+    let low := firstn (length limb_widths) us in
+    let wrap := map (Z.mul c) high in
+    BaseSystem.add low wrap.
+
+  Definition mul (us vs : digits) := reduce (BaseSystem.mul ext_base us vs).
+
+  (* In order to subtract without underflowing, we add a multiple of the modulus first. *)
+  Definition sub (us vs : digits) := BaseSystem.sub (add modulus_multiple us) vs.
+
+  (*
+  Definition carry_and_reduce :=
+    carry_gen limb_widths (fun ci => c * ci).
+   *)
+  Definition carry_and_reduce i := fun us =>
+    let di := us [i] in
+    let us' := set_nth i (Z.pow2_mod di (limb_widths [i]))  us in
+    add_to_nth   0  (c * (Z.shiftr   di (limb_widths [i]))) us'.
+
+  Definition carry i : digits -> digits :=
+    if eq_nat_dec i (pred (length base))
+    then carry_and_reduce i
+    else carry_simple limb_widths i.
+
+  Definition modulus_digits := encodeZ limb_widths modulus.
+
+  (* compute at compile time *)
+  Definition max_ones := Z.ones (fold_right Z.max 0 limb_widths).
+
+  (* Constant-time comparison with modulus; only works if all digits of [us]
+    are less than 2 ^ their respective limb width. *)
+  Fixpoint ge_modulus' us acc i :=
+    match i with
+    | O => andb (Z.ltb (modulus_digits [0]) (us [0])) acc
+    | S i' => ge_modulus' us (andb (Z.eqb (modulus_digits [i]) (us [i])) acc) i'
+    end.
+
+  Definition ge_modulus us := ge_modulus' us true (length base - 1)%nat.
+
+  Definition conditional_subtract_modulus (us : digits) (cond : bool) :=
+     let and_term := if cond then max_ones else 0 in
+    (* [and_term] is all ones if us' is full, so the subtractions subtract q overall.
+       Otherwise, it's all zeroes, and the subtractions do nothing. *)
+     map2 (fun x y => x - y) us (map (Z.land and_term) modulus_digits).
+
+End Defs.
\ No newline at end of file
diff --git a/src/ModularArithmetic/ModularBaseSystemListProofs.v b/src/ModularArithmetic/ModularBaseSystemListProofs.v
new file mode 100644
index 000000000..688d45e1c
--- /dev/null
+++ b/src/ModularArithmetic/ModularBaseSystemListProofs.v
@@ -0,0 +1,95 @@
+Require Import Zpower ZArith.
+Require Import Coq.Numbers.Natural.Peano.NPeano.
+Require Import List.
+Require Import VerdiTactics.
+Require Import Crypto.BaseSystemProofs.
+Require Import Crypto.ModularArithmetic.Pow2Base.
+Require Import Crypto.ModularArithmetic.Pow2BaseProofs.
+Require Import Crypto.ModularArithmetic.ExtendedBaseVector.
+Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
+Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParams.
+Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParamProofs.
+Require Import Crypto.Util.Tactics.
+Require Import Crypto.Util.ListUtil.
+Require Import Crypto.Util.Notations.
+
+Require Import Crypto.ModularArithmetic.ModularBaseSystemList.
+Local Open Scope Z_scope.
+
+Section LengthProofs.
+  Context `{prm :PseudoMersenneBaseParams}.
+  Local Notation base := (base_from_limb_widths limb_widths).
+
+  Lemma length_encode {x} : length (encode x) = length limb_widths.
+  Proof.
+    cbv [encode encodeZ]; intros.
+    rewrite encode'_spec;
+      auto using encode'_length, limb_widths_nonneg, Nat.eq_le_incl, base_length.
+  Qed.
+
+  Lemma length_reduce : forall us,
+      (length limb_widths <= length us <= length ext_base)%nat ->
+      (length (reduce us) = length limb_widths)%nat.
+  Proof.
+    rewrite extended_base_length.
+    unfold reduce; intros.
+    rewrite add_length_exact.
+    pose proof base_length.
+    rewrite map_length, firstn_length, skipn_length, Min.min_l, Max.max_l;
+      omega.
+  Qed.
+
+  Lemma length_mul {u v} :
+      length u = length limb_widths
+      -> length v = length limb_widths
+      -> length (mul u v) = length limb_widths.
+  Proof.
+    cbv [mul]; intros.
+    apply length_reduce.
+    destruct u; try congruence.
+    + rewrite @nil_length0 in *; omega.
+    + rewrite mul_length_exact, extended_base_length, base_length; try omega.
+      congruence.
+  Qed.
+
+  Section Sub.
+  Context {mm : list Z} (mm_length : length mm = length limb_widths).
+
+  Lemma length_sub {u v} :
+      length u = length limb_widths
+      -> length v = length limb_widths
+      -> length (sub mm u v) = length limb_widths.
+  Proof.
+    cbv [sub]; intros.
+    rewrite sub_length, add_length_exact.
+    repeat rewrite Max.max_r; omega.
+  Qed.
+  End Sub.
+
+  Lemma length_carry_and_reduce {us}: forall i, length (carry_and_reduce i us) = length us.
+  Proof. intros; unfold carry_and_reduce; autorewrite with distr_length; reflexivity. Qed.
+  Hint Rewrite @length_carry_and_reduce : distr_length.
+
+  Lemma length_carry {u i} :
+    length u = length limb_widths
+    -> length (carry i u) = length limb_widths.
+  Proof. intros; unfold carry; break_if; autorewrite with distr_length; omega. Qed.
+  Hint Rewrite @length_carry : distr_length.
+
+  Lemma length_modulus_digits : length modulus_digits = length limb_widths.
+  Proof.
+    intros; unfold modulus_digits, encodeZ.
+    rewrite encode'_spec, encode'_length;
+      auto using encode'_length, limb_widths_nonneg, Nat.eq_le_incl, base_length.
+  Qed.
+
+  Lemma length_conditional_subtract_modulus {u cond} :
+    length u = length limb_widths
+    -> length (conditional_subtract_modulus u cond) = length limb_widths.
+  Proof.
+    intros; unfold conditional_subtract_modulus.
+    rewrite map2_length, map_length, length_modulus_digits.
+    apply Min.min_case; omega.
+  Qed.
+
+End LengthProofs.
\ No newline at end of file
diff --git a/src/ModularArithmetic/ModularBaseSystemOpt.v b/src/ModularArithmetic/ModularBaseSystemOpt.v
index 696f10438..c4d4ccca0 100644
--- a/src/ModularArithmetic/ModularBaseSystemOpt.v
+++ b/src/ModularArithmetic/ModularBaseSystemOpt.v
@@ -4,8 +4,12 @@ Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParamProofs.
 Require Import Crypto.ModularArithmetic.ModularBaseSystemProofs.
 Require Import Crypto.ModularArithmetic.ExtendedBaseVector.
 Require Import Crypto.ModularArithmetic.Pow2BaseProofs.
-Require Import Crypto.BaseSystem Crypto.ModularArithmetic.ModularBaseSystem.
+Require Import Crypto.BaseSystem.
+Require Import Crypto.ModularArithmetic.ModularBaseSystemList.
+Require Import Crypto.ModularArithmetic.ModularBaseSystemListProofs.
+Require Import Crypto.ModularArithmetic.ModularBaseSystem.
 Require Import Coq.Lists.List.
+Require Import Crypto.Util.Tuple.
 Require Import Crypto.Util.ListUtil Crypto.Util.ZUtil Crypto.Util.NatUtil Crypto.Util.CaseUtil.
 Import ListNotations.
 Require Import Coq.ZArith.ZArith Coq.ZArith.Zpower Coq.ZArith.ZArith Coq.ZArith.Znumtheory.
@@ -14,8 +18,7 @@ Require Import Crypto.Tactics.VerdiTactics.
 Local Open Scope Z.
 
 Class SubtractionCoefficient (m : Z) (prm : PseudoMersenneBaseParams m) := {
-  coeff : BaseSystem.digits;
-  coeff_length : (length coeff = length (Pow2Base.base_from_limb_widths limb_widths))%nat;
+  coeff : tuple Z (length limb_widths);
   coeff_mod: decode coeff = 0%F
 }.
 
@@ -37,9 +40,9 @@ Definition map_opt {A B} := Eval compute in @map A B.
 Definition full_carry_chain_opt := Eval compute in @Pow2Base.full_carry_chain.
 Definition length_opt := Eval compute in length.
 Definition base_from_limb_widths_opt := Eval compute in @Pow2Base.base_from_limb_widths.
-Definition max_ones_opt := Eval compute in @max_ones.
-Definition max_bound_opt := Eval compute in @max_bound.
 Definition minus_opt := Eval compute in minus.
+Definition max_ones_opt := Eval compute in @max_ones.
+Definition from_list_default_opt {A} := Eval compute in (@from_list_default A).
 
 Definition Let_In {A P} (x : A) (f : forall y : A, P y)
   := let y := x in f y.
@@ -110,14 +113,16 @@ Section Carries.
     (* allows caller to precompute k and c *)
     (k_ c_ : Z) (k_subst : k = k_) (c_subst : c = c_).
   Local Notation base := (Pow2Base.base_from_limb_widths limb_widths).
+  Local Notation digits := (tuple Z (length limb_widths)).
 
   Definition carry_opt_sig
              (i : nat) (b : digits)
     : { d : digits | (i < length limb_widths)%nat -> d = carry i b }.
   Proof.
     eexists ; intros.
-    cbv [carry].
-    rewrite <- pull_app_if_sumbool.
+    cbv [carry ModularBaseSystemList.carry].
+    rewrite <-from_list_default_eq with (d := 0%Z).
+    rewrite <-pull_app_if_sumbool.
     cbv beta delta
       [carry carry_and_reduce Pow2Base.carry_gen Pow2Base.carry_and_reduce_single Pow2Base.carry_simple
        Z.pow2_mod Z.ones Z.pred
@@ -127,12 +132,13 @@ Section Carries.
     change @nth_default with @nth_default_opt in *.
     change @set_nth with @set_nth_opt in *.
     lazymatch goal with
-    | [ |- _ = (if ?br then ?c else ?d) ]
+    | [ |- _ = _ (if ?br then ?c else ?d) ]
       => let x := fresh "x" in let y := fresh "y" in evar (x:digits); evar (y:digits); transitivity (if br then x else y); subst x; subst y
     end.
     2:cbv zeta.
     2:break_if; reflexivity.
 
+    change @from_list_default with @from_list_default_opt.
     change @nth_default with @nth_default_opt.
     rewrite c_subst.
     change @set_nth with @set_nth_opt.
@@ -141,10 +147,12 @@ Section Carries.
     reflexivity.
   Defined.
 
-  Definition carry_opt i b
-    := Eval cbv beta iota delta [proj1_sig carry_opt_sig] in proj1_sig (carry_opt_sig i b).
+  Definition carry_opt is us := Eval cbv [proj1_sig carry_opt_sig] in
+                                          proj1_sig (carry_opt_sig is us).
 
-  Definition carry_opt_correct i b : (i < length limb_widths)%nat -> carry_opt i b = carry i b := proj2_sig (carry_opt_sig i b).
+  Definition carry_opt_correct i us
+    : (i < length limb_widths)%nat -> carry_opt i us = carry i us
+    := proj2_sig (carry_opt_sig i us).
 
   Definition carry_sequence_opt_sig (is : list nat) (us : digits)
     : { b : digits | (forall i, In i is -> i < length base)%nat -> b = carry_sequence is us }.
@@ -183,8 +191,8 @@ Section Carries.
     cbv beta iota delta [carry_opt].
     let LHS := match goal with |- ?LHS = ?RHS => LHS end in
     let RHS := match goal with |- ?LHS = ?RHS => RHS end in
-    let RHSf := match (eval pattern (nth_default_opt 0%Z b i) in RHS) with ?RHSf _ => RHSf end in
-    change (LHS = Let_In (nth_default_opt 0%Z b i) RHSf).
+    let RHSf := match (eval pattern (nth_default_opt 0%Z (to_list _ b) i) in RHS) with ?RHSf _ => RHSf end in
+    change (LHS = Let_In (nth_default_opt 0%Z (to_list _ b) i) RHSf).
     change Z.shiftl with Z_shiftl_opt.
     change (-1) with (Z_opp_opt 1).
     change Z.add with Z_add_opt at 5 9 17 21.
@@ -265,13 +273,13 @@ Section Carries.
 
 
   Lemma carry_sequence_opt_cps_rep
-       : forall (is : list nat) (us : list Z) (x : F modulus),
+       : forall (is : list nat) (us : digits) (x : F modulus),
          (forall i : nat, In i is -> i < length base)%nat ->
          rep us x -> rep (carry_sequence_opt_cps is us) x.
   Proof.
     intros.
     rewrite carry_sequence_opt_cps_correct by assumption.
-    apply carry_sequence_rep; eauto using rep_length.
+    auto using carry_sequence_rep.
   Qed.
 
   Lemma full_carry_chain_bounds : forall i, In i (Pow2Base.full_carry_chain limb_widths) -> (i < length base)%nat.
@@ -320,6 +328,7 @@ End Carries.
 
 Section Addition.
   Context `{prm : PseudoMersenneBaseParams} {sc : SubtractionCoefficient modulus prm}.
+  Local Notation digits := (tuple Z (length limb_widths)).
 
   Definition add_opt_sig (us vs : digits) : { b : digits | b = add us vs }.
   Proof.
@@ -338,6 +347,7 @@ End Addition.
 
 Section Subtraction.
   Context `{prm : PseudoMersenneBaseParams} {sc : SubtractionCoefficient modulus prm}.
+  Local Notation digits := (tuple Z (length limb_widths)).
 
   Definition sub_opt_sig (us vs : digits) : { b : digits | b = sub coeff us vs }.
   Proof.
@@ -358,9 +368,11 @@ Section Multiplication.
   Context `{prm : PseudoMersenneBaseParams} {sc : SubtractionCoefficient modulus prm}
     (* allows caller to precompute k and c *)
     (k_ c_ : Z) (k_subst : k = k_) (c_subst : c = c_).
+  Local Notation digits := (tuple Z (length limb_widths)).
+
   Definition mul_bi'_step
-             (mul_bi' : nat -> digits -> list Z -> list Z)
-             (i : nat) (vsr : digits) (bs : list Z)
+             (mul_bi' : nat -> list Z -> list Z -> list Z)
+             (i : nat) (vsr : list Z) (bs : list Z)
     : list Z
     := match vsr with
        | [] => []
@@ -368,8 +380,8 @@ Section Multiplication.
        end.
 
   Definition mul_bi'_opt_step_sig
-             (mul_bi' : nat -> digits -> list Z -> list Z)
-             (i : nat) (vsr : digits) (bs : list Z)
+             (mul_bi' : nat -> list Z -> list Z -> list Z)
+             (i : nat) (vsr : list Z) (bs : list Z)
     : { l : list Z | l = mul_bi'_step mul_bi' i vsr bs }.
   Proof.
     eexists.
@@ -384,19 +396,19 @@ Section Multiplication.
   Defined.
 
   Definition mul_bi'_opt_step
-             (mul_bi' : nat -> digits -> list Z -> list Z)
-             (i : nat) (vsr : digits) (bs : list Z)
+             (mul_bi' : nat -> list Z -> list Z -> list Z)
+             (i : nat) (vsr : list Z) (bs : list Z)
     : list Z
     := Eval cbv [proj1_sig mul_bi'_opt_step_sig] in
         proj1_sig (mul_bi'_opt_step_sig mul_bi' i vsr bs).
 
   Fixpoint mul_bi'_opt
-           (i : nat) (vsr : digits) (bs : list Z) {struct vsr}
+           (i : nat) (vsr : list Z) (bs : list Z) {struct vsr}
     : list Z
     := mul_bi'_opt_step mul_bi'_opt i vsr bs.
 
   Definition mul_bi'_opt_correct
-             (i : nat) (vsr : digits) (bs : list Z)
+             (i : nat) (vsr : list Z) (bs : list Z)
     : mul_bi'_opt i vsr bs = mul_bi' bs i vsr.
   Proof.
     revert i; induction vsr as [|vsr vsrs IHvsr]; intros.
@@ -413,12 +425,12 @@ Section Multiplication.
   Qed.
 
   Definition mul'_step
-             (mul' : digits -> digits -> list Z -> digits)
-             (usr vs : digits) (bs : list Z)
-    : digits
+             (mul' : list Z -> list Z -> list Z -> list Z)
+             (usr vs : list Z) (bs : list Z)
+    : list Z
     := match usr with
        | [] => []
-       | u :: usr' => add (mul_each u (mul_bi bs (length usr') vs)) (mul' usr' vs bs)
+       | u :: usr' => BaseSystem.add (mul_each u (mul_bi bs (length usr') vs)) (mul' usr' vs bs)
        end.
 
   Lemma map_zeros : forall a n l,
@@ -428,9 +440,9 @@ Section Multiplication.
   Qed.
 
   Definition mul'_opt_step_sig
-             (mul' : digits -> digits -> list Z -> digits)
-             (usr vs : digits) (bs : list Z)
-    : { d : digits | d = mul'_step mul' usr vs bs }.
+             (mul' : list Z -> list Z -> list Z -> list Z)
+             (usr vs : list Z) (bs : list Z)
+    : { d : list Z | d = mul'_step mul' usr vs bs }.
   Proof.
     eexists.
     cbv [mul'_step].
@@ -449,18 +461,18 @@ Section Multiplication.
   Defined.
 
   Definition mul'_opt_step
-             (mul' : digits -> digits -> list Z -> digits)
-             (usr vs : digits) (bs : list Z)
-    : digits
+             (mul' : list Z -> list Z -> list Z -> list Z)
+             (usr vs : list Z) (bs : list Z)
+    : list Z
     := Eval cbv [proj1_sig mul'_opt_step_sig] in proj1_sig (mul'_opt_step_sig mul' usr vs bs).
 
   Fixpoint mul'_opt
-           (usr vs : digits) (bs : list Z)
-    : digits
+           (usr vs : list Z) (bs : list Z)
+    : list Z
     := mul'_opt_step mul'_opt usr vs bs.
 
   Definition mul'_opt_correct
-           (usr vs : digits) (bs : list Z)
+           (usr vs : list Z) (bs : list Z)
     : mul'_opt usr vs bs = mul' bs usr vs.
   Proof.
     revert vs; induction usr as [|usr usrs IHusr]; intros.
@@ -471,13 +483,17 @@ Section Multiplication.
       cbv [mul_each mul_bi].
       rewrite map_zeros.
       rewrite <- mul_bi'_opt_correct.
+      cbv [zeros].
       reflexivity. }
   Qed.
 
   Definition mul_opt_sig (us vs : digits) : { b : digits | b = mul us vs }.
   Proof.
     eexists.
-    cbv [BaseSystem.mul mul mul_each mul_bi mul_bi' zeros reduce].
+    cbv [mul ModularBaseSystemList.mul BaseSystem.mul mul_each mul_bi mul_bi' zeros reduce].
+    rewrite <- from_list_default_eq with (d := 0%Z).
+    change (@from_list_default Z) with (@from_list_default_opt Z).
+    apply f_equal.
     rewrite ext_base_alt.
     rewrite <- mul'_opt_correct.
     change @Pow2Base.base_from_limb_widths with base_from_limb_widths_opt.
@@ -525,8 +541,8 @@ Section with_base.
         int_width_pos : 0 < int_width;
         int_width_compat : forall w, In w limb_widths -> w <= int_width;
         c_pos : 0 < c;
-        c_reduce1 : c * (Z.ones (int_width - log_cap (pred (length base)))) < max_bound 0 + 1;
-        c_reduce2 : c <= max_bound 0 - c;
+        c_reduce1 : c * (Z.ones (int_width - log_cap (pred (length base)))) < 2 ^ log_cap 0;
+        c_reduce2 : c < 2 ^ log_cap 0 - c;
         two_pow_k_le_2modulus : 2 ^ k <= 2 * modulus
       }.
 End with_base.
@@ -538,30 +554,26 @@ Section Canonicalization.
     (* allows caller to precompute k and c *)
     (k_ c_ : Z) (k_subst : k = k_) (c_subst : c = c_)
     {int_width} (preconditions : freezePreconditions prm int_width).
+  Local Notation digits := (tuple Z (length limb_widths)).
+
+  Definition encodeZ_opt := Eval compute in Pow2Base.encodeZ.
 
   Definition modulus_digits_opt_sig :
-    { b : digits | b = modulus_digits }.
+    { b : list Z | b = modulus_digits }.
   Proof.
     eexists.
-    cbv beta iota delta [modulus_digits modulus_digits' app].
-    change @max_bound with max_bound_opt.
-    rewrite c_subst.
-    change length with length_opt.
-    change minus with minus_opt.
-    change Z.add with Z_add_opt.
-    change Z.sub with Z_sub_opt.
-    change @Pow2Base.base_from_limb_widths with base_from_limb_widths_opt.
+    cbv beta iota delta [modulus_digits].
+    change Pow2Base.encodeZ with encodeZ_opt.
     reflexivity.
   Defined.
 
-  Definition modulus_digits_opt : digits
+  Definition modulus_digits_opt : list Z
     := Eval cbv [proj1_sig modulus_digits_opt_sig] in proj1_sig (modulus_digits_opt_sig).
 
   Definition modulus_digits_opt_correct
     : modulus_digits_opt = modulus_digits
     := proj2_sig (modulus_digits_opt_sig).
 
-
   Definition carry_full_3_opt_cps_sig
              {T} (f : digits -> T)
              (us : digits)
@@ -587,20 +599,20 @@ Section Canonicalization.
     { b : digits | b = freeze us }.
   Proof.
     eexists.
-    cbv [freeze].
-    cbv [and_term].
+    cbv [freeze conditional_subtract_modulus].
+    rewrite <-from_list_default_eq with (d := 0%Z).
+    change (@from_list_default Z) with (@from_list_default_opt Z).
     let LHS := match goal with |- ?LHS = ?RHS => LHS end in
     let RHS := match goal with |- ?LHS = ?RHS => RHS end in
-    let RHSf := match (eval pattern (isFull (carry_full (carry_full (carry_full us)))) in RHS) with ?RHSf _ => RHSf end in
-    change (LHS = Let_In (isFull(carry_full (carry_full (carry_full us)))) RHSf).
+    let RHSf := match (eval pattern (to_list (length limb_widths) (carry_full (carry_full (carry_full us)))) in RHS) with ?RHSf _ => RHSf end in
+    change (LHS = Let_In (to_list (length limb_widths)  (carry_full (carry_full (carry_full us)))) RHSf).
     let LHS := match goal with |- ?LHS = ?RHS => LHS end in
     let RHS := match goal with |- ?LHS = ?RHS => RHS end in
     let RHSf := match (eval pattern (carry_full (carry_full (carry_full us))) in RHS) with ?RHSf _ => RHSf end in
     rewrite <-carry_full_3_opt_cps_correct with (f := RHSf).
-    cbv beta iota delta [and_term isFull isFull'].
+    cbv beta iota delta [ge_modulus ge_modulus'].
     change length with length_opt.
-    change @max_bound with max_bound_opt.
-    rewrite c_subst.
+    change (nth_default 0 modulus_digits) with (nth_default_opt 0 modulus_digits_opt).
     change @max_ones with max_ones_opt.
     change @Pow2Base.base_from_limb_widths with base_from_limb_widths_opt.
     change minus with minus_opt.
@@ -616,7 +628,7 @@ Section Canonicalization.
   Definition freeze_opt_correct us
     : freeze_opt us = freeze us
     := proj2_sig (freeze_opt_sig us).
-
+(*
   Lemma freeze_opt_canonical: forall us vs x,
     @pre_carry_bounds _ _ int_width us -> rep us x ->
     @pre_carry_bounds _ _ int_width vs -> rep vs x ->
@@ -643,5 +655,5 @@ Section Canonicalization.
     split; eauto using freeze_opt_canonical.
     auto using freeze_opt_preserves_rep.
   Qed.
-
-End Canonicalization.
+*)
+End Canonicalization.
\ No newline at end of file
diff --git a/src/Specific/GF1305.v b/src/Specific/GF1305.v
index 077c98954..9e9b69dbd 100644
--- a/src/Specific/GF1305.v
+++ b/src/Specific/GF1305.v
@@ -1,13 +1,14 @@
-Require Import Crypto.ModularArithmetic.ModularBaseSystem.
+Require Import Crypto.BaseSystem.
+Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
 Require Import Crypto.ModularArithmetic.ModularBaseSystemOpt.
 Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParams.
 Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParamProofs.
+Require Import Crypto.ModularArithmetic.ModularBaseSystem.
+Require Import Crypto.ModularArithmetic.ModularBaseSystemProofs.
 Require Import Coq.Lists.List Crypto.Util.ListUtil.
-Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
-Require Import Crypto.ModularArithmetic.ModularBaseSystemInterface.
 Require Import Crypto.Tactics.VerdiTactics.
-Require Import Crypto.BaseSystem.
 Require Import Crypto.Util.ZUtil.
+Require Import Crypto.Util.Tuple.
 Require Import Crypto.Util.Notations.
 Require Import Crypto.Algebra.
 Import ListNotations.
@@ -26,12 +27,13 @@ Instance params1305 : PseudoMersenneBaseParams modulus.
   construct_params prime_modulus 5%nat 130.
 Defined.
 
-Definition mul2modulus := Eval compute in (construct_mul2modulus params1305).
+Definition fe1305 := Eval compute in (tuple Z (length limb_widths)).
+
+Definition mul2modulus : fe1305 :=
+  Eval compute in (from_list_default 0%Z (length limb_widths) (construct_mul2modulus params1305)).
 
 Instance subCoeff : SubtractionCoefficient modulus params1305.
   apply Build_SubtractionCoefficient with (coeff := mul2modulus).
-  cbv; auto.
-  cbv [ModularBaseSystem.decode].
   apply ZToField_eqmod.
   cbv; reflexivity.
 Defined.
@@ -49,9 +51,7 @@ Definition c_ := Eval compute in c.
 Definition k_subst : k = k_ := eq_refl k_.
 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 phi.
+Local Opaque Z.shiftr Z.shiftl Z.land Z.mul Z.add Z.sub Let_In.
 
 Definition app_5 (f : fe1305) (P : fe1305 -> fe1305) : fe1305.
 Proof.
@@ -80,7 +80,7 @@ Proof.
 Qed.
 
 Definition add_sig (f g : fe1305) :
-  { fg : fe1305 | fg = ModularBaseSystemInterface.add f g}.
+  { fg : fe1305 | fg = ModularBaseSystem.add f g}.
 Proof.
   eexists.
   rewrite <-appify2_correct. (* Coq 8.4 : 6s *)
@@ -93,12 +93,12 @@ Definition add (f g : fe1305) : fe1305 :=
   proj1_sig (add_sig f g).
 
 Definition add_correct (f g : fe1305)
-  : add f g = ModularBaseSystemInterface.add f g :=
+  : add f g = ModularBaseSystem.add f g :=
   Eval cbv beta iota delta [proj1_sig add_sig] in
   proj2_sig (add_sig f g). (* Coq 8.4 : 10s *)
 
 Definition sub_sig (f g : fe1305) :
-  { fg : fe1305 | fg = ModularBaseSystemInterface.sub f g}.
+  { fg : fe1305 | fg = ModularBaseSystem.sub mul2modulus f g}.
 Proof.
   eexists.
   rewrite <-appify2_correct.
@@ -111,16 +111,19 @@ Definition sub (f g : fe1305) : fe1305 :=
   proj1_sig (sub_sig f g).
 
 Definition sub_correct (f g : fe1305)
-  : sub f g = ModularBaseSystemInterface.sub f g :=
+  : sub f g = ModularBaseSystem.sub mul2modulus f g :=
   Eval cbv beta iota delta [proj1_sig sub_sig] in
   proj2_sig (sub_sig f g). (* Coq 8.4 : 10s *)
 
+(* For multiplication, we add another layer of definition so that we can
+   rewrite under the [let] binders. *)
 Definition mul_simpl_sig (f g : fe1305) :
-  { fg : fe1305 | fg = ModularBaseSystemInterface.mul (k_ := k_) (c_ := c_) f g}.
+  { fg : fe1305 | fg = ModularBaseSystem.mul f g}.
 Proof.
   cbv [fe1305] in *.
   repeat match goal with p : (_ * Z)%type |- _ => destruct p end.
   eexists.
+  rewrite <-mul_opt_correct with (k_ := k_) (c_ := c_) by auto.
   cbv.
   autorewrite with zsimplify.
   reflexivity.
@@ -131,18 +134,17 @@ Definition mul_simpl (f g : fe1305) : fe1305 :=
   proj1_sig (mul_simpl_sig f g).
 
 Definition mul_simpl_correct (f g : fe1305)
-  : mul_simpl f g = ModularBaseSystemInterface.mul (k_ := k_) (c_ := c_) f g :=
+  : mul_simpl f g = ModularBaseSystem.mul f g :=
   Eval cbv beta iota delta [proj1_sig mul_simpl_sig] in
   proj2_sig (mul_simpl_sig f g).
 
 Definition mul_sig (f g : fe1305) :
-  { fg : fe1305 | fg = ModularBaseSystemInterface.mul (k_ := k_) (c_ := c_) f g}.
+  { fg : fe1305 | fg = ModularBaseSystem.mul f g}.
 Proof.
   eexists.
   rewrite <-mul_simpl_correct.
   rewrite <-appify2_correct.
   cbv.
-  autorewrite with zsimplify.
   reflexivity.
 Defined. (* Coq 8.4 : 14s *)
 
@@ -151,25 +153,45 @@ Definition mul (f g : fe1305) : fe1305 :=
   proj1_sig (mul_sig f g).
 
 Definition mul_correct (f g : fe1305)
-  : mul f g = ModularBaseSystemInterface.mul (k_ := k_) (c_ := c_) f g :=
+  : mul f g = ModularBaseSystem.mul f g :=
   Eval cbv beta iota delta [proj1_sig add_sig] in
   proj2_sig (mul_sig f g). (* Coq 8.4 : 5s *)
 
+Definition decode := Eval compute in ModularBaseSystem.decode.
+
 Import Morphisms.
 
-Lemma field1305 : @field fe eq zero one opp add sub mul inv div.
+Lemma field1305 : @field fe1305 eq zero one opp add sub mul inv div.
 Proof.
   pose proof (Equivalence_Reflexive : Reflexive eq).
-  eapply (Field.equivalent_operations_field (fieldR := modular_base_system_field k_subst c_subst)).
+  eapply (Field.isomorphism_to_subfield_field (phi := decode)
+    (fieldR := PrimeFieldTheorems.field_modulo (prime_q := prime_modulus))).
   Grab Existential Variables.
-  + reflexivity.
-  + reflexivity.
-  + reflexivity.
-  + intros; rewrite mul_correct; reflexivity.
-  + intros; rewrite sub_correct; reflexivity.
-  + intros; rewrite add_correct; reflexivity.
-  + reflexivity.
-  + reflexivity.
+  + intros; change decode with ModularBaseSystem.decode; apply encode_rep.
+  + intros; change decode with ModularBaseSystem.decode; apply encode_rep.
+  + intros; change decode with ModularBaseSystem.decode; apply encode_rep.
+  + intros; change decode with ModularBaseSystem.decode; apply encode_rep.
+  + intros; change decode with ModularBaseSystem.decode.
+    rewrite mul_correct; apply mul_rep; reflexivity.
+  + intros; change decode with ModularBaseSystem.decode.
+    rewrite sub_correct; apply sub_rep; try reflexivity.
+    rewrite <- coeff_mod. reflexivity.
+  + intros; change decode with ModularBaseSystem.decode.
+    rewrite add_correct; apply add_rep; reflexivity.
+  + intros; change decode with ModularBaseSystem.decode; apply encode_rep.
+  + cbv [eq zero one]. change decode with ModularBaseSystem.decode.
+    rewrite !encode_rep. intro A.
+    eapply (PrimeFieldTheorems.Fq_1_neq_0 (prime_q := prime_modulus)). congruence.
+  + trivial.
+  + repeat intro. cbv [div]. congruence.
+  + repeat intro. cbv [inv]. congruence.
+  + repeat intro. cbv [eq] in *. rewrite !mul_correct, !mul_rep by reflexivity; congruence.
+  + repeat intro. cbv [eq] in *. rewrite !sub_correct. rewrite !sub_rep by
+      (rewrite <-?coeff_mod; reflexivity); congruence.
+  + repeat intro. cbv [eq] in *. rewrite !add_correct, !add_rep by reflexivity; congruence.
+  + repeat intro. cbv [opp]. congruence.
+  + cbv [eq]. auto using ModularArithmeticTheorems.F_eq_dec.
+  + apply (eq_Equivalence (prm := params1305)).
 Qed.
 
 (*
diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v
index 6298941db..2f1da1846 100644
--- a/src/Specific/GF25519.v
+++ b/src/Specific/GF25519.v
@@ -1,16 +1,18 @@
-Require Import Crypto.ModularArithmetic.ModularBaseSystem.
+Require Import Crypto.BaseSystem.
+Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
 Require Import Crypto.ModularArithmetic.ModularBaseSystemOpt.
 Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParams.
 Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParamProofs.
+Require Import Crypto.ModularArithmetic.ModularBaseSystem.
+Require Import Crypto.ModularArithmetic.ModularBaseSystemProofs.
 Require Import Coq.Lists.List Crypto.Util.ListUtil.
-Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
-Require Import Crypto.ModularArithmetic.ModularBaseSystemInterface.
 Require Import Crypto.Tactics.VerdiTactics.
-Require Import Crypto.BaseSystem.
-Require Import Algebra.
+Require Import Crypto.Util.ZUtil.
+Require Import Crypto.Util.Tuple.
+Require Import Crypto.Util.Notations.
+Require Import Crypto.Algebra.
 Import ListNotations.
 Require Import Coq.ZArith.ZArith Coq.ZArith.Zpower Coq.ZArith.ZArith Coq.ZArith.Znumtheory.
-Require Import Crypto.Util.Notations.
 Local Open Scope Z.
 
 (* BEGIN PseudoMersenneBaseParams instance construction. *)
@@ -23,12 +25,13 @@ Instance params25519 : PseudoMersenneBaseParams modulus.
   construct_params prime_modulus 10%nat 255.
 Defined.
 
-Definition mul2modulus := Eval compute in (construct_mul2modulus params25519).
+Definition fe25519 := Eval compute in (tuple Z (length limb_widths)).
+
+Definition mul2modulus := 
+  Eval compute in (from_list_default 0%Z (length limb_widths) (construct_mul2modulus params25519)).
 
 Instance subCoeff : SubtractionCoefficient modulus params25519.
   apply Build_SubtractionCoefficient with (coeff := mul2modulus).
-  cbv; auto.
-  cbv [ModularBaseSystem.decode].
   apply ZToField_eqmod.
   cbv; reflexivity.
 Defined.
@@ -45,7 +48,6 @@ 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.
 
 Local Opaque Z.shiftr Z.shiftl Z.land Z.mul Z.add Z.sub Let_In.
 
@@ -76,7 +78,7 @@ Proof.
 Qed.
 
 Definition add_sig (f g : fe25519) :
-  { fg : fe25519 | fg = ModularBaseSystemInterface.add f g}.
+  { fg : fe25519 | fg = ModularBaseSystem.add f g}.
 Proof.
   eexists.
   rewrite <-appify2_correct.
@@ -89,12 +91,12 @@ Definition add (f g : fe25519) : fe25519 :=
   proj1_sig (add_sig f g).
 
 Definition add_correct (f g : fe25519)
-  : add f g = ModularBaseSystemInterface.add f g :=
+  : add f g = ModularBaseSystem.add f g :=
   Eval cbv beta iota delta [proj1_sig add_sig] in
-  proj2_sig (add_sig f g).
+  proj2_sig (add_sig f g). (* Coq 8.4 : 10s *)
 
 Definition sub_sig (f g : fe25519) :
-  { fg : fe25519 | fg = ModularBaseSystemInterface.sub f g}.
+  { fg : fe25519 | fg = ModularBaseSystem.sub mul2modulus f g}.
 Proof.
   eexists.
   rewrite <-appify2_correct.
@@ -107,16 +109,19 @@ Definition sub (f g : fe25519) : fe25519 :=
   proj1_sig (sub_sig f g).
 
 Definition sub_correct (f g : fe25519)
-  : sub f g = ModularBaseSystemInterface.sub f g :=
+  : sub f g = ModularBaseSystem.sub mul2modulus f g :=
   Eval cbv beta iota delta [proj1_sig sub_sig] in
   proj2_sig (sub_sig f g).
 
+(* For multiplication, we add another layer of definition so that we can
+   rewrite under the [let] binders. *)
 Definition mul_simpl_sig (f g : fe25519) :
-  { fg : fe25519 | fg = ModularBaseSystemInterface.mul (k_ := k_) (c_ := c_) f g}.
+  { fg : fe25519 | fg = ModularBaseSystem.mul f g}.
 Proof.
   cbv [fe25519] in *.
   repeat match goal with p : (_ * Z)%type |- _ => destruct p end.
   eexists.
+  rewrite <-mul_opt_correct with (k_ := k_) (c_ := c_) by auto.
   cbv.
   autorewrite with zsimplify.
   reflexivity.
@@ -127,15 +132,15 @@ Definition mul_simpl (f g : fe25519) : fe25519 :=
   proj1_sig (mul_simpl_sig f g).
 
 Definition mul_simpl_correct (f g : fe25519)
-  : mul_simpl f g = ModularBaseSystemInterface.mul (k_ := k_) (c_ := c_) f g :=
+  : mul_simpl f g = ModularBaseSystem.mul f g :=
   Eval cbv beta iota delta [proj1_sig mul_simpl_sig] in
   proj2_sig (mul_simpl_sig f g).
 
 Definition mul_sig (f g : fe25519) :
-  { fg : fe25519 | fg = ModularBaseSystemInterface.mul (k_ := k_) (c_ := c_) f g}.
+  { fg : fe25519 | fg = ModularBaseSystem.mul f g}.
 Proof.
   eexists.
-  rewrite <- mul_simpl_correct.
+  rewrite <-mul_simpl_correct.
   rewrite <-appify2_correct.
   cbv.
   reflexivity.
@@ -146,25 +151,45 @@ Definition mul (f g : fe25519) : fe25519 :=
   proj1_sig (mul_sig f g).
 
 Definition mul_correct (f g : fe25519)
-  : mul f g = ModularBaseSystemInterface.mul (k_ := k_) (c_ := c_) f g :=
-  Eval cbv beta iota delta [proj1_sig mul_sig] in
+  : mul f g = ModularBaseSystem.mul f g :=
+  Eval cbv beta iota delta [proj1_sig add_sig] in
   proj2_sig (mul_sig f g).
 
+Definition decode := Eval compute in ModularBaseSystem.decode.
+
 Import Morphisms.
 
 Lemma field25519 : @field fe25519 eq zero one opp add sub mul inv div.
 Proof.
   pose proof (Equivalence_Reflexive : Reflexive eq).
-  eapply (Field.equivalent_operations_field (fieldR := modular_base_system_field k_subst c_subst)).
+  eapply (Field.isomorphism_to_subfield_field (phi := decode)
+    (fieldR := PrimeFieldTheorems.field_modulo (prime_q := prime_modulus))).
   Grab Existential Variables.
-  + reflexivity.
-  + reflexivity.
-  + reflexivity.
-  + intros; rewrite mul_correct; reflexivity.
-  + intros; rewrite sub_correct; reflexivity.
-  + intros; rewrite add_correct; reflexivity.
-  + reflexivity.
-  + reflexivity.
+  + intros; change decode with ModularBaseSystem.decode; apply encode_rep.
+  + intros; change decode with ModularBaseSystem.decode; apply encode_rep.
+  + intros; change decode with ModularBaseSystem.decode; apply encode_rep.
+  + intros; change decode with ModularBaseSystem.decode; apply encode_rep.
+  + intros; change decode with ModularBaseSystem.decode.
+    rewrite mul_correct; apply mul_rep; reflexivity.
+  + intros; change decode with ModularBaseSystem.decode.
+    rewrite sub_correct; apply sub_rep; try reflexivity.
+    rewrite <- coeff_mod. reflexivity.
+  + intros; change decode with ModularBaseSystem.decode.
+    rewrite add_correct; apply add_rep; reflexivity.
+  + intros; change decode with ModularBaseSystem.decode; apply encode_rep.
+  + cbv [eq zero one]. change decode with ModularBaseSystem.decode.
+    rewrite !encode_rep. intro A.
+    eapply (PrimeFieldTheorems.Fq_1_neq_0 (prime_q := prime_modulus)). congruence.
+  + trivial.
+  + repeat intro. cbv [div]. congruence.
+  + repeat intro. cbv [inv]. congruence.
+  + repeat intro. cbv [eq] in *. rewrite !mul_correct, !mul_rep by reflexivity; congruence.
+  + repeat intro. cbv [eq] in *. rewrite !sub_correct. rewrite !sub_rep by
+      (rewrite <-?coeff_mod; reflexivity); congruence.
+  + repeat intro. cbv [eq] in *. rewrite !add_correct, !add_rep by reflexivity; congruence.
+  + repeat intro. cbv [opp]. congruence.
+  + cbv [eq]. auto using ModularArithmeticTheorems.F_eq_dec.
+  + apply (eq_Equivalence (prm := params25519)).
 Qed.
 
 
-- 
cgit v1.2.3