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
|
(** Properties about the hashmap *)
module Hashmap.Properties
open Primitives
open FStar.List.Tot
open FStar.Mul
open Hashmap.Types
open Hashmap.Clauses
open Hashmap.Funs
#set-options "--z3rlimit 50 --fuel 0 --ifuel 1"
// Small trick to align the .fst and the .fsti
val _align_fsti : unit
(*** Utilities *)
type key : eqtype = usize
type hash : eqtype = usize
val hash_map_t_inv (#t : Type0) (hm : hash_map_t t) : Type0
val len_s (#t : Type0) (hm : hash_map_t t) : nat
val find_s (#t : Type0) (hm : hash_map_t t) (k : key) : option t
(*** new *)
/// [new] doesn't fail and returns an empty hash map
val hash_map_new_fwd_lem (t : Type0) :
Lemma
(ensures (
match hash_map_new_fwd t with
| Fail -> False
| Return hm ->
// The hash map invariant is satisfied
hash_map_t_inv hm /\
// The hash map has a length of 0
len_s hm = 0 /\
// It contains no bindings
(forall k. find_s hm k == None)))
(*** [clear] *)
/// [clear] doesn't fail and turns the hash map into an empty map
val hash_map_clear_fwd_back_lem
(#t : Type0) (self : hash_map_t t) :
Lemma
(requires (hash_map_t_inv self))
(ensures (
match hash_map_clear_fwd_back t self with
| Fail -> False
| Return hm ->
// The hash map invariant is satisfied
hash_map_t_inv hm /\
// The hash map has a length of 0
len_s hm = 0 /\
// It contains no bindings
(forall k. find_s hm k == None)))
(*** [len] *)
/// [len] can't fail and returns the length (the number of elements) of the hash map
val hash_map_len_fwd_lem (#t : Type0) (self : hash_map_t t) :
Lemma
(requires (hash_map_t_inv self))
(ensures (
match hash_map_len_fwd t self with
| Fail -> False
| Return l -> l = len_s self))
(*** [insert'fwd_back] *)
/// The backward function for [insert] (note it is named "...'fwd_back" because
/// the forward function doesn't return anything, and is was thus filtered - in a
/// sense the effect of applying the forward function then the backward function is
/// entirely given by the backward function alone).
/// [insert'fwd_back] simply inserts a binding.
val hash_map_insert_fwd_back_lem
(#t : Type0) (self : hash_map_t t) (key : usize) (value : t) :
Lemma
(requires (hash_map_t_inv self))
(ensures (
match hash_map_insert_fwd_back t self key value with
| Fail ->
// We can fail only if:
// - the key is not in the map and we thus need to add it
None? (find_s self key) /\
// - and we are already saturated (we can't increment the internal counter)
len_s self = usize_max
| Return hm' ->
// The invariant is preserved
hash_map_t_inv hm' /\
// [key] maps to [value]
find_s hm' key == Some value /\
// The other bindings are preserved
(forall k'. k' <> key ==> find_s hm' k' == find_s self k') /\
begin
// The length is incremented, iff we inserted a new key
match find_s self key with
| None -> len_s hm' = len_s self + 1
| Some _ -> len_s hm' = len_s self
end))
(*** [contains_key] *)
/// [contains_key'fwd] can't fail and return `true` if and only if there is
/// a binding for key [key]
val hash_map_contains_key_fwd_lem
(#t : Type0) (self : hash_map_t t) (key : usize) :
Lemma
(requires (hash_map_t_inv self))
(ensures (
match hash_map_contains_key_fwd t self key with
| Fail -> False
| Return b -> b = Some? (find_s self key)))
(*** [get'fwd] *)
/// [get] returns (a shared borrow to) the binding for key [key]
val hash_map_get_fwd_lem
(#t : Type0) (self : hash_map_t t) (key : usize) :
Lemma
(requires (hash_map_t_inv self))
(ensures (
match hash_map_get_fwd t self key, find_s self key with
| Fail, None -> True
| Return x, Some x' -> x == x'
| _ -> False))
(*** [get_mut'fwd] *)
/// [get_mut'fwd] returns (mutable borrows to) the binding for key [key].
val hash_map_get_mut_fwd_lem
(#t : Type0) (self : hash_map_t t) (key : usize) :
Lemma
(requires (hash_map_t_inv self))
(ensures (
match hash_map_get_mut_fwd t self key, find_s self key with
| Fail, None -> True
| Return x, Some x' -> x == x'
| _ -> False))
(*** [get_mut'back] *)
/// [get_mut'back] updates the binding for key [key], without failing.
/// A call to [get_mut'back] must follow a call to [get_mut'fwd], which gives
/// us that there must be a binding for key [key] in the map (otherwise we
/// can't prove the absence of failure).
val hash_map_get_mut_back_lem
(#t : Type0) (hm : hash_map_t t) (key : usize) (ret : t) :
Lemma
(requires (
hash_map_t_inv hm /\
// A call to the backward function must follow a call to the forward
// function, whose success gives us that there is a binding for the key.
Some? (find_s hm key)))
(ensures (
match hash_map_get_mut_back t hm key ret with
| Fail -> False // Can't fail
| Return hm' ->
// The invariant is preserved
hash_map_t_inv hm' /\
// The length is preserved
len_s hm' = len_s hm /\
// [key] maps to the update value, [ret]
find_s hm' key == Some ret /\
// The other bindings are preserved
(forall k'. k' <> key ==> find_s hm' k' == find_s hm k')))
(*** [remove'fwd] *)
/// [remove'fwd] returns the (optional) element which has been removed from the map
/// (the rust function *moves* it out of the map).
val hash_map_remove_fwd_lem
(#t : Type0) (self : hash_map_t t) (key : usize) :
Lemma
(requires (hash_map_t_inv self))
(ensures (
match hash_map_remove_fwd t self key with
| Fail -> False
| Return opt_x -> opt_x == find_s self key))
(*** [remove'back] *)
/// The hash map given as parameter to [remove] is given through a mutable borrow:
/// hence the backward function which gives back the updated map, without the
/// binding.
val hash_map_remove_back_lem
(#t : Type0) (self : hash_map_t t) (key : usize) :
Lemma
(requires (hash_map_t_inv self))
(ensures (
match hash_map_remove_back t self key with
| Fail -> False
| Return hm' ->
// The invariant is preserved
hash_map_t_inv self /\
// The binding for [key] is not there anymore
find_s hm' key == None /\
// The other bindings are preserved
(forall k'. k' <> key ==> find_s hm' k' == find_s self k') /\
begin
// The length is decremented iff the key was in the map
let len = len_s self in
let len' = len_s hm' in
match find_s self key with
| None -> len = len'
| Some _ -> len = len' + 1
end))
|
