1 import Base 2 import ../../lib/logic.bend as L 3 import ../../lib/list.bend as LL 4 import ../../lib/order.bend as O 5 import ../../../spec/lib/common.bend as SC 6 import ../../../spec/containers/balanced_search_tree/main.bend as S 7 import ../../../src/containers/balanced_search_tree.bend as M 8 import ./state.bend as ST 9 import ./prim.bend as PR 10 import ./frame.bend as FR 11 import ./agree.bend as AG 12 import ./ends.bend as EN 13 import ../../lib/nat_list.bend as NL 14 15 # A list grown by one slot, or rewritten at one: every other position reads 16 # as before, the slot reads the new value; so the entries, links and free 17 # chain of ids avoiding the slot are unchanged. (source: tools/generators/tm_hand/slot.src) 18 19 20 def nth_snoc_other(-X: Data, +xs: List<&2, X>, +x: X, +i: Nat, +dv: X, +h: {Nat.is_eq(i, SC.length(X, xs)) == False{} : Bool}) -> {ST.nth_or(X, SC.snoc(X, xs, x), i, dv) == ST.nth_or(X, xs, i, dv) : X}: 21 match xs i: 22 case Nil{} 0n: 23 Empty.absurd({ST.nth_or(X, SC.snoc(X, Nil{}, x), 0n, dv) == ST.nth_or(X, Nil{}, 0n, dv) : X}, L.true_false(h)) 24 case Nil{} 1n+j: 25 {==} 26 case Con{+hd, +t} 0n: 27 {==} 28 case Con{+hd, +t} 1n+j: 29 nth_snoc_other(X, t, x, j, dv, h) 30 31 def nth_snoc_same(-X: Data, +xs: List<&2, X>, +x: X, +dv: X) -> {ST.nth_or(X, SC.snoc(X, xs, x), SC.length(X, xs), dv) == x : X}: 32 match xs: 33 case Nil{}: 34 {==} 35 case Con{+hd, +t}: 36 nth_snoc_same(X, t, x, dv) 37 38 def nth_upd_c(-X: Data, +xs: List<&2, X>, +i: Nat, +x: X, +j: Nat, +dv: X, +hne: {Nat.is_eq(i, j) == False{} : Bool}, +b: Bool) -> {ST.nth_or(X, ST.pk(List<&2, X>, b, SC.update(X, xs, i, x), xs), j, dv) == ST.nth_or(X, xs, j, dv) : X}: 39 match b: 40 case True{}: 41 %Equal.sym(X, ST.nth_or(X, SC.update(X, xs, i, x), j, dv), PR.or_else(X, SC.nth(X, SC.update(X, xs, i, x), j), dv), PR.nth_or_nth(X, SC.update(X, xs, i, x), j, dv)) : {_ == ST.nth_or(X, xs, j, dv) : X} 42 %Equal.sym(X, ST.nth_or(X, xs, j, dv), PR.or_else(X, SC.nth(X, xs, j), dv), PR.nth_or_nth(X, xs, j, dv)) : {PR.or_else(X, SC.nth(X, SC.update(X, xs, i, x), j), dv) == _ : X} 43 %Equal.sym(Maybe<&2, X>, SC.nth(X, SC.update(X, xs, i, x), j), SC.nth(X, xs, j), LL.nth_update_other(X, xs, i, j, x, hne)) : {PR.or_else(X, _, dv) == PR.or_else(X, SC.nth(X, xs, j), dv) : X} 44 {==} 45 case False{}: 46 {==} 47 48 # ---- the node list ---- 49 50 51 def nd_snoc_other(-K: Data, +nl: List<&2, M.Node>, +x: M.Node, +j: Nat, +h: {Nat.is_eq(j, 1n+SC.length(M.Node, nl)) == False{} : Bool}) -> {ST.nd(K, SC.snoc(M.Node, nl, x), j) == ST.nd(K, nl, j) : M.Node}: 52 match j: 53 case 0n: 54 {==} 55 case 1n+i: 56 nth_snoc_other(M.Node, nl, x, i, M.Free{0n}, h) 57 58 def nd_snoc_same(-K: Data, +nl: List<&2, M.Node>, +x: M.Node) -> {ST.nd(K, SC.snoc(M.Node, nl, x), 1n+SC.length(M.Node, nl)) == x : M.Node}: 59 nth_snoc_same(M.Node, nl, x, M.Free{0n}) 60 61 62 # a new slot agrees off it 63 def agr_snoc(~K: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +xs: List<&2, Nat>, +nl: List<&2, M.Node>, +x: M.Node, +hn: {NL.memn(1n+SC.length(M.Node, nl), xs) == False{} : Bool}) -> {AG.agr(~K, ~cmp, xs, nl, SC.snoc(M.Node, nl, x)) == True{} : Bool}: 64 match xs: 65 case Nil{}: 66 {==} 67 case Con{+j, +t}: 68 L.and_intro(AG.ndeq(~K, ~cmp, ST.nd(K, nl, j), ST.nd(K, SC.snoc(M.Node, nl, x), j)), AG.agr(~K, ~cmp, t, nl, SC.snoc(M.Node, nl, x)), AG.ndeq_of_eq(~K, ~cmp, ~o, ST.nd(K, nl, j), ST.nd(K, SC.snoc(M.Node, nl, x), j), Equal.sym(M.Node, ST.nd(K, SC.snoc(M.Node, nl, x), j), ST.nd(K, nl, j), nd_snoc_other(K, nl, x, j, FR.or_f_l(Nat.is_eq(j, 1n+SC.length(M.Node, nl)), NL.memn(1n+SC.length(M.Node, nl), t), hn)))), agr_snoc(~K, ~cmp, ~o, t, nl, x, FR.or_f_r(Nat.is_eq(j, 1n+SC.length(M.Node, nl)), NL.memn(1n+SC.length(M.Node, nl), t), hn))) 69 70 # ---- the payload list ---- 71 72 73 def pv_snoc_other(-V: Data, +pl: List<&2, Maybe<&2, V>>, +w: Maybe<&2, V>, +j: Nat, +h: {Nat.is_eq(j, 1n+SC.length(Maybe<&2, V>, pl)) == False{} : Bool}) -> {ST.pv(V, SC.snoc(Maybe<&2, V>, pl, w), j) == ST.pv(V, pl, j) : Maybe<&2, V>}: 74 match j: 75 case 0n: 76 {==} 77 case 1n+i: 78 nth_snoc_other(Maybe<&2, V>, pl, w, i, None{}, h) 79 80 def pv_snoc_same(-V: Data, +pl: List<&2, Maybe<&2, V>>, +w: Maybe<&2, V>) -> {ST.pv(V, SC.snoc(Maybe<&2, V>, pl, w), 1n+SC.length(Maybe<&2, V>, pl)) == w : Maybe<&2, V>}: 81 nth_snoc_same(Maybe<&2, V>, pl, w, None{}) 82 83 def pv_ex_other(-V: Data, +pl: List<&2, Maybe<&2, V>>, +id: Nat, +w: Maybe<&2, V>, +j: Nat, +hne: {Nat.is_eq(id, j) == False{} : Bool}) -> {ST.pv(V, PR.ex_pl(V, pl, id, w), j) == ST.pv(V, pl, j) : Maybe<&2, V>}: 84 match id j: 85 case 0n +j: 86 {==} 87 case 1n+i 0n: 88 {==} 89 case 1n+i 1n+jj: 90 nth_upd_c(Maybe<&2, V>, pl, i, w, jj, None{}, hne, Nat.is_lt(i, SC.length(Maybe<&2, V>, pl))) 91 92 def pv_ex_same(-V: Data, +pl: List<&2, Maybe<&2, V>>, +i: Nat, +w: Maybe<&2, V>, +h: {Nat.is_lt(i, SC.length(Maybe<&2, V>, pl)) == True{} : Bool}) -> {ST.pv(V, PR.ex_pl(V, pl, 1n+i, w), 1n+i) == w : Maybe<&2, V>}: 93 %Equal.sym(Bool, Nat.is_lt(i, SC.length(Maybe<&2, V>, pl)), True{}, h) : {ST.nth_or(Maybe<&2, V>, ST.pk(List<&2, Maybe<&2, V>>, _, SC.update(Maybe<&2, V>, pl, i, w), pl), i, None{}) == w : Maybe<&2, V>} 94 %Equal.sym(Maybe<&2, V>, ST.nth_or(Maybe<&2, V>, SC.update(Maybe<&2, V>, pl, i, w), i, None{}), PR.or_else(Maybe<&2, V>, SC.nth(Maybe<&2, V>, SC.update(Maybe<&2, V>, pl, i, w), i), None{}), PR.nth_or_nth(Maybe<&2, V>, SC.update(Maybe<&2, V>, pl, i, w), i, None{})) : {_ == w : Maybe<&2, V>} 95 %Equal.sym(Maybe<&2, Maybe<&2, V>>, SC.nth(Maybe<&2, V>, SC.update(Maybe<&2, V>, pl, i, w), i), Some{w}, LL.nth_update_same(Maybe<&2, V>, pl, i, w, h)) : {PR.or_else(Maybe<&2, V>, _, None{}) == w : Maybe<&2, V>} 96 {==} 97 98 99 def ents_psnoc(~K: Data, ~V: Data, +xs: List<&2, Nat>, +nl: List<&2, M.Node>, +pl: List<&2, Maybe<&2, V>>, +w: Maybe<&2, V>, +hn: {NL.memn(1n+SC.length(Maybe<&2, V>, pl), xs) == False{} : Bool}) -> {ST.ents(~K, ~V, xs, nl, SC.snoc(Maybe<&2, V>, pl, w)) == ST.ents(~K, ~V, xs, nl, pl) : List<&2, M.Entry>}: 100 match xs: 101 case Nil{}: 102 {==} 103 case Con{+j, +t}: 104 %Equal.sym(Maybe<&2, V>, ST.pv(V, SC.snoc(Maybe<&2, V>, pl, w), j), ST.pv(V, pl, j), pv_snoc_other(V, pl, w, j, FR.or_f_l(Nat.is_eq(j, 1n+SC.length(Maybe<&2, V>, pl)), NL.memn(1n+SC.length(Maybe<&2, V>, pl), t), hn))) : {ST.cons_m(M.Entry, ST.ent(K, V, ST.nd(K, nl, j), _), ST.ents(~K, ~V, t, nl, SC.snoc(Maybe<&2, V>, pl, w))) == ST.ents(~K, ~V, Con{j, t}, nl, pl) : List<&2, M.Entry>} 105 %Equal.sym(List<&2, M.Entry>, ST.ents(~K, ~V, t, nl, SC.snoc(Maybe<&2, V>, pl, w)), ST.ents(~K, ~V, t, nl, pl), ents_psnoc(~K, ~V, t, nl, pl, w, FR.or_f_r(Nat.is_eq(j, 1n+SC.length(Maybe<&2, V>, pl)), NL.memn(1n+SC.length(Maybe<&2, V>, pl), t), hn))) : {ST.cons_m(M.Entry, ST.ent(K, V, ST.nd(K, nl, j), ST.pv(V, pl, j)), _) == ST.ents(~K, ~V, Con{j, t}, nl, pl) : List<&2, M.Entry>} 106 {==} 107 108 def ents_pex(~K: Data, ~V: Data, +xs: List<&2, Nat>, +nl: List<&2, M.Node>, +pl: List<&2, Maybe<&2, V>>, +id: Nat, +w: Maybe<&2, V>, +hn: {NL.memn(id, xs) == False{} : Bool}) -> {ST.ents(~K, ~V, xs, nl, PR.ex_pl(V, pl, id, w)) == ST.ents(~K, ~V, xs, nl, pl) : List<&2, M.Entry>}: 109 match xs: 110 case Nil{}: 111 {==} 112 case Con{+j, +t}: 113 %Equal.sym(Maybe<&2, V>, ST.pv(V, PR.ex_pl(V, pl, id, w), j), ST.pv(V, pl, j), pv_ex_other(V, pl, id, w, j, FR.ne_sym(j, id, FR.or_f_l(Nat.is_eq(j, id), NL.memn(id, t), hn)))) : {ST.cons_m(M.Entry, ST.ent(K, V, ST.nd(K, nl, j), _), ST.ents(~K, ~V, t, nl, PR.ex_pl(V, pl, id, w))) == ST.ents(~K, ~V, Con{j, t}, nl, pl) : List<&2, M.Entry>} 114 %Equal.sym(List<&2, M.Entry>, ST.ents(~K, ~V, t, nl, PR.ex_pl(V, pl, id, w)), ST.ents(~K, ~V, t, nl, pl), ents_pex(~K, ~V, t, nl, pl, id, w, FR.or_f_r(Nat.is_eq(j, id), NL.memn(id, t), hn))) : {ST.cons_m(M.Entry, ST.ent(K, V, ST.nd(K, nl, j), ST.pv(V, pl, j)), _) == ST.ents(~K, ~V, Con{j, t}, nl, pl) : List<&2, M.Entry>} 115 {==} 116 117 118 def oks_psnoc(~K: Data, ~V: Data, +xs: List<&2, Nat>, +nl: List<&2, M.Node>, +pl: List<&2, Maybe<&2, V>>, +w: Maybe<&2, V>, +hn: {NL.memn(1n+SC.length(Maybe<&2, V>, pl), xs) == False{} : Bool}) -> {EN.oks(~K, ~V, xs, nl, SC.snoc(Maybe<&2, V>, pl, w)) == EN.oks(~K, ~V, xs, nl, pl) : Bool}: 119 match xs: 120 case Nil{}: 121 {==} 122 case Con{+j, +t}: 123 %Equal.sym(Maybe<&2, V>, ST.pv(V, SC.snoc(Maybe<&2, V>, pl, w), j), ST.pv(V, pl, j), pv_snoc_other(V, pl, w, j, FR.or_f_l(Nat.is_eq(j, 1n+SC.length(Maybe<&2, V>, pl)), NL.memn(1n+SC.length(Maybe<&2, V>, pl), t), hn))) : {Bool.and(S.is_some(M.Entry, ST.ent(K, V, ST.nd(K, nl, j), _)), EN.oks(~K, ~V, t, nl, SC.snoc(Maybe<&2, V>, pl, w))) == EN.oks(~K, ~V, Con{j, t}, nl, pl) : Bool} 124 %Equal.sym(Bool, EN.oks(~K, ~V, t, nl, SC.snoc(Maybe<&2, V>, pl, w)), EN.oks(~K, ~V, t, nl, pl), oks_psnoc(~K, ~V, t, nl, pl, w, FR.or_f_r(Nat.is_eq(j, 1n+SC.length(Maybe<&2, V>, pl)), NL.memn(1n+SC.length(Maybe<&2, V>, pl), t), hn))) : {Bool.and(S.is_some(M.Entry, ST.ent(K, V, ST.nd(K, nl, j), ST.pv(V, pl, j))), _) == EN.oks(~K, ~V, Con{j, t}, nl, pl) : Bool} 125 {==} 126 127 def oks_pex(~K: Data, ~V: Data, +xs: List<&2, Nat>, +nl: List<&2, M.Node>, +pl: List<&2, Maybe<&2, V>>, +id: Nat, +w: Maybe<&2, V>, +hn: {NL.memn(id, xs) == False{} : Bool}) -> {EN.oks(~K, ~V, xs, nl, PR.ex_pl(V, pl, id, w)) == EN.oks(~K, ~V, xs, nl, pl) : Bool}: 128 match xs: 129 case Nil{}: 130 {==} 131 case Con{+j, +t}: 132 %Equal.sym(Maybe<&2, V>, ST.pv(V, PR.ex_pl(V, pl, id, w), j), ST.pv(V, pl, j), pv_ex_other(V, pl, id, w, j, FR.ne_sym(j, id, FR.or_f_l(Nat.is_eq(j, id), NL.memn(id, t), hn)))) : {Bool.and(S.is_some(M.Entry, ST.ent(K, V, ST.nd(K, nl, j), _)), EN.oks(~K, ~V, t, nl, PR.ex_pl(V, pl, id, w))) == EN.oks(~K, ~V, Con{j, t}, nl, pl) : Bool} 133 %Equal.sym(Bool, EN.oks(~K, ~V, t, nl, PR.ex_pl(V, pl, id, w)), EN.oks(~K, ~V, t, nl, pl), oks_pex(~K, ~V, t, nl, pl, id, w, FR.or_f_r(Nat.is_eq(j, id), NL.memn(id, t), hn))) : {Bool.and(S.is_some(M.Entry, ST.ent(K, V, ST.nd(K, nl, j), ST.pv(V, pl, j))), _) == EN.oks(~K, ~V, Con{j, t}, nl, pl) : Bool} 134 {==} 135 136 # ---- values from entries ---- 137 138 def some_of_ent(-K: Data, -V: Data, +x: M.Node, +m: Maybe<&2, V>, +h: {S.is_some(M.Entry, ST.ent(K, V, x, m)) == True{} : Bool}) -> {ST.some2(V, m) == True{} : Bool}: 139 match x m: 140 case M.Free{f} +m: 141 Empty.absurd({ST.some2(V, m) == True{} : Bool}, L.false_true(h)) 142 case M.N{c, a, b, q, k} None{}: 143 Empty.absurd({ST.some2(V, None{}) == True{} : Bool}, L.false_true(h)) 144 case M.N{c, a, b, q, k} Some{w}: 145 {==} 146 147 148 def oks_split_l(~K: Data, ~V: Data, +a: List<&2, Nat>, +b: List<&2, Nat>, +nl: List<&2, M.Node>, +pl: List<&2, Maybe<&2, V>>, +h: {EN.oks(~K, ~V, SC.append(Nat, a, b), nl, pl) == True{} : Bool}) -> {EN.oks(~K, ~V, a, nl, pl) == True{} : Bool}: 149 match a: 150 case Nil{}: 151 {==} 152 case Con{+j, +t}: 153 L.and_intro(S.is_some(M.Entry, ST.ent(K, V, ST.nd(K, nl, j), ST.pv(V, pl, j))), EN.oks(~K, ~V, t, nl, pl), L.and_left(S.is_some(M.Entry, ST.ent(K, V, ST.nd(K, nl, j), ST.pv(V, pl, j))), EN.oks(~K, ~V, SC.append(Nat, t, b), nl, pl), h), oks_split_l(~K, ~V, t, b, nl, pl, L.and_right(S.is_some(M.Entry, ST.ent(K, V, ST.nd(K, nl, j), ST.pv(V, pl, j))), EN.oks(~K, ~V, SC.append(Nat, t, b), nl, pl), h))) 154 155 def oks_split_r(~K: Data, ~V: Data, +a: List<&2, Nat>, +b: List<&2, Nat>, +nl: List<&2, M.Node>, +pl: List<&2, Maybe<&2, V>>, +h: {EN.oks(~K, ~V, SC.append(Nat, a, b), nl, pl) == True{} : Bool}) -> {EN.oks(~K, ~V, b, nl, pl) == True{} : Bool}: 156 match a: 157 case Nil{}: 158 h 159 case Con{+j, +t}: 160 oks_split_r(~K, ~V, t, b, nl, pl, L.and_right(S.is_some(M.Entry, ST.ent(K, V, ST.nd(K, nl, j), ST.pv(V, pl, j))), EN.oks(~K, ~V, SC.append(Nat, t, b), nl, pl), h)) 161 162 # a tree whose ids all have entries has values 163 def pay_oks(~K: Data, ~V: Data, +t: ST.Tr, +nl: List<&2, M.Node>, +pl: List<&2, Maybe<&2, V>>, +h: {EN.oks(~K, ~V, ST.ids(t), nl, pl) == True{} : Bool}) -> {ST.pay(~V, t, pl) == True{} : Bool}: 164 match t: 165 case ST.TE{}: 166 {==} 167 case ST.TN{+i, +a, +b}: 168 +hr = oks_split_r(~K, ~V, ST.ids(a), Con{i, ST.ids(b)}, nl, pl, h) 169 L.and_intro(ST.some2(V, ST.pv(V, pl, i)), Bool.and(ST.pay(~V, a, pl), ST.pay(~V, b, pl)), some_of_ent(K, V, ST.nd(K, nl, i), ST.pv(V, pl, i), L.and_left(S.is_some(M.Entry, ST.ent(K, V, ST.nd(K, nl, i), ST.pv(V, pl, i))), EN.oks(~K, ~V, ST.ids(b), nl, pl), hr)), L.and_intro(ST.pay(~V, a, pl), ST.pay(~V, b, pl), pay_oks(~K, ~V, a, nl, pl, oks_split_l(~K, ~V, ST.ids(a), Con{i, ST.ids(b)}, nl, pl, h)), pay_oks(~K, ~V, b, nl, pl, L.and_right(S.is_some(M.Entry, ST.ent(K, V, ST.nd(K, nl, i), ST.pv(V, pl, i))), EN.oks(~K, ~V, ST.ids(b), nl, pl), hr)))) 170 171 def len_ex_c(-V: Data, +pl: List<&2, Maybe<&2, V>>, +i: Nat, +w: Maybe<&2, V>, +b: Bool) -> {SC.length(Maybe<&2, V>, ST.pk(List<&2, Maybe<&2, V>>, b, SC.update(Maybe<&2, V>, pl, i, w), pl)) == SC.length(Maybe<&2, V>, pl) : Nat}: 172 match b: 173 case True{}: 174 LL.length_update(Maybe<&2, V>, pl, i, w) 175 case False{}: 176 {==} 177 178 def len_ex(-V: Data, +pl: List<&2, Maybe<&2, V>>, +id: Nat, +w: Maybe<&2, V>) -> {SC.length(Maybe<&2, V>, PR.ex_pl(V, pl, id, w)) == SC.length(Maybe<&2, V>, pl) : Nat}: 179 match id: 180 case 0n: 181 {==} 182 case 1n+i: 183 len_ex_c(V, pl, i, w, Nat.is_lt(i, SC.length(Maybe<&2, V>, pl)))