1 import Base 2 import ../../lib/logic.bend as L 3 import ../../lib/order.bend as O 4 import ../../../spec/lib/common.bend as SC 5 import ../../../spec/containers/balanced_search_tree/main.bend as S 6 import ../../../src/containers/balanced_search_tree.bend as M 7 import ./state.bend as ST 8 import ./mirror.bend as MI 9 import ./sim.bend as SM 10 import ./ok.bend as OK 11 import ./reads.bend as RD 12 import ./putm.bend as PM 13 import ./rmv.bend as RV 14 import ./cur.bend as CU 15 import ./vdef.bend as VD 16 17 # The implementation's views refine the specification's: a view of a good 18 # shadow is realized by the implementation's view and modelled by the 19 # specification's over the shadow's model; every view operation gives the 20 # real view (and answer) of a good view whose model is the specification's 21 # result. (source: tools/generators/tm_hand/vw.src) 22 23 24 # ---- making views ---- 25 26 def head_map_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +sh: ST.Sh, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}, +up: M.Bound) -> VD.VOK(~K, ~V, ~cmp, S.head_map(K, V, ST.model(~K, ~V, ~cmp, sh), up), M.head_map(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh), up)): 27 (MI.MV{sh, M.Unbounded{}, up, False{}}, (SM.head_map_s(~K, ~V, ~cmp, sh, up, OK.dg_good(~K, ~V, ~cmp, sh, hg)), ({==}, hg))) 28 29 def tail_map_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +sh: ST.Sh, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}, +lw: M.Bound) -> VD.VOK(~K, ~V, ~cmp, S.tail_map(K, V, ST.model(~K, ~V, ~cmp, sh), lw), M.tail_map(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh), lw)): 30 (MI.MV{sh, lw, M.Unbounded{}, False{}}, (SM.tail_map_s(~K, ~V, ~cmp, sh, lw, OK.dg_good(~K, ~V, ~cmp, sh, hg)), ({==}, hg))) 31 32 def descending_map_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +sh: ST.Sh, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}) -> VD.VOK(~K, ~V, ~cmp, S.descending_map(K, V, ST.model(~K, ~V, ~cmp, sh)), M.descending_map(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh))): 33 (MI.MV{sh, M.Unbounded{}, M.Unbounded{}, True{}}, (SM.descending_map_s(~K, ~V, ~cmp, sh, OK.dg_good(~K, ~V, ~cmp, sh, hg)), ({==}, hg))) 34 35 def view_reverse_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +w: MI.MView, +hw: {VD.vgood(~K, ~V, ~cmp, w) == True{} : Bool}) -> VD.VOK(~K, ~V, ~cmp, S.view_reverse(K, V, VD.vmod(~K, ~V, ~cmp, w)), M.view_reverse(~K, ~V, ~cmp, MI.rv(~K, ~V, ~cmp, w))): 36 match w: 37 case MI.MV{+s, +lo2, +hi2, +d2}: 38 (MI.MV{s, lo2, hi2, Bool.not(d2)}, (SM.view_reverse_s(~K, ~V, ~cmp, MI.MV{s, lo2, hi2, d2}, OK.dg_good(~K, ~V, ~cmp, s, hw)), ({==}, hw))) 39 40 41 def view_finish_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +w: MI.MView, +hw: {VD.vgood(~K, ~V, ~cmp, w) == True{} : Bool}) -> Sigma<&1, &1, ST.Sh, s2 => {M.view_finish(~K, ~V, ~cmp, MI.rv(~K, ~V, ~cmp, w)) == ST.real(~K, ~V, ~cmp, s2) : M.TreeMap} & ({S.view_finish(K, V, VD.vmod(~K, ~V, ~cmp, w)) == ST.model(~K, ~V, ~cmp, s2) : S.Model} & {ST.good(~K, ~V, ~cmp, s2) == True{} : Bool})>: 42 match w: 43 case MI.MV{+s, +lo2, +hi2, +d2}: 44 (s, (SM.view_finish_s(~K, ~V, ~cmp, MI.MV{s, lo2, hi2, d2}, OK.dg_good(~K, ~V, ~cmp, s, hw)), ({==}, hw))) 45 46 # ---- sub_map: the bounds checked ---- 47 48 def rmod(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, r: Result<&1, &1, MI.MInvalid, MI.MView>) -> Result<&1, &1, S.InvalidView, S.View>: 49 match r: 50 case Done{w}: 51 Done{VD.vmod(~K, ~V, ~cmp, w)} 52 case Fail{MI.MI{s, e}}: 53 Fail{S.IV{ST.model(~K, ~V, ~cmp, s), e}} 54 55 def rgood(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, r: Result<&1, &1, MI.MInvalid, MI.MView>) -> Bool: 56 match r: 57 case Done{w}: 58 VD.vgood(~K, ~V, ~cmp, w) 59 case Fail{MI.MI{s, e}}: 60 ST.good(~K, ~V, ~cmp, s) 61 62 def ROK(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, sp: Result<&1, &1, S.InvalidView, S.View>, r: Result<&1, &1, M.InvalidView, M.View>) -> Type: 63 Sigma<&1, &1, Result<&1, &1, MI.MInvalid, MI.MView>, x => {r == MI.rr(~K, ~V, ~cmp, x) : Result<&1, &1, M.InvalidView, M.View>} & ({sp == rmod(~K, ~V, ~cmp, x) : Result<&1, &1, S.InvalidView, S.View>} & {rgood(~K, ~V, ~cmp, x) == True{} : Bool})> 64 65 def bv_eq(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +a: M.Bound, +b: M.Bound) -> {M.bounds_valid(~K, ~V, ~cmp, a, b) == S.bounds_valid(~K, ~cmp, a, b) : Bool}: 66 match a b: 67 case M.Unbounded{} M.Unbounded{}: 68 {==} 69 case M.Unbounded{} M.Inclusive{y}: 70 {==} 71 case M.Unbounded{} M.Exclusive{y}: 72 {==} 73 case M.Inclusive{x} M.Unbounded{}: 74 {==} 75 case M.Exclusive{x} M.Unbounded{}: 76 {==} 77 case M.Inclusive{+x} M.Inclusive{+y}: 78 CU.oo_eq(cmp(x, y), True{}) 79 case M.Inclusive{+x} M.Exclusive{+y}: 80 CU.oo_eq(cmp(x, y), True{}) 81 case M.Exclusive{+x} M.Inclusive{+y}: 82 CU.oo_eq(cmp(x, y), True{}) 83 case M.Exclusive{+x} M.Exclusive{+y}: 84 CU.oo_eq(cmp(x, y), True{}) 85 86 def sub_b(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +sh: ST.Sh, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}, +lw: M.Bound, +up: M.Bound, +b: Bool) -> {S.view_checked(K, V, ST.model(~K, ~V, ~cmp, sh), lw, up, b) == rmod(~K, ~V, ~cmp, MI.view_checked(~K, ~V, ~cmp, sh, lw, up, False{}, b)) : Result<&1, &1, S.InvalidView, S.View>} & {rgood(~K, ~V, ~cmp, MI.view_checked(~K, ~V, ~cmp, sh, lw, up, False{}, b)) == True{} : Bool}: 87 match b: 88 case True{}: 89 ({==}, hg) 90 case False{}: 91 ({==}, hg) 92 93 def sub_map_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +sh: ST.Sh, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}, +lw: M.Bound, +up: M.Bound) -> ROK(~K, ~V, ~cmp, S.sub_map(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, sh), lw, up), M.sub_map(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh), lw, up)): 94 %bv_eq(~K, ~V, ~cmp, lw, up) : ROK(~K, ~V, ~cmp, S.view_checked(K, V, ST.model(~K, ~V, ~cmp, sh), lw, up, _), M.sub_map(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh), lw, up)) 95 (MI.sub_map(~K, ~V, ~cmp, sh, lw, up), (SM.sub_map_s(~K, ~V, ~cmp, sh, lw, up, OK.dg_good(~K, ~V, ~cmp, sh, hg)), sub_b(~K, ~V, ~cmp, sh, hg, lw, up, M.bounds_valid(~K, ~V, ~cmp, lw, up)))) 96 97 # ---- get and contains_key: the key in range, then the map's ---- 98 99 100 def vget_b(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}) == True{} : Bool}, +lo2: M.Bound, +hi2: M.Bound, +d2: Bool, +k: K, +b: Bool) -> {MI.view_get_checked(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, k, lo2, hi2, d2, b) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}, S.pick(Maybe<&2, V>, b, S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), None{})) : MI.MView & Maybe<&2, V>}: 101 match b: 102 case True{}: 103 %Equal.sym(ST.Sh & Maybe<&2, V>, MI.get(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, k), (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl))), RD.get_m(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, k, hg)) : {MI.view_value(~K, ~V, ~cmp, lo2, hi2, d2, _) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}, S.pick(Maybe<&2, V>, True{}, S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), None{})) : MI.MView & Maybe<&2, V>} 104 {==} 105 case False{}: 106 {==} 107 108 def vget_m(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}) == True{} : Bool}, +lo2: M.Bound, +hi2: M.Bound, +d2: Bool, +k: K) -> {MI.view_get(~K, ~V, ~cmp, MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}, k) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}, S.pick(Maybe<&2, V>, S.in_range(~K, ~cmp, k, lo2, hi2), S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), None{})) : MI.MView & Maybe<&2, V>}: 109 %Equal.sym(Bool, M.in_range(~K, ~V, ~cmp, k, lo2, hi2), S.in_range(~K, ~cmp, k, lo2, hi2), CU.inr_eq(~K, ~V, ~cmp, k, lo2, hi2)) : {MI.view_get_checked(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, k, lo2, hi2, d2, _) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}, S.pick(Maybe<&2, V>, S.in_range(~K, ~cmp, k, lo2, hi2), S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), None{})) : MI.MView & Maybe<&2, V>} 110 vget_b(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, lo2, hi2, d2, k, S.in_range(~K, ~cmp, k, lo2, hi2)) 111 112 def view_get_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +w: MI.MView, +hw: {VD.vgood(~K, ~V, ~cmp, w) == True{} : Bool}, +k: K) -> VD.VPOK(~K, ~V, ~cmp, Maybe<&2, V>, S.view_get(~K, ~V, ~cmp, VD.vmod(~K, ~V, ~cmp, w), k), M.view_get(~K, ~V, ~cmp, MI.rv(~K, ~V, ~cmp, w), k)): 113 match w: 114 case MI.MV{ST.SH{+n, +root, +lo, +hi, +free, +l, +d, +nl, +pl, +tg, +fl}, +lo2, +hi2, +d2}: 115 VD.vm_pok(~K, ~V, ~cmp, Maybe<&2, V>, S.view_get(~K, ~V, ~cmp, VD.vmod(~K, ~V, ~cmp, MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}), k), MI.view_get(~K, ~V, ~cmp, MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}, k), M.view_get(~K, ~V, ~cmp, MI.rv(~K, ~V, ~cmp, MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}), k), SM.view_get_s(~K, ~V, ~cmp, MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}, k, OK.dg_good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, hw)), VD.vm_exact(~K, ~V, ~cmp, Maybe<&2, V>, S.view_get(~K, ~V, ~cmp, VD.vmod(~K, ~V, ~cmp, MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}), k), MI.view_get(~K, ~V, ~cmp, MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}, k), MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}, S.pick(Maybe<&2, V>, S.in_range(~K, ~cmp, k, lo2, hi2), S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), None{}), vget_m(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hw, lo2, hi2, d2, k), {==}, hw)) 116 117 def vcv_eq(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +w2: MI.MView, +o: Maybe<&2, V>) -> {MI.view_contains_value(~K, ~V, ~cmp, (w2, o)) == (w2, S.is_some(V, o)) : MI.MView & Bool}: 118 match o: 119 case None{}: 120 {==} 121 case Some{x}: 122 {==} 123 124 def view_contains_key_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +w: MI.MView, +hw: {VD.vgood(~K, ~V, ~cmp, w) == True{} : Bool}, +k: K) -> VD.VPOK(~K, ~V, ~cmp, Bool, S.view_contains_key(~K, ~V, ~cmp, VD.vmod(~K, ~V, ~cmp, w), k), M.view_contains_key(~K, ~V, ~cmp, MI.rv(~K, ~V, ~cmp, w), k)): 125 match w: 126 case MI.MV{ST.SH{+n, +root, +lo, +hi, +free, +l, +d, +nl, +pl, +tg, +fl}, +lo2, +hi2, +d2}: 127 +hm = Equal.trans(MI.MView & Bool, MI.view_contains_key(~K, ~V, ~cmp, MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}, k), MI.view_contains_value(~K, ~V, ~cmp, (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}, S.pick(Maybe<&2, V>, S.in_range(~K, ~cmp, k, lo2, hi2), S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), None{}))), (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}, S.is_some(V, S.pick(Maybe<&2, V>, S.in_range(~K, ~cmp, k, lo2, hi2), S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), None{}))), L.subst(MI.MView & Maybe<&2, V>, z => {MI.view_contains_value(~K, ~V, ~cmp, MI.view_get(~K, ~V, ~cmp, MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}, k)) == MI.view_contains_value(~K, ~V, ~cmp, z) : MI.MView & Bool}, MI.view_get(~K, ~V, ~cmp, MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}, k), (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}, S.pick(Maybe<&2, V>, S.in_range(~K, ~cmp, k, lo2, hi2), S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), None{})), vget_m(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hw, lo2, hi2, d2, k), {==}), vcv_eq(~K, ~V, ~cmp, MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}, S.pick(Maybe<&2, V>, S.in_range(~K, ~cmp, k, lo2, hi2), S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), None{}))) 128 VD.vm_pok(~K, ~V, ~cmp, Bool, S.view_contains_key(~K, ~V, ~cmp, VD.vmod(~K, ~V, ~cmp, MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}), k), MI.view_contains_key(~K, ~V, ~cmp, MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}, k), M.view_contains_key(~K, ~V, ~cmp, MI.rv(~K, ~V, ~cmp, MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}), k), SM.view_contains_key_s(~K, ~V, ~cmp, MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}, k, OK.dg_good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, hw)), VD.vm_exact(~K, ~V, ~cmp, Bool, S.view_contains_key(~K, ~V, ~cmp, VD.vmod(~K, ~V, ~cmp, MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}), k), MI.view_contains_key(~K, ~V, ~cmp, MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}, k), MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}, S.is_some(V, S.pick(Maybe<&2, V>, S.in_range(~K, ~cmp, k, lo2, hi2), S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), None{})), hm, {==}, hw)) 129 130 # ---- put and remove: the key in range, then the map's ---- 131 132 # a map result rewrapped in the view's bounds 133 def rw_put(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +lo2: M.Bound, +hi2: M.Bound, +d2: Bool, r: ST.Sh & Result<&2, &2, M.Rejected, Maybe<&2, V>>, -a: M.TreeMap, +o: Result<&2, &2, M.Rejected, Maybe<&2, V>>, +h: {MI.rp(~K, ~V, ~cmp, Result<&2, &2, M.Rejected, Maybe<&2, V>>, r) == (a, o) : M.TreeMap & Result<&2, &2, M.Rejected, Maybe<&2, V>>}) -> {MI.rvp(~K, ~V, ~cmp, Result<&2, &2, M.Rejected, Maybe<&2, V>>, MI.view_put_finish(~K, ~V, ~cmp, lo2, hi2, d2, r)) == (M.View{a, lo2, hi2, d2}, o) : M.View & Result<&2, &2, M.Rejected, Maybe<&2, V>>}: 134 match r: 135 case Tuple{+m, +x}: 136 L.subst(M.TreeMap & Result<&2, &2, M.Rejected, Maybe<&2, V>>, z => {(M.View{ST.real(~K, ~V, ~cmp, m), lo2, hi2, d2}, x) == (M.View{Pair.fst(M.TreeMap, Result<&2, &2, M.Rejected, Maybe<&2, V>>, z), lo2, hi2, d2}, Pair.snd(M.TreeMap, Result<&2, &2, M.Rejected, Maybe<&2, V>>, z)) : M.View & Result<&2, &2, M.Rejected, Maybe<&2, V>>}, (ST.real(~K, ~V, ~cmp, m), x), (a, o), h, {==}) 137 138 def rw_val(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +lo2: M.Bound, +hi2: M.Bound, +d2: Bool, r: ST.Sh & Maybe<&2, V>, -a: M.TreeMap, +o: Maybe<&2, V>, +h: {MI.rp(~K, ~V, ~cmp, Maybe<&2, V>, r) == (a, o) : M.TreeMap & Maybe<&2, V>}) -> {MI.rvp(~K, ~V, ~cmp, Maybe<&2, V>, MI.view_value(~K, ~V, ~cmp, lo2, hi2, d2, r)) == (M.View{a, lo2, hi2, d2}, o) : M.View & Maybe<&2, V>}: 139 match r: 140 case Tuple{+m, +x}: 141 L.subst(M.TreeMap & Maybe<&2, V>, z => {(M.View{ST.real(~K, ~V, ~cmp, m), lo2, hi2, d2}, x) == (M.View{Pair.fst(M.TreeMap, Maybe<&2, V>, z), lo2, hi2, d2}, Pair.snd(M.TreeMap, Maybe<&2, V>, z)) : M.View & Maybe<&2, V>}, (ST.real(~K, ~V, ~cmp, m), x), (a, o), h, {==}) 142 143 144 def vput_t(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +lo2: M.Bound, +hi2: M.Bound, +d2: Bool, +k: K, +v: V, p: OK.MOK(~K, ~V, ~cmp, Result<&2, &2, M.Rejected, Maybe<&2, V>>, S.put(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, v), MI.put(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, k, v))) -> VD.VM(~K, ~V, ~cmp, Result<&2, &2, M.Rejected, Maybe<&2, V>>, S.view_put_at(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, v, lo2, hi2, d2, True{}), MI.view_put_checked(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, k, v, lo2, hi2, d2, True{})): 145 match p: 146 case Tuple{+s2, Tuple{+o, Tuple{+h1, Tuple{+h2, h3}}}}: 147 %Equal.sym(S.Model & Result<&2, &2, M.Rejected, Maybe<&2, V>>, S.put(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, v), (ST.model(~K, ~V, ~cmp, s2), o), h2) : VD.VM(~K, ~V, ~cmp, Result<&2, &2, M.Rejected, Maybe<&2, V>>, S.rewrap_put(K, V, lo2, hi2, d2, _), MI.view_put_checked(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, k, v, lo2, hi2, d2, True{})) 148 (MI.MV{s2, lo2, hi2, d2}, (o, (rw_put(~K, ~V, ~cmp, lo2, hi2, d2, MI.put(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, k, v), ST.real(~K, ~V, ~cmp, s2), o, h1), ({==}, h3)))) 149 150 def vput_b(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}) == True{} : Bool}, +lo2: M.Bound, +hi2: M.Bound, +d2: Bool, +k: K, +v: V, +b: Bool) -> VD.VM(~K, ~V, ~cmp, Result<&2, &2, M.Rejected, Maybe<&2, V>>, S.view_put_at(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, v, lo2, hi2, d2, b), MI.view_put_checked(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, k, v, lo2, hi2, d2, b)): 151 match b: 152 case True{}: 153 vput_t(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, lo2, hi2, d2, k, v, PM.put_m(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, v)) 154 case False{}: 155 (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}, (Fail{M.Rejected{M.OutOfRange{}, k, v}}, ({==}, ({==}, hg)))) 156 157 def view_put_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +w: MI.MView, +hw: {VD.vgood(~K, ~V, ~cmp, w) == True{} : Bool}, +k: K, +v: V) -> VD.VPOK(~K, ~V, ~cmp, Result<&2, &2, M.Rejected, Maybe<&2, V>>, S.view_put(~K, ~V, ~cmp, VD.vmod(~K, ~V, ~cmp, w), k, v), M.view_put(~K, ~V, ~cmp, MI.rv(~K, ~V, ~cmp, w), k, v)): 158 match w: 159 case MI.MV{ST.SH{+n, +root, +lo, +hi, +free, +l, +d, +nl, +pl, +tg, +fl}, +lo2, +hi2, +d2}: 160 %CU.inr_eq(~K, ~V, ~cmp, k, lo2, hi2) : VD.VPOK(~K, ~V, ~cmp, Result<&2, &2, M.Rejected, Maybe<&2, V>>, S.view_put_at(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, v, lo2, hi2, d2, _), M.view_put(~K, ~V, ~cmp, MI.rv(~K, ~V, ~cmp, MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}), k, v)) 161 VD.vm_pok(~K, ~V, ~cmp, Result<&2, &2, M.Rejected, Maybe<&2, V>>, S.view_put_at(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, v, lo2, hi2, d2, M.in_range(~K, ~V, ~cmp, k, lo2, hi2)), MI.view_put(~K, ~V, ~cmp, MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}, k, v), M.view_put(~K, ~V, ~cmp, MI.rv(~K, ~V, ~cmp, MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}), k, v), SM.view_put_s(~K, ~V, ~cmp, MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}, k, v, OK.dg_good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, hw)), vput_b(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hw, lo2, hi2, d2, k, v, M.in_range(~K, ~V, ~cmp, k, lo2, hi2))) 162 163 164 def vrem_t(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +lo2: M.Bound, +hi2: M.Bound, +d2: Bool, +k: K, p: OK.MOK(~K, ~V, ~cmp, Maybe<&2, V>, S.remove(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k), MI.remove(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, k))) -> VD.VM(~K, ~V, ~cmp, Maybe<&2, V>, S.view_remove_at(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, lo2, hi2, d2, True{}), MI.view_remove_checked(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, k, lo2, hi2, d2, True{})): 165 match p: 166 case Tuple{+s2, Tuple{+o, Tuple{+h1, Tuple{+h2, h3}}}}: 167 %Equal.sym(S.Model & Maybe<&2, V>, S.remove(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k), (ST.model(~K, ~V, ~cmp, s2), o), h2) : VD.VM(~K, ~V, ~cmp, Maybe<&2, V>, S.rewrap_val(K, V, lo2, hi2, d2, _), MI.view_remove_checked(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, k, lo2, hi2, d2, True{})) 168 (MI.MV{s2, lo2, hi2, d2}, (o, (rw_val(~K, ~V, ~cmp, lo2, hi2, d2, MI.remove(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, k), ST.real(~K, ~V, ~cmp, s2), o, h1), ({==}, h3)))) 169 170 def vrem_b(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}) == True{} : Bool}, +lo2: M.Bound, +hi2: M.Bound, +d2: Bool, +k: K, +b: Bool) -> VD.VM(~K, ~V, ~cmp, Maybe<&2, V>, S.view_remove_at(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, lo2, hi2, d2, b), MI.view_remove_checked(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, k, lo2, hi2, d2, b)): 171 match b: 172 case True{}: 173 vrem_t(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, lo2, hi2, d2, k, RV.rm_m(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k)) 174 case False{}: 175 (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}, (None{}, ({==}, ({==}, hg)))) 176 177 def view_remove_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +w: MI.MView, +hw: {VD.vgood(~K, ~V, ~cmp, w) == True{} : Bool}, +k: K) -> VD.VPOK(~K, ~V, ~cmp, Maybe<&2, V>, S.view_remove(~K, ~V, ~cmp, VD.vmod(~K, ~V, ~cmp, w), k), M.view_remove(~K, ~V, ~cmp, MI.rv(~K, ~V, ~cmp, w), k)): 178 match w: 179 case MI.MV{ST.SH{+n, +root, +lo, +hi, +free, +l, +d, +nl, +pl, +tg, +fl}, +lo2, +hi2, +d2}: 180 %CU.inr_eq(~K, ~V, ~cmp, k, lo2, hi2) : VD.VPOK(~K, ~V, ~cmp, Maybe<&2, V>, S.view_remove_at(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, lo2, hi2, d2, _), M.view_remove(~K, ~V, ~cmp, MI.rv(~K, ~V, ~cmp, MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}), k)) 181 VD.vm_pok(~K, ~V, ~cmp, Maybe<&2, V>, S.view_remove_at(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, lo2, hi2, d2, M.in_range(~K, ~V, ~cmp, k, lo2, hi2)), MI.view_remove(~K, ~V, ~cmp, MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}, k), M.view_remove(~K, ~V, ~cmp, MI.rv(~K, ~V, ~cmp, MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}), k), SM.view_remove_s(~K, ~V, ~cmp, MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}, k, OK.dg_good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, hw)), vrem_b(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hw, lo2, hi2, d2, k, M.in_range(~K, ~V, ~cmp, k, lo2, hi2)))