From 2adac8f52dcd9ee88f98ce9ec604eaaa9c6a115f Mon Sep 17 00:00:00 2001
From: Andres Erbsen <andreser@mit.edu>
Date: Thu, 6 Apr 2017 13:20:46 -0400
Subject: remove Encoding stuff

---
 src/Spec/Encoding.v            |  8 --------
 src/Spec/ModularWordEncoding.v | 40 ----------------------------------------
 2 files changed, 48 deletions(-)
 delete mode 100644 src/Spec/Encoding.v
 delete mode 100644 src/Spec/ModularWordEncoding.v

(limited to 'src/Spec')

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
-- 
cgit v1.2.3