blob: bc28cccb01ebbc9247fbc09efec89e75f4d5cb7b (
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
|
Require Import Coq.ZArith.ZArith.
Require Import Coq.Lists.List.
Local Open Scope Z_scope.
Require Import Crypto.Algebra.
Require Import Crypto.NewBaseSystem.
Require Import Crypto.Util.FixedWordSizes.
Require Import Crypto.Specific.NewBaseSystemTest.
Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
Require Import Crypto.Util.Tuple Crypto.Util.Notations Crypto.Util.ZRange.
Import ListNotations.
Section Pre.
Definition BoundedWord n (bitwidth : nat)
(bounds : tuple zrange n) : Type :=
{ x : tuple (wordT bitwidth) n
| is_bounded_by (Some (Z.of_nat bitwidth)) bounds
(map wordToZ x)}.
Definition BoundedWordToZ n w b (BW :BoundedWord n w b)
: tuple Z n := map wordToZ (proj1_sig BW).
End Pre.
Section BoundedField25p5.
Local Coercion Z.of_nat : nat >-> Z.
(* TODO(jgross) : what goes here? *)
Let bounds: tuple zrange 10 := repeat (Build_zrange 0 (2^32)) 10.
Let feZ : Type := tuple Z 10.
Let feW : Type := tuple word32 10.
Let feBW : Type := BoundedWord 10 32 bounds.
Let phi : feBW -> F m :=
fun x => B.Positional.Fdecode wt (BoundedWordToZ _ _ _ x).
(* TODO : change this to field once field isomorphism happens *)
Definition mul :
{ mul : feBW -> feBW -> feBW
| forall a b, phi (mul a b) = (phi a * phi b)%F }.
Proof.
eexists; intros. cbv [phi].
destruct mul_sig as [mulZ phi_mulZ].
rewrite <-phi_mulZ.
apply f_equal.
(* jgross start here! *)
Admitted.
End BoundedField25p5.
|
