Moved sign_bit definition to Spec.

2 files changed, 8 insertions, 4 deletions

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;