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
let build_array init next len =
let xi = ref init in
Array.init len (fun _ ->
let i = !xi in
xi := next !xi;
i)
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
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 repr list transcript =
let open Hash in
let st = init () in
update st transcript;
List.iter (fun a -> update st (Plompiler.Utils.to_bytes repr a)) list;
finish st
let expand_transcript : 'a Repr.t -> 'a -> bytes -> bytes =
fun repr x transcript -> list_expand_transcript repr [ x ] transcript
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