Changed name of Encoding to CanonicalEncoding, and changed notation to match.

5 files changed, 11 insertions, 11 deletions

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;