Update field names in SpecificGen

9 files changed, 54 insertions, 48 deletions

diff --git a/_CoqProject b/_CoqProject
index ff4a22fc8..35fd5108d 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -173,26 +173,32 @@ src/Specific/GF25519Reflective/Reified/Unpack.v
 src/SpecificGen/GF2213_32.v
 src/SpecificGen/GF2213_32Bounded.v
 src/SpecificGen/GF2213_32BoundedCommon.v
+src/SpecificGen/GF2213_32ExtendedAddCoordinates.v
 src/SpecificGen/GF2213_32Reflective.v
 src/SpecificGen/GF2519_32.v
 src/SpecificGen/GF2519_32Bounded.v
 src/SpecificGen/GF2519_32BoundedCommon.v
+src/SpecificGen/GF2519_32ExtendedAddCoordinates.v
 src/SpecificGen/GF2519_32Reflective.v
 src/SpecificGen/GF25519_32.v
 src/SpecificGen/GF25519_32Bounded.v
 src/SpecificGen/GF25519_32BoundedCommon.v
+src/SpecificGen/GF25519_32ExtendedAddCoordinates.v
 src/SpecificGen/GF25519_32Reflective.v
 src/SpecificGen/GF25519_64.v
 src/SpecificGen/GF25519_64Bounded.v
 src/SpecificGen/GF25519_64BoundedCommon.v
+src/SpecificGen/GF25519_64ExtendedAddCoordinates.v
 src/SpecificGen/GF25519_64Reflective.v
 src/SpecificGen/GF41417_32.v
 src/SpecificGen/GF41417_32Bounded.v
 src/SpecificGen/GF41417_32BoundedCommon.v
+src/SpecificGen/GF41417_32ExtendedAddCoordinates.v
 src/SpecificGen/GF41417_32Reflective.v
 src/SpecificGen/GF5211_32.v
 src/SpecificGen/GF5211_32Bounded.v
 src/SpecificGen/GF5211_32BoundedCommon.v
+src/SpecificGen/GF5211_32ExtendedAddCoordinates.v
 src/SpecificGen/GF5211_32Reflective.v
 src/SpecificGen/GF2213_32Reflective/Common.v
 src/SpecificGen/GF2213_32Reflective/CommonBinOp.v
diff --git a/src/SpecificGen/GF2213_32.v b/src/SpecificGen/GF2213_32.v
index 58d9f2559..87da8dbcc 100644
--- a/src/SpecificGen/GF2213_32.v
+++ b/src/SpecificGen/GF2213_32.v
@@ -428,7 +428,7 @@ Proof.
   { intros; apply encode_rep. }
 Qed.
 
-Definition field2213 : @field fe2213_32 eq zero_ one_ opp add sub mul inv div := proj1 field_and_homomorphisms.
+Definition field2213_32 : @field fe2213_32 eq zero_ one_ opp add sub mul inv div := proj1 field_and_homomorphisms.
 
 Lemma carry_field_and_homomorphisms
   : @field fe2213_32 eq zero_ one_ carry_opp carry_add carry_sub mul inv div
@@ -454,22 +454,22 @@ Proof.
   { intros; apply encode_rep. }
 Qed.
 
-Definition carry_field : @field fe2213_32 eq zero_ one_ carry_opp carry_add carry_sub mul inv div := proj1 carry_field_and_homomorphisms.
+Definition carry_field2213_32 : @field fe2213_32 eq zero_ one_ carry_opp carry_add carry_sub mul inv div := proj1 carry_field_and_homomorphisms.
 
-Lemma homomorphism_F_encode
+Lemma homomorphism_F2213_32_encode
   : @Ring.is_homomorphism (F modulus) Logic.eq F.one F.add F.mul fe2213_32 eq one add mul encode.
 Proof. apply field_and_homomorphisms. Qed.
 
