PointFormats/EdDSA: scoping tweaks in PointFormats, small changes of phrasing in EdDSA to make proofs more convenient.

3 files changed, 29 insertions, 35 deletions

diff --git a/src/Curves/Curve25519.v b/src/Curves/Curve25519.v
index edcf6a24c..8bb2148db 100644
--- a/src/Curves/Curve25519.v
+++ b/src/Curves/Curve25519.v
@@ -10,6 +10,7 @@ End Modulus25519.
 
 Module Curve25519Params <: TwistedEdwardsParams Modulus25519 <: Minus1Params Modulus25519.
   Module Import GFDefs := GaloisDefs Modulus25519.
+  Local Open Scope GF_scope.
   Coercion inject : Z >-> GF.
 
   Definition a : GF := -1.
diff --git a/src/Curves/PointFormats.v b/src/Curves/PointFormats.v
index 2cf5d3665..1e8df9337 100644
--- a/src/Curves/PointFormats.v
+++ b/src/Curves/PointFormats.v
@@ -5,11 +5,11 @@ Require Import BinNums NArith.
 
 Module GaloisDefs (M : Modulus).
   Module Export GT := GaloisTheory M.
-  Open Scope GF_scope.
 End GaloisDefs.
 
 Module Type TwistedEdwardsParams (M : Modulus).
   Module Export GFDefs := GaloisDefs M.
+  Local Open Scope GF_scope.
   Parameter a : GF.
   Axiom a_nonzero : a <> 0.
   Axiom a_square : exists x, x * x = a.
@@ -54,7 +54,7 @@ Proof.
   case_eq (b - S i); intros; simpl; auto.
 Qed.
 
-Lemma iter_op_xI : forall {A} p i op z b (a : A), (i < S b) ->
+Lemma iter_op_step_xI : forall {A} p i op z b (a : A), (i < S b) ->
   iter_op op z (S b) p~1 i a = iter_op op z b p i a.
 Proof.
   induction i; intros; [pose proof (Gt.gt_irrefl 0); intuition | ].
@@ -64,7 +64,7 @@ Proof.
   rewrite IHi by omega; auto.
 Qed.
 
-Lemma iter_op_xO : forall {A} p i op z b (a : A), (i < S b) ->
+Lemma iter_op_step_xO : forall {A} p i op z b (a : A), (i < S b) ->
   iter_op op z (S b) p~0 i a = iter_op op z b p i a.
 Proof.
   induction i; intros; [pose proof (Gt.gt_irrefl 0); intuition | ].
@@ -74,7 +74,7 @@ Proof.
   rewrite IHi by omega; auto.
 Qed.
 
-Lemma iter_op_1 : forall {A} i op z b (a : A), (i < S b) ->
+Lemma iter_op_step_1 : forall {A} i op z b (a : A), (i < S b) ->
   iter_op op z (S b) 1%positive i a = z.
 Proof.
   induction i; intros; [pose proof (Gt.gt_irrefl 0); intuition | ].
@@ -90,36 +90,23 @@ Proof.
 Qed.
 Hint Resolve pos_size_gt0.
 
