Moved sign_bit definition to Spec.

4 files changed, 16 insertions, 25 deletions

diff --git a/src/Encoding/ModularWordEncodingTheorems.v b/src/Encoding/ModularWordEncodingTheorems.v
index a74ccb522..7251ac1e6 100644
--- a/src/Encoding/ModularWordEncodingTheorems.v
+++ b/src/Encoding/ModularWordEncodingTheorems.v
@@ -13,42 +13,29 @@ Local Open Scope F_scope.
 
 Section SignBit.
   Context {m : Z} {prime_m : prime m} {two_lt_m : (2 < m)%Z} {sz : nat} {bound_check : (Z.to_nat m < 2 ^ sz)%nat}.
-  Lemma m_pos : (0 < m)%Z.
-  Proof.
-    apply prime_ge_2 in prime_m; omega.
-  Qed.
-
-  Arguments modular_word_encoding {m} {sz} m_pos bound_check.
-  Let Fm_encoding := modular_word_encoding m_pos bound_check.
-
-  Definition sign_bit (x : F m) :=
-  match (@enc _ _ Fm_encoding x) with
-    | Word.WO => false
-    | Word.WS b _ w' => b
-  end.
 
-  Lemma sign_bit_parity : forall x, sign_bit x = Z.odd x.
+  Lemma sign_bit_parity : forall x, @sign_bit m sz x = Z.odd x.
   Proof.
-    unfold sign_bit; intros.
-    unfold Fm_encoding, enc, modular_word_encoding, Fm_enc.
+    unfold sign_bit, Fm_enc; intros.
     pose proof (shatter_word (NToWord sz (Z.to_N x))) as shatter.
     case_eq sz; intros; subst; rewrite shatter.
     + pose proof (prime_ge_2 m prime_m).
       simpl in bound_check.
       assert (m < 1)%Z by (apply Z2Nat.inj_lt; try omega; assumption).
       omega.
-    + pose proof (FieldToZ_range x m_pos).  
+    + assert (0 < m)%Z as m_pos by (pose proof prime_ge_2 m prime_m; omega).
+      pose proof (FieldToZ_range x m_pos).  
       destruct (FieldToZ x); auto.
       - destruct p; auto.
       - pose proof (Pos2Z.neg_is_neg p); omega.
    Qed.
 
-  Lemma sign_bit_zero : sign_bit 0 = false.
+  Lemma sign_bit_zero : @sign_bit m sz 0 = false.
   Proof.
     rewrite sign_bit_parity; auto.
   Qed.
 
-  Lemma sign_bit_opp : forall (x : F m), x <> 0 -> negb (sign_bit x) = sign_bit (opp x).
+  Lemma sign_bit_opp : forall (x : F m), x <> 0 -> negb (@sign_bit m sz x) = @sign_bit m sz (opp x).
   Proof.
     intros.
     pose proof sign_bit_zero as sign_zero.
@@ -56,7 +43,7 @@ Section SignBit.
     pose proof (F_opp_spec x) as opp_spec_x.
     apply F_eq in opp_spec_x.
     rewrite FieldToZ_add in opp_spec_x.
-    rewrite <-opp_spec_x, Z_odd_mod in sign_zero by omega.
+    rewrite <-opp_spec_x, Z_odd_mod in sign_zero by (pose proof prime_ge_2 m prime_m; omega).
     replace (Z.odd m) with true in sign_zero by (destruct (ZUtil.prime_odd_or_2 m prime_m); auto || omega).
     rewrite Z.odd_add, F_FieldToZ_add_opp, Z.div_same, Bool.xorb_true_r in sign_zero by assumption || omega.
     apply Bool.xorb_eq.
diff --git a/src/Spec/Ed25519.v b/src/Spec/Ed25519.v
index 9ae03dcd5..cddd72aaf 100644
--- a/src/Spec/Ed25519.v
+++ b/src/Spec/Ed25519.v
@@ -143,11 +143,9 @@ Proof.
   reflexivity.
 Qed.
 
-Lemma b_minus1_nonzero : 0 < b - 1. Proof. cbv. omega. Qed.
-
 Definition PointEncoding : encoding of E.point as (word b) :=
-  (@point_encoding curve25519params (b - 1) q_5mod8 sqrt_minus1_valid FqEncoding
-  (@sign_bit _ prime_q two_lt_q (b - 1) b_valid) sign_bit_zero sign_bit_opp).
+  (@point_encoding curve25519params (b - 1) q_5mod8 sqrt_minus1_valid FqEncoding sign_bit
+  (@sign_bit_zero _ prime_q two_lt_q _ b_valid) (@sign_bit_opp _ prime_q two_lt_q _ b_valid)).
 
 Definition H : forall n : nat, word n -> word (b + b). Admitted.
 Definition B : E.point. Admitted. (* TODO: B = decodePoint (y=4/5, x="positive") *)
diff --git a/src/Spec/ModularWordEncoding.v b/src/Spec/ModularWordEncoding.v
index 262b1054d..7772a124c 100644
--- a/src/Spec/ModularWordEncoding.v
+++ b/src/Spec/ModularWordEncoding.v
@@ -22,6 +22,12 @@ Section ModularWordEncoding.
       else None
   .
 
+  Definition sign_bit (x : F m) :=
+  match (Fm_enc x) with
+    | Word.WO => false
+    | Word.WS b _ w' => b
+  end.
+
   Instance modular_word_encoding : encoding of F m as word sz := {
     enc := Fm_enc;
     dec := Fm_dec;
diff --git a/src/Specific/Ed25519.v b/src/Specific/Ed25519.v
index 5107c1468..fa1c44d08 100644
--- a/src/Specific/Ed25519.v
+++ b/src/Specific/Ed25519.v
@@ -359,7 +359,7 @@ Proof.
     reflexivity. }
   Unfocus.
 
-  cbv iota beta delta [point_dec_coordinates ModularWordEncodingTheorems.sign_bit dec FqEncoding modular_word_encoding E.solve_for_x2 sqrt_mod_q].
+  cbv iota beta delta [point_dec_coordinates sign_bit dec FqEncoding modular_word_encoding E.solve_for_x2 sqrt_mod_q].
 
   etransitivity.
   Focus 2. {