summaryrefslogtreecommitdiff
path: root/tests/fstar/hashmap/Hashmap.Funs.fst
blob: 0e991720354c3aaedb287c81d5ef3014b504ec56 (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
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
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
(** [hashmap]: function definitions *)
module Hashmap.Funs
open Primitives
include Hashmap.Types
include Hashmap.FunsExternal
include Hashmap.Clauses

#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"

(** [hashmap::hash_key]:
    Source: 'tests/src/hashmap.rs', lines 37:0-37:32 *)
let hash_key (k : usize) : result usize =
  Ok k

(** [hashmap::{hashmap::HashMap<T>}::allocate_slots]: loop 0:
    Source: 'tests/src/hashmap.rs', lines 60:4-66:5 *)
let rec hashMap_allocate_slots_loop
  (t : Type0) (slots : alloc_vec_Vec (list_t t)) (n : usize) :
  Tot (result (alloc_vec_Vec (list_t t)))
  (decreases (hashMap_allocate_slots_loop_decreases t slots n))
  =
  if n > 0
  then
    let* slots1 = alloc_vec_Vec_push (list_t t) slots List_Nil in
    let* n1 = usize_sub n 1 in
    hashMap_allocate_slots_loop t slots1 n1
  else Ok slots

(** [hashmap::{hashmap::HashMap<T>}::allocate_slots]:
    Source: 'tests/src/hashmap.rs', lines 60:4-60:76 *)
let hashMap_allocate_slots
  (t : Type0) (slots : alloc_vec_Vec (list_t t)) (n : usize) :
  result (alloc_vec_Vec (list_t t))
  =
  hashMap_allocate_slots_loop t slots n

(** [hashmap::{hashmap::HashMap<T>}::new_with_capacity]:
    Source: 'tests/src/hashmap.rs', lines 69:4-73:13 *)
let hashMap_new_with_capacity
  (t : Type0) (capacity : usize) (max_load_dividend : usize)
  (max_load_divisor : usize) :
  result (hashMap_t t)
  =
  let* slots = hashMap_allocate_slots t (alloc_vec_Vec_new (list_t t)) capacity
    in
  let* i = usize_mul capacity max_load_dividend in
  let* i1 = usize_div i max_load_divisor in
  Ok
    {
      num_entries = 0;
      max_load_factor = (max_load_dividend, max_load_divisor);
      max_load = i1;
      slots = slots
    }

(** [hashmap::{hashmap::HashMap<T>}::new]:
    Source: 'tests/src/hashmap.rs', lines 85:4-85:24 *)
let hashMap_new (t : Type0) : result (hashMap_t t) =
  hashMap_new_with_capacity t 32 4 5

(** [hashmap::{hashmap::HashMap<T>}::clear]: loop 0:
    Source: 'tests/src/hashmap.rs', lines 90:4-98:5 *)
let rec hashMap_clear_loop
  (t : Type0) (slots : alloc_vec_Vec (list_t t)) (i : usize) :
  Tot (result (alloc_vec_Vec (list_t t)))
  (decreases (hashMap_clear_loop_decreases t slots i))
  =
  let i1 = alloc_vec_Vec_len (list_t t) slots in
  if i < i1
  then
    let* (_, index_mut_back) =
      alloc_vec_Vec_index_mut (list_t t) usize
        (core_slice_index_SliceIndexUsizeSliceTInst (list_t t)) slots i in
    let* i2 = usize_add i 1 in
    let* slots1 = index_mut_back List_Nil in
    hashMap_clear_loop t slots1 i2
  else Ok slots

(** [hashmap::{hashmap::HashMap<T>}::clear]:
    Source: 'tests/src/hashmap.rs', lines 90:4-90:27 *)
let hashMap_clear (t : Type0) (self : hashMap_t t) : result (hashMap_t t) =
  let* hm = hashMap_clear_loop t self.slots 0 in
  Ok { self with num_entries = 0; slots = hm }

(** [hashmap::{hashmap::HashMap<T>}::len]:
    Source: 'tests/src/hashmap.rs', lines 100:4-100:30 *)
let hashMap_len (t : Type0) (self : hashMap_t t) : result usize =
  Ok self.num_entries

(** [hashmap::{hashmap::HashMap<T>}::insert_in_list]: loop 0:
    Source: 'tests/src/hashmap.rs', lines 107:4-124:5 *)
let rec hashMap_insert_in_list_loop
  (t : Type0) (key : usize) (value : t) (ls : list_t t) :
  Tot (result (bool & (list_t t)))
  (decreases (hashMap_insert_in_list_loop_decreases t key value ls))
  =
  begin match ls with
  | List_Cons ckey cvalue tl ->
    if ckey = key
    then Ok (false, List_Cons ckey value tl)
    else
      let* (b, tl1) = hashMap_insert_in_list_loop t key value tl in
      Ok (b, List_Cons ckey cvalue tl1)
  | List_Nil -> Ok (true, List_Cons key value List_Nil)
  end

(** [hashmap::{hashmap::HashMap<T>}::insert_in_list]:
    Source: 'tests/src/hashmap.rs', lines 107:4-107:71 *)
let hashMap_insert_in_list
  (t : Type0) (key : usize) (value : t) (ls : list_t t) :
  result (bool & (list_t t))
  =
  hashMap_insert_in_list_loop t key value ls

(** [hashmap::{hashmap::HashMap<T>}::insert_no_resize]:
    Source: 'tests/src/hashmap.rs', lines 127:4-127:54 *)
let hashMap_insert_no_resize
  (t : Type0) (self : hashMap_t t) (key : usize) (value : t) :
  result (hashMap_t t)
  =
  let* hash = hash_key key in
  let i = alloc_vec_Vec_len (list_t t) self.slots in
  let* hash_mod = usize_rem hash i in
  let* (l, index_mut_back) =
    alloc_vec_Vec_index_mut (list_t t) usize
      (core_slice_index_SliceIndexUsizeSliceTInst (list_t t)) self.slots
      hash_mod in
  let* (inserted, l1) = hashMap_insert_in_list t key value l in
  if inserted
  then
    let* i1 = usize_add self.num_entries 1 in
    let* v = index_mut_back l1 in
    Ok { self with num_entries = i1; slots = v }
  else let* v = index_mut_back l1 in Ok { self with slots = v }

(** [hashmap::{hashmap::HashMap<T>}::move_elements_from_list]: loop 0:
    Source: 'tests/src/hashmap.rs', lines 193:4-206:5 *)
let rec hashMap_move_elements_from_list_loop
  (t : Type0) (ntable : hashMap_t t) (ls : list_t t) :
  Tot (result (hashMap_t t))
  (decreases (hashMap_move_elements_from_list_loop_decreases t ntable ls))
  =
  begin match ls with
  | List_Cons k v tl ->
    let* ntable1 = hashMap_insert_no_resize t ntable k v in
    hashMap_move_elements_from_list_loop t ntable1 tl
  | List_Nil -> Ok ntable
  end

(** [hashmap::{hashmap::HashMap<T>}::move_elements_from_list]:
    Source: 'tests/src/hashmap.rs', lines 193:4-193:72 *)
let hashMap_move_elements_from_list
  (t : Type0) (ntable : hashMap_t t) (ls : list_t t) : result (hashMap_t t) =
  hashMap_move_elements_from_list_loop t ntable ls

(** [hashmap::{hashmap::HashMap<T>}::move_elements]: loop 0:
    Source: 'tests/src/hashmap.rs', lines 181:4-190:5 *)
let rec hashMap_move_elements_loop
  (t : Type0) (ntable : hashMap_t t) (slots : alloc_vec_Vec (list_t t))
  (i : usize) :
  Tot (result ((hashMap_t t) & (alloc_vec_Vec (list_t t))))
  (decreases (hashMap_move_elements_loop_decreases t ntable slots i))
  =
  let i1 = alloc_vec_Vec_len (list_t t) slots in
  if i < i1
  then
    let* (l, index_mut_back) =
      alloc_vec_Vec_index_mut (list_t t) usize
        (core_slice_index_SliceIndexUsizeSliceTInst (list_t t)) slots i in
    let (ls, l1) = core_mem_replace (list_t t) l List_Nil in
    let* ntable1 = hashMap_move_elements_from_list t ntable ls in
    let* i2 = usize_add i 1 in
    let* slots1 = index_mut_back l1 in
    hashMap_move_elements_loop t ntable1 slots1 i2
  else Ok (ntable, slots)

(** [hashmap::{hashmap::HashMap<T>}::move_elements]:
    Source: 'tests/src/hashmap.rs', lines 181:4-181:95 *)
let hashMap_move_elements
  (t : Type0) (ntable : hashMap_t t) (slots : alloc_vec_Vec (list_t t))
  (i : usize) :
  result ((hashMap_t t) & (alloc_vec_Vec (list_t t)))
  =
  hashMap_move_elements_loop t ntable slots i

(** [hashmap::{hashmap::HashMap<T>}::try_resize]:
    Source: 'tests/src/hashmap.rs', lines 150:4-150:28 *)
let hashMap_try_resize
  (t : Type0) (self : hashMap_t t) : result (hashMap_t t) =
  let* max_usize = scalar_cast U32 Usize core_u32_max in
  let capacity = alloc_vec_Vec_len (list_t t) self.slots in
  let* n1 = usize_div max_usize 2 in
  let (i, i1) = self.max_load_factor in
  let* i2 = usize_div n1 i in
  if capacity <= i2
  then
    let* i3 = usize_mul capacity 2 in
    let* ntable = hashMap_new_with_capacity t i3 i i1 in
    let* p = hashMap_move_elements t ntable self.slots 0 in
    let (ntable1, _) = p in
    Ok
      { ntable1 with num_entries = self.num_entries; max_load_factor = (i, i1)
      }
  else Ok { self with max_load_factor = (i, i1) }

(** [hashmap::{hashmap::HashMap<T>}::insert]:
    Source: 'tests/src/hashmap.rs', lines 139:4-139:48 *)
let hashMap_insert
  (t : Type0) (self : hashMap_t t) (key : usize) (value : t) :
  result (hashMap_t t)
  =
  let* self1 = hashMap_insert_no_resize t self key value in
  let* i = hashMap_len t self1 in
  if i > self1.max_load then hashMap_try_resize t self1 else Ok self1

(** [hashmap::{hashmap::HashMap<T>}::contains_key_in_list]: loop 0:
    Source: 'tests/src/hashmap.rs', lines 216:4-229:5 *)
let rec hashMap_contains_key_in_list_loop
  (t : Type0) (key : usize) (ls : list_t t) :
  Tot (result bool)
  (decreases (hashMap_contains_key_in_list_loop_decreases t key ls))
  =
  begin match ls with
  | List_Cons ckey _ tl ->
    if ckey = key then Ok true else hashMap_contains_key_in_list_loop t key tl
  | List_Nil -> Ok false
  end

(** [hashmap::{hashmap::HashMap<T>}::contains_key_in_list]:
    Source: 'tests/src/hashmap.rs', lines 216:4-216:68 *)
let hashMap_contains_key_in_list
  (t : Type0) (key : usize) (ls : list_t t) : result bool =
  hashMap_contains_key_in_list_loop t key ls

(** [hashmap::{hashmap::HashMap<T>}::contains_key]:
    Source: 'tests/src/hashmap.rs', lines 209:4-209:49 *)
let hashMap_contains_key
  (t : Type0) (self : hashMap_t t) (key : usize) : result bool =
  let* hash = hash_key key in
  let i = alloc_vec_Vec_len (list_t t) self.slots in
  let* hash_mod = usize_rem hash i in
  let* l =
    alloc_vec_Vec_index (list_t t) usize
      (core_slice_index_SliceIndexUsizeSliceTInst (list_t t)) self.slots
      hash_mod in
  hashMap_contains_key_in_list t key l

(** [hashmap::{hashmap::HashMap<T>}::get_in_list]: loop 0:
    Source: 'tests/src/hashmap.rs', lines 234:4-247:5 *)
let rec hashMap_get_in_list_loop
  (t : Type0) (key : usize) (ls : list_t t) :
  Tot (result t) (decreases (hashMap_get_in_list_loop_decreases t key ls))
  =
  begin match ls with
  | List_Cons ckey cvalue tl ->
    if ckey = key then Ok cvalue else hashMap_get_in_list_loop t key tl
  | List_Nil -> Fail Failure
  end

(** [hashmap::{hashmap::HashMap<T>}::get_in_list]:
    Source: 'tests/src/hashmap.rs', lines 234:4-234:70 *)
let hashMap_get_in_list (t : Type0) (key : usize) (ls : list_t t) : result t =
  hashMap_get_in_list_loop t key ls

(** [hashmap::{hashmap::HashMap<T>}::get]:
    Source: 'tests/src/hashmap.rs', lines 249:4-249:55 *)
let hashMap_get (t : Type0) (self : hashMap_t t) (key : usize) : result t =
  let* hash = hash_key key in
  let i = alloc_vec_Vec_len (list_t t) self.slots in
  let* hash_mod = usize_rem hash i in
  let* l =
    alloc_vec_Vec_index (list_t t) usize
      (core_slice_index_SliceIndexUsizeSliceTInst (list_t t)) self.slots
      hash_mod in
  hashMap_get_in_list t key l

(** [hashmap::{hashmap::HashMap<T>}::get_mut_in_list]: loop 0:
    Source: 'tests/src/hashmap.rs', lines 255:4-264:5 *)
let rec hashMap_get_mut_in_list_loop
  (t : Type0) (ls : list_t t) (key : usize) :
  Tot (result (t & (t -> result (list_t t))))
  (decreases (hashMap_get_mut_in_list_loop_decreases t ls key))
  =
  begin match ls with
  | List_Cons ckey cvalue tl ->
    if ckey = key
    then let back = fun ret -> Ok (List_Cons ckey ret tl) in Ok (cvalue, back)
    else
      let* (x, back) = hashMap_get_mut_in_list_loop t tl key in
      let back1 =
        fun ret -> let* tl1 = back ret in Ok (List_Cons ckey cvalue tl1) in
      Ok (x, back1)
  | List_Nil -> Fail Failure
  end

(** [hashmap::{hashmap::HashMap<T>}::get_mut_in_list]:
    Source: 'tests/src/hashmap.rs', lines 255:4-255:86 *)
let hashMap_get_mut_in_list
  (t : Type0) (ls : list_t t) (key : usize) :
  result (t & (t -> result (list_t t)))
  =
  hashMap_get_mut_in_list_loop t ls key

(** [hashmap::{hashmap::HashMap<T>}::get_mut]:
    Source: 'tests/src/hashmap.rs', lines 267:4-267:67 *)
let hashMap_get_mut
  (t : Type0) (self : hashMap_t t) (key : usize) :
  result (t & (t -> result (hashMap_t t)))
  =
  let* hash = hash_key key in
  let i = alloc_vec_Vec_len (list_t t) self.slots in
  let* hash_mod = usize_rem hash i in
  let* (l, index_mut_back) =
    alloc_vec_Vec_index_mut (list_t t) usize
      (core_slice_index_SliceIndexUsizeSliceTInst (list_t t)) self.slots
      hash_mod in
  let* (x, get_mut_in_list_back) = hashMap_get_mut_in_list t l key in
  let back =
    fun ret ->
      let* l1 = get_mut_in_list_back ret in
      let* v = index_mut_back l1 in
      Ok { self with slots = v } in
  Ok (x, back)

(** [hashmap::{hashmap::HashMap<T>}::remove_from_list]: loop 0:
    Source: 'tests/src/hashmap.rs', lines 275:4-301:5 *)
let rec hashMap_remove_from_list_loop
  (t : Type0) (key : usize) (ls : list_t t) :
  Tot (result ((option t) & (list_t t)))
  (decreases (hashMap_remove_from_list_loop_decreases t key ls))
  =
  begin match ls with
  | List_Cons ckey x tl ->
    if ckey = key
    then
      let (mv_ls, _) =
        core_mem_replace (list_t t) (List_Cons ckey x tl) List_Nil in
      begin match mv_ls with
      | List_Cons _ cvalue tl1 -> Ok (Some cvalue, tl1)
      | List_Nil -> Fail Failure
      end
    else
      let* (o, tl1) = hashMap_remove_from_list_loop t key tl in
      Ok (o, List_Cons ckey x tl1)
  | List_Nil -> Ok (None, List_Nil)
  end

(** [hashmap::{hashmap::HashMap<T>}::remove_from_list]:
    Source: 'tests/src/hashmap.rs', lines 275:4-275:69 *)
let hashMap_remove_from_list
  (t : Type0) (key : usize) (ls : list_t t) :
  result ((option t) & (list_t t))
  =
  hashMap_remove_from_list_loop t key ls

(** [hashmap::{hashmap::HashMap<T>}::remove]:
    Source: 'tests/src/hashmap.rs', lines 304:4-304:52 *)
let hashMap_remove
  (t : Type0) (self : hashMap_t t) (key : usize) :
  result ((option t) & (hashMap_t t))
  =
  let* hash = hash_key key in
  let i = alloc_vec_Vec_len (list_t t) self.slots in
  let* hash_mod = usize_rem hash i in
  let* (l, index_mut_back) =
    alloc_vec_Vec_index_mut (list_t t) usize
      (core_slice_index_SliceIndexUsizeSliceTInst (list_t t)) self.slots
      hash_mod in
  let* (x, l1) = hashMap_remove_from_list t key l in
  begin match x with
  | None -> let* v = index_mut_back l1 in Ok (None, { self with slots = v })
  | Some x1 ->
    let* i1 = usize_sub self.num_entries 1 in
    let* v = index_mut_back l1 in
    Ok (Some x1, { self with num_entries = i1; slots = v })
  end

(** [hashmap::insert_on_disk]:
    Source: 'tests/src/hashmap.rs', lines 335:0-335:43 *)
let insert_on_disk
  (key : usize) (value : u64) (st : state) : result (state & unit) =
  let* (st1, hm) = utils_deserialize st in
  let* hm1 = hashMap_insert u64 hm key value in
  utils_serialize hm1 st1

(** [hashmap::test1]:
    Source: 'tests/src/hashmap.rs', lines 350:0-350:10 *)
let test1 : result unit =
  let* hm = hashMap_new u64 in
  let* hm1 = hashMap_insert u64 hm 0 42 in
  let* hm2 = hashMap_insert u64 hm1 128 18 in
  let* hm3 = hashMap_insert u64 hm2 1024 138 in
  let* hm4 = hashMap_insert u64 hm3 1056 256 in
  let* i = hashMap_get u64 hm4 128 in
  if not (i = 18)
  then Fail Failure
  else
    let* (_, get_mut_back) = hashMap_get_mut u64 hm4 1024 in
    let* hm5 = get_mut_back 56 in
    let* i1 = hashMap_get u64 hm5 1024 in
    if not (i1 = 56)
    then Fail Failure
    else
      let* (x, hm6) = hashMap_remove u64 hm5 1024 in
      begin match x with
      | None -> Fail Failure
      | Some x1 ->
        if not (x1 = 56)
        then Fail Failure
        else
          let* i2 = hashMap_get u64 hm6 0 in
          if not (i2 = 42)
          then Fail Failure
          else
            let* i3 = hashMap_get u64 hm6 128 in
            if not (i3 = 18)
            then Fail Failure
            else
              let* i4 = hashMap_get u64 hm6 1056 in
              if not (i4 = 256) then Fail Failure else Ok ()
      end