blob: acd2bedbd1b7792dd4ab8abc0cc9e98fe3ad3511 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
|
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
.
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.
|
