diff options
author | Jade Philipoom <jadep@mit.edu> | 2016-02-15 19:34:51 -0500 |
---|---|---|
committer | Jade Philipoom <jadep@mit.edu> | 2016-02-15 19:34:51 -0500 |
commit | f14b26f8ab162aaef56b897450429b3134d6a3f5 (patch) | |
tree | e43b1a4feb49030fc44cd2993cad54157312f568 | |
parent | 2eff351163f1c6fedd4aea9629f2bd149601c873 (diff) |
EdDSA: tweaked l_bound
-rw-r--r-- | src/Spec/Ed25519.v | 16 |
1 files changed, 5 insertions, 11 deletions
diff --git a/src/Spec/Ed25519.v b/src/Spec/Ed25519.v index e5796b8f2..26e395b53 100644 --- a/src/Spec/Ed25519.v +++ b/src/Spec/Ed25519.v @@ -99,28 +99,22 @@ Proof. apply lt_plus_trans. compute; omega. Qed. -Lemma l_bound : l < pow2 b. -Proof. - rewrite Zpow_pow2. - unfold l. - rewrite <- Z2Nat.inj_lt; compute; congruence. -Qed. Lemma q_pos : (0 < q)%Z. q_bound. Qed. Definition FqEncoding : encoding of (F q) as word (b-1) := @modular_word_encoding q (b - 1) q_pos b_valid. -Check @modular_word_encoding. Lemma l_pos : (0 < Z.of_nat l)%Z. pose proof prime_l; prime_bound. Qed. -(* form of l_bound needed for FlEncoding *) -Lemma l_bound_encoding : Z.to_nat (Z.of_nat l) < 2 ^ b. +Lemma l_bound : Z.to_nat (Z.of_nat l) < 2 ^ b. Proof. rewrite Nat2Z.id. rewrite <- pow2_id. - exact l_bound. + rewrite Zpow_pow2. + unfold l. + apply Z2Nat.inj_lt; compute; congruence. Qed. Definition FlEncoding : encoding of F (Z.of_nat l) as word b := - @modular_word_encoding (Z.of_nat l) b l_pos l_bound_encoding. + @modular_word_encoding (Z.of_nat l) b l_pos l_bound. Definition H : forall n : nat, word n -> word (b + b). Admitted. Definition B : point. Admitted. (* TODO: B = decodePoint (y=4/5, x="positive") *) |