remove Encoding stuff

3 files changed, 0 insertions, 105 deletions

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.