-Lemma homomorphism_F_decode
+Lemma homomorphism_F2213_32_decode
   : @Ring.is_homomorphism fe2213_32 eq one add mul (F modulus) Logic.eq F.one F.add F.mul decode.
 Proof. apply field_and_homomorphisms. Qed.
 
 
-Lemma homomorphism_carry_F_encode
+Lemma homomorphism_carry_F2213_32_encode
   : @Ring.is_homomorphism (F modulus) Logic.eq F.one F.add F.mul fe2213_32 eq one carry_add mul encode.
 Proof. apply carry_field_and_homomorphisms. Qed.
 
-Lemma homomorphism_carry_F_decode
+Lemma homomorphism_carry_F2213_32_decode
   : @Ring.is_homomorphism fe2213_32 eq one carry_add mul (F modulus) Logic.eq F.one F.add F.mul decode.
 Proof. apply carry_field_and_homomorphisms. Qed.
 
diff --git a/src/SpecificGen/GF2519_32.v b/src/SpecificGen/GF2519_32.v
index d64b24088..b7fd074ae 100644
--- a/src/SpecificGen/GF2519_32.v
+++ b/src/SpecificGen/GF2519_32.v
@@ -420,7 +420,7 @@ Proof.
   { intros; apply encode_rep. }
 Qed.
 
-Definition field2519 : @field fe2519_32 eq zero_ one_ opp add sub mul inv div := proj1 field_and_homomorphisms.
+Definition field2519_32 : @field fe2519_32 eq zero_ one_ opp add sub mul inv div := proj1 field_and_homomorphisms.
 
 Lemma carry_field_and_homomorphisms
   : @field fe2519_32 eq zero_ one_ carry_opp carry_add carry_sub mul inv div
@@ -446,22 +446,22 @@ Proof.
   { intros; apply encode_rep. }
 Qed.
 
-Definition carry_field : @field fe2519_32 eq zero_ one_ carry_opp carry_add carry_sub mul inv div := proj1 carry_field_and_homomorphisms.
+Definition carry_field2519_32 : @field fe2519_32 eq zero_ one_ carry_opp carry_add carry_sub mul inv div := proj1 carry_field_and_homomorphisms.
 
-Lemma homomorphism_F_encode
+Lemma homomorphism_F2519_32_encode
   : @Ring.is_homomorphism (F modulus) Logic.eq F.one F.add F.mul fe2519_32 eq one add mul encode.
 Proof. apply field_and_homomorphisms. Qed.
 
-Lemma homomorphism_F_decode
+Lemma homomorphism_F2519_32_decode
   : @Ring.is_homomorphism fe2519_32 eq one add mul (F modulus) Logic.eq F.one F.add F.mul decode.
 Proof. apply field_and_homomorphisms. Qed.
 
 
-Lemma homomorphism_carry_F_encode
+Lemma homomorphism_carry_F2519_32_encode
   : @Ring.is_homomorphism (F modulus) Logic.eq F.one F.add F.mul fe2519_32 eq one carry_add mul encode.
 Proof. apply carry_field_and_homomorphisms. Qed.
 
-Lemma homomorphism_carry_F_decode
+Lemma homomorphism_carry_F2519_32_decode
   : @Ring.is_homomorphism fe2519_32 eq one carry_add mul (F modulus) Logic.eq F.one F.add F.mul decode.
 Proof. apply carry_field_and_homomorphisms. Qed.
 
diff --git a/src/SpecificGen/GF25519_32.v b/src/SpecificGen/GF25519_32.v
index 920da6dde..30d01f87d 100644
--- a/src/SpecificGen/GF25519_32.v
+++ b/src/SpecificGen/GF25519_32.v
@@ -428,7 +428,7 @@ Proof.
   { intros; apply encode_rep. }
 Qed.
 
-Definition field25519 : @field fe25519_32 eq zero_ one_ opp add sub mul inv div := proj1 field_and_homomorphisms.
+Definition field25519_32 : @field fe25519_32 eq zero_ one_ opp add sub mul inv div := proj1 field_and_homomorphisms.
 
 Lemma carry_field_and_homomorphisms
   : @field fe25519_32 eq zero_ one_ carry_opp carry_add carry_sub mul inv div
