diff options
author | Andres Erbsen <andreser@mit.edu> | 2017-04-06 13:20:46 -0400 |
---|---|---|
committer | Andres Erbsen <andreser@mit.edu> | 2017-04-06 13:20:46 -0400 |
commit | 2adac8f52dcd9ee88f98ce9ec604eaaa9c6a115f (patch) | |
tree | b289ae0a3f4279e621610163acd44ca5431e79c7 | |
parent | 6763db2413fe56661fa5113bd981c42bc42f2ca8 (diff) |
remove Encoding stuff
-rw-r--r-- | _CoqProject | 5 | ||||
-rw-r--r-- | src/Encoding/EncodingTheorems.v | 14 | ||||
-rw-r--r-- | src/Encoding/ModularWordEncodingPre.v | 45 | ||||
-rw-r--r-- | src/Encoding/ModularWordEncodingTheorems.v | 46 | ||||
-rw-r--r-- | src/Spec/Encoding.v | 8 | ||||
-rw-r--r-- | src/Spec/ModularWordEncoding.v | 40 |
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 |