blob: 19450f83129ae5f2db9dfb196703a86d65346205 (
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
|
(*** Implementing ℤ-Like via Architecture *)
Require Import Coq.ZArith.ZArith.
Require Import Crypto.LegacyArithmetic.Interface.
Require Import Crypto.LegacyArithmetic.Double.Core.
Require Import Crypto.LegacyArithmetic.ZBounded.
Require Import Crypto.Util.Tuple.
Require Import Crypto.Util.LetIn.
Local Open Scope Z_scope.
Section fancy_machine_p256_montgomery_foundation.
Context {n_over_two : Z}.
Local Notation n := (2 * n_over_two).
Context (ops : fancy_machine.instructions n) (modulus : Z).
Local Instance ZLikeOps_of_ArchitectureBoundedOps_Factored (smaller_bound_exp : Z)
ldi_modulus ldi_0
: ZLikeOps (2^n) (2^smaller_bound_exp) modulus :=
{ LargeT := tuple fancy_machine.W 2;
SmallT := fancy_machine.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 := addm y (ldi_0) (ldi_modulus) }.
Global Instance ZLikeOps_of_ArchitectureBoundedOps (smaller_bound_exp : Z)
: ZLikeOps (2^n) (2^smaller_bound_exp) modulus :=
@ZLikeOps_of_ArchitectureBoundedOps_Factored smaller_bound_exp (ldi modulus) (ldi 0).
End fancy_machine_p256_montgomery_foundation.
|