@@ -454,22 +454,22 @@ Proof.
   { intros; apply encode_rep. }
 Qed.
 
-Definition carry_field : @field fe25519_32 eq zero_ one_ carry_opp carry_add carry_sub mul inv div := proj1 carry_field_and_homomorphisms.
+Definition carry_field25519_32 : @field fe25519_32 eq zero_ one_ carry_opp carry_add carry_sub mul inv div := proj1 carry_field_and_homomorphisms.
 
-Lemma homomorphism_F_encode
+Lemma homomorphism_F25519_32_encode
   : @Ring.is_homomorphism (F modulus) Logic.eq F.one F.add F.mul fe25519_32 eq one add mul encode.
 Proof. apply field_and_homomorphisms. Qed.
 
-Lemma homomorphism_F_decode
+Lemma homomorphism_F25519_32_decode
   : @Ring.is_homomorphism fe25519_32 eq one add mul (F modulus) Logic.eq F.one F.add F.mul decode.
 Proof. apply field_and_homomorphisms. Qed.
 
 
-Lemma homomorphism_carry_F_encode
+Lemma homomorphism_carry_F25519_32_encode
   : @Ring.is_homomorphism (F modulus) Logic.eq F.one F.add F.mul fe25519_32 eq one carry_add mul encode.
 Proof. apply carry_field_and_homomorphisms. Qed.
 
-Lemma homomorphism_carry_F_decode
+Lemma homomorphism_carry_F25519_32_decode
   : @Ring.is_homomorphism fe25519_32 eq one carry_add mul (F modulus) Logic.eq F.one F.add F.mul decode.
 Proof. apply carry_field_and_homomorphisms. Qed.
 
diff --git a/src/SpecificGen/GF25519_64.v b/src/SpecificGen/GF25519_64.v
index f68c52382..49b5fb2c4 100644
--- a/src/SpecificGen/GF25519_64.v
+++ b/src/SpecificGen/GF25519_64.v
@@ -428,7 +428,7 @@ Proof.
   { intros; apply encode_rep. }
 Qed.
 
-Definition field25519 : @field fe25519_64 eq zero_ one_ opp add sub mul inv div := proj1 field_and_homomorphisms.
+Definition field25519_64 : @field fe25519_64 eq zero_ one_ opp add sub mul inv div := proj1 field_and_homomorphisms.
 
 Lemma carry_field_and_homomorphisms
   : @field fe25519_64 eq zero_ one_ carry_opp carry_add carry_sub mul inv div
@@ -454,22 +454,22 @@ Proof.
   { intros; apply encode_rep. }
 Qed.
 
-Definition carry_field : @field fe25519_64 eq zero_ one_ carry_opp carry_add carry_sub mul inv div := proj1 carry_field_and_homomorphisms.
+Definition carry_field25519_64 : @field fe25519_64 eq zero_ one_ carry_opp carry_add carry_sub mul inv div := proj1 carry_field_and_homomorphisms.
 
-Lemma homomorphism_F_encode
+Lemma homomorphism_F25519_64_encode
   : @Ring.is_homomorphism (F modulus) Logic.eq F.one F.add F.mul fe25519_64 eq one add mul encode.
 Proof. apply field_and_homomorphisms. Qed.
 
-Lemma homomorphism_F_decode
+Lemma homomorphism_F25519_64_decode
   : @Ring.is_homomorphism fe25519_64 eq one add mul (F modulus) Logic.eq F.one F.add F.mul decode.
 Proof. apply field_and_homomorphisms. Qed.
 
 
-Lemma homomorphism_carry_F_encode
+Lemma homomorphism_carry_F25519_64_encode
   : @Ring.is_homomorphism (F modulus) Logic.eq F.one F.add F.mul fe25519_64 eq one carry_add mul encode.
 Proof. apply carry_field_and_homomorphisms. Qed.
 