-Lemma test_low_bit_xI : forall p b, testbit_rev p~1 b b = true.
-Proof.
-  unfold testbit_rev; intros; rewrite Minus.minus_diag; auto.
-Qed.
-
-Lemma test_low_bit_xO : forall p b, testbit_rev p~0 b b = false.
-Proof.
-  unfold testbit_rev; intros; rewrite Minus.minus_diag; auto.
-Qed.
-
-Lemma test_low_bit_1 : forall b, testbit_rev 1%positive b b = true.
-Proof.
-  unfold testbit_rev; intros; rewrite Minus.minus_diag; auto.
-Qed.
-
-Ltac low_bit := match goal with
-| [ |- context[testbit_rev ?p~1 ?b ?b] ] => rewrite test_low_bit_xI; f_equal; rewrite iter_op_xI
-| [ |- context[testbit_rev ?p~0 ?b ?b] ] => rewrite test_low_bit_xO; rewrite iter_op_xO
-| [ |- context[testbit_rev 1%positive ?b ?b] ] => rewrite test_low_bit_1; rewrite iter_op_1 
+Ltac iter_op_step := match goal with
+| [ |- context[iter_op ?op ?z ?b ?p~1 ?i ?a] ] => rewrite iter_op_step_xI
+| [ |- context[iter_op ?op ?z ?b ?p~0 ?i ?a] ] => rewrite iter_op_step_xO
+| [ |- context[iter_op ?op ?z ?b 1%positive ?i ?a] ] => rewrite iter_op_step_1
 end; auto.
 
 Lemma iter_op_spec : forall b p {A} op z (a : A) (zero_id : forall x : A, op x z = x), (Pos.size_nat p <= b) ->
   iter_op op z b p b a = Pos.iter_op op p a.
 Proof.
   induction b; intros; [pose proof (pos_size_gt0 p); omega |].
-  case_eq p; intros; simpl; low_bit; apply IHb;
-    rewrite H0 in *; simpl in H; apply Le.le_S_n in H; auto.
+  simpl; unfold testbit_rev; rewrite Minus.minus_diag.
+  case_eq p; intros; simpl; iter_op_step; simpl; 
+  rewrite IHb; rewrite H0 in *; simpl in H; apply Le.le_S_n in H; auto.
 Qed.
 
 Module CompleteTwistedEdwardsCurve (M : Modulus) (Import P : TwistedEdwardsParams M).
