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 /src/Spec | |
parent | 6763db2413fe56661fa5113bd981c42bc42f2ca8 (diff) |
remove Encoding stuff
Diffstat (limited to 'src/Spec')
-rw-r--r-- | src/Spec/Encoding.v | 8 | ||||
-rw-r--r-- | src/Spec/ModularWordEncoding.v | 40 |
2 files changed, 0 insertions, 48 deletions
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 |