-Lemma homomorphism_carry_F_decode
+Lemma homomorphism_carry_F25519_64_decode
   : @Ring.is_homomorphism fe25519_64 eq one carry_add mul (F modulus) Logic.eq F.one F.add F.mul decode.
 Proof. apply carry_field_and_homomorphisms. Qed.
 
diff --git a/src/SpecificGen/GF41417_32.v b/src/SpecificGen/GF41417_32.v
index 61c13766b..04ad4c173 100644
--- a/src/SpecificGen/GF41417_32.v
+++ b/src/SpecificGen/GF41417_32.v
@@ -420,7 +420,7 @@ Proof.
   { intros; apply encode_rep. }
 Qed.
 
-Definition field41417 : @field fe41417_32 eq zero_ one_ opp add sub mul inv div := proj1 field_and_homomorphisms.
+Definition field41417_32 : @field fe41417_32 eq zero_ one_ opp add sub mul inv div := proj1 field_and_homomorphisms.
 
 Lemma carry_field_and_homomorphisms
   : @field fe41417_32 eq zero_ one_ carry_opp carry_add carry_sub mul inv div
@@ -446,22 +446,22 @@ Proof.
   { intros; apply encode_rep. }
 Qed.
 
-Definition carry_field : @field fe41417_32 eq zero_ one_ carry_opp carry_add carry_sub mul inv div := proj1 carry_field_and_homomorphisms.
+Definition carry_field41417_32 : @field fe41417_32 eq zero_ one_ carry_opp carry_add carry_sub mul inv div := proj1 carry_field_and_homomorphisms.
 
-Lemma homomorphism_F_encode
+Lemma homomorphism_F41417_32_encode
   : @Ring.is_homomorphism (F modulus) Logic.eq F.one F.add F.mul fe41417_32 eq one add mul encode.
 Proof. apply field_and_homomorphisms. Qed.
 
-Lemma homomorphism_F_decode
+Lemma homomorphism_F41417_32_decode
   : @Ring.is_homomorphism fe41417_32 eq one add mul (F modulus) Logic.eq F.one F.add F.mul decode.
 Proof. apply field_and_homomorphisms. Qed.
 
 
-Lemma homomorphism_carry_F_encode
+Lemma homomorphism_carry_F41417_32_encode
   : @Ring.is_homomorphism (F modulus) Logic.eq F.one F.add F.mul fe41417_32 eq one carry_add mul encode.
 Proof. apply carry_field_and_homomorphisms. Qed.
 
-Lemma homomorphism_carry_F_decode
+Lemma homomorphism_carry_F41417_32_decode
   : @Ring.is_homomorphism fe41417_32 eq one carry_add mul (F modulus) Logic.eq F.one F.add F.mul decode.
 Proof. apply carry_field_and_homomorphisms. Qed.
 
diff --git a/src/SpecificGen/GF5211_32.v b/src/SpecificGen/GF5211_32.v
index 2a40a932d..ea75b2983 100644
--- a/src/SpecificGen/GF5211_32.v
+++ b/src/SpecificGen/GF5211_32.v
@@ -420,7 +420,7 @@ Proof.
   { intros; apply encode_rep. }
 Qed.
 
-Definition field5211 : @field fe5211_32 eq zero_ one_ opp add sub mul inv div := proj1 field_and_homomorphisms.
+Definition field5211_32 : @field fe5211_32 eq zero_ one_ opp add sub mul inv div := proj1 field_and_homomorphisms.
 
 Lemma carry_field_and_homomorphisms
   : @field fe5211_32 eq zero_ one_ carry_opp carry_add carry_sub mul inv div
@@ -446,22 +446,22 @@ Proof.
   { intros; apply encode_rep. }
 Qed.
 
