aboutsummaryrefslogtreecommitdiff
path: root/src/Spec/ModularWordEncoding.v
diff options
context:
space:
mode:
authorGravatar jadep <jade.philipoom@gmail.com>2016-04-25 19:07:38 -0400
committerGravatar jadep <jade.philipoom@gmail.com>2016-04-25 19:07:38 -0400
commit6c3c953d836ac43a8acff1975d73eb3204902ef2 (patch)
tree568f815a4ef0715c8bf0cc91e0e318a2151137ec /src/Spec/ModularWordEncoding.v
parentb9c8f539cf3e9f9fdcd6861ef9691fe079bcd321 (diff)
Reorganization and revision of Encoding code and redefinition of sign_bit function.
Diffstat (limited to 'src/Spec/ModularWordEncoding.v')
-rw-r--r--src/Spec/ModularWordEncoding.v31
1 files changed, 31 insertions, 0 deletions
diff --git a/src/Spec/ModularWordEncoding.v b/src/Spec/ModularWordEncoding.v
new file mode 100644
index 000000000..9f7e3340b
--- /dev/null
+++ b/src/Spec/ModularWordEncoding.v
@@ -0,0 +1,31 @@
+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 : Z} {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 (FieldToZ 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 (ZToField z)
+ else None
+ .
+
+ Instance modular_word_encoding : 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
+ }.
+
+End ModularWordEncoding.