pushing through a tweak to the arguments of [sub], and defining a field over ModularBaseSystemInterface using some placeholder operations.

2 files changed, 28 insertions, 5 deletions

diff --git a/src/Specific/GF1305.v b/src/Specific/GF1305.v
index 2b917086b..e539eaa8d 100644
--- a/src/Specific/GF1305.v
+++ b/src/Specific/GF1305.v
@@ -2,13 +2,14 @@ Require Import Crypto.ModularArithmetic.ModularBaseSystem.
 Require Import Crypto.ModularArithmetic.ModularBaseSystemOpt.
 Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParams.
 Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParamProofs.
-Require Import Crypto.ModularArithmetic.ModularBaseSystemInterface.
 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.Notations.
+Require Import Crypto.Algebra.
 Import ListNotations.
 Require Import Coq.ZArith.ZArith Coq.ZArith.Zpower Coq.ZArith.ZArith Coq.ZArith.Znumtheory.
 Local Open Scope Z.
@@ -28,7 +29,11 @@ Defined.
 Definition mul2modulus := Eval compute in (construct_mul2modulus params1305).
 
 Instance subCoeff : SubtractionCoefficient modulus params1305.
-  apply Build_SubtractionCoefficient with (coeff := mul2modulus); cbv; auto.
+  apply Build_SubtractionCoefficient with (coeff := mul2modulus).
+  cbv; auto.
+  cbv [ModularBaseSystem.decode].
+  apply ZToField_eqmod.
+  cbv; reflexivity.
 Defined.
 
 Definition freezePreconditions1305 : freezePreconditions params1305 int_width.
@@ -48,7 +53,7 @@ Definition fe1305 : Type := Eval cbv in fe.
 
 Local Opaque Z.shiftr Z.shiftl Z.land Z.mul Z.add Z.sub Let_In phi.
 
-Definition add (f g:fe1305) : { fg | phi fg = @ModularArithmetic.add modulus (phi f) (phi g) }.
+Definition add_formula (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.
@@ -58,8 +63,21 @@ Proof.
   apply f_equal.
   reflexivity.
 Qed.
+Definition add f g := proj1_sig (add_formula f g).
+
+Definition sub_formula (f g:fe1305) : { fg | phi fg = @ModularArithmetic.sub modulus (phi f) (phi g) }.
+Proof.
+  cbv [fe1305] in *.
+  repeat match goal with [p : (_*Z)%type |- _ ] => destruct p end.
+  eexists.
+  rewrite <-sub_phi.
+  cbv.
+  apply f_equal.
+  reflexivity.
+Qed.
+Definition sub f g := proj1_sig (sub_formula f g).
 
-Definition mul (f g:fe1305) : { fg | phi fg = @ModularArithmetic.mul modulus (phi f) (phi g) }.
+Definition mul_formula (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.
@@ -71,6 +89,7 @@ Proof.
   repeat match goal with |- appcontext[?a * 1] => rewrite (Z.mul_1_r a) end.
   reflexivity.
 Qed.
+Definition mul f g := proj1_sig (mul_formula f g).
 
 (*
 Local Transparent Let_In.
diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v
index b668459bf..a361e7207 100644
--- a/src/Specific/GF25519.v
+++ b/src/Specific/GF25519.v
@@ -25,7 +25,11 @@ Defined.
 Definition mul2modulus := Eval compute in (construct_mul2modulus params25519).
 
 Instance subCoeff : SubtractionCoefficient modulus params25519.
-  apply Build_SubtractionCoefficient with (coeff := mul2modulus); cbv; auto.
+  apply Build_SubtractionCoefficient with (coeff := mul2modulus).
+  cbv; auto.
+  cbv [ModularBaseSystem.decode].
+  apply ZToField_eqmod.
+  cbv; reflexivity.
 Defined.
 
 Definition freezePreconditions25519 : freezePreconditions params25519 int_width.