-Definition carry_field : @field fe5211_32 eq zero_ one_ carry_opp carry_add carry_sub mul inv div := proj1 carry_field_and_homomorphisms.
+Definition carry_field5211_32 : @field fe5211_32 eq zero_ one_ carry_opp carry_add carry_sub mul inv div := proj1 carry_field_and_homomorphisms.
 
-Lemma homomorphism_F_encode
+Lemma homomorphism_F5211_32_encode
   : @Ring.is_homomorphism (F modulus) Logic.eq F.one F.add F.mul fe5211_32 eq one add mul encode.
 Proof. apply field_and_homomorphisms. Qed.
 
-Lemma homomorphism_F_decode
+Lemma homomorphism_F5211_32_decode
   : @Ring.is_homomorphism fe5211_32 eq one add mul (F modulus) Logic.eq F.one F.add F.mul decode.
 Proof. apply field_and_homomorphisms. Qed.
 
 
-Lemma homomorphism_carry_F_encode
+Lemma homomorphism_carry_F5211_32_encode
   : @Ring.is_homomorphism (F modulus) Logic.eq F.one F.add F.mul fe5211_32 eq one carry_add mul encode.
 Proof. apply carry_field_and_homomorphisms. Qed.
 
-Lemma homomorphism_carry_F_decode
+Lemma homomorphism_carry_F5211_32_decode
   : @Ring.is_homomorphism fe5211_32 eq one carry_add mul (F modulus) Logic.eq F.one F.add F.mul decode.
 Proof. apply carry_field_and_homomorphisms. Qed.
 
diff --git a/src/SpecificGen/GFtemplate3mod4 b/src/SpecificGen/GFtemplate3mod4
index ccee86d1a..d255befeb 100644
--- a/src/SpecificGen/GFtemplate3mod4
+++ b/src/SpecificGen/GFtemplate3mod4
@@ -420,7 +420,7 @@ Proof.
   { intros; apply encode_rep. }
 Qed.
 
-Definition field{{{k}}}{{{c}}} : @field fe{{{k}}}{{{c}}}_{{{w}}} eq zero_ one_ opp add sub mul inv div := proj1 field_and_homomorphisms.
+Definition field{{{k}}}{{{c}}}_{{{w}}} : @field fe{{{k}}}{{{c}}}_{{{w}}} eq zero_ one_ opp add sub mul inv div := proj1 field_and_homomorphisms.
 
 Lemma carry_field_and_homomorphisms
   : @field fe{{{k}}}{{{c}}}_{{{w}}} eq zero_ one_ carry_opp carry_add carry_sub mul inv div
@@ -446,22 +446,22 @@ Proof.
   { intros; apply encode_rep. }
 Qed.
 
-Definition carry_field : @field fe{{{k}}}{{{c}}}_{{{w}}} eq zero_ one_ carry_opp carry_add carry_sub mul inv div := proj1 carry_field_and_homomorphisms.
+Definition carry_field{{{k}}}{{{c}}}_{{{w}}} : @field fe{{{k}}}{{{c}}}_{{{w}}} eq zero_ one_ carry_opp carry_add carry_sub mul inv div := proj1 carry_field_and_homomorphisms.
 
-Lemma homomorphism_F_encode
+Lemma homomorphism_F{{{k}}}{{{c}}}_{{{w}}}_encode
   : @Ring.is_homomorphism (F modulus) Logic.eq F.one F.add F.mul fe{{{k}}}{{{c}}}_{{{w}}} eq one add mul encode.
 Proof. apply field_and_homomorphisms. Qed.
 
-Lemma homomorphism_F_decode
+Lemma homomorphism_F{{{k}}}{{{c}}}_{{{w}}}_decode
   : @Ring.is_homomorphism fe{{{k}}}{{{c}}}_{{{w}}} eq one add mul (F modulus) Logic.eq F.one F.add F.mul decode.
 Proof. apply field_and_homomorphisms. Qed.
 
 
