diff options
author | jadep <jade.philipoom@gmail.com> | 2016-04-25 19:07:38 -0400 |
---|---|---|
committer | jadep <jade.philipoom@gmail.com> | 2016-04-25 19:07:38 -0400 |
commit | 6c3c953d836ac43a8acff1975d73eb3204902ef2 (patch) | |
tree | 568f815a4ef0715c8bf0cc91e0e318a2151137ec /src/Encoding/ModularWordEncodingPre.v | |
parent | b9c8f539cf3e9f9fdcd6861ef9691fe079bcd321 (diff) |
Reorganization and revision of Encoding code and redefinition of sign_bit function.
Diffstat (limited to 'src/Encoding/ModularWordEncodingPre.v')
-rw-r--r-- | src/Encoding/ModularWordEncodingPre.v | 53 |
1 files changed, 53 insertions, 0 deletions
diff --git a/src/Encoding/ModularWordEncodingPre.v b/src/Encoding/ModularWordEncodingPre.v new file mode 100644 index 000000000..272748103 --- /dev/null +++ b/src/Encoding/ModularWordEncodingPre.v @@ -0,0 +1,53 @@ +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. + +Local Open Scope nat_scope. + +Section ModularWordEncodingPre. + Context {m : Z} {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 (FieldToZ 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 (ZToField z) + else None + . + + (* TODO : move to ZUtil *) + Lemma bound_check_N : forall x : F m, (Z.to_N x < Npow2 sz)%N. + Proof. + intro. + pose proof (FieldToZ_range x m_pos) as x_range. + rewrite <- Nnat.N2Nat.id. + rewrite Npow2_nat. + replace (Z.to_N x) with (N.of_nat (Z.to_nat x)) by apply Z_nat_N. + apply (Nat2N_inj_lt _ (pow2 sz)). + rewrite Zpow_pow2. + destruct x_range as [x_low x_high]. + apply Z2Nat.inj_lt in x_high; try omega. + rewrite <- ZUtil.pow_Z2N_Zpow by omega. + replace (Z.to_nat 2) with 2%nat by auto. + omega. + Qed. + + Lemma Fm_encoding_valid : forall x, Fm_dec (Fm_enc x) = Some x. + Proof. + unfold Fm_dec, Fm_enc; intros. + pose proof (FieldToZ_range x m_pos). + rewrite wordToN_nat, NToWord_nat. + rewrite wordToNat_natToWord_idempotent by + (rewrite Nnat.N2Nat.id; apply bound_check_N). + rewrite Nnat.N2Nat.id, Z2N.id by omega. + rewrite ZToField_idempotent. + break_if; auto; omega. + Qed. + +End ModularWordEncodingPre. |