From f14b26f8ab162aaef56b897450429b3134d6a3f5 Mon Sep 17 00:00:00 2001 From: Jade Philipoom Date: Mon, 15 Feb 2016 19:34:51 -0500 Subject: EdDSA: tweaked l_bound --- src/Spec/Ed25519.v | 16 +++++----------- 1 file changed, 5 insertions(+), 11 deletions(-) (limited to 'src/Spec/Ed25519.v') 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") *) -- cgit v1.2.3