fresh take at specifications using implicit arguments instead of module parameters

2 files changed, 109 insertions, 0 deletions

diff --git a/src/Spec/CompleteEwardsCurve.v b/src/Spec/CompleteEwardsCurve.v
new file mode 100644
index 000000000..7ebf35988
--- /dev/null
+++ b/src/Spec/CompleteEwardsCurve.v
@@ -0,0 +1,49 @@
+Require BinInt Znumtheory.
+
+Require Crypto.CompleteEwardsCurve.Pre.
+
+Require Import Crypto.Spec.ModularArithmetic.
+Local Open Scope F_scope.
+
+Class TwistedEdwardsParams := {
+  p : BinInt.Z;
+  a : F p;
+  d : F p;
+  modulus_prime : Znumtheory.prime p;
+  a_nonzero : a <> 0;
+  a_square : exists sqrt_a, sqrt_a^2 = a;
+  d_nonsquare : forall x, x^2 <> d
+}.
+
+Section TwistedEdwardsCurves.
+  Context `{prm:TwistedEdwardsParams}.
+  (* Twisted Edwards curves with complete addition laws. References:
+  * <https://eprint.iacr.org/2008/013.pdf>
+  * <http://ed25519.cr.yp.to/ed25519-20110926.pdf>
+  * <https://eprint.iacr.org/2015/677.pdf>
+  *)
+  Definition onCurve P := let '(x,y) := P in a*x^2 + y^2 = 1 + d*x^2*y^2.
+  Definition point := { P | onCurve P}.
+  Definition mkPoint xy proof : point := exist onCurve xy proof.
+  Definition projX (P:point) : F p := fst (proj1_sig P).
+  Definition projY (P:point) : F p:= snd (proj1_sig P).
+
+  Definition zero : point := mkPoint (0, 1) Pre.zeroOnCurve.
+  
+  (* NOTE: the two matches on P1 can probably be merged, not sure whether good idea... *)
+  Definition unifiedAdd (P1 P2 : point) : point :=
+    let 'exist P1' pf1 := P1 in
+    let 'exist P2' pf2 := P2 in
+    mkPoint
+      ( let '(x1, y1) := P1' in
+        let '(x2, y2) := P2' in
+        (((x1*y2  +  y1*x2)/(1 + d*x1*x2*y1*y2)) , ((y1*y2 - a*x1*x2)/(1 - d*x1*x2*y1*y2))))
+      (Pre.unifiedAdd'_onCurve _ _ pf1 pf2).
+  Local Infix "+" := unifiedAdd.
+
+  Fixpoint scalarMult (n:nat) (P : point) : point :=
+    match n with
+    | O => zero
+    | S n' => P + scalarMult n' P
+    end.
+End TwistedEdwardsCurves.
\ No newline at end of file
diff --git a/src/Spec/ModularArithmetic.v b/src/Spec/ModularArithmetic.v
new file mode 100644
index 000000000..7f31161e2
--- /dev/null
+++ b/src/Spec/ModularArithmetic.v
@@ -0,0 +1,60 @@
+Require Znumtheory BinInt BinNums.
+
+Require Crypto.ModularArithmetic.Pre.
+
+Delimit Scope N_scope with N.
+Infix "+" := BinNat.N.add : N_scope.
+Infix "*" := BinNat.N.mul : N_scope.
+Infix "-" := BinNat.N.sub : N_scope.
+Infix "/" := BinNat.N.div : N_scope.
+Infix "^" := BinNat.N.pow : N_scope.
+
+Delimit Scope Z_scope with Z.
+Infix "+" := BinInt.Z.add : Z_scope.
+Infix "*" := BinInt.Z.mul : Z_scope.
+Infix "-" := BinInt.Z.sub : Z_scope.
+Infix "/" := BinInt.Z.div : Z_scope.
+Infix "^" := BinInt.Z.pow : Z_scope.
+Infix "mod" := BinInt.Z.modulo (at level 40, no associativity) : Z_scope.
+Local Open Scope Z_scope.
+
+Definition F (modulus : BinInt.Z) := { z : BinInt.Z | z = z mod modulus }.
+Section FieldOperations.
+  Context {m : BinInt.Z}.
+
+  Let Fm := F m. (* TODO: if inlined, coercions say "anomaly please report" *)
+  Coercion ZToField (a:BinInt.Z) : Fm := exist _ (a mod m) (Pre.Z_mod_mod a m).
+  Coercion FieldToZ (a:Fm) : BinInt.Z := proj1_sig a.
+
+  Definition add (a b:Fm) : Fm := ZToField (a + b).
+  Definition mul (a b:Fm) : Fm := ZToField (a * b).
+
+  Parameter opp : Fm -> Fm. 
+  Axiom F_opp_spec : forall (a:Fm), add a (opp a) = 0 /\ opp a = opp a mod m.
+  Definition sub (a b:Fm) : Fm := add a (opp b).
+
+  Parameter inv : Fm -> Fm. 
+  Axiom F_inv_spec : forall (a:Fm), mul a (inv a) = 1 /\ inv 0 = 0 /\ inv a = inv a mod m.
+  Definition div (a b:Fm) : Fm := mul a (inv b).
+
+  Parameter pow : Fm -> BinNums.N ->  Fm. 
+  Axiom F_pow_spec : forall a, pow a 0%N = 1 /\ forall x y, pow a (x + y)%N = pow a x * pow a y.
+End FieldOperations.
+
+Delimit Scope F_scope with F.
+Arguments ZToField {_} _%Z : simpl never.
+Arguments add {_} _%F _%F : simpl never.
+Arguments mul {_} _%F _%F : simpl never.
+Arguments sub {_} _%F _%F : simpl never.
+Arguments div {_} _%F _%F : simpl never.
+Arguments pow {_} _%F _%N : simpl never.
+Arguments inv {_} _%F : simpl never.
+Arguments opp {_} _%F : simpl never.
+Local Open Scope F_scope.
+Infix "+" := add : F_scope.
+Infix "*" := mul : F_scope.
+Infix "-" := sub : F_scope.
+Infix "/" := div : F_scope.
+Infix "^" := pow : F_scope.
+Notation "0" := (ZToField 0) : F_scope.
+Notation "1" := (ZToField 1) : F_scope.