blob: 4005adc2a66f9322f170af4b02e4108c7c958b09 (
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
41
42
43
44
45
46
47
48
49
50
51
52
|
Require Import Crypto.Galois.Galois Crypto.Galois.GaloisTheory.
Module GFBits (M: Modulus).
Module T := GaloisTheory Modulus31.
Import M T T.Field.
Local Open Scope GF_scope.
Definition wordSize: nat := 32.
Definition bits {k} (word k) := k.
(* I think we shouldn't fix this, but rather have a lemma for how
* many bits we need to represent a given prime *)
Definition numWords: nat :=
let b := (bits (NtoWord (Z.to_N modulus)))
in (1 + b / 32)%nat.
Definition BinGF :=
{lst: list (word wordSize) | length lst = numWords}.
Fixpoint splitWords {sz} (len: nat) (x: word sz): {x: list (word wordSize) | length x = len} :=
match len with
| O => []
| S len' =>
if(sz - wordSize >? 0)
then Cons (split1 wordSize (sz - wordSize) x)
(splitWords len' (split2 wordSize (sz - wordSize) x))
else zext x wordSize
end.
Fixpoint combineAll (b: BinGF) :=
match (proj1_sig b) with
| [] => natToWord 0
| Cons x xs => combine x (combineAll xs)
end.
wordEq a b := wordToN (combineAll a) = wordToN (combineAll b)
Definition toZ (b: BinGF) := Z.of_N (wordToN (combineAll b)).
Definition toGF (b: BinGF) := ZToGF ((toZ b) mod modulus)
Definition fromZ (x: Z) := splitWords numWords (NToWord (Z.to_N x))
Definition fromGF (x: GF) := fromZ (proj1_sig x).
toZ a + toZ b = toZ (a ^+ b)
Lemma equivalent_GF : BinEquiv x y <-> x = toGF y.
Admitted.
Lemma equivalent_word : BinEquiv x y <-> weq y (fromGF x).
Admitted.
End GFBits.
|
