From 728b2f95dc83329c58aef7624283cb945c77b919 Mon Sep 17 00:00:00 2001 From: jadep Date: Fri, 29 Apr 2016 18:27:26 -0400 Subject: Changed name of Encoding to CanonicalEncoding, and changed notation to match. --- src/Spec/Ed25519.v | 6 +++--- src/Spec/EdDSA.v | 6 +++--- src/Spec/Encoding.v | 4 ++-- src/Spec/ModularWordEncoding.v | 2 +- src/Spec/PointEncoding.v | 4 ++-- 5 files changed, 11 insertions(+), 11 deletions(-) (limited to 'src/Spec') diff --git a/src/Spec/Ed25519.v b/src/Spec/Ed25519.v index cddd72aaf..4876bb8d1 100644 --- a/src/Spec/Ed25519.v +++ b/src/Spec/Ed25519.v @@ -118,7 +118,7 @@ Qed. Require Import Crypto.Spec.Encoding. Lemma q_pos : (0 < q)%Z. q_bound. Qed. -Definition FqEncoding : encoding of (F q) as word (b-1) := +Definition FqEncoding : canonical encoding of (F q) as word (b-1) := @modular_word_encoding q (b - 1) q_pos b_valid. Lemma l_pos : (0 < Z.of_nat l)%Z. pose proof prime_l; prime_bound. Qed. @@ -130,7 +130,7 @@ Proof. unfold l. apply Z2Nat.inj_lt; compute; congruence. Qed. -Definition FlEncoding : encoding of F (Z.of_nat l) as word b := +Definition FlEncoding : canonical encoding of F (Z.of_nat l) as word b := @modular_word_encoding (Z.of_nat l) b l_pos l_bound. Lemma q_5mod8 : (q mod 8 = 5)%Z. cbv; reflexivity. Qed. @@ -143,7 +143,7 @@ Proof. reflexivity. Qed. -Definition PointEncoding : encoding of E.point as (word b) := +Definition PointEncoding : canonical encoding of E.point as (word b) := (@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)). diff --git a/src/Spec/EdDSA.v b/src/Spec/EdDSA.v index 80aed4a20..99f0766e0 100644 --- a/src/Spec/EdDSA.v +++ b/src/Spec/EdDSA.v @@ -21,8 +21,8 @@ Section EdDSAParams. b : nat; (* public keys are k bits, signatures are 2*k bits *) b_valid : 2^(b - 1) > BinInt.Z.to_nat q; - FqEncoding : encoding of F q as Word.word (b-1); - PointEncoding : encoding of E.point as Word.word b; + FqEncoding : canonical encoding of F q as Word.word (b-1); + PointEncoding : canonical encoding of E.point as Word.word b; H : forall {n}, Word.word n -> Word.word (b + b); (* main hash function *) @@ -40,7 +40,7 @@ Section EdDSAParams. l_prime : Znumtheory.prime (BinInt.Z.of_nat l); l_odd : l > 2; l_order_B : (l*B)%E = E.zero; - FlEncoding : encoding of F (BinInt.Z.of_nat l) as Word.word b + FlEncoding : canonical encoding of F (BinInt.Z.of_nat l) as Word.word b }. End EdDSAParams. diff --git a/src/Spec/Encoding.v b/src/Spec/Encoding.v index 17dcb4b3e..b063b638f 100644 --- a/src/Spec/Encoding.v +++ b/src/Spec/Encoding.v @@ -1,8 +1,8 @@ -Class Encoding (T B:Type) := { +Class CanonicalEncoding (T B:Type) := { enc : T -> B ; dec : B -> option T ; encoding_valid : forall x, dec (enc x) = Some x ; encoding_canonical : forall x_enc x, dec x_enc = Some x -> enc x = x_enc }. -Notation "'encoding' 'of' T 'as' B" := (Encoding T B) (at level 50). \ No newline at end of file +Notation "'canonical' 'encoding' 'of' T 'as' B" := (CanonicalEncoding T B) (at level 50). \ No newline at end of file diff --git a/src/Spec/ModularWordEncoding.v b/src/Spec/ModularWordEncoding.v index 7772a124c..d6f6bcb3c 100644 --- a/src/Spec/ModularWordEncoding.v +++ b/src/Spec/ModularWordEncoding.v @@ -28,7 +28,7 @@ Section ModularWordEncoding. | Word.WS b _ w' => b end. - Instance modular_word_encoding : encoding of F m as word sz := { + Instance modular_word_encoding : canonical encoding of F m as word sz := { enc := Fm_enc; dec := Fm_dec; encoding_valid := diff --git a/src/Spec/PointEncoding.v b/src/Spec/PointEncoding.v index 484c5f0df..f4634f52f 100644 --- a/src/Spec/PointEncoding.v +++ b/src/Spec/PointEncoding.v @@ -17,7 +17,7 @@ Section PointEncoding. Context {prm: TwistedEdwardsParams} {sz : nat} {sz_nonzero : (0 < sz)%nat} {bound_check : (BinInt.Z.to_nat q < NPeano.Nat.pow 2 sz)%nat} {q_5mod8 : (q mod 8 = 5)%Z} {sqrt_minus1_valid : (@ZToField q 2 ^ BinInt.Z.to_N (q / 4)) ^ 2 = opp 1} - {FqEncoding : encoding of (F q) as (Word.word sz)} + {FqEncoding : canonical encoding of (F q) as (Word.word sz)} {sign_bit : F q -> bool} {sign_bit_zero : sign_bit 0 = false} {sign_bit_opp : forall x, x <> 0 -> negb (sign_bit x) = sign_bit (opp x)}. Existing Instance prime_q. @@ -38,7 +38,7 @@ Section PointEncoding. Definition point_encoding_canonical : forall x_enc x, point_dec x_enc = Some x -> point_enc x = x_enc := PointEncodingPre.point_encoding_canonical. - Instance point_encoding : encoding of E.point as (Word.word (S sz)) := { + Instance point_encoding : canonical encoding of E.point as (Word.word (S sz)) := { enc := point_enc; dec := point_dec; encoding_valid := point_encoding_valid; -- cgit v1.2.3