+  Local Open Scope GF_scope.
   (** Twisted Ewdwards curves with complete addition laws. References:
   * <https://eprint.iacr.org/2008/013.pdf>
   * <http://ed25519.cr.yp.to/ed25519-20110926.pdf>
@@ -173,6 +160,7 @@ End CompleteTwistedEdwardsCurve.
 
 
 Module Type CompleteTwistedEdwardsPointFormat (M : Modulus) (Import P : TwistedEdwardsParams M).
+  Local Open Scope GF_scope.
   Module Curve := CompleteTwistedEdwardsCurve M P.
   Parameter point : Type.
   Parameter encode : (GF*GF) -> point.
@@ -189,6 +177,7 @@ Module Type CompleteTwistedEdwardsPointFormat (M : Modulus) (Import P : TwistedE
 End CompleteTwistedEdwardsPointFormat.
 
 Module CompleteTwistedEdwardsFacts (M : Modulus) (Import P : TwistedEdwardsParams M).
+  Local Open Scope GF_scope.
   Module Import Curve := CompleteTwistedEdwardsCurve M P.
   Lemma twistedAddCompletePlus : forall (P1 P2:point),
     let '(x1, y1) := proj1_sig P1 in
@@ -365,7 +354,7 @@ End CompleteTwistedEdwardsFacts.
 
 Module Type Minus1Params (Import M : Modulus) <: TwistedEdwardsParams M.
   Module Export GFDefs := GaloisDefs M.
-  Open Scope GF_scope.
+  Local Open Scope GF_scope.
   Definition a := inject (- 1).
   Axiom a_nonzero : a <> 0.
   Axiom a_square : exists x, x * x = a.
@@ -374,6 +363,7 @@ Module Type Minus1Params (Import M : Modulus) <: TwistedEdwardsParams M.
 End Minus1Params.
 
 Module Minus1Format (M : Modulus) (Import P : Minus1Params M) <: CompleteTwistedEdwardsPointFormat M P.
+  Local Open Scope GF_scope.
   Module Import Facts := CompleteTwistedEdwardsFacts M P.
   Module Import Curve := Facts.Curve.
   (** [projective] represents a point on an elliptic curve using projective
diff --git a/src/Galois/EdDSA.v b/src/Galois/EdDSA.v
index a2df23076..af4f892ca 100644
--- a/src/Galois/EdDSA.v
+++ b/src/Galois/EdDSA.v
@@ -5,8 +5,7 @@ Require Import Crypto.Galois.BaseSystem Crypto.Galois.GaloisTheory.
 Require Import Util.ListUtil Util.CaseUtil Util.ZUtil.
 Require Import VerdiTactics.
 
-Open Scope nat_scope.
-
+Local Open Scope nat_scope.
 Local Coercion Z.to_nat : Z >-> nat.
 
 (* TODO : where should this be? *)
@@ -27,6 +26,7 @@ Notation "'encoding' 'of' T 'as' B" := (Encoding T B) (at level 50).
 Module Type EdDSAParams.
   Parameter q : Prime.
   Axiom q_odd : q > 2.
+
   (* Choosing q sufficiently large is important for security, since the size of
    * q constrains the size of l below. *)
 
@@ -34,10 +34,9 @@ Module Type EdDSAParams.
   Module Modulus_q <: Modulus.
     Definition modulus := q.
   End Modulus_q.
-  Module Export GFDefs := GaloisDefs Modulus_q.
 
   Parameter b : nat.
-  Axiom b_valid : 2^(b - 1) > q.
+  Axiom b_valid : (2^(Z.of_nat b - 1) > q)%Z.
   Notation secretkey := (word b) (only parsing).
   Notation publickey := (word b) (only parsing).
   Notation signature := (word (b + b)) (only parsing).
@@ -54,6 +53,10 @@ Module Type EdDSAParams.
   Parameter n : nat.
   Axiom n_ge_c : n >= c.
   Axiom n_le_b : n <= b.
+
+  Module Import GFDefs := GaloisDefs Modulus_q.
+  Local Open Scope GF_scope.
+
   (* Secret EdDSA scalars have exactly n + 1 bits, with the top bit
    *   (the 2n position) always set and the bottom c bits always cleared.
    * The original specification of EdDSA did not include this parameter:
@@ -64,7 +67,7 @@ Module Type EdDSAParams.
 
   Parameter a : GF.
   Axiom a_nonzero : a <> 0%GF.
-  Axiom a_square : exists x, x^2 = a.
+  Axiom a_square : exists x, x * x = a.
   (* The usual recommendation for best performance is a = −1 if q mod 4 = 1,
    *   and a = 1 if q mod 4 = 3.
    * The original specification of EdDSA did not include this parameter:
@@ -100,7 +103,7 @@ Module Type EdDSAParams.
    *   EdDSA secret key from an EdDSA public key.
    *)
   Parameter l : Prime.
-  Axiom l_odd : l > 2.
+  Axiom l_odd : (l > 2)%nat.
   Axiom l_order_B : scalarMult l B = zero.
   (* TODO: (2^c)l = #E *)
 
@@ -116,7 +119,7 @@ Module Type EdDSAParams.
   Parameter H' : forall {n}, word n -> word (H'_out_len n).
 
   Parameter FqEncoding : encoding of GF as word (b-1).
-  Parameter FlEncoding : encoding of {s:nat | s = s mod l} as word b.
+  Parameter FlEncoding : encoding of {s:nat | s mod l = s} as word b.
   Parameter PointEncoding : encoding of point as word b.
   
 End EdDSAParams.
@@ -130,7 +133,7 @@ Ltac arith := arith';
                     | [ H : _ |- _ ] => rewrite H; arith'
                     end.
 
-Definition modularNat (l : nat) (l_odd : l > 2) (n : nat) : {s : nat | s = s mod l}.
+Definition modularNat (l : nat) (l_odd : l > 2) (n : nat) : {s : nat | s mod l = s}.
   exists (n mod l); abstract arith.
 Defined.
 
@@ -163,7 +166,7 @@ Module Type EdDSA (Import P : EdDSAParams).
     let S_ := split2 b b sig in
     exists A, dec A_ = Some A /\
     exists R, dec R_ = Some R /\
-    exists S : {s:nat | s = s mod l}, dec S_ = Some S /\
+    exists S : {s:nat | s mod l = s}, dec S_ = Some S /\
     proj1_sig S * B = R + wordToNat (H (R_ ++ A_ ++ M)) * A).
 End EdDSA.