1 import Base 2 import ../../../spec/containers/hash_table.bend as S 3 import ../../../spec/lib/common.bend as SC 4 import ../../../src/containers/hash_table.bend as H 5 import ./state.bend as ST 6 import ./new.bend as NW 7 import ./get.bend as G 8 import ./has.bend as HA 9 import ./size.bend as SZ 10 import ./set.bend as ST2 11 import ./setok.bend as SO 12 import ./pop.bend as PO 13 import ./keysw.bend as KW 14 import ./keys.bend as K 15 import ./speclem.bend as SL 16 import ../../lib/logic.bend as L 17 import ../../lib/array.bend as AR 18 import ./poplem.bend as PL 19 import ./table.bend as TB 20 import ../../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 50 def 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>}): 51 NW.new_ok(~V) 52 53 def get_ok(~V: Data, +sh: ST.Sh, +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 56 def has_ok(~V: Data, +sh: ST.Sh, +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 59 def size_ok(~V: Data, +sh: ST.Sh, +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 62 def set_ok(~V: Data, +sh: ST.Sh, +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 65 def pop_ok(~V: Data, +sh: ST.Sh, +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 68 def del_ok(~V: Data, +sh: ST.Sh, +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 71 def keys_ok(~V: Data, +sh: ST.Sh, +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 ---- 79 def key_refl(+a: String) -> S.Equivalent_Keys.key_refl(a): 80 K.str_refl(a) 81 82 def key_sym(+a: String, +b: String) -> S.Equivalent_Keys.key_sym(a, b): 83 K.str_sym(a, b) 84 85 def 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 89 def 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 93 def 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 ---- 97 def mh_c(~V: Data, +j: String, +v: V, +t: List<&2, S.Entry>, +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 107 def mem_has(~V: Data, +m: List<&2, S.Entry>, +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 115 def keys_len(~V: Data, +m: List<&2, S.Entry>) -> {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 123 def 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 130 def ssp(~V: Data, +m: List<&2, S.Entry>, +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 140 def size_set(~V: Data, +m: List<&2, S.Entry>, +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 143 def srp(~V: Data, +m: List<&2, S.Entry>, +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>, 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 153 def size_remove(~V: Data, +m: List<&2, S.Entry>, +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 156 def hso_c(~V: Data, +m: List<&2, S.Entry>, +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 165 def hro_c(~V: Data, +m: List<&2, S.Entry>, +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 ---- 175 def model_nodup(~V: Data, +sh: ST.Sh, +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 180 def keys_post(~V: Data, +sh: ST.Sh, +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 184 def KeysContract(~V: Data, +sh: ST.Sh, r: H.HashMap<&2, V> & List<&2, String>) -> Type: 185 Sigma<&1, &1, ST.Sh, 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>}) & S.KeysPost(~V, ST.model(~V, sh)))> 186 187 def kc_from(~V: Data, +sh: ST.Sh, +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 192 def SetContract(~V: Data, +sh: ST.Sh, +key: String, +x: V, r: H.HashMap<&2, V>) -> Type: 193 Sigma<&1, &1, ST.Sh, 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 195 def set_same(~V: Data, +m: List<&2, S.Entry>, +m2: List<&2, S.Entry>, +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 198 def set_other(~V: Data, +m: List<&2, S.Entry>, +m2: List<&2, S.Entry>, +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 201 def set_mem(~V: Data, +m: List<&2, S.Entry>, +m2: List<&2, S.Entry>, +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 205 def set_post(~V: Data, ~m: List<&2, S.Entry>, ~m2: List<&2, S.Entry>, ~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 212 def sc_from(~V: Data, +sh: ST.Sh, +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 219 def PopContract(~V: Data, +sh: ST.Sh, +key: String, r: H.HashMap<&2, V> & Maybe<&2, V>) -> Type: 220 Sigma<&1, &1, ST.Sh, 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 222 def DelContract(~V: Data, +sh: ST.Sh, +key: String, r: H.HashMap<&2, V>) -> Type: 223 Sigma<&1, &1, ST.Sh, 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 225 def del_absent(~V: Data, +m: List<&2, S.Entry>, +m2: List<&2, S.Entry>, +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>, 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 228 def del_other(~V: Data, +m: List<&2, S.Entry>, +m2: List<&2, S.Entry>, +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 231 def del_mem(~V: Data, +m: List<&2, S.Entry>, +m2: List<&2, S.Entry>, +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 235 def del_post(~V: Data, ~m: List<&2, S.Entry>, ~m2: List<&2, S.Entry>, ~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 243 def pc_from(~V: Data, +sh: ST.Sh, +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 249 def dc_from(~V: Data, +sh: ST.Sh, +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) ---- 256 def gv_of(~V: Data, +sh: ST.Sh, +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 263 def element_value(~V: Data, +sh: ST.Sh, +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) 269 def element_default(~V: Data, +sh: ST.Sh, +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 274 def hv_of(~V: Data, +sh: ST.Sh, +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) 281 def contains_value(~V: Data, +sh: ST.Sh, +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 285 def length_value(~V: Data, +sh: ST.Sh, +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 289 def length_frame(~V: Data, +sh: ST.Sh, +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 293 def 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>}, 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>}, NW.new_ok(~V))) 295 296 def new_length(~V: Data) -> S.Empty_Map.new_length(~V, ST.model(~V, NW.empty(~V))): 297 %Equal.sym(List<&2, S.Entry>, ST.model(~V, NW.empty(~V)), Nil{}, new_model(~V)) : {S.size(~V, _) == 0n : Nat} 298 {==} 299 300 def 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>, 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 306 def set_contract(~V: Data, +sh: ST.Sh, +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 309 def pop_contract(~V: Data, +sh: ST.Sh, +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 312 def del_contract(~V: Data, +sh: ST.Sh, +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 315 def keys_contract(~V: Data, +sh: ST.Sh, +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))