1 import Base 2 import ../../lib/logic.bend as L 3 import ../../lib/nat.bend as N 4 import ../../lib/list.bend as LL 5 import ../../../spec/lib/common.bend as SC 6 import ../../../src/containers/balanced_search_tree.bend as M 7 import ./state.bend as ST 8 import ./mirror.bend as MI 9 10 # The ghost tree: its height is at most its size, and the search loop over 11 # the node list walks it: from a subtree's root, with fuel above the height, 12 # the loop returns the ghost search of the subtree. 13 # (source: tools/generators/tm_hand/tree.src) 14 15 16 # ---- height ---- 17 18 def nmax(+a: Nat, +b: Nat) -> Nat: 19 ST.pk(Nat, Nat.is_lt(a, b), b, a) 20 21 def ht(t: ST.Tr) -> Nat: 22 match t: 23 case ST.TE{}: 24 0n 25 case ST.TN{i, tl, tr}: 26 1n+nmax(ht(tl), ht(tr)) 27 28 def max_c(+a: Nat, +b: Nat, +c: Nat, +ha: {Nat.is_le(a, c) == True{} : Bool}, +hb: {Nat.is_le(b, c) == True{} : Bool}, +x: Bool) -> {Nat.is_le(ST.pk(Nat, x, b, a), c) == True{} : Bool}: 29 match x: 30 case True{}: 31 hb 32 case False{}: 33 ha 34 35 # max(a, b) <= c when both are 36 def max_le(+a: Nat, +b: Nat, +c: Nat, +ha: {Nat.is_le(a, c) == True{} : Bool}, +hb: {Nat.is_le(b, c) == True{} : Bool}) -> {Nat.is_le(nmax(a, b), c) == True{} : Bool}: 37 max_c(a, b, c, ha, hb, Nat.is_lt(a, b)) 38 39 def le_max_c(+a: Nat, +b: Nat, +x: Bool, +hx: {Nat.is_lt(a, b) == x : Bool}) -> {Nat.is_le(a, ST.pk(Nat, x, b, a)) == True{} : Bool} & {Nat.is_le(b, ST.pk(Nat, x, b, a)) == True{} : Bool}: 40 match x: 41 case True{}: 42 (N.lt_le(a, b, hx), N.le_refl(b)) 43 case False{}: 44 (N.le_refl(a), N.not_lt_le(a, b, hx)) 45 46 def le_max_l(+a: Nat, +b: Nat) -> {Nat.is_le(a, nmax(a, b)) == True{} : Bool}: 47 Pair.fst({Nat.is_le(a, nmax(a, b)) == True{} : Bool}, {Nat.is_le(b, nmax(a, b)) == True{} : Bool}, le_max_c(a, b, Nat.is_lt(a, b), {==})) 48 49 def le_max_r(+a: Nat, +b: Nat) -> {Nat.is_le(b, nmax(a, b)) == True{} : Bool}: 50 Pair.snd({Nat.is_le(a, nmax(a, b)) == True{} : Bool}, {Nat.is_le(b, nmax(a, b)) == True{} : Bool}, le_max_c(a, b, Nat.is_lt(a, b), {==})) 51 52 53 def le_add_l(+a: Nat, +b: Nat) -> {Nat.is_le(b, Nat.add(a, b)) == True{} : Bool}: 54 %Equal.sym(Nat, Nat.add(a, b), Nat.add(b, a), N.add_comm(a, b)) : {Nat.is_le(b, _) == True{} : Bool} 55 N.le_add_right(b, a) 56 57 # the height is at most the number of ids 58 def ht_le(+t: ST.Tr) -> {Nat.is_le(ht(t), SC.length(Nat, ST.ids(t))) == True{} : Bool}: 59 match t: 60 case ST.TE{}: 61 {==} 62 case ST.TN{+i, +tl, +tr}: 63 %Equal.sym(Nat, SC.length(Nat, ST.ids(ST.TN{i, tl, tr})), Nat.add(SC.length(Nat, ST.ids(tl)), 1n+SC.length(Nat, ST.ids(tr))), LL.length_append(Nat, ST.ids(tl), Con{i, ST.ids(tr)})) : {Nat.is_le(1n+nmax(ht(tl), ht(tr)), _) == True{} : Bool} 64 %Equal.sym(Nat, Nat.add(SC.length(Nat, ST.ids(tl)), 1n+SC.length(Nat, ST.ids(tr))), 1n+Nat.add(SC.length(Nat, ST.ids(tl)), SC.length(Nat, ST.ids(tr))), N.add_succ(SC.length(Nat, ST.ids(tl)), SC.length(Nat, ST.ids(tr)))) : {Nat.is_le(1n+nmax(ht(tl), ht(tr)), _) == True{} : Bool} 65 max_le(ht(tl), ht(tr), Nat.add(SC.length(Nat, ST.ids(tl)), SC.length(Nat, ST.ids(tr))), N.le_trans(ht(tl), SC.length(Nat, ST.ids(tl)), Nat.add(SC.length(Nat, ST.ids(tl)), SC.length(Nat, ST.ids(tr))), ht_le(tl), N.le_add_right(SC.length(Nat, ST.ids(tl)), SC.length(Nat, ST.ids(tr)))), N.le_trans(ht(tr), SC.length(Nat, ST.ids(tr)), Nat.add(SC.length(Nat, ST.ids(tl)), SC.length(Nat, ST.ids(tr))), ht_le(tr), le_add_l(SC.length(Nat, ST.ids(tl)), SC.length(Nat, ST.ids(tr))))) 66 67 def ht_l(+i: Nat, +tl: ST.Tr, +tr: ST.Tr, +f: Nat, +h: {Nat.is_lt(ht(ST.TN{i, tl, tr}), 1n+f) == True{} : Bool}) -> {Nat.is_lt(ht(tl), f) == True{} : Bool}: 68 N.le_lt_trans(ht(tl), nmax(ht(tl), ht(tr)), f, le_max_l(ht(tl), ht(tr)), h) 69 70 def ht_r(+i: Nat, +tl: ST.Tr, +tr: ST.Tr, +f: Nat, +h: {Nat.is_lt(ht(ST.TN{i, tl, tr}), 1n+f) == True{} : Bool}) -> {Nat.is_lt(ht(tr), f) == True{} : Bool}: 71 N.le_lt_trans(ht(tr), nmax(ht(tl), ht(tr)), f, le_max_r(ht(tl), ht(tr)), h) 72 73 # ---- the ghost search ---- 74 75 # the comparison of k with a node's key (a free node: equal, as probe does) 76 def kc(~K: Data, ~cmp: K -> K -> Cmp, +k: K, x: M.Node) -> Cmp: 77 match x: 78 case M.Free{f}: 79 EQ{} 80 case M.N{c, a, b, q, key}: 81 cmp(k, key) 82 83 def pk3(-T: Data, +c: Cmp, x: T, y: T, z: T) -> T: 84 match c: 85 case LT{}: 86 x 87 case GT{}: 88 y 89 case EQ{}: 90 z 91 92 def tsearch(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, t: ST.Tr, +nl: List<&2, M.Node>, +k: K, +p: Nat, +left: Bool) -> M.Search: 93 match t: 94 case ST.TE{}: 95 M.Search{0n, p, left} 96 case ST.TN{+i, tl, tr}: 97 pk3(M.Search, kc(~K, ~cmp, k, ST.nd(K, nl, i)), tsearch(~K, ~V, ~cmp, tl, nl, k, i, True{}), tsearch(~K, ~V, ~cmp, tr, nl, k, i, False{}), M.Search{i, p, left}) 98 99 100 def sl_c(~K: Data, ~V: Data, ~cmp: K -> 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>, +i: Nat, +tl: ST.Tr, +tr: ST.Tr, +p: Nat, +left: Bool, +k: K, +f: Nat, +c: Bool, +a: Nat, +b: Nat, +q: Nat, +key: K, +ea: {a == ST.rid(tl) : Nat}, +eb: {b == ST.rid(tr) : Nat}, +ihl: {MI.search_loop(~K, ~V, ~cmp, f, k, ST.rid(tl), i, True{}, MI.probe(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, ST.rid(tl), k)) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, tsearch(~K, ~V, ~cmp, tl, nl, k, i, True{})) : ST.Sh & M.Search}, +ihr: {MI.search_loop(~K, ~V, ~cmp, f, k, ST.rid(tr), i, False{}, MI.probe(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, ST.rid(tr), k)) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, tsearch(~K, ~V, ~cmp, tr, nl, k, i, False{})) : ST.Sh & M.Search}, +cc: Cmp) -> {MI.search_loop(~K, ~V, ~cmp, 1n+f, k, i, p, left, (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, (M.N{c, a, b, q, key}, cc))) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, pk3(M.Search, cc, tsearch(~K, ~V, ~cmp, tl, nl, k, i, True{}), tsearch(~K, ~V, ~cmp, tr, nl, k, i, False{}), M.Search{i, p, left})) : ST.Sh & M.Search}: 101 match cc: 102 case LT{}: 103 %Equal.sym(Nat, a, ST.rid(tl), ea) : {MI.search_loop(~K, ~V, ~cmp, f, k, _, i, True{}, MI.probe(~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}, tsearch(~K, ~V, ~cmp, tl, nl, k, i, True{})) : ST.Sh & M.Search} 104 ihl 105 case GT{}: 106 %Equal.sym(Nat, b, ST.rid(tr), eb) : {MI.search_loop(~K, ~V, ~cmp, f, k, _, i, False{}, MI.probe(~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}, tsearch(~K, ~V, ~cmp, tr, nl, k, i, False{})) : ST.Sh & M.Search} 107 ihr 108 case EQ{}: 109 {==} 110 111 def sl_node(~K: Data, ~V: Data, ~cmp: K -> 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>, +i: Nat, +tl: ST.Tr, +tr: ST.Tr, +p: Nat, +left: Bool, +k: K, +f: Nat, +x: M.Node, +hx: {ST.is_node(K, x, ST.rid(tl), ST.rid(tr), p) == True{} : Bool}, +ihl: {MI.search_loop(~K, ~V, ~cmp, f, k, ST.rid(tl), i, True{}, MI.probe(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, ST.rid(tl), k)) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, tsearch(~K, ~V, ~cmp, tl, nl, k, i, True{})) : ST.Sh & M.Search}, +ihr: {MI.search_loop(~K, ~V, ~cmp, f, k, ST.rid(tr), i, False{}, MI.probe(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, ST.rid(tr), k)) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, tsearch(~K, ~V, ~cmp, tr, nl, k, i, False{})) : ST.Sh & M.Search}) -> {MI.search_loop(~K, ~V, ~cmp, 1n+f, k, i, p, left, MI.probe_node(~K, ~V, ~cmp, i, k, (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, x))) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, pk3(M.Search, kc(~K, ~cmp, k, x), tsearch(~K, ~V, ~cmp, tl, nl, k, i, True{}), tsearch(~K, ~V, ~cmp, tr, nl, k, i, False{}), M.Search{i, p, left})) : ST.Sh & M.Search}: 112 match x: 113 case M.Free{fx}: 114 Empty.absurd({MI.search_loop(~K, ~V, ~cmp, 1n+f, k, i, p, left, MI.probe_node(~K, ~V, ~cmp, i, k, (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, M.Free{fx}))) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, pk3(M.Search, EQ{}, tsearch(~K, ~V, ~cmp, tl, nl, k, i, True{}), tsearch(~K, ~V, ~cmp, tr, nl, k, i, False{}), M.Search{i, p, left})) : ST.Sh & M.Search}, L.false_true(hx)) 115 case M.N{+c, +a, +b, +q, +key}: 116 +ha = L.and_left(Nat.is_eq(a, ST.rid(tl)), Bool.and(Nat.is_eq(b, ST.rid(tr)), Nat.is_eq(q, p)), hx) 117 +hb = L.and_left(Nat.is_eq(b, ST.rid(tr)), Nat.is_eq(q, p), L.and_right(Nat.is_eq(a, ST.rid(tl)), Bool.and(Nat.is_eq(b, ST.rid(tr)), Nat.is_eq(q, p)), hx)) 118 sl_c(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, i, tl, tr, p, left, k, f, c, a, b, q, key, N.eq_from_is_eq(a, ST.rid(tl), ha), N.eq_from_is_eq(b, ST.rid(tr), hb), ihl, ihr, cmp(k, key)) 119 120 121 def rep_parts(~K: Data, +i: Nat, +tl: ST.Tr, +tr: ST.Tr, +p: Nat, +nl: List<&2, M.Node>, +h: {ST.rep(~K, ST.TN{i, tl, tr}, p, nl) == True{} : Bool}) -> {ST.is_node(K, ST.nd(K, nl, i), ST.rid(tl), ST.rid(tr), p) == True{} : Bool} & ({ST.rep(~K, tl, i, nl) == True{} : Bool} & {ST.rep(~K, tr, i, nl) == True{} : Bool}): 122 +h2 = L.and_right(Nat.is_lt(0n, i), Bool.and(ST.is_node(K, ST.nd(K, nl, i), ST.rid(tl), ST.rid(tr), p), Bool.and(ST.rep(~K, tl, i, nl), ST.rep(~K, tr, i, nl))), h) 123 +h3 = L.and_right(ST.is_node(K, ST.nd(K, nl, i), ST.rid(tl), ST.rid(tr), p), Bool.and(ST.rep(~K, tl, i, nl), ST.rep(~K, tr, i, nl)), h2) 124 (L.and_left(ST.is_node(K, ST.nd(K, nl, i), ST.rid(tl), ST.rid(tr), p), Bool.and(ST.rep(~K, tl, i, nl), ST.rep(~K, tr, i, nl)), h2), (L.and_left(ST.rep(~K, tl, i, nl), ST.rep(~K, tr, i, nl), h3), L.and_right(ST.rep(~K, tl, i, nl), ST.rep(~K, tr, i, nl), h3))) 125 126 def rep_node(~K: Data, +i: Nat, +tl: ST.Tr, +tr: ST.Tr, +p: Nat, +nl: List<&2, M.Node>, +h: {ST.rep(~K, ST.TN{i, tl, tr}, p, nl) == True{} : Bool}) -> {ST.is_node(K, ST.nd(K, nl, i), ST.rid(tl), ST.rid(tr), p) == True{} : Bool}: 127 L.and_left(ST.is_node(K, ST.nd(K, nl, i), ST.rid(tl), ST.rid(tr), p), Bool.and(ST.rep(~K, tl, i, nl), ST.rep(~K, tr, i, nl)), L.and_right(Nat.is_lt(0n, i), Bool.and(ST.is_node(K, ST.nd(K, nl, i), ST.rid(tl), ST.rid(tr), p), Bool.and(ST.rep(~K, tl, i, nl), ST.rep(~K, tr, i, nl))), h)) 128 129 def rep_l(~K: Data, +i: Nat, +tl: ST.Tr, +tr: ST.Tr, +p: Nat, +nl: List<&2, M.Node>, +h: {ST.rep(~K, ST.TN{i, tl, tr}, p, nl) == True{} : Bool}) -> {ST.rep(~K, tl, i, nl) == True{} : Bool}: 130 L.and_left(ST.rep(~K, tl, i, nl), ST.rep(~K, tr, i, nl), L.and_right(ST.is_node(K, ST.nd(K, nl, i), ST.rid(tl), ST.rid(tr), p), Bool.and(ST.rep(~K, tl, i, nl), ST.rep(~K, tr, i, nl)), L.and_right(Nat.is_lt(0n, i), Bool.and(ST.is_node(K, ST.nd(K, nl, i), ST.rid(tl), ST.rid(tr), p), Bool.and(ST.rep(~K, tl, i, nl), ST.rep(~K, tr, i, nl))), h))) 131 132 def rep_r(~K: Data, +i: Nat, +tl: ST.Tr, +tr: ST.Tr, +p: Nat, +nl: List<&2, M.Node>, +h: {ST.rep(~K, ST.TN{i, tl, tr}, p, nl) == True{} : Bool}) -> {ST.rep(~K, tr, i, nl) == True{} : Bool}: 133 L.and_right(ST.rep(~K, tl, i, nl), ST.rep(~K, tr, i, nl), L.and_right(ST.is_node(K, ST.nd(K, nl, i), ST.rid(tl), ST.rid(tr), p), Bool.and(ST.rep(~K, tl, i, nl), ST.rep(~K, tr, i, nl)), L.and_right(Nat.is_lt(0n, i), Bool.and(ST.is_node(K, ST.nd(K, nl, i), ST.rid(tl), ST.rid(tr), p), Bool.and(ST.rep(~K, tl, i, nl), ST.rep(~K, tr, i, nl))), h))) 134 135 # the search loop from a subtree's root is the ghost search of the subtree 136 def sl(~K: Data, ~V: Data, ~cmp: K -> 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>, +f: Nat, +t: ST.Tr, +p: Nat, +left: Bool, +k: K, +hr: {ST.rep(~K, t, p, nl) == True{} : Bool}, +hf: {Nat.is_lt(ht(t), f) == True{} : Bool}) -> {MI.search_loop(~K, ~V, ~cmp, f, k, ST.rid(t), p, left, MI.probe(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, ST.rid(t), k)) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, tsearch(~K, ~V, ~cmp, t, nl, k, p, left)) : ST.Sh & M.Search}: 137 match f t: 138 case 0n _: 139 Empty.absurd({MI.search_loop(~K, ~V, ~cmp, 0n, k, ST.rid(t), p, left, MI.probe(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, ST.rid(t), k)) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, tsearch(~K, ~V, ~cmp, t, nl, k, p, left)) : ST.Sh & M.Search}, L.true_not_false(Nat.is_lt(ht(t), 0n), hf, N.not_lt_zero(ht(t)))) 140 case 1n+g ST.TE{}: 141 {==} 142 case 1n+g ST.TN{+i, +tl, +tr}: 143 +ihl = sl(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, g, tl, i, True{}, k, rep_l(~K, i, tl, tr, p, nl, hr), ht_l(i, tl, tr, g, hf)) 144 +ihr = sl(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, g, tr, i, False{}, k, rep_r(~K, i, tl, tr, p, nl, hr), ht_r(i, tl, tr, g, hf)) 145 sl_node(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, i, tl, tr, p, left, k, g, ST.nd(K, nl, i), rep_node(~K, i, tl, tr, p, nl, hr), ihl, ihr)