re-introduced extra field isomorphism layer for 8.4 compatibility and better organization of reasoning.

5 files changed, 130 insertions, 91 deletions

diff --git a/src/ModularArithmetic/ModularBaseSystemField.v b/src/ModularArithmetic/ModularBaseSystemField.v
new file mode 100644
index 000000000..f5bedd644
--- /dev/null
+++ b/src/ModularArithmetic/ModularBaseSystemField.v
@@ -0,0 +1,71 @@
+Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
+Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParams.
+Require Import Crypto.ModularArithmetic.ModularBaseSystem.
+Require Import Crypto.ModularArithmetic.ModularBaseSystemProofs.
+Require Import Crypto.ModularArithmetic.ModularBaseSystemOpt.
+Require Import Coq.ZArith.ZArith.
+Require Import Crypto.Algebra. Import Field.
+Require Import Crypto.Util.Tuple Crypto.Util.Notations.
+Local Open Scope Z_scope.
+
+Section ModularBaseSystemField.
+  Context `{prm : PseudoMersenneBaseParams} {sc : SubtractionCoefficient modulus prm}
+    (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)).
+
+  Lemma add_decode : forall a b : digits,
+    decode (add_opt a b) = (decode a + decode b)%F.
+  Proof.
+    intros; rewrite add_opt_correct by assumption.
+    apply add_rep; apply decode_rep.
+  Qed.
+
+  Lemma sub_decode : forall a b : digits,
+    decode (sub_opt a b) = (decode a - decode b)%F.
+  Proof.
+    intros; rewrite sub_opt_correct by assumption.
+    apply sub_rep; auto using coeff_mod, decode_rep.
+  Qed.
+
+  Lemma mul_decode : forall a b : digits,
+    decode (carry_mul_opt k_ c_ a b) = (decode a * decode b)%F.
+  Proof.
+    intros; rewrite carry_mul_opt_correct by assumption.
+    apply carry_mul_rep; apply decode_rep.
+  Qed.
+
+  Lemma zero_neq_one : eq zero one -> False.
+  Proof.
+   cbv [eq zero one]. erewrite !encode_rep. intro A.
+   eapply (PrimeFieldTheorems.Fq_1_neq_0 (prime_q := prime_modulus)).
+   congruence.
+  Qed.
+
+  Lemma modular_base_system_field :
+    @field digits eq zero one opp add_opt sub_opt (carry_mul_opt k_ c_) inv div.
+  Proof.
+    eapply (Field.isomorphism_to_subfield_field (phi := decode) (fieldR := PrimeFieldTheorems.field_modulo  (prime_q := prime_modulus))).
+    Grab Existential Variables.
+    + intros; eapply encode_rep.
+    + intros; eapply encode_rep.
+    + intros; eapply encode_rep.
+    + intros; eapply encode_rep.
+    + intros; eapply mul_decode.
+    + intros; eapply sub_decode.
+    + intros; eapply add_decode.
+    + intros; eapply encode_rep.
+    + cbv [eq zero one]. erewrite !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]. erewrite !mul_decode. congruence.
+    + repeat intro. cbv [eq]. erewrite !sub_decode. congruence.
+    + repeat intro. cbv [eq]. erewrite !add_decode. congruence.
+    + repeat intro. cbv [opp]. congruence.
+    + cbv [eq]. auto using ModularArithmeticTheorems.F_eq_dec.
+  Qed.
+
+End ModularBaseSystemField.
\ No newline at end of file
diff --git a/src/ModularArithmetic/ModularBaseSystemOpt.v b/src/ModularArithmetic/ModularBaseSystemOpt.v
index d1a6f6228..4543ff67d 100644
--- a/src/ModularArithmetic/ModularBaseSystemOpt.v
+++ b/src/ModularArithmetic/ModularBaseSystemOpt.v
@@ -528,6 +528,13 @@ Section Multiplication.
   Definition carry_mul_opt_cps_correct {T} (f:digits -> T) (us vs : digits)
     : carry_mul_opt_cps f us vs = f (carry_mul us vs)
     := proj2_sig (carry_mul_opt_sig f us vs).
+
+  Definition carry_mul_opt := carry_mul_opt_cps id.
+
+  Definition carry_mul_opt_correct (us vs : digits)
+    : carry_mul_opt us vs = carry_mul us vs :=
+    carry_mul_opt_cps_correct id us vs.
+
 End Multiplication.
 
 Section with_base.
diff --git a/src/ModularArithmetic/Pow2Base.v b/src/ModularArithmetic/Pow2Base.v
index acc96ad73..c23cf8f40 100644
--- a/src/ModularArithmetic/Pow2Base.v
+++ b/src/ModularArithmetic/Pow2Base.v
@@ -39,7 +39,6 @@ Section Pow2Base.
        encode' z i' ++ (Z.shiftr (Z.land z (Z.ones (lw i))) (lw i')) :: nil
     end.
 
-  (* max must be greater than input; this is used to truncate last digit *)
   Definition encodeZ x:= encode' x (length limb_widths).
 
   (** ** Carrying *)
diff --git a/src/Specific/GF1305.v b/src/Specific/GF1305.v
index 9e9b69dbd..c30485f5e 100644
--- a/src/Specific/GF1305.v
+++ b/src/Specific/GF1305.v
@@ -1,10 +1,11 @@
 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 Crypto.ModularArithmetic.ModularBaseSystemOpt.
+Require Import Crypto.ModularArithmetic.ModularBaseSystemField.
 Require Import Coq.Lists.List Crypto.Util.ListUtil.
 Require Import Crypto.Tactics.VerdiTactics.
 Require Import Crypto.Util.ZUtil.
@@ -80,25 +81,25 @@ Proof.
 Qed.
 
 Definition add_sig (f g : fe1305) :
-  { fg : fe1305 | fg = ModularBaseSystem.add f g}.
+  { fg : fe1305 | fg = add_opt f g}.
 Proof.
   eexists.
-  rewrite <-appify2_correct. (* Coq 8.4 : 6s *)
+  rewrite <-appify2_correct.
   cbv.
   reflexivity.
-Defined. (* Coq 8.4 : 7s *)
+Defined.
 
 Definition add (f g : fe1305) : fe1305 :=
   Eval cbv beta iota delta [proj1_sig add_sig] in
   proj1_sig (add_sig f g).
 
 Definition add_correct (f g : fe1305)
-  : add f g = ModularBaseSystem.add f g :=
+  : add f g = add_opt f g :=
   Eval cbv beta iota delta [proj1_sig add_sig] in
-  proj2_sig (add_sig f g). (* Coq 8.4 : 10s *)
+  proj2_sig (add_sig f g).
 
 Definition sub_sig (f g : fe1305) :
-  { fg : fe1305 | fg = ModularBaseSystem.sub mul2modulus f g}.
+  { fg : fe1305 | fg = sub_opt f g}.
 Proof.
   eexists.
   rewrite <-appify2_correct.
@@ -111,19 +112,18 @@ Definition sub (f g : fe1305) : fe1305 :=
   proj1_sig (sub_sig f g).
 
 Definition sub_correct (f g : fe1305)
-  : sub f g = ModularBaseSystem.sub mul2modulus f g :=
+  : sub f g = sub_opt f g :=
   Eval cbv beta iota delta [proj1_sig sub_sig] in
-  proj2_sig (sub_sig f g). (* Coq 8.4 : 10s *)
+  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 : fe1305) :
-  { fg : fe1305 | fg = ModularBaseSystem.mul f g}.
+  { fg : fe1305 | fg = carry_mul_opt k_ c_ 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.
@@ -134,64 +134,46 @@ 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 = ModularBaseSystem.mul f g :=
+  : mul_simpl f g = carry_mul_opt k_ c_ 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 = ModularBaseSystem.mul f g}.
+  { fg : fe1305 | fg = carry_mul_opt k_ c_ f g}.
 Proof.
   eexists.
   rewrite <-mul_simpl_correct.
   rewrite <-appify2_correct.
   cbv.
   reflexivity.
-Defined. (* Coq 8.4 : 14s *)
+Defined.
 
 Definition mul (f g : fe1305) : fe1305 :=
   Eval cbv beta iota delta [proj1_sig mul_sig] in
   proj1_sig (mul_sig f g).
 
+Print mul.
+
 Definition mul_correct (f g : fe1305)
-  : mul f g = ModularBaseSystem.mul f g :=
+  : mul f g = carry_mul_opt k_ c_ 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.
+  proj2_sig (mul_sig f g).
 
 Import Morphisms.
 
 Lemma field1305 : @field fe1305 eq zero one opp add sub mul inv div.
 Proof.
   pose proof (Equivalence_Reflexive : Reflexive eq).
-  eapply (Field.isomorphism_to_subfield_field (phi := decode)
-    (fieldR := PrimeFieldTheorems.field_modulo (prime_q := prime_modulus))).
+  eapply (Field.equivalent_operations_field (fieldR := modular_base_system_field k_ c_ k_subst c_subst)).
   Grab Existential Variables.
-  + 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)).
+  + reflexivity.
+  + reflexivity.
+  + reflexivity.
+  + intros; rewrite mul_correct. reflexivity.
+  + intros; rewrite sub_correct; reflexivity.
+  + intros; rewrite add_correct; reflexivity.
+  + reflexivity.
+  + reflexivity.
 Qed.
 
 (*
diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v
index 2f1da1846..7ece3a5da 100644
--- a/src/Specific/GF25519.v
+++ b/src/Specific/GF25519.v
@@ -1,10 +1,11 @@
 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 Crypto.ModularArithmetic.ModularBaseSystemOpt.
+Require Import Crypto.ModularArithmetic.ModularBaseSystemField.
 Require Import Coq.Lists.List Crypto.Util.ListUtil.
 Require Import Crypto.Tactics.VerdiTactics.
 Require Import Crypto.Util.ZUtil.
@@ -27,7 +28,7 @@ Defined.
 
 Definition fe25519 := Eval compute in (tuple Z (length limb_widths)).
 
-Definition mul2modulus := 
+Definition mul2modulus : fe25519 :=
   Eval compute in (from_list_default 0%Z (length limb_widths) (construct_mul2modulus params25519)).
 
 Instance subCoeff : SubtractionCoefficient modulus params25519.
@@ -51,7 +52,7 @@ Definition c_subst : c = c_ := eq_refl c_.
 
 Local Opaque Z.shiftr Z.shiftl Z.land Z.mul Z.add Z.sub Let_In.
 
-Definition app_10 (f : fe25519) (P : fe25519 -> fe25519) : fe25519.
+Definition app_5 (f : fe25519) (P : fe25519 -> fe25519) : fe25519.
 Proof.
   cbv [fe25519] in *.
   set (f0 := f).
@@ -60,7 +61,7 @@ Proof.
   apply f0.
 Defined.
 
-Lemma app_10_correct : forall f P, app_10 f P = P f.
+Definition app_5_correct f (P : fe25519 -> fe25519) : app_5 f P = P f.
 Proof.
   intros.
   cbv [fe25519] in *.
@@ -69,16 +70,16 @@ Proof.
 Qed.
 
 Definition appify2 (op : fe25519 -> fe25519 -> fe25519) (f g : fe25519):= 
-  app_10 f (fun f0 => (app_10 g (fun g0 => op f0 g0))).
+  app_5 f (fun f0 => (app_5 g (fun g0 => op f0 g0))).
 
 Lemma appify2_correct : forall op f g, appify2 op f g = op f g.
 Proof.
   intros. cbv [appify2].
-  etransitivity; apply app_10_correct.
+  etransitivity; apply app_5_correct.
 Qed.
 
 Definition add_sig (f g : fe25519) :
-  { fg : fe25519 | fg = ModularBaseSystem.add f g}.
+  { fg : fe25519 | fg = add_opt f g}.
 Proof.
   eexists.
   rewrite <-appify2_correct.
@@ -91,12 +92,12 @@ Definition add (f g : fe25519) : fe25519 :=
   proj1_sig (add_sig f g).
 
 Definition add_correct (f g : fe25519)
-  : add f g = ModularBaseSystem.add f g :=
+  : add f g = add_opt f g :=
   Eval cbv beta iota delta [proj1_sig add_sig] in
-  proj2_sig (add_sig f g). (* Coq 8.4 : 10s *)
+  proj2_sig (add_sig f g).
 
 Definition sub_sig (f g : fe25519) :
-  { fg : fe25519 | fg = ModularBaseSystem.sub mul2modulus f g}.
+  { fg : fe25519 | fg = sub_opt f g}.
 Proof.
   eexists.
   rewrite <-appify2_correct.
@@ -109,19 +110,18 @@ Definition sub (f g : fe25519) : fe25519 :=
   proj1_sig (sub_sig f g).
 
 Definition sub_correct (f g : fe25519)
-  : sub f g = ModularBaseSystem.sub mul2modulus f g :=
+  : sub f g = sub_opt 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 = ModularBaseSystem.mul f g}.
+  { fg : fe25519 | fg = carry_mul_opt k_ c_ 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.
@@ -132,12 +132,12 @@ 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 = ModularBaseSystem.mul f g :=
+  : mul_simpl f g = carry_mul_opt k_ c_ 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 = ModularBaseSystem.mul f g}.
+  { fg : fe25519 | fg = carry_mul_opt k_ c_ f g}.
 Proof.
   eexists.
   rewrite <-mul_simpl_correct.
@@ -151,45 +151,25 @@ Definition mul (f g : fe25519) : fe25519 :=
   proj1_sig (mul_sig f g).
 
 Definition mul_correct (f g : fe25519)
-  : mul f g = ModularBaseSystem.mul f g :=
+  : mul f g = carry_mul_opt k_ c_ 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.isomorphism_to_subfield_field (phi := decode)
-    (fieldR := PrimeFieldTheorems.field_modulo (prime_q := prime_modulus))).
+  eapply (Field.equivalent_operations_field (fieldR := modular_base_system_field k_ c_ k_subst c_subst)).
   Grab Existential Variables.
-  + 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)).
+  + reflexivity.
+  + reflexivity.
+  + reflexivity.
+  + intros; rewrite mul_correct. reflexivity.
+  + intros; rewrite sub_correct; reflexivity.
+  + intros; rewrite add_correct; reflexivity.
+  + reflexivity.
+  + reflexivity.
 Qed.