-Lemma homomorphism_carry_F_encode
+Lemma homomorphism_carry_F{{{k}}}{{{c}}}_{{{w}}}_encode
   : @Ring.is_homomorphism (F modulus) Logic.eq F.one F.add F.mul fe{{{k}}}{{{c}}}_{{{w}}} eq one carry_add mul encode.
 Proof. apply carry_field_and_homomorphisms. Qed.
 
-Lemma homomorphism_carry_F_decode
+Lemma homomorphism_carry_F{{{k}}}{{{c}}}_{{{w}}}_decode
   : @Ring.is_homomorphism fe{{{k}}}{{{c}}}_{{{w}}} eq one carry_add mul (F modulus) Logic.eq F.one F.add F.mul decode.
 Proof. apply carry_field_and_homomorphisms. Qed.
 
diff --git a/src/SpecificGen/GFtemplate5mod8 b/src/SpecificGen/GFtemplate5mod8
index c5d0d1cfe..008010efd 100644
--- a/src/SpecificGen/GFtemplate5mod8
+++ b/src/SpecificGen/GFtemplate5mod8
@@ -428,7 +428,7 @@ Proof.
   { intros; apply encode_rep. }
 Qed.
 
-Definition field{{{k}}}{{{c}}} : @field fe{{{k}}}{{{c}}}_{{{w}}} eq zero_ one_ opp add sub mul inv div := proj1 field_and_homomorphisms.
+Definition field{{{k}}}{{{c}}}_{{{w}}} : @field fe{{{k}}}{{{c}}}_{{{w}}} eq zero_ one_ opp add sub mul inv div := proj1 field_and_homomorphisms.
 
 Lemma carry_field_and_homomorphisms
   : @field fe{{{k}}}{{{c}}}_{{{w}}} eq zero_ one_ carry_opp carry_add carry_sub mul inv div
@@ -454,22 +454,22 @@ Proof.
   { intros; apply encode_rep. }
 Qed.
 
-Definition carry_field : @field fe{{{k}}}{{{c}}}_{{{w}}} eq zero_ one_ carry_opp carry_add carry_sub mul inv div := proj1 carry_field_and_homomorphisms.
+Definition carry_field{{{k}}}{{{c}}}_{{{w}}} : @field fe{{{k}}}{{{c}}}_{{{w}}} eq zero_ one_ carry_opp carry_add carry_sub mul inv div := proj1 carry_field_and_homomorphisms.
 
-Lemma homomorphism_F_encode
+Lemma homomorphism_F{{{k}}}{{{c}}}_{{{w}}}_encode
   : @Ring.is_homomorphism (F modulus) Logic.eq F.one F.add F.mul fe{{{k}}}{{{c}}}_{{{w}}} eq one add mul encode.
 Proof. apply field_and_homomorphisms. Qed.
 
-Lemma homomorphism_F_decode
+Lemma homomorphism_F{{{k}}}{{{c}}}_{{{w}}}_decode
   : @Ring.is_homomorphism fe{{{k}}}{{{c}}}_{{{w}}} eq one add mul (F modulus) Logic.eq F.one F.add F.mul decode.
 Proof. apply field_and_homomorphisms. Qed.
 
 
-Lemma homomorphism_carry_F_encode
+Lemma homomorphism_carry_F{{{k}}}{{{c}}}_{{{w}}}_encode
   : @Ring.is_homomorphism (F modulus) Logic.eq F.one F.add F.mul fe{{{k}}}{{{c}}}_{{{w}}} eq one carry_add mul encode.
 Proof. apply carry_field_and_homomorphisms. Qed.
 
-Lemma homomorphism_carry_F_decode
+Lemma homomorphism_carry_F{{{k}}}{{{c}}}_{{{w}}}_decode
   : @Ring.is_homomorphism fe{{{k}}}{{{c}}}_{{{w}}} eq one carry_add mul (F modulus) Logic.eq F.one F.add F.mul decode.
 Proof. apply carry_field_and_homomorphisms. Qed.