proofs/containers/hash_table/proof.bend
bend-collections-laws-containers@1.0.0.0 · 316 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/spec/containers/hash_table.bend as S
3import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
4import bend-collections-laws-containers@1.0.0.0/src/containers/hash_table.bend as H
5import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/state.bend as ST
6import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/new.bend as NW
7import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/get.bend as G
8import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/has.bend as HA
9import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/size.bend as SZ
10import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/set.bend as ST2
11import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/setok.bend as SO
12import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/pop.bend as PO
13import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/keysw.bend as KW
14import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/keys.bend as K
15import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/speclem.bend as SL
16import bend-collections-laws-containers@1.0.0.0/proofs/lib/logic.bend as L
17import bend-collections-laws-containers@1.0.0.0/proofs/lib/array.bend as AR
18import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/poplem.bend as PL
19import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/table.bend as TB
20import bend-collections-laws-containers@1.0.0.0/proofs/lib/u32div.bend as UD
21
22# Hash map (src/containers/hash_table.bend): public proof entry point.
23# shadow ST.Sh: the map's U32 fields, the table and arena exponents
24# and a mirror tree for each array; ST.real(sh) is the map
25# abstraction ST.model(sh): the entries of the full buckets, in bucket
26# order, as a proofs/spec/hash_table.bend association list
27# invariant ST.good(sh): clusters, check words, unique keys and links,
28# live slots, the count and load, and the exact free list
29# (proofs/hash_table/state.bend, generated by
30# tools/generators/hash_table_state.py)
31#
32# Every operation is proved for every shadow satisfying the invariant, keys
33# of every length, and every value type V (Data):
34# new the empty model
35# get/has/size the specification's answer; map and model kept
36# set every lookup and the size are the specification's set's
37# (precondition: 2(n + 1) <= 2^cap with cap <= 30, i.e. the
38# table stays below 2^31 buckets)
39# pop/del the specification's lookup, then its remove
40# keys the model's keys, in order
41# and each result shadow satisfies the invariant again.
42#
43# The *_contract theorems restate set, pop, del and keys as SPARK-style
44# contracts (stated in spec/containers/hash_table.bend, after SPARKlib's
45# formal hashed maps): what each operation changes and what it preserves in
46# the model (the value of every key), the length and the key sequence. The
47# key_* laws make key comparison an equivalence under which equivalent keys
48# are identical, so every function of a key (the hash too) agrees on them.
49
50def new_ok(~V: Data) -> {H.new(&2, V) == ST.real(~V, NW.empty(~V)) : H.HashMap<&2, V>} & ({ST.good(~V, NW.empty(~V)) == True{} : Bool} & {ST.model(~V, NW.empty(~V)) == Nil{} : List<&2, S.Entry<V>>}):
51 NW.new_ok(~V)
52
53def get_ok(~V: Data, +sh: ST.Sh<V>, +hg: {ST.good(~V, sh) == True{} : Bool}, +dflt: V, +key: String) -> G.GetOK(~V, sh, dflt, key, H.get(V, dflt, ST.real(~V, sh), key)):
54 G.get_ok(~V, sh, hg, dflt, key)
55
56def has_ok(~V: Data, +sh: ST.Sh<V>, +hg: {ST.good(~V, sh) == True{} : Bool}, +key: String) -> HA.HasOK(~V, sh, key, H.has(&2, V, ST.real(~V, sh), key)):
57 HA.has_ok(~V, sh, hg, key)
58
59def size_ok(~V: Data, +sh: ST.Sh<V>, +hg: {ST.good(~V, sh) == True{} : Bool}) -> {H.size(&2, V, ST.real(~V, sh)) == (ST.real(~V, sh), Pair.snd(H.HashMap<&2, V>, U32, H.size(&2, V, ST.real(~V, sh)))) : H.HashMap<&2, V> & U32} & {U32.to_nat(Pair.snd(H.HashMap<&2, V>, U32, H.size(&2, V, ST.real(~V, sh)))) == S.size(~V, ST.model(~V, sh)) : Nat}:
60 SZ.size_ok(~V, sh, hg)
61
62def set_ok(~V: Data, +sh: ST.Sh<V>, +hg: {ST.good(~V, sh) == True{} : Bool}, +cap: Nat, +hc30: {Nat.is_le(cap, 30n) == True{} : Bool}, +hcap: {Nat.is_le(Nat.double(1n+S.size(~V, ST.model(~V, sh))), SC.pow2(cap)) == True{} : Bool}, +key: String, +x: V) -> ST2.SetOK(~V, sh, key, x, H.set(&2, V, ST.real(~V, sh), key, x)):
63 SO.set_ok(~V, sh, hg, cap, hc30, hcap, key, x)
64
65def pop_ok(~V: Data, +sh: ST.Sh<V>, +hg: {ST.good(~V, sh) == True{} : Bool}, +key: String) -> PO.PopOK(~V, sh, key, H.pop(&2, V, ST.real(~V, sh), key)):
66 PO.pop_ok(~V, sh, hg, key)
67
68def del_ok(~V: Data, +sh: ST.Sh<V>, +hg: {ST.good(~V, sh) == True{} : Bool}, +key: String) -> PO.DelOK(~V, sh, key, H.del(&2, V, ST.real(~V, sh), key)):
69 PO.del_ok(~V, sh, hg, key)
70
71def keys_ok(~V: Data, +sh: ST.Sh<V>, +hg: {ST.good(~V, sh) == True{} : Bool}) -> KW.KeysOK(~V, sh, H.keys(&2, V, ST.real(~V, sh))):
72 KW.keys_ok(~V, sh, hg)
73
74# ---- contracts ----
75
76# ==== the contract of hash_table (stated in spec/containers/hash_table.bend) ====================
77
78# ---- key equivalence ----
79def key_refl(+a: String) -> S.Equivalent_Keys.key_refl(a):
80 K.str_refl(a)
81
82def key_sym(+a: String, +b: String) -> S.Equivalent_Keys.key_sym(a, b):
83 K.str_sym(a, b)
84
85def key_trans(+a: String, +b: String, +c: String, +hab: {S.str_eq(a, b) == True{} : Bool}, +hbc: {S.str_eq(b, c) == True{} : Bool}) -> S.Equivalent_Keys.key_trans(a, b, c, hab, hbc):
86 SL.eq_tr(a, b, c, hab, True{}, hbc)
87
88# equivalent keys are the same string
89def key_same(+a: String, +b: String, +h: {S.str_eq(a, b) == True{} : Bool}) -> S.Equivalent_Keys.key_same(a, b, h):
90 K.str_eq_of(a, b, h)
91
92# and so every function of a key (the hash included) agrees on them
93def key_respect(~A: Data, ~f: String -> A, +a: String, +b: String, +h: {S.str_eq(a, b) == True{} : Bool}) -> S.Equivalent_Keys.key_respect(~A, ~f, a, b, h):
94 Equal.cong(String, A, f, a, b, K.str_eq_of(a, b, h))
95
96# ---- facts about the specification ----
97def mh_c(~V: Data, +j: String, +v: V, +t: List<&2, S.Entry<V>>, +q: String, +c: Bool, +hc: {S.str_eq(j, q) == c : Bool}, +ih: {S.mem(q, S.keys(~V, t)) == S.has(~V, t, q) : Bool}) -> {Bool.or(S.str_eq(j, q), S.mem(q, S.keys(~V, t))) == S.is_some(~V, Bool.pick(Maybe<&2, V>, S.str_eq(j, q), Some{v}, S.lookup(~V, t, q))) : Bool}:
98 match c:
99 case True{}:
100 %Equal.sym(Bool, S.str_eq(j, q), True{}, hc) : {Bool.or(_, S.mem(q, S.keys(~V, t))) == S.is_some(~V, Bool.pick(Maybe<&2, V>, _, Some{v}, S.lookup(~V, t, q))) : Bool}
101 {==}
102 case False{}:
103 %Equal.sym(Bool, S.str_eq(j, q), False{}, hc) : {Bool.or(_, S.mem(q, S.keys(~V, t))) == S.is_some(~V, Bool.pick(Maybe<&2, V>, _, Some{v}, S.lookup(~V, t, q))) : Bool}
104 ih
105
106# a key is in the key sequence exactly when the model has it
107def mem_has(~V: Data, +m: List<&2, S.Entry<V>>, +q: String) -> {S.mem(q, S.keys(~V, m)) == S.has(~V, m, q) : Bool}:
108 match m:
109 case Nil{}:
110 {==}
111 case Con{S.E{+j, +v}, +t}:
112 mh_c(~V, j, v, t, q, S.str_eq(j, q), {==}, mem_has(~V, t, q))
113
114# the key sequence is as long as the map
115def keys_len(~V: Data, +m: List<&2, S.Entry<V>>) -> {SC.length(String, S.keys(~V, m)) == S.size(~V, m) : Nat}:
116 match m:
117 case Nil{}:
118 {==}
119 case Con{S.E{+j, +v}, +t}:
120 Equal.cong(Nat, Nat, z => 1n+z, SC.length(String, S.keys(~V, t)), S.size(~V, t), keys_len(~V, t))
121
122# has is false exactly when the lookup is None
123def none_of(~V: Data, +mv: Maybe<&2, V>, +h: {S.is_some(~V, mv) == False{} : Bool}) -> {mv == None{} : Maybe<&2, V>}:
124 match mv:
125 case None{}:
126 {==}
127 case Some{v}:
128 Empty.absurd({Some{v} == None{} : Maybe<&2, V>}, L.true_false(h))
129
130def ssp(~V: Data, +m: List<&2, S.Entry<V>>, +key: String, +x: V, +mv: Maybe<&2, V>, +hmv: {S.lookup(~V, m, key) == mv : Maybe<&2, V>}) -> {S.size(~V, S.set(~V, m, key, x)) == Bool.pick(Nat, S.has(~V, m, key), S.size(~V, m), 1n+S.size(~V, m)) : Nat}:
131 match mv:
132 case None{}:
133 %Equal.sym(Maybe<&2, V>, S.lookup(~V, m, key), None{}, hmv) : {S.size(~V, S.set(~V, m, key, x)) == Bool.pick(Nat, S.is_some(~V, _), S.size(~V, m), 1n+S.size(~V, m)) : Nat}
134 SL.size_set_new(~V, m, key, x, hmv)
135 case Some{+v0}:
136 %Equal.sym(Maybe<&2, V>, S.lookup(~V, m, key), Some{v0}, hmv) : {S.size(~V, S.set(~V, m, key, x)) == Bool.pick(Nat, S.is_some(~V, _), S.size(~V, m), 1n+S.size(~V, m)) : Nat}
137 SL.size_set_old(~V, m, key, x, v0, hmv)
138
139# set grows the map by one exactly when the key was absent
140def size_set(~V: Data, +m: List<&2, S.Entry<V>>, +key: String, +x: V) -> {S.size(~V, S.set(~V, m, key, x)) == Bool.pick(Nat, S.has(~V, m, key), S.size(~V, m), 1n+S.size(~V, m)) : Nat}:
141 ssp(~V, m, key, x, S.lookup(~V, m, key), {==})
142
143def srp(~V: Data, +m: List<&2, S.Entry<V>>, +key: String, +mv: Maybe<&2, V>, +hmv: {S.lookup(~V, m, key) == mv : Maybe<&2, V>}) -> {Bool.pick(Nat, S.has(~V, m, key), 1n+S.size(~V, S.remove(~V, m, key)), S.size(~V, S.remove(~V, m, key))) == S.size(~V, m) : Nat}:
144 match mv:
145 case None{}:
146 %Equal.sym(Maybe<&2, V>, S.lookup(~V, m, key), None{}, hmv) : {Bool.pick(Nat, S.is_some(~V, _), 1n+S.size(~V, S.remove(~V, m, key)), S.size(~V, S.remove(~V, m, key))) == S.size(~V, m) : Nat}
147 Equal.cong(List<&2, S.Entry<V>>, Nat, z => S.size(~V, z), S.remove(~V, m, key), m, SL.remove_none(~V, m, key, hmv))
148 case Some{+v0}:
149 %Equal.sym(Maybe<&2, V>, S.lookup(~V, m, key), Some{v0}, hmv) : {Bool.pick(Nat, S.is_some(~V, _), 1n+S.size(~V, S.remove(~V, m, key)), S.size(~V, S.remove(~V, m, key))) == S.size(~V, m) : Nat}
150 SL.size_remove_old(~V, m, key, v0, hmv)
151
152# remove shrinks the map by one exactly when the key was present
153def size_remove(~V: Data, +m: List<&2, S.Entry<V>>, +key: String) -> {Bool.pick(Nat, S.has(~V, m, key), 1n+S.size(~V, S.remove(~V, m, key)), S.size(~V, S.remove(~V, m, key))) == S.size(~V, m) : Nat}:
154 srp(~V, m, key, S.lookup(~V, m, key), {==})
155
156def hso_c(~V: Data, +m: List<&2, S.Entry<V>>, +key: String, +x: V, +q: String, +c: Bool, +hc: {S.str_eq(key, q) == c : Bool}) -> {S.has(~V, S.set(~V, m, key, x), q) == Bool.or(c, S.mem(q, S.keys(~V, m))) : Bool}:
157 match c:
158 case True{}:
159 %Equal.sym(Maybe<&2, V>, S.lookup(~V, S.set(~V, m, key, x), q), Some{x}, SL.lookup_set_same(~V, m, key, x, q, hc)) : {S.is_some(~V, _) == Bool.or(True{}, S.mem(q, S.keys(~V, m))) : Bool}
160 {==}
161 case False{}:
162 %Equal.sym(Maybe<&2, V>, S.lookup(~V, S.set(~V, m, key, x), q), S.lookup(~V, m, q), SL.lookup_set_other(~V, m, key, x, q, hc)) : {S.is_some(~V, _) == Bool.or(False{}, S.mem(q, S.keys(~V, m))) : Bool}
163 Equal.sym(Bool, S.mem(q, S.keys(~V, m)), S.has(~V, m, q), mem_has(~V, m, q))
164
165def hro_c(~V: Data, +m: List<&2, S.Entry<V>>, +key: String, +q: String, +hnd: {S.nodup(S.keys(~V, m)) == True{} : Bool}, +c: Bool, +hc: {S.str_eq(key, q) == c : Bool}) -> {S.has(~V, S.remove(~V, m, key), q) == Bool.and(Bool.not(c), S.mem(q, S.keys(~V, m))) : Bool}:
166 match c:
167 case True{}:
168 %Equal.sym(Maybe<&2, V>, S.lookup(~V, S.remove(~V, m, key), q), None{}, SL.lookup_remove_same(~V, m, key, q, hc, hnd)) : {S.is_some(~V, _) == Bool.and(Bool.not(True{}), S.mem(q, S.keys(~V, m))) : Bool}
169 {==}
170 case False{}:
171 %Equal.sym(Maybe<&2, V>, S.lookup(~V, S.remove(~V, m, key), q), S.lookup(~V, m, q), SL.lookup_remove_other(~V, m, key, q, hc)) : {S.is_some(~V, _) == Bool.and(Bool.not(False{}), S.mem(q, S.keys(~V, m))) : Bool}
172 Equal.sym(Bool, S.mem(q, S.keys(~V, m)), S.has(~V, m, q), mem_has(~V, m, q))
173
174# ---- the invariant keeps keys unique ----
175def model_nodup(~V: Data, +sh: ST.Sh<V>, +hg: {ST.good(~V, sh) == True{} : Bool}) -> {S.nodup(S.keys(~V, ST.model(~V, sh))) == True{} : Bool}:
176 match sh:
177 case ST.HS{+n, +k, +td, +fresh, +sz, +sd, +sdU, +free, +tabT, +ksT, +vsT, +nxT}:
178 PL.nodup_model(~V, TB.buckets(AR.slots(U32, tabT), AR.slots(String, ksT), SC.pow2(k)), AR.slots(Maybe<&2, V>, vsT), UD.v(fresh), SC.pow2(k), ST.g_clive(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg), ST.g_cuniq(~V, n, k, td, fresh, sz, sd, sdU, free, tabT, AR.slots(String, ksT), AR.perfect(String, sd, ksT), vsT, nxT, hg))
179
180def keys_post(~V: Data, +sh: ST.Sh<V>, +hg: {ST.good(~V, sh) == True{} : Bool}) -> S.KeysPost(~V, ST.model(~V, sh)):
181 (model_nodup(~V, sh, hg), (keys_len(~V, ST.model(~V, sh)), q => mem_has(~V, ST.model(~V, sh), q)))
182
183# keys returns the key sequence and changes nothing
184def KeysContract(~V: Data, +sh: ST.Sh<V>, r: H.HashMap<&2, V> & List<&2, String>) -> Type:
185 Sigma<&1, &1, ST.Sh<V>, sh2 => {r == (ST.real(~V, sh2), S.keys(~V, ST.model(~V, sh))) : H.HashMap<&2, V> & List<&2, String>} & (({ST.good(~V, sh2) == True{} : Bool} & {ST.model(~V, sh2) == ST.model(~V, sh) : List<&2, S.Entry<V>>}) & S.KeysPost(~V, ST.model(~V, sh)))>
186
187def kc_from(~V: Data, +sh: ST.Sh<V>, +hg: {ST.good(~V, sh) == True{} : Bool}, -r: H.HashMap<&2, V> & List<&2, String>, ko: KW.KeysOK(~V, sh, r)) -> KeysContract(~V, sh, r):
188 match ko:
189 case Tuple{+sh2, Tuple{+e, rest}}:
190 (sh2, (e, (rest, keys_post(~V, sh, hg))))
191
192def SetContract(~V: Data, +sh: ST.Sh<V>, +key: String, +x: V, r: H.HashMap<&2, V>) -> Type:
193 Sigma<&1, &1, ST.Sh<V>, sh2 => {r == ST.real(~V, sh2) : H.HashMap<&2, V>} & ({ST.good(~V, sh2) == True{} : Bool} & S.SetPost(~V, ST.model(~V, sh), ST.model(~V, sh2), key, x))>
194
195def set_same(~V: Data, +m: List<&2, S.Entry<V>>, +m2: List<&2, S.Entry<V>>, +key: String, +x: V, +q: String, +hq: {S.str_eq(key, q) == True{} : Bool}, +hl: {S.lookup(~V, m2, q) == S.lookup(~V, S.set(~V, m, key, x), q) : Maybe<&2, V>}) -> {S.lookup(~V, m2, q) == Some{x} : Maybe<&2, V>}:
196 Equal.trans(Maybe<&2, V>, S.lookup(~V, m2, q), S.lookup(~V, S.set(~V, m, key, x), q), Some{x}, hl, SL.lookup_set_same(~V, m, key, x, q, hq))
197
198def set_other(~V: Data, +m: List<&2, S.Entry<V>>, +m2: List<&2, S.Entry<V>>, +key: String, +x: V, +q: String, +hq: {S.str_eq(key, q) == False{} : Bool}, +hl: {S.lookup(~V, m2, q) == S.lookup(~V, S.set(~V, m, key, x), q) : Maybe<&2, V>}) -> {S.lookup(~V, m2, q) == S.lookup(~V, m, q) : Maybe<&2, V>}:
199 Equal.trans(Maybe<&2, V>, S.lookup(~V, m2, q), S.lookup(~V, S.set(~V, m, key, x), q), S.lookup(~V, m, q), hl, SL.lookup_set_other(~V, m, key, x, q, hq))
200
201def set_mem(~V: Data, +m: List<&2, S.Entry<V>>, +m2: List<&2, S.Entry<V>>, +key: String, +x: V, +q: String, +hl: {S.lookup(~V, m2, q) == S.lookup(~V, S.set(~V, m, key, x), q) : Maybe<&2, V>}) -> {S.mem(q, S.keys(~V, m2)) == Bool.or(S.str_eq(key, q), S.mem(q, S.keys(~V, m))) : Bool}:
202 Equal.trans(Bool, S.mem(q, S.keys(~V, m2)), S.has(~V, m2, q), Bool.or(S.str_eq(key, q), S.mem(q, S.keys(~V, m))), mem_has(~V, m2, q),
203 Equal.trans(Bool, S.has(~V, m2, q), S.has(~V, S.set(~V, m, key, x), q), Bool.or(S.str_eq(key, q), S.mem(q, S.keys(~V, m))), Equal.cong(Maybe<&2, V>, Bool, z => S.is_some(~V, z), S.lookup(~V, m2, q), S.lookup(~V, S.set(~V, m, key, x), q), hl), hso_c(~V, m, key, x, q, S.str_eq(key, q), {==})))
204
205def set_post(~V: Data, ~m: List<&2, S.Entry<V>>, ~m2: List<&2, S.Entry<V>>, ~key: String, ~x: V, ~hp: (@+q: String -> {S.lookup(~V, m2, q) == S.lookup(~V, S.set(~V, m, key, x), q) : Maybe<&2, V>}) & {S.size(~V, m2) == S.size(~V, S.set(~V, m, key, x)) : Nat}, +hnd: {S.nodup(S.keys(~V, m2)) == True{} : Bool}, hk: @+hq0: {S.has(~V, m, key) == True{} : Bool} -> {S.keys(~V, m2) == S.keys(~V, m) : List<&2, String>}) -> S.Include.set_post(~V, ~m, ~m2, ~key, ~x, ~hp, hnd, hk):
206 (Equal.cong(Maybe<&2, V>, Bool, z => S.is_some(~V, z), S.lookup(~V, m2, key), Some{x}, set_same(~V, m, m2, key, x, key, K.str_refl(key), Pair.fst(@+q: String -> {S.lookup(~V, m2, q) == S.lookup(~V, S.set(~V, m, key, x), q) : Maybe<&2, V>}, {S.size(~V, m2) == S.size(~V, S.set(~V, m, key, x)) : Nat}, hp)(key))),
207 (q => hq => set_same(~V, m, m2, key, x, q, hq, Pair.fst(@+q: String -> {S.lookup(~V, m2, q) == S.lookup(~V, S.set(~V, m, key, x), q) : Maybe<&2, V>}, {S.size(~V, m2) == S.size(~V, S.set(~V, m, key, x)) : Nat}, hp)(q)),
208 (q => hq => set_other(~V, m, m2, key, x, q, hq, Pair.fst(@+q: String -> {S.lookup(~V, m2, q) == S.lookup(~V, S.set(~V, m, key, x), q) : Maybe<&2, V>}, {S.size(~V, m2) == S.size(~V, S.set(~V, m, key, x)) : Nat}, hp)(q)),
209 (Equal.trans(Nat, S.size(~V, m2), S.size(~V, S.set(~V, m, key, x)), Bool.pick(Nat, S.has(~V, m, key), S.size(~V, m), 1n+S.size(~V, m)), Pair.snd(@+q: String -> {S.lookup(~V, m2, q) == S.lookup(~V, S.set(~V, m, key, x), q) : Maybe<&2, V>}, {S.size(~V, m2) == S.size(~V, S.set(~V, m, key, x)) : Nat}, hp), size_set(~V, m, key, x)),
210 (q => set_mem(~V, m, m2, key, x, q, Pair.fst(@+q: String -> {S.lookup(~V, m2, q) == S.lookup(~V, S.set(~V, m, key, x), q) : Maybe<&2, V>}, {S.size(~V, m2) == S.size(~V, S.set(~V, m, key, x)) : Nat}, hp)(q)), (hnd, hk))))))
211
212def sc_from(~V: Data, +sh: ST.Sh<V>, +key: String, +x: V, -r: H.HashMap<&2, V>, so: ST2.SetOK(~V, sh, key, x, r)) -> SetContract(~V, sh, key, x, r):
213 match so:
214 case Tuple{+sh2, Tuple{+e, rest}}:
215 (old, kk) = rest
216 (+hg2, rest2) = old
217 (sh2, (e, (hg2, set_post(~V, ~ST.model(~V, sh), ~ST.model(~V, sh2), ~key, ~x, ~rest2, model_nodup(~V, sh2, hg2), kk))))
218
219def PopContract(~V: Data, +sh: ST.Sh<V>, +key: String, r: H.HashMap<&2, V> & Maybe<&2, V>) -> Type:
220 Sigma<&1, &1, ST.Sh<V>, sh2 => {r == (ST.real(~V, sh2), S.lookup(~V, ST.model(~V, sh), key)) : H.HashMap<&2, V> & Maybe<&2, V>} & ({ST.good(~V, sh2) == True{} : Bool} & S.DelPost(~V, ST.model(~V, sh), ST.model(~V, sh2), key))>
221
222def DelContract(~V: Data, +sh: ST.Sh<V>, +key: String, r: H.HashMap<&2, V>) -> Type:
223 Sigma<&1, &1, ST.Sh<V>, sh2 => {r == ST.real(~V, sh2) : H.HashMap<&2, V>} & ({ST.good(~V, sh2) == True{} : Bool} & S.DelPost(~V, ST.model(~V, sh), ST.model(~V, sh2), key))>
224
225def del_absent(~V: Data, +m: List<&2, S.Entry<V>>, +m2: List<&2, S.Entry<V>>, +key: String, +hn: {S.has(~V, m, key) == False{} : Bool}, +q: String, +hl: {S.lookup(~V, m2, q) == S.lookup(~V, S.remove(~V, m, key), q) : Maybe<&2, V>}) -> {S.lookup(~V, m2, q) == S.lookup(~V, m, q) : Maybe<&2, V>}:
226 Equal.trans(Maybe<&2, V>, S.lookup(~V, m2, q), S.lookup(~V, S.remove(~V, m, key), q), S.lookup(~V, m, q), hl, Equal.cong(List<&2, S.Entry<V>>, Maybe<&2, V>, z => S.lookup(~V, z, q), S.remove(~V, m, key), m, SL.remove_none(~V, m, key, none_of(~V, S.lookup(~V, m, key), hn))))
227
228def del_other(~V: Data, +m: List<&2, S.Entry<V>>, +m2: List<&2, S.Entry<V>>, +key: String, +q: String, +hq: {S.str_eq(key, q) == False{} : Bool}, +hl: {S.lookup(~V, m2, q) == S.lookup(~V, S.remove(~V, m, key), q) : Maybe<&2, V>}) -> {S.lookup(~V, m2, q) == S.lookup(~V, m, q) : Maybe<&2, V>}:
229 Equal.trans(Maybe<&2, V>, S.lookup(~V, m2, q), S.lookup(~V, S.remove(~V, m, key), q), S.lookup(~V, m, q), hl, SL.lookup_remove_other(~V, m, key, q, hq))
230
231def del_mem(~V: Data, +m: List<&2, S.Entry<V>>, +m2: List<&2, S.Entry<V>>, +key: String, +hnd: {S.nodup(S.keys(~V, m)) == True{} : Bool}, +q: String, +hl: {S.lookup(~V, m2, q) == S.lookup(~V, S.remove(~V, m, key), q) : Maybe<&2, V>}) -> {S.mem(q, S.keys(~V, m2)) == Bool.and(Bool.not(S.str_eq(key, q)), S.mem(q, S.keys(~V, m))) : Bool}:
232 Equal.trans(Bool, S.mem(q, S.keys(~V, m2)), S.has(~V, m2, q), Bool.and(Bool.not(S.str_eq(key, q)), S.mem(q, S.keys(~V, m))), mem_has(~V, m2, q),
233 Equal.trans(Bool, S.has(~V, m2, q), S.has(~V, S.remove(~V, m, key), q), Bool.and(Bool.not(S.str_eq(key, q)), S.mem(q, S.keys(~V, m))), Equal.cong(Maybe<&2, V>, Bool, z => S.is_some(~V, z), S.lookup(~V, m2, q), S.lookup(~V, S.remove(~V, m, key), q), hl), hro_c(~V, m, key, q, hnd, S.str_eq(key, q), {==})))
234
235def del_post(~V: Data, ~m: List<&2, S.Entry<V>>, ~m2: List<&2, S.Entry<V>>, ~key: String, ~hp: (@+q: String -> {S.lookup(~V, m2, q) == S.lookup(~V, S.remove(~V, m, key), q) : Maybe<&2, V>}) & {S.size(~V, m2) == S.size(~V, S.remove(~V, m, key)) : Nat}, +hnd: {S.nodup(S.keys(~V, m)) == True{} : Bool}, +hnd2: {S.nodup(S.keys(~V, m2)) == True{} : Bool}) -> S.DelPost(~V, m, m2, key):
236 (Equal.cong(Maybe<&2, V>, Bool, z => S.is_some(~V, z), S.lookup(~V, m2, key), None{}, Equal.trans(Maybe<&2, V>, S.lookup(~V, m2, key), S.lookup(~V, S.remove(~V, m, key), key), None{}, Pair.fst(@+q: String -> {S.lookup(~V, m2, q) == S.lookup(~V, S.remove(~V, m, key), q) : Maybe<&2, V>}, {S.size(~V, m2) == S.size(~V, S.remove(~V, m, key)) : Nat}, hp)(key), SL.lookup_remove_same(~V, m, key, key, K.str_refl(key), hnd))),
237 (q => hq => del_other(~V, m, m2, key, q, hq, Pair.fst(@+q: String -> {S.lookup(~V, m2, q) == S.lookup(~V, S.remove(~V, m, key), q) : Maybe<&2, V>}, {S.size(~V, m2) == S.size(~V, S.remove(~V, m, key)) : Nat}, hp)(q)),
238 (hn => q => del_absent(~V, m, m2, key, hn, q, Pair.fst(@+q: String -> {S.lookup(~V, m2, q) == S.lookup(~V, S.remove(~V, m, key), q) : Maybe<&2, V>}, {S.size(~V, m2) == S.size(~V, S.remove(~V, m, key)) : Nat}, hp)(q)),
239 (%Equal.sym(Nat, S.size(~V, m2), S.size(~V, S.remove(~V, m, key)), Pair.snd(@+q: String -> {S.lookup(~V, m2, q) == S.lookup(~V, S.remove(~V, m, key), q) : Maybe<&2, V>}, {S.size(~V, m2) == S.size(~V, S.remove(~V, m, key)) : Nat}, hp)) : {Bool.pick(Nat, S.has(~V, m, key), 1n+_, _) == S.size(~V, m) : Nat}
240 size_remove(~V, m, key),
241 (q => del_mem(~V, m, m2, key, hnd, q, Pair.fst(@+q: String -> {S.lookup(~V, m2, q) == S.lookup(~V, S.remove(~V, m, key), q) : Maybe<&2, V>}, {S.size(~V, m2) == S.size(~V, S.remove(~V, m, key)) : Nat}, hp)(q)), hnd2)))))
242
243def pc_from(~V: Data, +sh: ST.Sh<V>, +hg: {ST.good(~V, sh) == True{} : Bool}, +key: String, -r: H.HashMap<&2, V> & Maybe<&2, V>, po: PO.PopOK(~V, sh, key, r)) -> PopContract(~V, sh, key, r):
244 match po:
245 case Tuple{+sh2, Tuple{+e, rest}}:
246 (+hg2, rest2) = rest
247 (sh2, (e, (hg2, del_post(~V, ~ST.model(~V, sh), ~ST.model(~V, sh2), ~key, ~rest2, model_nodup(~V, sh, hg), model_nodup(~V, sh2, hg2)))))
248
249def dc_from(~V: Data, +sh: ST.Sh<V>, +hg: {ST.good(~V, sh) == True{} : Bool}, +key: String, -r: H.HashMap<&2, V>, po: PO.DelOK(~V, sh, key, r)) -> DelContract(~V, sh, key, r):
250 match po:
251 case Tuple{+sh2, Tuple{+e, rest}}:
252 (+hg2, rest2) = rest
253 (sh2, (e, (hg2, del_post(~V, ~ST.model(~V, sh), ~ST.model(~V, sh2), ~key, ~rest2, model_nodup(~V, sh, hg), model_nodup(~V, sh2, hg2)))))
254
255# ---- reads (SPARK's Element, Contains, Length, Empty_Map) ----
256def gv_of(~V: Data, +sh: ST.Sh<V>, +dflt: V, +key: String, -r: H.HashMap<&2, V> & V, ok: G.GetOK(~V, sh, dflt, key, r)) -> {Pair.snd(H.HashMap<&2, V>, V, r) == S.get(~V, dflt, ST.model(~V, sh), key) : V}:
257 match ok:
258 case Tuple{+sh2, Tuple{+e, rest}}:
259 %Equal.sym(H.HashMap<&2, V> & V, r, (ST.real(~V, sh2), S.get(~V, dflt, ST.model(~V, sh), key)), e) : {Pair.snd(H.HashMap<&2, V>, V, _) == S.get(~V, dflt, ST.model(~V, sh), key) : V}
260 {==}
261
262# Element (Container, Key) = Element (Model, Key) when the key is present
263def element_value(~V: Data, +sh: ST.Sh<V>, +hg: {ST.good(~V, sh) == True{} : Bool}, +dflt: V, +key: String, +x: V, +hl: {S.lookup(~V, ST.model(~V, sh), key) == Some{x} : Maybe<&2, V>}) -> S.Element.element_value(~V, ST.model(~V, sh), key, x, hl, Pair.snd(H.HashMap<&2, V>, V, H.get(V, dflt, ST.real(~V, sh), key))):
264 %Equal.sym(V, Pair.snd(H.HashMap<&2, V>, V, H.get(V, dflt, ST.real(~V, sh), key)), S.get(~V, dflt, ST.model(~V, sh), key), gv_of(~V, sh, dflt, key, H.get(V, dflt, ST.real(~V, sh), key), G.get_ok(~V, sh, hg, dflt, key))) : {_ == x : V}
265 %Equal.sym(Maybe<&2, V>, S.lookup(~V, ST.model(~V, sh), key), Some{x}, hl) : {S.get_m(~V, dflt, _) == x : V}
266 {==}
267
268# a missing key reads as the default (SPARK's Element has Pre => Contains)
269def element_default(~V: Data, +sh: ST.Sh<V>, +hg: {ST.good(~V, sh) == True{} : Bool}, +dflt: V, +key: String, +hl: {S.lookup(~V, ST.model(~V, sh), key) == None{} : Maybe<&2, V>}) -> S.Element.element_default(~V, ST.model(~V, sh), key, dflt, hl, Pair.snd(H.HashMap<&2, V>, V, H.get(V, dflt, ST.real(~V, sh), key))):
270 %Equal.sym(V, Pair.snd(H.HashMap<&2, V>, V, H.get(V, dflt, ST.real(~V, sh), key)), S.get(~V, dflt, ST.model(~V, sh), key), gv_of(~V, sh, dflt, key, H.get(V, dflt, ST.real(~V, sh), key), G.get_ok(~V, sh, hg, dflt, key))) : {_ == dflt : V}
271 %Equal.sym(Maybe<&2, V>, S.lookup(~V, ST.model(~V, sh), key), None{}, hl) : {S.get_m(~V, dflt, _) == dflt : V}
272 {==}
273
274def hv_of(~V: Data, +sh: ST.Sh<V>, +key: String, -r: H.HashMap<&2, V> & Bool, ok: HA.HasOK(~V, sh, key, r)) -> {Pair.snd(H.HashMap<&2, V>, Bool, r) == S.has(~V, ST.model(~V, sh), key) : Bool}:
275 match ok:
276 case Tuple{+sh2, Tuple{+e, rest}}:
277 %Equal.sym(H.HashMap<&2, V> & Bool, r, (ST.real(~V, sh2), S.has(~V, ST.model(~V, sh), key)), e) : {Pair.snd(H.HashMap<&2, V>, Bool, _) == S.has(~V, ST.model(~V, sh), key) : Bool}
278 {==}
279
280# Contains (Container, Key) = Has_Key (Model, Key)
281def contains_value(~V: Data, +sh: ST.Sh<V>, +hg: {ST.good(~V, sh) == True{} : Bool}, +key: String) -> S.Contains.contains_value(~V, ST.model(~V, sh), key, Pair.snd(H.HashMap<&2, V>, Bool, H.has(&2, V, ST.real(~V, sh), key))):
282 hv_of(~V, sh, key, H.has(&2, V, ST.real(~V, sh), key), HA.has_ok(~V, sh, hg, key))
283
284# Length (Container) = Length (Model), and Length = the number of keys
285def length_value(~V: Data, +sh: ST.Sh<V>, +hg: {ST.good(~V, sh) == True{} : Bool}) -> S.Length.length_value(~V, ST.model(~V, sh), U32.to_nat(Pair.snd(H.HashMap<&2, V>, U32, H.size(&2, V, ST.real(~V, sh))))):
286 Equal.trans(Nat, U32.to_nat(Pair.snd(H.HashMap<&2, V>, U32, H.size(&2, V, ST.real(~V, sh)))), S.size(~V, ST.model(~V, sh)), SC.length(String, S.keys(~V, ST.model(~V, sh))), Pair.snd({H.size(&2, V, ST.real(~V, sh)) == (ST.real(~V, sh), Pair.snd(H.HashMap<&2, V>, U32, H.size(&2, V, ST.real(~V, sh)))) : H.HashMap<&2, V> & U32}, {U32.to_nat(Pair.snd(H.HashMap<&2, V>, U32, H.size(&2, V, ST.real(~V, sh)))) == S.size(~V, ST.model(~V, sh)) : Nat}, SZ.size_ok(~V, sh, hg)), Equal.sym(Nat, SC.length(String, S.keys(~V, ST.model(~V, sh))), S.size(~V, ST.model(~V, sh)), keys_len(~V, ST.model(~V, sh))))
287
288# Length does not change the map
289def length_frame(~V: Data, +sh: ST.Sh<V>, +hg: {ST.good(~V, sh) == True{} : Bool}) -> S.Length.length_frame(~V, ST.real(~V, sh), Pair.fst(H.HashMap<&2, V>, U32, H.size(&2, V, ST.real(~V, sh)))):
290 Equal.cong(H.HashMap<&2, V> & U32, H.HashMap<&2, V>, p => Pair.fst(H.HashMap<&2, V>, U32, p), H.size(&2, V, ST.real(~V, sh)), (ST.real(~V, sh), Pair.snd(H.HashMap<&2, V>, U32, H.size(&2, V, ST.real(~V, sh)))), Pair.fst({H.size(&2, V, ST.real(~V, sh)) == (ST.real(~V, sh), Pair.snd(H.HashMap<&2, V>, U32, H.size(&2, V, ST.real(~V, sh)))) : H.HashMap<&2, V> & U32}, {U32.to_nat(Pair.snd(H.HashMap<&2, V>, U32, H.size(&2, V, ST.real(~V, sh)))) == S.size(~V, ST.model(~V, sh)) : Nat}, SZ.size_ok(~V, sh, hg)))
291
292# Empty_Map: Length = 0 and no key is present
293def new_model(~V: Data) -> S.Empty_Map.new_model(~V, ST.model(~V, NW.empty(~V))):
294 Pair.snd({ST.good(~V, NW.empty(~V)) == True{} : Bool}, {ST.model(~V, NW.empty(~V)) == Nil{} : List<&2, S.Entry<V>>}, Pair.snd({H.new(&2, V) == ST.real(~V, NW.empty(~V)) : H.HashMap<&2, V>}, {ST.good(~V, NW.empty(~V)) == True{} : Bool} & {ST.model(~V, NW.empty(~V)) == Nil{} : List<&2, S.Entry<V>>}, NW.new_ok(~V)))
295
296def new_length(~V: Data) -> S.Empty_Map.new_length(~V, ST.model(~V, NW.empty(~V))):
297 %Equal.sym(List<&2, S.Entry<V>>, ST.model(~V, NW.empty(~V)), Nil{}, new_model(~V)) : {S.size(~V, _) == 0n : Nat}
298 {==}
299
300def new_absent(~V: Data, +key: String) -> S.Empty_Map.new_absent(~V, ST.model(~V, NW.empty(~V)), key):
301 %Equal.sym(List<&2, S.Entry<V>>, ST.model(~V, NW.empty(~V)), Nil{}, new_model(~V)) : {S.lookup(~V, _, key) == None{} : Maybe<&2, V>}
302 {==}
303
304# ---- the four contracts on the implementation, re-exported ----
305
306def set_contract(~V: Data, +sh: ST.Sh<V>, +hg: {ST.good(~V, sh) == True{} : Bool}, +cap: Nat, +hc30: {Nat.is_le(cap, 30n) == True{} : Bool}, +hcap: {Nat.is_le(Nat.double(1n+S.size(~V, ST.model(~V, sh))), SC.pow2(cap)) == True{} : Bool}, +key: String, +x: V) -> SetContract(~V, sh, key, x, H.set(&2, V, ST.real(~V, sh), key, x)):
307 sc_from(~V, sh, key, x, H.set(&2, V, ST.real(~V, sh), key, x), SO.set_ok(~V, sh, hg, cap, hc30, hcap, key, x))
308
309def pop_contract(~V: Data, +sh: ST.Sh<V>, +hg: {ST.good(~V, sh) == True{} : Bool}, +key: String) -> PopContract(~V, sh, key, H.pop(&2, V, ST.real(~V, sh), key)):
310 pc_from(~V, sh, hg, key, H.pop(&2, V, ST.real(~V, sh), key), PO.pop_ok(~V, sh, hg, key))
311
312def del_contract(~V: Data, +sh: ST.Sh<V>, +hg: {ST.good(~V, sh) == True{} : Bool}, +key: String) -> DelContract(~V, sh, key, H.del(&2, V, ST.real(~V, sh), key)):
313 dc_from(~V, sh, hg, key, H.del(&2, V, ST.real(~V, sh), key), PO.del_ok(~V, sh, hg, key))
314
315def keys_contract(~V: Data, +sh: ST.Sh<V>, +hg: {ST.good(~V, sh) == True{} : Bool}) -> KeysContract(~V, sh, H.keys(&2, V, ST.real(~V, sh))):
316 kc_from(~V, sh, hg, H.keys(&2, V, ST.real(~V, sh)), KW.keys_ok(~V, sh, hg))