blob: d71550413944c532a862861a2fade5ab15e2a4f1 (
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 ZArith.BinInt.
Require Import List Util.ListUtil.
Section ScalarMult.
Variable G : Type.
Variable neutral : G.
Variable add : G -> G -> G.
Local Infix "+" := add.
Fixpoint scalarMultSpec (n:nat) (g:G) : G :=
match n with
| O => neutral
| S n' => g + scalarMultSpec n' g
end
.
(* ng =
* (n/2)(g+g) + g if n odd
* (n/2)(g+g) if n even
* g if n == 1
*)
Fixpoint scalarMultPos (n:positive) (g:G) : G :=
match n with
| xI n' => scalarMultPos n' (g + g) + g
| xO n' => scalarMultPos n' (g + g)
| xH => g
end
.
Definition scalarMultNat (n:nat) (g:G) : G :=
match n with
| O => neutral
| S n' => scalarMultPos (Pos.of_succ_nat n') g
end
.
Definition sel {T} (b:bool) (x y:T) := if b then y else x.
Definition scalarMultStaticZ (bitLengthN:nat) (n:Z) (g:G): G :=
fst (fold_right
(fun (i : nat) (s : G * G) => let (Q, P) := s in
let Q' := sel (Z.testbit (Z.of_nat i) n) Q (Q + P) in
let P' := P+P in
(Q', P + P))
(neutral, g) (* initial state *)
(seq 0 bitLengthN)) (* range of i *)
.
End ScalarMult.
|
