summaryrefslogtreecommitdiff
path: root/tests/hashmap_on_disk/HashmapMain.Properties.fst
blob: 99b5424ad46a11663ced080984dcb51ba6e91cd5 (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
(** Properties about the hashmap written on disk *)
module HashmapMain.Properties
open Primitives
open HashmapMain.Funs

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

/// Below, we focus on the functions to read from disk/write to disk to showcase
/// how such reasoning which mixes opaque functions together with a state-error
/// monad can be performed.

/// Also note that for now, whenever we want to use a state-error monad, we translate
/// all the LLBC functions to pure functions living in the state-error monad (this
/// is the reason why we regenerate all the hash map definitions for this example).
/// 
/// In the future, we will probably do some analysis to use the proper monad when
/// generating the definitions (no monad if functions can't fail, error monad if
/// they can fail but don't need manipulate the state, etc. in addition to proper
/// lifting).


(*** Hypotheses *)

/// [state_v] gives us the hash map currently stored on disk
assume
val state_v : state -> hashmap_hash_map_t u64

/// [serialize] updates the hash map stored on disk
assume
val serialize_lem (hm : hashmap_hash_map_t u64) (st : state) : Lemma (
  match hashmap_utils_serialize_fwd hm st with
  | Fail -> True
  | Return (st', ()) -> state_v st' == hm)
  [SMTPat (hashmap_utils_serialize_fwd hm st)]

/// [deserialize] gives us the hash map stored on disk, without updating it
assume
val deserialize_lem (st : state) : Lemma (
  match hashmap_utils_deserialize_fwd st with
  | Fail -> True
  | Return (st', hm) -> hm == state_v st /\ st' == st)
  [SMTPat (hashmap_utils_deserialize_fwd st)]

(*** Lemmas - auxiliary *)

/// The below proofs are trivial: we just prove that the hashmap insert function
/// doesn't update the state... As F* is made for *intrinsic* proofs, we have to
/// copy-paste the definitions to insert the proper lemma calls wherever needed,
/// hence the verbosity...

#push-options "--fuel 1"
let rec hashmap_hash_map_insert_in_list_fwd_lem
  (t : Type0) (key : usize) (value : t) (ls : hashmap_list_t t) (st : state) :
  Lemma
  (ensures (
    match hashmap_hash_map_insert_in_list_fwd t key value ls st with
    | Fail -> True
    | Return (st', _) -> st' == st))
  (decreases (hashmap_hash_map_insert_in_list_decreases t key value ls st))
  =
  begin match ls with
  | HashmapListCons ckey cvalue ls0 ->
    if ckey = key
    then ()
    else
      hashmap_hash_map_insert_in_list_fwd_lem t key value ls0 st
  | HashmapListNil -> ()
  end
#pop-options

#push-options "--fuel 1"
let rec hashmap_hash_map_insert_in_list_back_lem
  (t : Type0) (key : usize) (value : t) (ls : hashmap_list_t t) (st : state) :
  Lemma
  (ensures (
    match hashmap_hash_map_insert_in_list_back t key value ls st with
    | Fail -> True
    | Return (st', _) -> st' == st))
  (decreases (hashmap_hash_map_insert_in_list_decreases t key value ls st))
  =
  begin match ls with
  | HashmapListCons ckey cvalue ls0 ->
    if ckey = key then ()
    else hashmap_hash_map_insert_in_list_back_lem t key value ls0 st
  | HashmapListNil -> ()
  end
#pop-options

let hashmap_hash_map_insert_no_resize_back_lem
  (t : Type0) (self : hashmap_hash_map_t t) (key : usize) (value : t)
  (st : state) :
  Lemma
  (ensures (
    match hashmap_hash_map_insert_no_resize_back t self key value st with
    | Fail -> True
    | Return (st', _) -> st' == st))
  =
  begin match hashmap_hash_key_fwd key st with
  | Fail -> ()
  | Return (st0, i) ->
    let i0 = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
    begin match usize_rem i i0 with
    | Fail -> ()
    | Return hash_mod ->
      begin match
        vec_index_mut_fwd (hashmap_list_t t) self.hashmap_hash_map_slots
          hash_mod with
      | Fail -> ()
      | Return l ->
        hashmap_hash_map_insert_in_list_fwd_lem t key value l st0;
        begin match hashmap_hash_map_insert_in_list_fwd t key value l st0 with
        | Fail -> ()
        | Return (st1, b) ->
          if b
          then
            begin match usize_add self.hashmap_hash_map_num_entries 1 with
            | Fail -> ()
            | Return i1 -> hashmap_hash_map_insert_in_list_back_lem t key value l st1
            end
          else hashmap_hash_map_insert_in_list_back_lem t key value l st1
        end
      end
    end
  end

#push-options "--fuel 1"
let rec hashmap_hash_map_allocate_slots_fwd_lem
  (t : Type0) (slots : vec (hashmap_list_t t)) (n : usize) (st : state) :
  Lemma (ensures (
    match hashmap_hash_map_allocate_slots_fwd t slots n st with
    | Fail -> True
    | Return (st', _) -> st' == st))
  (decreases (hashmap_hash_map_allocate_slots_decreases t slots n st))
  =
  begin match n with
  | 0 -> ()
  | _ ->
    begin match vec_push_back (hashmap_list_t t) slots HashmapListNil with
    | Fail -> ()
    | Return v ->
      begin match usize_sub n 1 with
      | Fail ->  ()
      | Return i ->
        hashmap_hash_map_allocate_slots_fwd_lem t v i st 
      end
    end
  end
#pop-options

let hashmap_hash_map_new_with_capacity_fwd_lem
  (t : Type0) (capacity : usize) (max_load_dividend : usize)
  (max_load_divisor : usize) (st : state) :
  Lemma (ensures (
    match hashmap_hash_map_new_with_capacity_fwd t capacity max_load_dividend max_load_divisor st with
    | Fail -> True
    | Return (st', _) -> st' == st))
  =
  let v = vec_new (hashmap_list_t t) in
  hashmap_hash_map_allocate_slots_fwd_lem t v capacity st

#push-options "--fuel 1"
let rec hashmap_hash_map_move_elements_from_list_back_lem
  (t : Type0) (ntable : hashmap_hash_map_t t) (ls : hashmap_list_t t)
  (st : state) :
  Lemma (ensures (
    match hashmap_hash_map_move_elements_from_list_back t ntable ls st with
    | Fail -> True
    | Return (st', _) -> st' == st))
  (decreases (hashmap_hash_map_move_elements_from_list_decreases t ntable ls st))
  =
  begin match ls with
  | HashmapListCons k v tl ->
    hashmap_hash_map_insert_no_resize_back_lem t ntable k v st;
    begin match hashmap_hash_map_insert_no_resize_back t ntable k v st with
    | Fail -> ()
    | Return (st0, hm) ->
      hashmap_hash_map_move_elements_from_list_back_lem t hm tl st0
    end
  | HashmapListNil -> ()
  end
#pop-options

#push-options "--fuel 1"
let rec hashmap_hash_map_move_elements_back_lem
  (t : Type0) (ntable : hashmap_hash_map_t t) (slots : vec (hashmap_list_t t))
  (i : usize) (st : state) :
  Lemma (ensures (
    match hashmap_hash_map_move_elements_back t ntable slots i st with
    | Fail -> True
    | Return (st', _) -> st' == st))
  (decreases (hashmap_hash_map_move_elements_decreases t ntable slots i st))
  =
  let i0 = vec_len (hashmap_list_t t) slots in
  if i < i0
  then
    begin match vec_index_mut_fwd (hashmap_list_t t) slots i with
    | Fail -> ()
    | Return l ->
      let l0 = mem_replace_fwd (hashmap_list_t t) l HashmapListNil in
      hashmap_hash_map_move_elements_from_list_back_lem t ntable l0 st;
      begin match hashmap_hash_map_move_elements_from_list_back t ntable l0 st
        with
      | Fail -> ()
      | Return (st0, hm) ->
        let l1 = mem_replace_back (hashmap_list_t t) l HashmapListNil in
        begin match vec_index_mut_back (hashmap_list_t t) slots i l1 with
        | Fail -> ()
        | Return v ->
          begin match usize_add i 1 with
          | Fail -> ()
          | Return i1 -> hashmap_hash_map_move_elements_back_lem t hm v i1 st0
          end
        end
      end
    end
  else ()
#pop-options

let hashmap_hash_map_try_resize_back_lem
  (t : Type0) (self : hashmap_hash_map_t t) (st : state) :
  Lemma (ensures (
    match hashmap_hash_map_try_resize_back t self st with
    | Fail -> True
    | Return (st', _) -> st' == st))
  =
  let i = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
  begin match usize_div 4294967295 2 with
  | Fail -> ()
  | Return n1 ->
    let (i0, i1) = self.hashmap_hash_map_max_load_factor in
    begin match usize_div n1 i0 with
    | Fail -> ()
    | Return i2 ->
      if i <= i2
      then
        begin match usize_mul i 2 with
        | Fail -> ()
        | Return i3 ->
          hashmap_hash_map_new_with_capacity_fwd_lem t i3 i0 i1 st;
          begin match hashmap_hash_map_new_with_capacity_fwd t i3 i0 i1 st with
          | Fail -> ()
          | Return (st0, hm) ->
            hashmap_hash_map_move_elements_back_lem t hm self.hashmap_hash_map_slots 0 st0
          end
        end
      else ()
    end
  end

let hashmap_hash_map_insert_back_lem
  (t : Type0) (self : hashmap_hash_map_t t) (key : usize) (value : t)
  (st : state) :
  Lemma (ensures (
    match hashmap_hash_map_insert_back t self key value st with
    | Fail -> True
    | Return (st', _) -> st' == st))
  [SMTPat (hashmap_hash_map_insert_back t self key value st)]
  =
  hashmap_hash_map_insert_no_resize_back_lem t self key value st;
  begin match hashmap_hash_map_insert_no_resize_back t self key value st with
  | Fail -> ()
  | Return (st0, hm) ->
    begin match hashmap_hash_map_len_fwd t hm st0 with
    | Fail -> ()
    | Return (st1, i) ->
      if i > hm.hashmap_hash_map_max_load
      then
        hashmap_hash_map_try_resize_back_lem t (Mkhashmap_hash_map_t
            hm.hashmap_hash_map_num_entries hm.hashmap_hash_map_max_load_factor
            hm.hashmap_hash_map_max_load hm.hashmap_hash_map_slots) st1
      else ()
    end
  end


(*** Lemmas *)

/// The obvious lemma about [insert_on_disk]: the updated hash map stored on disk
/// is exactly the hash map produced from inserting the binding ([key], [value])
/// in the hash map previously stored on disk.
val insert_on_disk_fwd_lem (key : usize) (value : u64) (st : state) : Lemma (
  match insert_on_disk_fwd key value st with
  | Fail -> True
  | Return (st', ()) ->
    let hm = state_v st in
    match hashmap_hash_map_insert_back u64 hm key value st with
    | Fail -> False
    | Return (_, hm') -> hm' == state_v st')

let insert_on_disk_fwd_lem key value st =
  deserialize_lem st;
  begin match hashmap_utils_deserialize_fwd st with
  | Fail -> ()
  | Return (st0, hm) ->
    hashmap_hash_map_insert_back_lem u64 hm key value st0;
    begin match hashmap_hash_map_insert_back u64 hm key value st0 with
    | Fail -> ()
    | Return (st1, hm0) ->
      serialize_lem hm0 st1;
      begin match hashmap_utils_serialize_fwd hm0 st1 with
      | Fail -> ()
      | Return (st2, _) -> ()
      end
    end
  end