6 files changed, 0 insertions, 158 deletions
diff --git a/_CoqProject b/_CoqProject
index cc1272093..952b493ac 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -55,9 +55,6 @@ src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
 src/CompleteEdwardsCurve/EdwardsMontgomery.v
 src/CompleteEdwardsCurve/ExtendedCoordinates.v
 src/CompleteEdwardsCurve/Pre.v
-src/Encoding/EncodingTheorems.v
-src/Encoding/ModularWordEncodingPre.v
-src/Encoding/ModularWordEncodingTheorems.v
 src/Experiments/ExtrHaskellNats.v
 src/Experiments/GenericFieldPow.v
 src/ModularArithmetic/Conversion.v
@@ -211,9 +208,7 @@ src/Reflection/Z/Syntax/Util.v
 src/Spec/CompleteEdwardsCurve.v
 src/Spec/Ed25519.v
 src/Spec/EdDSA.v
-src/Spec/Encoding.v
 src/Spec/ModularArithmetic.v
-src/Spec/ModularWordEncoding.v
 src/Spec/MontgomeryCurve.v
 src/Spec/MxDH.v
 src/Spec/WeierstrassCurve.v
diff --git a/src/Encoding/EncodingTheorems.v b/src/Encoding/EncodingTheorems.v
deleted file mode 100644
index c6f48a0ab..000000000
--- a/src/Encoding/EncodingTheorems.v
+++ /dev/null
@@ -1,14 +0,0 @@
-Require Import Crypto.Spec.Encoding.
-
-Section EncodingTheorems.
-  Context {A B : Type} {E : canonical encoding of A as B}.
-
-  Lemma encoding_inj : forall x y, enc x = enc y -> x = y.
-  Proof.
-    intros.
-    assert (dec (enc x) = dec (enc y)) as dec_enc_eq by (f_equal; auto).
-    do 2 rewrite encoding_valid in dec_enc_eq.
-    inversion dec_enc_eq; auto.
-  Qed.
-
-End EncodingTheorems.
diff --git a/src/Encoding/ModularWordEncodingPre.v b/src/Encoding/ModularWordEncodingPre.v
deleted file mode 100644
index 874bfdc9d..000000000
--- a/src/Encoding/ModularWordEncodingPre.v
+++ /dev/null
@@ -1,45 +0,0 @@
-Require Import Coq.ZArith.ZArith.
-Require Import Coq.Numbers.Natural.Peano.NPeano.
-Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
-Require Import Bedrock.Word.
-Require Import Crypto.Tactics.VerdiTactics.
-Require Import Crypto.Util.ZUtil Crypto.Util.WordUtil.
-Require Import Crypto.Spec.Encoding.
-
-Local Open Scope nat_scope.
-
-Section ModularWordEncodingPre.
-  Context {m : positive} {sz : nat} {m_pos : (0 < m)%Z} {bound_check : Z.to_nat m < 2 ^ sz}.
-
-  Let Fm_enc (x : F m) : word sz := NToWord sz (Z.to_N (F.to_Z x)).
-
-  Let Fm_dec (x_ : word sz) : option (F m) :=
-    let z := Z.of_N (wordToN (x_)) in
-    if Z_lt_dec z m
-      then Some (F.of_Z m z)
-      else None
-  .
-
-  Lemma Fm_encoding_valid : forall x, Fm_dec (Fm_enc x) = Some x.
-  Proof using bound_check m_pos.
-    unfold Fm_dec, Fm_enc; intros.
-    pose proof (F.to_Z_range x m_pos).
-    rewrite wordToN_NToWord_idempotent by (apply bound_check_nat_N;
-     assert (Z.to_nat (F.to_Z x) < Z.to_nat m) by (apply Z2Nat.inj_lt; omega); omega).
-    rewrite Z2N.id by omega.
-    rewrite F.of_Z_to_Z.
-    break_if; auto; omega.
-  Qed.
-
-  Lemma Fm_encoding_canonical : forall w x, Fm_dec w = Some x -> Fm_enc x = w.
-  Proof using bound_check.
-    unfold Fm_dec, Fm_enc; intros ? ? dec_Some.
-    break_if; [ | congruence ].
-    inversion dec_Some.
-    rewrite F.to_Z_of_Z.
-    rewrite Z.mod_small by (pose proof (N2Z.is_nonneg (wordToN w)); try omega).
-    rewrite N2Z.id.
-    apply NToWord_wordToN.
-  Qed.
-
-End ModularWordEncodingPre.
diff --git a/src/Encoding/ModularWordEncodingTheorems.v b/src/Encoding/ModularWordEncodingTheorems.v
deleted file mode 100644
index 81d4fc5d3..000000000
--- a/src/Encoding/ModularWordEncodingTheorems.v
+++ /dev/null
@@ -1,46 +0,0 @@
-Require Import Coq.ZArith.ZArith Coq.ZArith.Znumtheory.
-Require Import Coq.Numbers.Natural.Peano.NPeano.
-Require Import Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems.
-Require Import Crypto.ModularArithmetic.PrimeFieldTheorems Crypto.ModularArithmetic.ModularArithmeticTheorems.
-Require Import Bedrock.Word.
-Require Import Crypto.Spec.Encoding.
-Require Import Crypto.Util.ZUtil.
-Require Import Crypto.Util.Tactics.SpecializeBy.
-Require Import Crypto.Util.FixCoqMistakes.
-Require Import Crypto.Spec.ModularWordEncoding.
-
-
-Local Open Scope F_scope.
-
-Section SignBit.
-  Context {m : positive} {prime_m : prime m} {two_lt_m : (2 < m)%Z} {sz : nat} {bound_check : (Z.to_nat m < 2 ^ sz)%nat}.
-
-  Lemma sign_bit_parity : forall x, @sign_bit m sz x = Z.odd (F.to_Z x).
-  Proof using Type*.
-    unfold sign_bit, Fm_enc; intros.
-    pose proof (shatter_word (NToWord sz (Z.to_N (F.to_Z x)))) as shatter.
-    case_eq sz; intros; subst; rewrite shatter.
-    + pose proof (prime_ge_2 m prime_m).
-      simpl in bound_check.
-      assert (m < 1)%Z by (apply Z2Nat.inj_lt; try omega; assumption).
-      omega.
-    + assert (0 < m)%Z as m_pos by (pose proof prime_ge_2 m prime_m; omega).
-      pose proof (F.to_Z_range x m_pos).
-      destruct (F.to_Z x); auto.
-      - destruct p; auto.
-      - pose proof (Pos2Z.neg_is_neg p); omega.
-   Qed.
-
-  Lemma sign_bit_zero : @sign_bit m sz 0 = false.
-  Proof using Type*.
-    rewrite sign_bit_parity; auto.
-  Qed.
-
-  Lemma sign_bit_opp (x : F m) (Hnz:x <> 0) : negb (@sign_bit m sz x) = @sign_bit m sz (F.opp x).
-  Proof using Type*.
-    pose proof F.to_Z_nonzero_range x Hnz; specialize_by omega.
-    rewrite !sign_bit_parity, F.to_Z_opp, Z_mod_nz_opp_full, Zmod_small,
-      Z.odd_sub, (NumTheoryUtil.p_odd m), (Bool.xorb_true_l (Z.odd (F.to_Z x)));
-      try eapply Zrel_prime_neq_mod_0, rel_prime_le_prime; intuition omega.
-  Qed.
-End SignBit.
diff --git a/src/Spec/Encoding.v b/src/Spec/Encoding.v
deleted file mode 100644
index b063b638f..000000000
--- a/src/Spec/Encoding.v
+++ /dev/null
@@ -1,8 +0,0 @@
-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 "'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
deleted file mode 100644
index 5b0bdb545..000000000
--- a/src/Spec/ModularWordEncoding.v
+++ /dev/null
@@ -1,40 +0,0 @@
-Require Import Coq.ZArith.ZArith.
-Require Import Coq.Numbers.Natural.Peano.NPeano.
-Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
-Require Import Bedrock.Word.
-Require Import Crypto.Tactics.VerdiTactics.
-Require Import Crypto.Util.NatUtil.
-Require Import Crypto.Util.WordUtil.
-Require Import Crypto.Spec.Encoding.
-Require Crypto.Encoding.ModularWordEncodingPre.
-
-Local Open Scope nat_scope.
-
-Section ModularWordEncoding.
-  Context {m : positive} {sz : nat} {m_pos : (0 < m)%Z} {bound_check : Z.to_nat m < 2 ^ sz}.
-
-  Definition Fm_enc (x : F m) : word sz := NToWord sz (Z.to_N (F.to_Z x)).
-
-  Definition Fm_dec (x_ : word sz) : option (F m) :=
-    let z := Z.of_N (wordToN (x_)) in
-    if Z_lt_dec z m
-      then Some (F.of_Z m z)
-      else None
-  .
-
-  Definition sign_bit (x : F m) :=
-  match (Fm_enc x) with
-    | Word.WO => false
-    | Word.WS b _ w' => b
-  end.
-
-  Global Instance modular_word_encoding : canonical encoding of F m as word sz := {
-    enc := Fm_enc;
-    dec := Fm_dec;
-    encoding_valid :=
-      @ModularWordEncodingPre.Fm_encoding_valid m sz m_pos bound_check;
-    encoding_canonical :=
-      @ModularWordEncodingPre.Fm_encoding_canonical m sz bound_check
-  }.
-
-End ModularWordEncoding.
-\ No newline at end of file