blob: 29e777c0e843af60b8280771077e791d73e3a814 (
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
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
|
(*** Implementing ℤ-Like via Architecture *)
Require Import Coq.ZArith.ZArith.
Require Import Crypto.BoundedArithmetic.Interface.
Require Import Crypto.BoundedArithmetic.Double.Core.
Require Import Crypto.BoundedArithmetic.Double.Repeated.Core.
Require Import Crypto.BoundedArithmetic.StripCF.
Require Import Crypto.ModularArithmetic.ZBounded.
Require Import Crypto.Util.Tuple.
Require Import Crypto.Util.LetIn.
Import NPeano.
Local Open Scope Z_scope.
Local Coercion Z.of_nat : nat >-> Z.
Section x86_gen_barrett_foundation.
Context (full_width : nat) (n : nat) (ops : x86.instructions n) (modulus : Z).
Local Notation W := (repeated_tuple x86.W 2 (Nat.log2 (full_width / n))). (* full_width-width words *)
Local Instance ZLikeOps_of_x86_gen_Factored (smaller_bound_exp : Z)
(ldi_modulus ldi_0 : W)
: ZLikeOps (2^full_width) (2^smaller_bound_exp) modulus
:= { LargeT := tuple W 2;
SmallT := W;
modulus_digits := ldi_modulus;
decode_large := decode;
decode_small := decode;
Mod_SmallBound v := fst v;
DivBy_SmallBound v := snd v;
DivBy_SmallerBound v := if smaller_bound_exp =? n
then snd v
else dlet v := v in shrd (snd v) (fst v) smaller_bound_exp;
Mul x y := muldw x y;
CarryAdd x y := adc x y false;
CarrySubSmall x y := subc x y false;
ConditionalSubtract b x := let v := selc b (ldi_modulus) (ldi_0) in snd (subc x v false);
ConditionalSubtractModulus y := dlet y := y in
let (CF, _) := subc y ldi_modulus false in
let maybe_modulus := ldi_0 in
let maybe_modulus := selc CF maybe_modulus ldi_modulus in
let (CF, y) := subc y maybe_modulus false in
y }.
Local Instance ZLikeOps_of_x86_gen (smaller_bound_exp : Z)
: ZLikeOps (2^full_width) (2^smaller_bound_exp) modulus :=
@ZLikeOps_of_x86_gen_Factored smaller_bound_exp (ldi modulus) (ldi 0).
End x86_gen_barrett_foundation.
Section x86_64_barrett_foundation.
Local Notation n := 64%nat.
Context (ops : x86.instructions n) (modulus : Z).
Local Notation W := (tuple (tuple x86.W 2) 2) (* 256-bit words *).
Local Instance ZLikeOps_of_x86_64_Factored (smaller_bound_exp : Z)
ldi_modulus ldi_0
: ZLikeOps (2^256) (2^smaller_bound_exp) modulus
:= @ZLikeOps_of_x86_gen_Factored 256 n ops modulus smaller_bound_exp ldi_modulus ldi_0.
Global Instance ZLikeOps_of_x86_64 (smaller_bound_exp : Z)
: ZLikeOps (2^256) (2^smaller_bound_exp) modulus :=
@ZLikeOps_of_x86_64_Factored smaller_bound_exp (ldi modulus) (ldi 0).
End x86_64_barrett_foundation.
Section x86_32_barrett_foundation.
Local Notation n := 32%nat.
Context (ops : x86.instructions n) (modulus : Z).
Local Notation W := (tuple (tuple (tuple x86.W 2) 2) 2) (* 256-bit words *).
Local Instance ZLikeOps_of_x86_32_Factored (smaller_bound_exp : Z)
ldi_modulus ldi_0
: ZLikeOps (2^256) (2^smaller_bound_exp) modulus
:= @ZLikeOps_of_x86_gen_Factored 256 n ops modulus smaller_bound_exp ldi_modulus ldi_0.
Global Instance ZLikeOps_of_x86_32 (smaller_bound_exp : Z)
: ZLikeOps (2^256) (2^smaller_bound_exp) modulus :=
@ZLikeOps_of_x86_32_Factored smaller_bound_exp (ldi modulus) (ldi 0).
End x86_32_barrett_foundation.
|
