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 ../../lib/order.bend as O 6 import ../../lib/u32.bend as U 7 import ../../lib/array.bend as AR 8 import ../../../spec/lib/common.bend as SC 9 import ../../../spec/containers/binary_heap.bend as S 10 import ../../../src/containers/binary_heap.bend as H 11 import ../../../src/containers/types/binary_heap.bend as E 12 import ./idx.bend as IX 13 import ./u32idx.bend as UX 14 import ./slots.bend as SL 15 import ./vals.bend as V 16 import ./root.bend as RT 17 import ./state.bend as ST 18 import ./push.bend as PU 19 import ./pop.bend as PO 20 import ./sorted.bend as SO 21 import ./budget.bend as BG 22 23 # One actual public operation on a good shadow's block yields the block of a 24 # new good shadow, and (abstract state, observation) equals the spec step. 25 # 26 # The fourth component bounds the new depth: a push doubles the block at most 27 # once and from_list at most once per element it pushes; every other 28 # operation leaves the depth alone. The capacity premise itself is stated in 29 # terms of the heap's size (see step_ok below), which is what lets the trace 30 # law carry a single premise for a whole operation list (trace.bend). 31 32 def pushcost(~A: Data, op: E.Op) -> Nat: 33 match op: 34 case E.Length{}: 35 0n 36 case E.Push{x}: 37 1n 38 case E.Peek{}: 39 0n 40 case E.Pop{}: 41 0n 42 case E.FromList{items}: 43 SC.length(A, items) 44 case E.ToSortedList{}: 45 0n 46 47 def StepOK(~A: Data, ~cmp: A -> A -> Cmp, sh: ST.Shadow, op: E.Op) -> Type: 48 Sigma<&1, &1, ST.Shadow, sh2 => Sigma<&1, &1, E.Obs, o => {H.step(~A, ~cmp, ST.real(~A, sh), op) == (ST.real(~A, sh2), o) : H.Heap & E.Obs} & ({ST.good(~A, ~cmp, sh2) == True{} : Bool} & ({(ST.model(~A, ~cmp, sh2), o) == S.step(~A, ~cmp, ST.model(~A, ~cmp, sh), op) : List<&2, A> & E.Obs} & {Nat.is_le(ST.sh_depth(~A, sh2), Nat.add(ST.sh_depth(~A, sh), pushcost(~A, op))) == True{} : Bool}))>> 49 50 def mk(~A: Data, ~cmp: A -> A -> Cmp, -sh: ST.Shadow, -op: E.Op, sh2: ST.Shadow, o: E.Obs, e1: {H.step(~A, ~cmp, ST.real(~A, sh), op) == (ST.real(~A, sh2), o) : H.Heap & E.Obs}, e2: {ST.good(~A, ~cmp, sh2) == True{} : Bool}, e3: {(ST.model(~A, ~cmp, sh2), o) == S.step(~A, ~cmp, ST.model(~A, ~cmp, sh), op) : List<&2, A> & E.Obs}, e4: {Nat.is_le(ST.sh_depth(~A, sh2), Nat.add(ST.sh_depth(~A, sh), pushcost(~A, op))) == True{} : Bool}) -> StepOK(~A, ~cmp, sh, op): 51 (sh2, (o, (e1, (e2, (e3, e4))))) 52 53 def le_same(+d: Nat) -> {Nat.is_le(d, Nat.add(d, 0n)) == True{} : Bool}: 54 %Equal.sym(Nat, Nat.add(d, 0n), d, N.add_zero(d)) : {Nat.is_le(d, _) == True{} : Bool} 55 N.le_refl(d) 56 57 def le_succ_add(+d: Nat) -> {Nat.is_le(1n+d, Nat.add(d, 1n)) == True{} : Bool}: 58 %Equal.sym(Nat, Nat.add(d, 1n), 1n+Nat.add(d, 0n), N.add_succ(d, 0n)) : {Nat.is_le(1n+d, _) == True{} : Bool} 59 %Equal.sym(Nat, Nat.add(d, 0n), d, N.add_zero(d)) : {Nat.is_le(1n+d, 1n+_) == True{} : Bool} 60 N.le_refl(1n+d) 61 62 # the empty/nonempty decision the implementation makes, in Nat 63 def empty_bridge(+size: Nat, +depth: Nat, +hd: {Nat.is_le(depth, 31n) == True{} : Bool}, +hs: {Nat.is_le(size, SC.pow2(depth)) == True{} : Bool}) -> {U32.is_eq(U32.from_nat(size), U32.from_nat(0n)) == Nat.is_eq(size, 0n) : Bool}: 64 UX.eq_bridge(size, 0n, 1n+depth, hd, 65 N.le_lt_trans(size, SC.pow2(depth), SC.pow2(1n+depth), hs, N.pow2_lt_succ(depth)), 66 N.lt_le_trans(0n, SC.pow2(depth), SC.pow2(1n+depth), N.succ_le_lt(0n, SC.pow2(depth), N.pow2_pos(depth)), N.lt_le(SC.pow2(depth), SC.pow2(1n+depth), N.pow2_lt_succ(depth)))) 67 68 # ---- length ---- 69 70 def length_ok(~A: Data, ~cmp: A -> A -> Cmp, +size: Nat, +depth: Nat, +t: AR.Tree>, +g: {ST.good(~A, ~cmp, ST.Sh{size, depth, t}) == True{} : Bool}) -> StepOK(~A, ~cmp, ST.Sh{size, depth, t}, E.Length{}): 71 mk(~A, ~cmp, ST.Sh{size, depth, t}, E.Length{}, ST.Sh{size, depth, t}, E.ONat{size}, {==}, g, 72 Equal.cong(Nat, List<&2, A> & E.Obs, k => (ST.model(~A, ~cmp, ST.Sh{size, depth, t}), E.ONat{k}), size, SC.length(A, ST.model(~A, ~cmp, ST.Sh{size, depth, t})), 73 Equal.sym(Nat, SC.length(A, ST.model(~A, ~cmp, ST.Sh{size, depth, t})), size, RT.model_length(~A, ~cmp, AR.slots(Maybe<&2, A>, t), size, ST.g_lay(~A, ~cmp, size, depth, t, g)))), 74 le_same(depth)) 75 76 # ---- peek ---- 77 78 def peek_at(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +m: Nat, +depth: Nat, +t: AR.Tree>, +root: A, +g: {ST.good(~A, ~cmp, ST.Sh{1n+m, depth, t}) == True{} : Bool}, +h0: {SL.slot(~A, AR.slots(Maybe<&2, A>, t), 0n) == Some{root} : Maybe<&2, A>}) -> StepOK(~A, ~cmp, ST.Sh{1n+m, depth, t}, E.Peek{}): 79 +hd = ST.g_depth(~A, ~cmp, 1n+m, depth, t, g) 80 +pf = ST.g_perfect(~A, ~cmp, 1n+m, depth, t, g) 81 +hs = ST.g_size(~A, ~cmp, 1n+m, depth, t, g) 82 mk(~A, ~cmp, ST.Sh{1n+m, depth, t}, E.Peek{}, ST.Sh{1n+m, depth, t}, E.OItem{Done{root}}, 83 %Equal.sym(Bool, U32.is_eq(U32.from_nat(1n+m), U32.from_nat(0n)), Nat.is_eq(1n+m, 0n), empty_bridge(1n+m, depth, hd, hs)) : {H.obs_item(~A, H.peek_go(~A, 1n+m, U32.from_nat(1n+m), depth, U.pow2u(depth), AR.thaw(Maybe<&2, A>, t), _)) == (ST.real(~A, ST.Sh{1n+m, depth, t}), E.OItem{Done{root}}) : H.Heap & E.Obs} 84 %Equal.sym(Array> & Maybe<&2, A>, Array.get(Maybe<&2, A>, AR.thaw(Maybe<&2, A>, t), 0), (AR.thaw(Maybe<&2, A>, t), Some{root}), PO.get_root(~A, depth, t, root, ST.depth_lt32(depth, hd), pf, h0)) : {H.obs_item(~A, H.peek_found(~A, 1n+m, U32.from_nat(1n+m), depth, U.pow2u(depth), _)) == (ST.real(~A, ST.Sh{1n+m, depth, t}), E.OItem{Done{root}}) : H.Heap & E.Obs} 85 {==}, 86 g, 87 Equal.cong(List<&2, A>, List<&2, A> & E.Obs, zs => (ST.model(~A, ~cmp, ST.Sh{1n+m, depth, t}), E.OItem{S.item(A, SC.head(A, zs))}), Con{root, V.msort(~A, ~cmp, V.vals(~A, SC.update(Maybe<&2, A>, AR.slots(Maybe<&2, A>, t), 0n, None{}), 1n+m))}, ST.model(~A, ~cmp, ST.Sh{1n+m, depth, t}), 88 Equal.sym(List<&2, A>, ST.model(~A, ~cmp, ST.Sh{1n+m, depth, t}), Con{root, V.msort(~A, ~cmp, V.vals(~A, SC.update(Maybe<&2, A>, AR.slots(Maybe<&2, A>, t), 0n, None{}), 1n+m))}, 89 RT.head_root(~A, ~cmp, ~o, AR.slots(Maybe<&2, A>, t), 1n+m, root, N.succ_le_lt(0n, 1n+m, N.zero_le(m)), ST.g_ho(~A, ~cmp, 1n+m, depth, t, g), ST.g_lay(~A, ~cmp, 1n+m, depth, t, g), h0))), 90 le_same(depth)) 91 92 def peek_some(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +m: Nat, +depth: Nat, +t: AR.Tree>, +g: {ST.good(~A, ~cmp, ST.Sh{1n+m, depth, t}) == True{} : Bool}, sig: Sigma<&1, &1, A, v => {SL.slot(~A, AR.slots(Maybe<&2, A>, t), 0n) == Some{v} : Maybe<&2, A>}>) -> StepOK(~A, ~cmp, ST.Sh{1n+m, depth, t}, E.Peek{}): 93 match sig: 94 case Tuple{+root, +h0}: 95 peek_at(~A, ~cmp, ~o, m, depth, t, root, g, h0) 96 97 def peek_ok(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), size: Nat, +depth: Nat, +t: AR.Tree>, +g: {ST.good(~A, ~cmp, ST.Sh{size, depth, t}) == True{} : Bool}) -> StepOK(~A, ~cmp, ST.Sh{size, depth, t}, E.Peek{}): 98 match size: 99 case 0n: 100 mk(~A, ~cmp, ST.Sh{0n, depth, t}, E.Peek{}, ST.Sh{0n, depth, t}, E.OItem{Fail{E.EmptyHeap{}}}, {==}, g, {==}, le_same(depth)) 101 case 1n+ +m: 102 peek_some(~A, ~cmp, ~o, m, depth, t, g, 103 SL.slot_some(~A, SL.slot(~A, AR.slots(Maybe<&2, A>, t), 0n), SL.lay_at(~A, AR.slots(Maybe<&2, A>, t), 1n+m, 0n, ST.g_lay(~A, ~cmp, 1n+m, depth, t, g), N.succ_le_lt(0n, 1n+m, N.zero_le(m))))) 104 105 def or_true(b: Bool) -> {Bool.or(b, True{}) == True{} : Bool}: 106 match b: 107 case True{}: 108 {==} 109 case False{}: 110 {==} 111 112 # ---- push ---- 113 114 def push_step(~A: Data, ~cmp: A -> A -> Cmp, +size: Nat, +depth: Nat, +t: AR.Tree>, +x: A, r: PU.PushOK(~A, ~cmp, ST.Sh{size, depth, t}, x)) -> StepOK(~A, ~cmp, ST.Sh{size, depth, t}, E.Push{x}): 115 match r: 116 case Tuple{+sh2, Tuple{ereal, Tuple{g2, Tuple{ems, edd}}}}: 117 mk(~A, ~cmp, ST.Sh{size, depth, t}, E.Push{x}, sh2, E.OUnit{}, 118 Equal.cong(H.Heap, H.Heap & E.Obs, hh => (hh, E.OUnit{}), H.push(~A, ~cmp, ST.real(~A, ST.Sh{size, depth, t}), x), ST.real(~A, sh2), ereal), 119 g2, 120 Equal.cong(List<&2, A>, List<&2, A> & E.Obs, zs => (zs, E.OUnit{}), ST.model(~A, ~cmp, sh2), S.ins(~A, ~cmp, x, ST.model(~A, ~cmp, ST.Sh{size, depth, t})), ems), 121 N.le_trans(ST.sh_depth(~A, sh2), 1n+depth, Nat.add(depth, 1n), edd, le_succ_add(depth))) 122 123 def push_ok(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +size: Nat, +depth: Nat, +t: AR.Tree>, +x: A, +g: {ST.good(~A, ~cmp, ST.Sh{size, depth, t}) == True{} : Bool}, +q: Nat, +hq: {Nat.is_le(q, 31n) == True{} : Bool}, +hs: {Nat.is_lt(size, SC.pow2(q)) == True{} : Bool}) -> StepOK(~A, ~cmp, ST.Sh{size, depth, t}, E.Push{x}): 124 push_step(~A, ~cmp, size, depth, t, x, 125 PU.push_ok(~A, ~cmp, ~o, size, depth, t, x, g, BG.room_or(size, depth, q, hq, hs), Nat.is_lt(size, SC.pow2(depth)), {==})) 126 127 # ---- pop ---- 128 129 def pop_step(~A: Data, ~cmp: A -> A -> Cmp, +size: Nat, +depth: Nat, +t: AR.Tree>, r: PO.PopRes(~A, ~cmp, ST.Sh{size, depth, t})) -> StepOK(~A, ~cmp, ST.Sh{size, depth, t}, E.Pop{}): 130 match r: 131 case Tuple{+sh2, Tuple{+res, Tuple{ereal, Tuple{g2, Tuple{espec, edep}}}}}: 132 mk(~A, ~cmp, ST.Sh{size, depth, t}, E.Pop{}, sh2, E.OItem{res}, 133 Equal.cong(H.Heap & Result<&2, &2, E.Error, A>, H.Heap & E.Obs, rr => H.obs_item(~A, rr), H.pop(~A, ~cmp, ST.real(~A, ST.Sh{size, depth, t})), (ST.real(~A, sh2), res), ereal), 134 g2, 135 espec, 136 L.subst(Nat, z => {Nat.is_le(z, Nat.add(depth, 0n)) == True{} : Bool}, depth, ST.sh_depth(~A, sh2), Equal.sym(Nat, ST.sh_depth(~A, sh2), depth, edep), le_same(depth))) 137 138 def pop_ok(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +size: Nat, +depth: Nat, +t: AR.Tree>, +g: {ST.good(~A, ~cmp, ST.Sh{size, depth, t}) == True{} : Bool}) -> StepOK(~A, ~cmp, ST.Sh{size, depth, t}, E.Pop{}): 139 pop_step(~A, ~cmp, size, depth, t, PO.pop_ok(~A, ~cmp, ~o, size, depth, t, g)) 140 141 # ---- to_sorted_list ---- 142 143 def sorted_ok(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +size: Nat, +depth: Nat, +t: AR.Tree>, +g: {ST.good(~A, ~cmp, ST.Sh{size, depth, t}) == True{} : Bool}) -> StepOK(~A, ~cmp, ST.Sh{size, depth, t}, E.ToSortedList{}): 144 mk(~A, ~cmp, ST.Sh{size, depth, t}, E.ToSortedList{}, ST.Sh{size, depth, t}, E.OList{ST.model(~A, ~cmp, ST.Sh{size, depth, t})}, 145 Equal.cong(H.Heap & List<&2, A>, H.Heap & E.Obs, rr => H.obs_list(~A, rr), H.to_sorted_list(~A, ~cmp, ST.real(~A, ST.Sh{size, depth, t})), (ST.real(~A, ST.Sh{size, depth, t}), ST.model(~A, ~cmp, ST.Sh{size, depth, t})), 146 SO.to_sorted_ok(~A, ~cmp, ~o, size, depth, t, g)), 147 g, {==}, le_same(depth)) 148 149 # ---- from_list ---- 150 # 151 # from_list replaces the heap by repeated push, so the capacity premise it 152 # carries is one doubling per element (the same conservative accounting the 153 # deque uses for its push budget). 154 155 def add_le_r(+a: Nat, +b: Nat, +c: Nat, +h: {Nat.is_le(a, b) == True{} : Bool}) -> {Nat.is_le(Nat.add(a, c), Nat.add(b, c)) == True{} : Bool}: 156 %Equal.sym(Nat, Nat.add(a, c), Nat.add(c, a), N.add_comm(a, c)) : {Nat.is_le(_, Nat.add(b, c)) == True{} : Bool} 157 %Equal.sym(Nat, Nat.add(b, c), Nat.add(c, b), N.add_comm(b, c)) : {Nat.is_le(Nat.add(c, a), _) == True{} : Bool} 158 N.le_add_left(a, b, c, h) 159 160 def add_succ_l(+d: Nat, +l: Nat) -> {Nat.add(1n+d, l) == 1n+Nat.add(d, l) : Nat}: 161 Equal.trans(Nat, Nat.add(1n+d, l), Nat.add(l, 1n+d), 1n+Nat.add(d, l), 162 N.add_comm(1n+d, l), 163 Equal.trans(Nat, Nat.add(l, 1n+d), 1n+Nat.add(l, d), 1n+Nat.add(d, l), 164 N.add_succ(l, d), 165 N.succ_cong(Nat.add(l, d), Nat.add(d, l), N.add_comm(l, d)))) 166 167 def add_shift(+d: Nat, +l: Nat) -> {Nat.add(d, 1n+l) == Nat.add(1n+d, l) : Nat}: 168 Equal.trans(Nat, Nat.add(d, 1n+l), 1n+Nat.add(d, l), Nat.add(1n+d, l), 169 N.add_succ(d, l), 170 Equal.sym(Nat, Nat.add(1n+d, l), 1n+Nat.add(d, l), add_succ_l(d, l))) 171 172 # the size budget after pushing y onto sh 173 def budget_rest(~A: Data, ~cmp: A -> A -> Cmp, +y: A, +rest: List<&2, A>, +sh: ST.Shadow, +sh1: ST.Shadow, +q: Nat, +g: {ST.good(~A, ~cmp, sh) == True{} : Bool}, +g1: {ST.good(~A, ~cmp, sh1) == True{} : Bool}, +ems: {ST.model(~A, ~cmp, sh1) == S.ins(~A, ~cmp, y, ST.model(~A, ~cmp, sh)) : List<&2, A>}, +h: {Nat.is_lt(Nat.add(ST.sh_size(~A, sh), 1n+SC.length(A, rest)), SC.pow2(q)) == True{} : Bool}) -> {Nat.is_lt(Nat.add(ST.sh_size(~A, sh1), SC.length(A, rest)), SC.pow2(q)) == True{} : Bool}: 174 L.subst(Nat, z => {Nat.is_lt(Nat.add(z, SC.length(A, rest)), SC.pow2(q)) == True{} : Bool}, 1n+ST.sh_size(~A, sh), ST.sh_size(~A, sh1), Equal.sym(Nat, ST.sh_size(~A, sh1), 1n+ST.sh_size(~A, sh), BG.push_size(~A, ~cmp, y, sh, sh1, g, g1, ems)), 175 L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(q)) == True{} : Bool}, Nat.add(ST.sh_size(~A, sh), 1n+SC.length(A, rest)), Nat.add(1n+ST.sh_size(~A, sh), SC.length(A, rest)), add_shift(ST.sh_size(~A, sh), SC.length(A, rest)), h)) 176 177 def budget_shift(+d: Nat, +l: Nat) -> {Nat.is_le(Nat.add(1n+d, l), Nat.add(d, 1n+l)) == True{} : Bool}: 178 L.subst(Nat, z => {Nat.is_le(z, Nat.add(d, 1n+l)) == True{} : Bool}, Nat.add(d, 1n+l), Nat.add(1n+d, l), add_shift(d, l), N.le_refl(Nat.add(d, 1n+l))) 179 180 def FromOK(~A: Data, ~cmp: A -> A -> Cmp, ys: List<&2, A>, sh: ST.Shadow) -> Type: 181 Sigma<&1, &1, ST.Shadow, sh2 => {H.from_list_go(~A, ~cmp, ys, ST.real(~A, sh)) == ST.real(~A, sh2) : H.Heap} & ({ST.good(~A, ~cmp, sh2) == True{} : Bool} & ({ST.model(~A, ~cmp, sh2) == S.from_list(~A, ~cmp, ys, ST.model(~A, ~cmp, sh)) : List<&2, A>} & {Nat.is_le(ST.sh_depth(~A, sh2), Nat.add(ST.sh_depth(~A, sh), SC.length(A, ys))) == True{} : Bool}))> 182 183 def FromRec(~A: Data, ~cmp: A -> A -> Cmp, rest: List<&2, A>, +q: Nat) -> Type: 184 @+sh1: ST.Shadow -> @+g1: {ST.good(~A, ~cmp, sh1) == True{} : Bool} -> @+r1: {Nat.is_lt(Nat.add(ST.sh_size(~A, sh1), SC.length(A, rest)), SC.pow2(q)) == True{} : Bool} -> FromOK(~A, ~cmp, rest, sh1) 185 186 def from_rest(~A: Data, ~cmp: A -> A -> Cmp, +y: A, +rest: List<&2, A>, +sh: ST.Shadow, +sh1: ST.Shadow, +ereal: {H.push(~A, ~cmp, ST.real(~A, sh), y) == ST.real(~A, sh1) : H.Heap}, +ems: {ST.model(~A, ~cmp, sh1) == S.ins(~A, ~cmp, y, ST.model(~A, ~cmp, sh)) : List<&2, A>}, +edd: {Nat.is_le(ST.sh_depth(~A, sh1), 1n+ST.sh_depth(~A, sh)) == True{} : Bool}, r: FromOK(~A, ~cmp, rest, sh1)) -> FromOK(~A, ~cmp, Con{y, rest}, sh): 187 match r: 188 case Tuple{+sh2, Tuple{ereal2, Tuple{g2, Tuple{ems2, edd2}}}}: 189 (sh2, 190 (Equal.trans(H.Heap, H.from_list_go(~A, ~cmp, Con{y, rest}, ST.real(~A, sh)), H.from_list_go(~A, ~cmp, rest, ST.real(~A, sh1)), ST.real(~A, sh2), 191 Equal.cong(H.Heap, H.Heap, hh => H.from_list_go(~A, ~cmp, rest, hh), H.push(~A, ~cmp, ST.real(~A, sh), y), ST.real(~A, sh1), ereal), 192 ereal2), 193 (g2, 194 (Equal.trans(List<&2, A>, ST.model(~A, ~cmp, sh2), S.from_list(~A, ~cmp, rest, ST.model(~A, ~cmp, sh1)), S.from_list(~A, ~cmp, Con{y, rest}, ST.model(~A, ~cmp, sh)), 195 ems2, 196 Equal.cong(List<&2, A>, List<&2, A>, zs => S.from_list(~A, ~cmp, rest, zs), ST.model(~A, ~cmp, sh1), S.ins(~A, ~cmp, y, ST.model(~A, ~cmp, sh)), ems)), 197 N.le_trans(ST.sh_depth(~A, sh2), Nat.add(ST.sh_depth(~A, sh1), SC.length(A, rest)), Nat.add(ST.sh_depth(~A, sh), 1n+SC.length(A, rest)), 198 edd2, 199 N.le_trans(Nat.add(ST.sh_depth(~A, sh1), SC.length(A, rest)), Nat.add(1n+ST.sh_depth(~A, sh), SC.length(A, rest)), Nat.add(ST.sh_depth(~A, sh), 1n+SC.length(A, rest)), 200 add_le_r(ST.sh_depth(~A, sh1), 1n+ST.sh_depth(~A, sh), SC.length(A, rest), edd), 201 budget_shift(ST.sh_depth(~A, sh), SC.length(A, rest)))))))) 202 203 def from_push(~A: Data, ~cmp: A -> A -> Cmp, +y: A, +rest: List<&2, A>, +sh: ST.Shadow, +g: {ST.good(~A, ~cmp, sh) == True{} : Bool}, +q: Nat, +room: {Nat.is_lt(Nat.add(ST.sh_size(~A, sh), 1n+SC.length(A, rest)), SC.pow2(q)) == True{} : Bool}, rec: FromRec(~A, ~cmp, rest, q), +sh1: ST.Shadow, +ereal: {H.push(~A, ~cmp, ST.real(~A, sh), y) == ST.real(~A, sh1) : H.Heap}, +g1: {ST.good(~A, ~cmp, sh1) == True{} : Bool}, +ems: {ST.model(~A, ~cmp, sh1) == S.ins(~A, ~cmp, y, ST.model(~A, ~cmp, sh)) : List<&2, A>}, +edd: {Nat.is_le(ST.sh_depth(~A, sh1), 1n+ST.sh_depth(~A, sh)) == True{} : Bool}) -> FromOK(~A, ~cmp, Con{y, rest}, sh): 204 from_rest(~A, ~cmp, y, rest, sh, sh1, ereal, ems, edd, 205 rec(sh1, g1, budget_rest(~A, ~cmp, y, rest, sh, sh1, q, g, g1, ems, room))) 206 207 def from_cons(~A: Data, ~cmp: A -> A -> Cmp, +y: A, +rest: List<&2, A>, +sh: ST.Shadow, +g: {ST.good(~A, ~cmp, sh) == True{} : Bool}, +q: Nat, +room: {Nat.is_lt(Nat.add(ST.sh_size(~A, sh), 1n+SC.length(A, rest)), SC.pow2(q)) == True{} : Bool}, rec: FromRec(~A, ~cmp, rest, q), r: PU.PushOK(~A, ~cmp, sh, y)) -> FromOK(~A, ~cmp, Con{y, rest}, sh): 208 match r: 209 case Tuple{sh1, Tuple{ereal, Tuple{g1, Tuple{ems, edd}}}}: 210 from_push(~A, ~cmp, y, rest, sh, g, q, room, rec, sh1, ereal, g1, ems, edd) 211 212 def from_list_ok(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), ys: List<&2, A>, sh: ST.Shadow, +g: {ST.good(~A, ~cmp, sh) == True{} : Bool}, +q: Nat, +hq: {Nat.is_le(q, 31n) == True{} : Bool}, +room: {Nat.is_lt(Nat.add(ST.sh_size(~A, sh), SC.length(A, ys)), SC.pow2(q)) == True{} : Bool}) -> FromOK(~A, ~cmp, ys, sh): 213 match ys sh: 214 case Nil{} ST.Sh{+size, +depth, +t}: 215 (ST.Sh{size, depth, t}, ({==}, (g, ({==}, le_same(depth))))) 216 case Con{+y, +rest} ST.Sh{+size, +depth, +t}: 217 from_cons(~A, ~cmp, y, rest, ST.Sh{size, depth, t}, g, q, room, 218 sh1 => g1 => r1 => from_list_ok(~A, ~cmp, ~o, rest, sh1, g1, q, hq, r1), 219 PU.push_ok(~A, ~cmp, ~o, size, depth, t, y, g, 220 BG.room_or(size, depth, q, hq, N.le_lt_trans(size, Nat.add(size, 1n+SC.length(A, rest)), SC.pow2(q), N.le_add_right(size, 1n+SC.length(A, rest)), room)), 221 Nat.is_lt(size, SC.pow2(depth)), {==})) 222 223 def le_add_zero(+l: Nat, +d: Nat) -> {Nat.is_le(Nat.add(0n, l), Nat.add(d, l)) == True{} : Bool}: 224 add_le_r(0n, d, l, N.zero_le(d)) 225 226 def from_list_step(~A: Data, ~cmp: A -> A -> Cmp, +size: Nat, +depth: Nat, +t: AR.Tree>, +ys: List<&2, A>, r: FromOK(~A, ~cmp, ys, ST.initial(~A))) -> StepOK(~A, ~cmp, ST.Sh{size, depth, t}, E.FromList{ys}): 227 match r: 228 case Tuple{+sh2, Tuple{ereal, Tuple{g2, Tuple{ems, edd}}}}: 229 mk(~A, ~cmp, ST.Sh{size, depth, t}, E.FromList{ys}, sh2, E.OUnit{}, 230 %Equal.sym(H.Heap, H.new(~A), ST.real(~A, ST.initial(~A)), ST.new_real(~A)) : {(H.from_list_go(~A, ~cmp, ys, _), E.OUnit{}) == (ST.real(~A, sh2), E.OUnit{}) : H.Heap & E.Obs} 231 Equal.cong(H.Heap, H.Heap & E.Obs, hh => (hh, E.OUnit{}), H.from_list_go(~A, ~cmp, ys, ST.real(~A, ST.initial(~A))), ST.real(~A, sh2), ereal), 232 g2, 233 Equal.cong(List<&2, A>, List<&2, A> & E.Obs, zs => (zs, E.OUnit{}), ST.model(~A, ~cmp, sh2), S.from_list(~A, ~cmp, ys, Nil{}), ems), 234 N.le_trans(ST.sh_depth(~A, sh2), Nat.add(0n, SC.length(A, ys)), Nat.add(depth, SC.length(A, ys)), edd, le_add_zero(SC.length(A, ys), depth))) 235 236 # ---- every operation ---- 237 # 238 # `room` is the capacity condition of the representation for this step, in 239 # terms of the heap's size: size + pushcost(op) < 2^q with q <= 31. A push 240 # doubles only a full block, where 2^depth = size < 2^q forces depth < 31, so 241 # every slot index stays a representable U32. It is the only premise besides 242 # the invariant, and trace.bend discharges it for a whole operation list. 243 244 def step_ok(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), sh: ST.Shadow, op: E.Op, +g: {ST.good(~A, ~cmp, sh) == True{} : Bool}, +q: Nat, +hq: {Nat.is_le(q, 31n) == True{} : Bool}, +room: {Nat.is_lt(Nat.add(ST.sh_size(~A, sh), pushcost(~A, op)), SC.pow2(q)) == True{} : Bool}) -> StepOK(~A, ~cmp, sh, op): 245 match sh op: 246 case ST.Sh{+size, +depth, +t} E.Length{}: 247 length_ok(~A, ~cmp, size, depth, t, g) 248 case ST.Sh{+size, +depth, +t} E.Push{+x}: 249 push_ok(~A, ~cmp, ~o, size, depth, t, x, g, q, hq, N.le_lt_trans(size, Nat.add(size, 1n), SC.pow2(q), N.le_add_right(size, 1n), room)) 250 case ST.Sh{+size, +depth, +t} E.Peek{}: 251 peek_ok(~A, ~cmp, ~o, size, depth, t, g) 252 case ST.Sh{+size, +depth, +t} E.Pop{}: 253 pop_ok(~A, ~cmp, ~o, size, depth, t, g) 254 case ST.Sh{+size, +depth, +t} E.FromList{+ys}: 255 from_list_step(~A, ~cmp, size, depth, t, ys, 256 from_list_ok(~A, ~cmp, ~o, ys, ST.initial(~A), ST.new_good(~A, ~cmp), q, hq, 257 N.le_lt_trans(Nat.add(0n, SC.length(A, ys)), Nat.add(size, SC.length(A, ys)), SC.pow2(q), le_add_zero(SC.length(A, ys), size), room))) 258 case ST.Sh{+size, +depth, +t} E.ToSortedList{}: 259 sorted_ok(~A, ~cmp, ~o, size, depth, t, g)