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
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
let build_array init next len =
let xi = ref init in
Array.init len (fun _ ->
let i = !xi in
xi := next !xi;
i)
let inner_product ~add ~mul v w =
let rec aux acc = function
| _, [] -> acc
| a :: v', b :: w' -> aux (add acc (mul a b)) (v', w')
| _ -> failwith "inner_product: first is shorter than second"
in
aux List.(mul (hd v) (hd w)) List.(tl v, tl w)
let read_vector a_size a_of_bytes len file =
let read_element ic bytes_buf =
Stdlib.really_input ic bytes_buf 0 a_size;
a_of_bytes bytes_buf
in
let ic = open_in file in
try
if in_channel_length ic < len * a_size then
failwith "Buffer is smaller than requested vector length";
let bytes_buf = Bytes.create a_size in
let vector = List.init len (fun _ -> read_element ic bytes_buf) in
close_in ic;
vector
with error ->
close_in ic;
raise error
let export_vector a_to_bytes vector file =
let oc = open_out_bin file in
List.iter (fun a -> output_bytes oc (a_to_bytes a)) vector;
close_out oc
let import_srs_g2 d srsfile =
let g2_size_compressed = Bls12_381.G2.size_in_bytes / 2 in
let buf = Bytes.create g2_size_compressed in
let read ic =
Stdlib.really_input ic buf 0 g2_size_compressed;
Bls12_381.G2.of_compressed_bytes_exn buf
in
let ic = open_in srsfile in
try
if in_channel_length ic < d * g2_size_compressed then
failwith (Printf.sprintf "SRS asked (%d) too big for %s" d srsfile);
let res = Array.init d (fun _ -> read ic) in
close_in ic;
res
with e ->
close_in ic;
raise e
module Hash : sig
type state
val init : unit -> state
val update : state -> bytes -> unit
val finish : state -> bytes
val hash_bytes : bytes list -> bytes
val bytes_to_seed : bytes -> int array * bytes
end = struct
type state = Hacl_star.EverCrypt.Hash.t
let init () =
Hacl_star.EverCrypt.Hash.init ~alg:Hacl_star.SharedDefs.HashDefs.BLAKE2b
let update st msg = Hacl_star.EverCrypt.Hash.update ~st ~msg
let finish st = Hacl_star.EverCrypt.Hash.finish ~st
let hash_bytes bytes =
let blake2b msg =
let digest_size = 32 in
let open Hacl_star in
if AutoConfig2.(has_feature VEC256) then
Hacl.Blake2b_256.hash msg digest_size
else Hacl.Blake2b_32.hash msg digest_size
in
blake2b (Bytes.concat Bytes.empty bytes)
let bytes_to_seed b =
let hashed_b = hash_bytes [ b ] in
assert (Bytes.length hashed_b = 32);
let sys_int_size = Sys.int_size - 1 in
let modulo = Z.pow (Z.of_int 2) sys_int_size in
let n0_raw = Z.of_bits (Bytes.sub_string hashed_b 0 8) in
let n0 = Z.to_int (Z.erem n0_raw modulo) in
let n1_raw = Z.of_bits (Bytes.sub_string hashed_b 8 8) in
let n1 = Z.to_int (Z.erem n1_raw modulo) in
let n2_raw = Z.of_bits (Bytes.sub_string hashed_b 16 8) in
let n2 = Z.to_int (Z.erem n2_raw modulo) in
let n3_raw = Z.of_bits (Bytes.sub_string hashed_b 24 8) in
let n3 = Z.to_int (Z.erem n3_raw modulo) in
([| n0; n1; n2; n3 |], hashed_b)
end
let list_expand_transcript ~to_bytes transcript list =
let open Hash in
let st = init () in
update st transcript;
List.iter (fun a -> update st (to_bytes a)) list;
finish st
let expand_transcript : to_bytes:('a -> bytes) -> bytes -> 'a -> bytes =
fun ~to_bytes transcript x -> list_expand_transcript ~to_bytes transcript [ x ]
let pad array final_size =
let size = Array.length array in
Array.init final_size (fun i ->
if i < size then array.(i) else array.(size - 1))
let array_resize array final_size =
let size = Array.length array in
if size = final_size then array
else if size > final_size then Array.sub array 0 final_size
else pad array final_size