spec/containers/hash_table.bend
bend-collections-laws-containers@1.0.0.0 · 204 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
3import bend-collections-laws-containers@1.0.0.0/src/containers/hash_table.bend as H
4
5# Independent model: a map from String keys to values is an association
6# list with at most one entry per key. Nothing here refers to buckets,
7# hashing, probing or slots.
8
9type Entry<-V: Data> is Data:
10 E{key: String, val: V}
11
12def chr_eq(a: Char, b: Char) -> Bool:
13 match a b:
14 case Chr{x} Chr{y}:
15 U32.is_eq(x, y)
16
17def str_eq(a: String, b: String) -> Bool:
18 match a b:
19 case SNil{} SNil{}:
20 True{}
21 case SNil{} SCon{h, t}:
22 False{}
23 case SCon{h, t} SNil{}:
24 False{}
25 case SCon{x, s} SCon{y, t}:
26 Bool.and(chr_eq(x, y), str_eq(s, t))
27
28def lookup(~V: Data, m: List<&2, Entry<V>>, +k: String) -> Maybe<&2, V>:
29 match m:
30 case Nil{}:
31 None{}
32 case Con{E{+j, +v}, t}:
33 Bool.pick(Maybe<&2, V>, str_eq(j, k), Some{v}, lookup(~V, t, k))
34
35def is_some(~V: Data, m: Maybe<&2, V>) -> Bool:
36 match m:
37 case None{}:
38 False{}
39 case Some{v}:
40 True{}
41
42def has(~V: Data, m: List<&2, Entry<V>>, +k: String) -> Bool:
43 is_some(~V, lookup(~V, m, k))
44
45# Replace the entry of k in place, or add it at the end.
46def set(~V: Data, m: List<&2, Entry<V>>, +k: String, +x: V) -> List<&2, Entry<V>>:
47 match m:
48 case Nil{}:
49 Con{E{k, x}, Nil{}}
50 case Con{E{+j, +v}, +t}:
51 Bool.pick(List<&2, Entry<V>>, str_eq(j, k), Con{E{k, x}, t}, Con{E{j, v}, set(~V, t, k, x)})
52
53def remove(~V: Data, m: List<&2, Entry<V>>, +k: String) -> List<&2, Entry<V>>:
54 match m:
55 case Nil{}:
56 Nil{}
57 case Con{E{+j, +v}, +t}:
58 Bool.pick(List<&2, Entry<V>>, str_eq(j, k), t, Con{E{j, v}, remove(~V, t, k)})
59
60def keys(~V: Data, m: List<&2, Entry<V>>) -> List<&2, String>:
61 match m:
62 case Nil{}:
63 Nil{}
64 case Con{E{j, v}, t}:
65 Con{j, keys(~V, t)}
66
67def size(~V: Data, m: List<&2, Entry<V>>) -> Nat:
68 match m:
69 case Nil{}:
70 0n
71 case Con{e, t}:
72 1n+size(~V, t)
73
74def mem(+k: String, ks: List<&2, String>) -> Bool:
75 match ks:
76 case Nil{}:
77 False{}
78 case Con{j, t}:
79 Bool.or(str_eq(j, k), mem(k, t))
80
81def nodup(ks: List<&2, String>) -> Bool:
82 match ks:
83 case Nil{}:
84 True{}
85 case Con{+j, +t}:
86 Bool.and(Bool.not(mem(j, t)), nodup(t))
87
88def get_m(~V: Data, dflt: V, m: Maybe<&2, V>) -> V:
89 match m:
90 case None{}:
91 dflt
92 case Some{v}:
93 v
94
95# the value of key, or dflt
96def get(~V: Data, dflt: V, m: List<&2, Entry<V>>, +key: String) -> V:
97 get_m(~V, dflt, lookup(~V, m, key))
98
99# ---- contract (SPARK formal containers) ----
100# Each `<Subprogram>.<clause>` definition below states one Post clause of
101# that SPARK subprogram, as a proposition on this model; the table names the
102# clauses. proofs/containers/hash_table/ proves every clause under its clause name,
103# and its `impl` lemma carries them to the implementation.
104#
105# Contracts of the hash map in the style of SPARK's formal hashed maps
106# (SPARKlib spark-containers-formal-hashed_maps.ads). The proofs in
107# set/pop/keysw.bend relate every operation to the specification's
108# association list; this module states, per operation, what changes and
109# what is preserved, over three views of a map sh:
110# Model S.lookup(ST.model(sh), q) the value of every key q
111# Length S.size(ST.model(sh))
112# Keys S.keys(ST.model(sh)) the keys, in iteration order
113# Keys are compared by S.str_eq, which is an equivalence under which equal
114# keys are identical strings (so, like SPARK's Equivalent_Keys, every
115# function of a key, the hash included, agrees on equivalent keys).
116# SPARK's cursor model (Positions) has no counterpart: the map has no
117# cursors.
118#
119# SPARK subprogram (hashed_maps.ads line, AdaCore/SPARKlib master) ours lemmas
120# Empty_Map (103) new new_model, new_length, new_absent
121# Length (117) size length_value, length_frame (P.size_ok)
122# Element (Key) (1039) get element_value, element_default (P.get_ok)
123# Contains (1032) has contains_value (P.has_ok)
124# Include (729) set SetContract / SetPost (set_post)
125# Delete (Key) (891), Exclude (851) pop, del PopContract, DelContract / DelPost
126# Iter_Model / Keys (1078) keys KeysContract / KeysPost
127# Equivalent_Keys str_eq key_refl, key_sym, key_trans, key_same, key_respect
128# Not in this API: "=", Capacity, Reserve_Capacity, Is_Empty, Clear,
129# Assign/Copy/Move, Replace_Element/Reference (by cursor), Insert (fails
130# if present) and Replace (fails if absent), which Include subsumes,
131# First/Next/Has_Element/Key (cursors), Find, Default_Modulus.
132
133# ---- keys ----
134# The key sequence (SPARK's Keys): no key twice, as long as the map, and
135# holding exactly the keys the model has.
136def KeysPost(~V: Data, m: List<&2, Entry<V>>) -> Type:
137 {nodup(keys(~V, m)) == True{} : Bool} & ({SC.length(String, keys(~V, m)) == size(~V, m) : Nat} & (@+q: String -> {mem(q, keys(~V, m)) == has(~V, m, q) : Bool}))
138
139# ---- set (SPARK's Include: insert, or replace the value) ----
140def SetPost(~V: Data, m: List<&2, Entry<V>>, m2: List<&2, Entry<V>>, key: String, x: V) -> Type:
141 {has(~V, m2, key) == True{} : Bool} & ((@+q: String -> @+hq: {str_eq(key, q) == True{} : Bool} -> {lookup(~V, m2, q) == Some{x} : Maybe<&2, V>}) & ((@+q: String -> @+hq: {str_eq(key, q) == False{} : Bool} -> {lookup(~V, m2, q) == lookup(~V, m, q) : Maybe<&2, V>}) & ({size(~V, m2) == Bool.pick(Nat, has(~V, m, key), size(~V, m), 1n+size(~V, m)) : Nat} & ((@+q: String -> {mem(q, keys(~V, m2)) == Bool.or(str_eq(key, q), mem(q, keys(~V, m))) : Bool}) & ({nodup(keys(~V, m2)) == True{} : Bool} & (@+hp: {has(~V, m, key) == True{} : Bool} -> {keys(~V, m2) == keys(~V, m) : List<&2, String>}))))))
142
143# ---- pop and del (SPARK's Delete/Exclude) ----
144def DelPost(~V: Data, m: List<&2, Entry<V>>, m2: List<&2, Entry<V>>, key: String) -> Type:
145 {has(~V, m2, key) == False{} : Bool} & ((@+q: String -> @+hq: {str_eq(key, q) == False{} : Bool} -> {lookup(~V, m2, q) == lookup(~V, m, q) : Maybe<&2, V>}) & ((@+hn: {has(~V, m, key) == False{} : Bool} -> @+q: String -> {lookup(~V, m2, q) == lookup(~V, m, q) : Maybe<&2, V>}) & ({Bool.pick(Nat, has(~V, m, key), 1n+size(~V, m2), size(~V, m2)) == size(~V, m) : Nat} & ((@+q: String -> {mem(q, keys(~V, m2)) == Bool.and(Bool.not(str_eq(key, q)), mem(q, keys(~V, m))) : Bool}) & {nodup(keys(~V, m2)) == True{} : Bool}))))
146
147# Equivalent_Keys
148def Equivalent_Keys.key_refl(+a: String) -> Type:
149 {str_eq(a, a) == True{} : Bool}
150
151# Equivalent_Keys
152def Equivalent_Keys.key_sym(+a: String, +b: String) -> Type:
153 {str_eq(a, b) == str_eq(b, a) : Bool}
154
155# Equivalent_Keys
156def Equivalent_Keys.key_trans(+a: String, +b: String, +c: String, +hab: {str_eq(a, b) == True{} : Bool}, +hbc: {str_eq(b, c) == True{} : Bool}) -> Type:
157 {str_eq(a, c) == True{} : Bool}
158
159# Equivalent_Keys
160def Equivalent_Keys.key_same(+a: String, +b: String, +h: {str_eq(a, b) == True{} : Bool}) -> Type:
161 {a == b : String}
162
163# Equivalent_Keys
164def Equivalent_Keys.key_respect(~A: Data, ~f: String -> A, +a: String, +b: String, +h: {str_eq(a, b) == True{} : Bool}) -> Type:
165 {f(a) == f(b) : A}
166
167# Include (729)
168def Include.set_post(~V: Data, ~m: List<&2, Entry<V>>, ~m2: List<&2, Entry<V>>, ~key: String, ~x: V, ~hp: (@+q: String -> {lookup(~V, m2, q) == lookup(~V, set(~V, m, key, x), q) : Maybe<&2, V>}) & {size(~V, m2) == size(~V, set(~V, m, key, x)) : Nat}, +hnd: {nodup(keys(~V, m2)) == True{} : Bool}, hk: @+hq0: {has(~V, m, key) == True{} : Bool} -> {keys(~V, m2) == keys(~V, m) : List<&2, String>}) -> Type:
169 SetPost(~V, m, m2, key, x)
170
171# The queries are stated on what they return: `r` is the value the operation
172# produces on a map whose model is `m` (the proof package instantiates it with
173# the implementation's result).
174
175# Element (SPARKlib formal-hashed-maps.ads): Element (Container, Key) = Get (Model, Key)
176def Element.element_value(~V: Data, m: List<&2, Entry<V>>, +key: String, +x: V, +hl: {lookup(~V, m, key) == Some{x} : Maybe<&2, V>}, r: V) -> Type:
177 {r == x : V}
178
179# Element without the key: get returns the caller's default (the Pre of
180# Element is Contains; here the absent case is defined, not excluded)
181def Element.element_default(~V: Data, m: List<&2, Entry<V>>, +key: String, +dflt: V, +hl: {lookup(~V, m, key) == None{} : Maybe<&2, V>}, r: V) -> Type:
182 {r == dflt : V}
183
184# Contains: Contains (Container, Key) = Has_Key (Model, Key)
185def Contains.contains_value(~V: Data, m: List<&2, Entry<V>>, +key: String, r: Bool) -> Type:
186 {r == is_some(~V, lookup(~V, m, key)) : Bool}
187
188# Length: Length (Container) = M.Length (Model)
189def Length.length_value(~V: Data, m: List<&2, Entry<V>>, +n: Nat) -> Type:
190 {n == SC.length(String, keys(~V, m)) : Nat}
191
192# Length is a query: the map is returned unchanged
193def Length.length_frame(~V: Data, a: H.HashMap<&2, V>, b: H.HashMap<&2, V>) -> Type:
194 {b == a : H.HashMap<&2, V>}
195
196# Empty_Map: Is_Empty (Model), Length = 0, no key present
197def Empty_Map.new_model(~V: Data, m: List<&2, Entry<V>>) -> Type:
198 {m == Nil{} : List<&2, Entry<V>>}
199
200def Empty_Map.new_length(~V: Data, m: List<&2, Entry<V>>) -> Type:
201 {size(~V, m) == 0n : Nat}
202
203def Empty_Map.new_absent(~V: Data, m: List<&2, Entry<V>>, +key: String) -> Type:
204 {lookup(~V, m, key) == None{} : Maybe<&2, V>}