proofs/containers/balanced_search_tree/capi.bend
bend-collections-laws-containers@1.0.0.0 · 96 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/proofs/lib/logic.bend as L
3import bend-collections-laws-containers@1.0.0.0/proofs/lib/order.bend as O
4import bend-collections-laws-containers@1.0.0.0/spec/containers/balanced_search_tree/main.bend as S
5import bend-collections-laws-containers@1.0.0.0/src/containers/balanced_search_tree.bend as M
6import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/state.bend as ST
7import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/mirror.bend as MI
8import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/sim.bend as SM
9import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/ok.bend as OK
10import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/prim.bend as PR
11import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/cur.bend as CU
12import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/cnx.bend as CX
13import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/csv.bend as CS
14import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/crm.bend as CR
15import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/rmv.bend as RV
16import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/ccv.bend as CV
17
18# The implementation's cursors refine the specification's: from a good
19# cursor (a good shadow, its ids 0 or in the tree), each operation gives the
20# real cursor of a good cursor whose model is the specification's result.
21# (source: tools/generators/tm_hand/capi.src)
22
23
24# ---- starting ----
25
26
27def cst_up(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, -sp: S.Cursor<K, V>, -mc: MI.MCursor<K, V>, -r: M.Cursor<K, V, cmp>, +hs: {r == MI.rc(~K, ~V, ~cmp, mc) : M.Cursor<K, V, cmp>}, p: Sigma<&1, &1, MI.MCursor<K, V>, c2 => {MI.rc(~K, ~V, ~cmp, mc) == MI.rc(~K, ~V, ~cmp, c2) : M.Cursor<K, V, cmp>} & ({sp == CU.cmod(~K, ~V, ~cmp, c2) : S.Cursor<K, V>} & {CU.cgood(~K, ~V, ~cmp, c2) == True{} : Bool})>) -> Sigma<&1, &1, MI.MCursor<K, V>, c2 => {r == MI.rc(~K, ~V, ~cmp, c2) : M.Cursor<K, V, cmp>} & ({sp == CU.cmod(~K, ~V, ~cmp, c2) : S.Cursor<K, V>} & {CU.cgood(~K, ~V, ~cmp, c2) == True{} : Bool})>:
28 match p:
29 case Tuple{+c2, Tuple{+h1, rest}}:
30 (c2, (Equal.trans(M.Cursor<K, V, cmp>, r, MI.rc(~K, ~V, ~cmp, mc), MI.rc(~K, ~V, ~cmp, c2), hs, h1), rest))
31
32def iterator_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +sh: ST.Sh<K, V>, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}) -> Sigma<&1, &1, MI.MCursor<K, V>, c2 => {M.iterator(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh)) == MI.rc(~K, ~V, ~cmp, c2) : M.Cursor<K, V, cmp>} & ({S.iterator(K, V, ST.model(~K, ~V, ~cmp, sh)) == CU.cmod(~K, ~V, ~cmp, c2) : S.Cursor<K, V>} & {CU.cgood(~K, ~V, ~cmp, c2) == True{} : Bool})>:
33 match sh:
34 case ST.SH{+n, +root, +lo, +hi, +free, +l, +d, +nl, +pl, +tg, +fl}:
35 cst_up(~K, ~V, ~cmp, S.iterator(K, V, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl})), MI.iterator(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), M.iterator(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl})), SM.iterator_s(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, OK.dg_good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, hg)), CU.iterator_m(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg))
36
37def descending_iterator_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +sh: ST.Sh<K, V>, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}) -> Sigma<&1, &1, MI.MCursor<K, V>, c2 => {M.descending_iterator(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh)) == MI.rc(~K, ~V, ~cmp, c2) : M.Cursor<K, V, cmp>} & ({S.descending_iterator(K, V, ST.model(~K, ~V, ~cmp, sh)) == CU.cmod(~K, ~V, ~cmp, c2) : S.Cursor<K, V>} & {CU.cgood(~K, ~V, ~cmp, c2) == True{} : Bool})>:
38 match sh:
39 case ST.SH{+n, +root, +lo, +hi, +free, +l, +d, +nl, +pl, +tg, +fl}:
40 cst_up(~K, ~V, ~cmp, S.descending_iterator(K, V, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl})), MI.descending_iterator(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), M.descending_iterator(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl})), SM.descending_iterator_s(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, OK.dg_good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, hg)), CU.descending_iterator_m(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg))
41
42# ---- stepping ----
43
44def iterator_has_next_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +c: MI.MCursor<K, V>, +hc: {CU.cgood(~K, ~V, ~cmp, c) == True{} : Bool}) -> CU.CPOK(~K, ~V, ~cmp, Bool, S.iterator_has_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c)), M.iterator_has_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c))):
45 match c:
46 case MI.MC{ST.SH{+n, +root, +lo, +hi, +free, +l, +d, +nl, +pl, +tg, +fl}, +nx, +cu, +lo2, +hi2, +fw}:
47 CU.cok_cpok(~K, ~V, ~cmp, Bool, S.iterator_has_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw})), MI.iterator_has_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw}), M.iterator_has_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw})), SM.iterator_has_next_s(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw}, OK.dg_good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, L.and_left(ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl), Bool.and(CU.idok(ST.ids(tg), nx), Bool.and(CU.idok(ST.ids(tg), cu), Bool.or(Nat.is_eq(nx, 0n), Bool.not(Nat.is_eq(nx, cu))))), hc))), CU.has_next_m(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, nx, cu, lo2, hi2, fw, hc))
48
49def iterator_next_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +c: MI.MCursor<K, V>, +hc: {CU.cgood(~K, ~V, ~cmp, c) == True{} : Bool}) -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c)), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c))):
50 match c:
51 case MI.MC{ST.SH{+n, +root, +lo, +hi, +free, +l, +d, +nl, +pl, +tg, +fl}, +nx, +cu, +lo2, +hi2, +fw}:
52 CU.cok_cpok(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw})), MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw}), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw})), SM.iterator_next_s(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw}, OK.dg_good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, L.and_left(ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl), Bool.and(CU.idok(ST.ids(tg), nx), Bool.and(CU.idok(ST.ids(tg), cu), Bool.or(Nat.is_eq(nx, 0n), Bool.not(Nat.is_eq(nx, cu))))), hc))), CU.cstep_cok(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw})), MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw}), ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, fw, CX.next_m(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, nx, cu, lo2, hi2, fw, hc)))
53
54def iterator_next_key_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +c: MI.MCursor<K, V>, +hc: {CU.cgood(~K, ~V, ~cmp, c) == True{} : Bool}) -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, K>, S.iterator_next_key(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c)), M.iterator_next_key(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c))):
55 match c:
56 case MI.MC{ST.SH{+n, +root, +lo, +hi, +free, +l, +d, +nl, +pl, +tg, +fl}, +nx, +cu, +lo2, +hi2, +fw}:
57 CU.cok_cpok(~K, ~V, ~cmp, Maybe<&2, K>, S.iterator_next_key(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw})), MI.iterator_next_key(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw}), M.iterator_next_key(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw})), SM.iterator_next_key_s(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw}, OK.dg_good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, L.and_left(ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl), Bool.and(CU.idok(ST.ids(tg), nx), Bool.and(CU.idok(ST.ids(tg), cu), Bool.or(Nat.is_eq(nx, 0n), Bool.not(Nat.is_eq(nx, cu))))), hc))), CX.next_key_m(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, nx, cu, lo2, hi2, fw, hc))
58
59def iterator_next_value_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +c: MI.MCursor<K, V>, +hc: {CU.cgood(~K, ~V, ~cmp, c) == True{} : Bool}) -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, V>, S.iterator_next_value(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c)), M.iterator_next_value(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c))):
60 match c:
61 case MI.MC{ST.SH{+n, +root, +lo, +hi, +free, +l, +d, +nl, +pl, +tg, +fl}, +nx, +cu, +lo2, +hi2, +fw}:
62 CU.cok_cpok(~K, ~V, ~cmp, Maybe<&2, V>, S.iterator_next_value(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw})), MI.iterator_next_value(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw}), M.iterator_next_value(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw})), SM.iterator_next_value_s(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw}, OK.dg_good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, L.and_left(ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl), Bool.and(CU.idok(ST.ids(tg), nx), Bool.and(CU.idok(ST.ids(tg), cu), Bool.or(Nat.is_eq(nx, 0n), Bool.not(Nat.is_eq(nx, cu))))), hc))), CX.next_value_m(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, nx, cu, lo2, hi2, fw, hc))
63
64# ---- changing the map through the cursor ----
65
66
67def iterator_set_value_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +c: MI.MCursor<K, V>, +hc: {CU.cgood(~K, ~V, ~cmp, c) == True{} : Bool}, +v: V) -> CU.CPOK(~K, ~V, ~cmp, Result<&2, &2, M.Error, V>, S.iterator_set_value(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c), v), M.iterator_set_value(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c), v)):
68 match c:
69 case MI.MC{ST.SH{+n, +root, +lo, +hi, +free, +l, +d, +nl, +pl, +tg, +fl}, +nx, +cu, +lo2, +hi2, +fw}:
70 CU.cok_cpok(~K, ~V, ~cmp, Result<&2, &2, M.Error, V>, S.iterator_set_value(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw}), v), MI.iterator_set_value(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw}, v), M.iterator_set_value(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw}), v), SM.iterator_set_value_s(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw}, v, OK.dg_good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, L.and_left(ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl), Bool.and(CU.idok(ST.ids(tg), nx), Bool.and(CU.idok(ST.ids(tg), cu), Bool.or(Nat.is_eq(nx, 0n), Bool.not(Nat.is_eq(nx, cu))))), hc))), CS.set_value_m(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, cu, nx, lo2, hi2, fw, v, hc))
71
72
73def iterator_remove_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +c: MI.MCursor<K, V>, +hc: {CU.cgood(~K, ~V, ~cmp, c) == True{} : Bool}) -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, V>, S.iterator_remove(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c)), M.iterator_remove(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c))):
74 match c:
75 case MI.MC{ST.SH{+n, +root, +lo, +hi, +free, +l, +d, +nl, +pl, +tg, +fl}, +nx, 0n, +lo2, +hi2, +fw}:
76 CU.cok_cpok(~K, ~V, ~cmp, Maybe<&2, V>, S.iterator_remove(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, 0n, lo2, hi2, fw})), MI.iterator_remove(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, 0n, lo2, hi2, fw}), M.iterator_remove(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, 0n, lo2, hi2, fw})), SM.iterator_remove_s(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, 0n, lo2, hi2, fw}, OK.dg_good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, L.and_left(ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl), Bool.and(CU.idok(ST.ids(tg), nx), Bool.and(CU.idok(ST.ids(tg), 0n), Bool.or(Nat.is_eq(nx, 0n), Bool.not(Nat.is_eq(nx, 0n))))), hc))), CR.rmz(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, lo2, hi2, fw, nx, hc))
77 case MI.MC{ST.SH{+n, +root, +lo, +hi, +free, +l, +d, +nl, +pl, +tg, +fl}, +nx, 1n+ +j, +lo2, +hi2, +fw}:
78 CU.cok_cpok(~K, ~V, ~cmp, Maybe<&2, V>, S.iterator_remove(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, 1n+j, lo2, hi2, fw})), MI.iterator_remove(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, 1n+j, lo2, hi2, fw}), M.iterator_remove(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, 1n+j, lo2, hi2, fw})), SM.iterator_remove_s(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, 1n+j, lo2, hi2, fw}, OK.dg_good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, L.and_left(ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl), Bool.and(CU.idok(ST.ids(tg), nx), Bool.and(CU.idok(ST.ids(tg), 1n+j), Bool.or(Nat.is_eq(nx, 0n), Bool.not(Nat.is_eq(nx, 1n+j))))), hc))), CR.rmu(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, lo2, hi2, fw, nx, j, hc, kk => pc => pa => pb => hbc => hplug => hr => hok => hfin => RV.rm_x(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, L.and_left(ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl), Bool.and(CU.idok(ST.ids(tg), nx), Bool.and(CU.idok(ST.ids(tg), 1n+j), Bool.or(Nat.is_eq(nx, 0n), Bool.not(Nat.is_eq(nx, 1n+j))))), hc), kk, pc, j, pa, pb, hbc, hplug, hr, hok, hfin, ST.nd(K, nl, 1n+j), {==}), kk => s2 => e => hd => Equal.trans(M.TreeMap<K, V, cmp> & M.Search, MI.rp(~K, ~V, ~cmp, M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), kk)), M.search(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j))))), kk), MI.rp(~K, ~V, ~cmp, M.Search, MI.search(~K, ~V, ~cmp, s2, kk)), Equal.sym(M.TreeMap<K, V, cmp> & M.Search, M.search(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j))))), kk), MI.rp(~K, ~V, ~cmp, M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), kk)), SM.search_s(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), kk, SM.remove_id_g(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, 1n+j, OK.dg_good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, L.and_left(ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl), Bool.and(CU.idok(ST.ids(tg), nx), Bool.and(CU.idok(ST.ids(tg), 1n+j), Bool.or(Nat.is_eq(nx, 0n), Bool.not(Nat.is_eq(nx, 1n+j))))), hc))))), Equal.trans(M.TreeMap<K, V, cmp> & M.Search, M.search(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j))))), kk), M.search(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, s2), kk), MI.rp(~K, ~V, ~cmp, M.Search, MI.search(~K, ~V, ~cmp, s2, kk)), L.subst(M.TreeMap<K, V, cmp>, z => {M.search(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j))))), kk) == M.search(~K, ~V, ~cmp, z, kk) : M.TreeMap<K, V, cmp> & M.Search}, ST.real(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j))))), ST.real(~K, ~V, ~cmp, s2), e, {==}), SM.search_s(~K, ~V, ~cmp, s2, kk, hd)))))
79
80# ---- finishing ----
81
82def iterator_finish_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +c: MI.MCursor<K, V>, +hc: {CU.cgood(~K, ~V, ~cmp, c) == True{} : Bool}) -> Sigma<&1, &1, ST.Sh<K, V>, s2 => {M.iterator_finish(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c)) == ST.real(~K, ~V, ~cmp, s2) : M.TreeMap<K, V, cmp>} & ({S.iterator_finish(K, V, CU.cmod(~K, ~V, ~cmp, c)) == ST.model(~K, ~V, ~cmp, s2) : S.Model<K, V>} & {ST.good(~K, ~V, ~cmp, s2) == True{} : Bool})>:
83 match c:
84 case MI.MC{ST.SH{+n, +root, +lo, +hi, +free, +l, +d, +nl, +pl, +tg, +fl}, +nx, +cu, +lo2, +hi2, +fw}:
85 (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, (SM.iterator_finish_s(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw}, OK.dg_good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, L.and_left(ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl), Bool.and(CU.idok(ST.ids(tg), nx), Bool.and(CU.idok(ST.ids(tg), cu), Bool.or(Nat.is_eq(nx, 0n), Bool.not(Nat.is_eq(nx, cu))))), hc))), ({==}, L.and_left(ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl), Bool.and(CU.idok(ST.ids(tg), nx), Bool.and(CU.idok(ST.ids(tg), cu), Bool.or(Nat.is_eq(nx, 0n), Bool.not(Nat.is_eq(nx, cu))))), hc))))
86
87# ---- contains_value: the walk over the entries ----
88
89
90def via_cv(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, -impl: M.TreeMap<K, V, cmp> & Bool, -mir: ST.Sh<K, V> & Bool, +s: ST.Sh<K, V>, +o: Bool, +hs: {impl == MI.rp(~K, ~V, ~cmp, Bool, mir) : M.TreeMap<K, V, cmp> & Bool}, +hm: {mir == (s, o) : ST.Sh<K, V> & Bool}) -> {impl == (ST.real(~K, ~V, ~cmp, s), o) : M.TreeMap<K, V, cmp> & Bool}:
91 L.subst(ST.Sh<K, V> & Bool, z => {impl == MI.rp(~K, ~V, ~cmp, Bool, z) : M.TreeMap<K, V, cmp> & Bool}, mir, (s, o), hm, hs)
92
93def contains_value_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), ~eq: V -> V -> Bool, +sh: ST.Sh<K, V>, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}, +w: V) -> OK.POK(~K, ~V, ~cmp, Bool, S.contains_value(~K, ~V, ~eq, ST.model(~K, ~V, ~cmp, sh), w), M.contains_value(~K, ~V, ~cmp, ~eq, ST.real(~K, ~V, ~cmp, sh), w)):
94 match sh:
95 case ST.SH{+n, +root, +lo, +hi, +free, +l, +d, +nl, +pl, +tg, +fl}:
96 OK.pok_read(~K, ~V, ~cmp, Bool, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, hg, S.any_value(~K, ~V, ~eq, w, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), S.contains_value(~K, ~V, ~eq, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), w), M.contains_value(~K, ~V, ~cmp, ~eq, ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), w), {==}, via_cv(~K, ~V, ~cmp, M.contains_value(~K, ~V, ~cmp, ~eq, ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), w), MI.contains_value(~K, ~V, ~cmp, ~eq, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, w), ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, S.any_value(~K, ~V, ~eq, w, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), SM.contains_value_s(~K, ~V, ~cmp, ~eq, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, w, OK.dg_good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, hg)), CV.contains_value_m(~K, ~V, ~cmp, ~o, ~eq, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, w)))