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 ./up.bend as UPS 18 import ./grow.bend as GR 19 import ./state.bend as ST 20 21 # push: the element is written at slot `size` and sifted up. The four 22 # hypotheses of the sift-up law hold at a fresh leaf: 23 # ho_exc every pair except the one into the new slot holds already, 24 # kids_le the new slot has no children inside the heap, 25 # lay the slots below `size` are untouched and slot `size` is now full, 26 # msort the multiset gains exactly x. 27 # If the block is full it is doubled first (grow.bend: nothing but the 28 # capacity changes). 29 30 # ---- the pairs below the new leaf are untouched ---- 31 32 def pair_off(~A: Data, ~cmp: A -> A -> Cmp, +t: AR.Tree>, +i: Nat, +x: A, m: Nat, +hmi: {Nat.is_lt(m, i) == True{} : Bool}, +h: {SL.pair_ok(~A, ~cmp, AR.slots(Maybe<&2, A>, t), m) == True{} : Bool}) -> {SL.pair_ok(~A, ~cmp, UPS.ulog(~A, t, i, x), m) == True{} : Bool}: 33 match m: 34 case 0n: 35 {==} 36 case 1n+ +p: 37 %Equal.sym(Maybe<&2, A>, SL.slot(~A, UPS.ulog(~A, t, i, x), 1n+p), SL.slot(~A, AR.slots(Maybe<&2, A>, t), 1n+p), UPS.ulog_off(~A, t, i, x, 1n+p, SL.ne_sym(i, 1n+p, N.is_eq_lt(1n+p, i, hmi)))) : {SL.mle(~A, ~cmp, SL.slot(~A, UPS.ulog(~A, t, i, x), IX.par(1n+p)), _) == True{} : Bool} 38 %Equal.sym(Maybe<&2, A>, SL.slot(~A, UPS.ulog(~A, t, i, x), IX.par(1n+p)), SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.par(1n+p)), UPS.ulog_off(~A, t, i, x, IX.par(1n+p), SL.ne_sym(i, IX.par(1n+p), N.is_eq_lt(IX.par(1n+p), i, N.lt_trans(IX.par(1n+p), 1n+p, i, IX.par_lt(1n+p, {==}), hmi))))) : {SL.mle(~A, ~cmp, _, SL.slot(~A, AR.slots(Maybe<&2, A>, t), 1n+p)) == True{} : Bool} 39 h 40 41 def exc_step(~A: Data, ~cmp: A -> A -> Cmp, +t: AR.Tree>, +i: Nat, +x: A, +m: Nat, +hm: {Nat.is_lt(m, 1n+i) == True{} : Bool}, +hho: {SL.ho_upto(~A, ~cmp, AR.slots(Maybe<&2, A>, t), i) == True{} : Bool}, b: Bool, +eb: {Nat.is_eq(m, i) == b : Bool}) -> {SL.pair_skip(~A, ~cmp, UPS.ulog(~A, t, i, x), m, i) == True{} : Bool}: 42 match b: 43 case True{}: 44 SL.skip_eq(~A, ~cmp, UPS.ulog(~A, t, i, x), m, i, eb) 45 case False{}: 46 +hmi = N.lt_or_eq(m, i, N.lt_succ_le(m, i, hm), eb) 47 SL.skip_ne(~A, ~cmp, UPS.ulog(~A, t, i, x), m, i, eb, 48 pair_off(~A, ~cmp, t, i, x, m, hmi, SL.ho_at(~A, ~cmp, AR.slots(Maybe<&2, A>, t), i, m, hho, hmi))) 49 50 def exc_up(~A: Data, ~cmp: A -> A -> Cmp, +t: AR.Tree>, +i: Nat, +x: A, k: Nat, +hk: {Nat.is_le(k, 1n+i) == True{} : Bool}, +hho: {SL.ho_upto(~A, ~cmp, AR.slots(Maybe<&2, A>, t), i) == True{} : Bool}) -> {SL.ho_exc(~A, ~cmp, UPS.ulog(~A, t, i, x), k, i) == True{} : Bool}: 51 match k: 52 case 0n: 53 {==} 54 case 1n+ +m: 55 L.and_intro(SL.pair_skip(~A, ~cmp, UPS.ulog(~A, t, i, x), m, i), SL.ho_exc(~A, ~cmp, UPS.ulog(~A, t, i, x), m, i), 56 exc_step(~A, ~cmp, t, i, x, m, N.succ_le_lt(m, 1n+i, hk), hho, Nat.is_eq(m, i), {==}), 57 exc_up(~A, ~cmp, t, i, x, m, N.le_trans(m, 1n+m, 1n+i, N.le_succ(m), hk), hho)) 58 59 # ---- the new leaf has no children inside the heap ---- 60 61 def kids_leaf(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, +u: Nat, +i: Nat) -> {SL.kids_le(~A, ~cmp, ss, 1n+i, u, i) == True{} : Bool}: 62 L.and_intro(SL.kid_le(~A, ~cmp, ss, 1n+i, u, IX.kidl(i)), SL.kid_le(~A, ~cmp, ss, 1n+i, u, IX.kidr(i)), 63 SL.kid_le_out(~A, ~cmp, ss, 1n+i, u, IX.kidl(i), N.le_not_lt(IX.kidl(i), 1n+i, IX.double_le(i))), 64 SL.kid_le_out(~A, ~cmp, ss, 1n+i, u, IX.kidr(i), N.le_not_lt(IX.kidr(i), 1n+i, N.le_trans(1n+i, IX.kidl(i), IX.kidr(i), IX.double_le(i), N.le_succ(IX.kidl(i)))))) 65 66 # ---- the layout below the new leaf is untouched ---- 67 68 def lay_off(~A: Data, +ss: List<&2, Maybe<&2, A>>, +i: Nat, +v: Maybe<&2, A>, k: Nat, +hk: {Nat.is_le(k, i) == True{} : Bool}, +h: {SL.lay(~A, ss, k) == True{} : Bool}) -> {SL.lay(~A, SC.update(Maybe<&2, A>, ss, i, v), k) == True{} : Bool}: 69 match k: 70 case 0n: 71 {==} 72 case 1n+ +m: 73 %Equal.sym(Maybe<&2, A>, SL.slot(~A, SC.update(Maybe<&2, A>, ss, i, v), m), SL.slot(~A, ss, m), SL.slot_other(~A, ss, i, m, v, SL.ne_sym(i, m, N.is_eq_lt(m, i, N.succ_le_lt(m, i, hk))))) : {Bool.and(Maybe.is_some(&2, A, _), SL.lay(~A, SC.update(Maybe<&2, A>, ss, i, v), m)) == True{} : Bool} 74 L.and_intro(Maybe.is_some(&2, A, SL.slot(~A, ss, m)), SL.lay(~A, SC.update(Maybe<&2, A>, ss, i, v), m), 75 L.and_left(Maybe.is_some(&2, A, SL.slot(~A, ss, m)), SL.lay(~A, ss, m), h), 76 lay_off(~A, ss, i, v, m, N.lt_le(m, i, N.succ_le_lt(m, i, hk)), L.and_right(Maybe.is_some(&2, A, SL.slot(~A, ss, m)), SL.lay(~A, ss, m), h))) 77 78 def lay_push(~A: Data, +d: Nat, +t: AR.Tree>, +i: Nat, +x: A, +hi: {Nat.is_lt(i, SC.pow2(d)) == True{} : Bool}, +pf: {AR.perfect(Maybe<&2, A>, d, t) == True{} : Bool}, +h: {SL.lay(~A, AR.slots(Maybe<&2, A>, t), i) == True{} : Bool}) -> {SL.lay(~A, UPS.ulog(~A, t, i, x), 1n+i) == True{} : Bool}: 79 L.and_intro(Maybe.is_some(&2, A, SL.slot(~A, UPS.ulog(~A, t, i, x), i)), SL.lay(~A, UPS.ulog(~A, t, i, x), i), 80 L.subst(Maybe<&2, A>, z => {Maybe.is_some(&2, A, z) == True{} : Bool}, Some{x}, SL.slot(~A, UPS.ulog(~A, t, i, x), i), Equal.sym(Maybe<&2, A>, SL.slot(~A, UPS.ulog(~A, t, i, x), i), Some{x}, UPS.ulog_at(~A, d, t, i, x, hi, pf)), {==}), 81 lay_off(~A, AR.slots(Maybe<&2, A>, t), i, Some{x}, i, N.le_refl(i), h)) 82 83 # ---- the multiset gains exactly x ---- 84 85 def ms_push(~A: Data, ~cmp: A -> A -> Cmp, +d: Nat, +t: AR.Tree>, +i: Nat, +x: A, +hi: {Nat.is_lt(i, SC.pow2(d)) == True{} : Bool}, +pf: {AR.perfect(Maybe<&2, A>, d, t) == True{} : Bool}) -> {V.msort(~A, ~cmp, V.vals(~A, UPS.ulog(~A, t, i, x), 1n+i)) == S.ins(~A, ~cmp, x, V.msort(~A, ~cmp, V.vals(~A, AR.slots(Maybe<&2, A>, t), i))) : List<&2, A>}: 86 %Equal.sym(Maybe<&2, A>, SL.slot(~A, UPS.ulog(~A, t, i, x), i), Some{x}, UPS.ulog_at(~A, d, t, i, x, hi, pf)) : {V.msort(~A, ~cmp, V.cons_slot(~A, _, V.vals(~A, UPS.ulog(~A, t, i, x), i))) == S.ins(~A, ~cmp, x, V.msort(~A, ~cmp, V.vals(~A, AR.slots(Maybe<&2, A>, t), i))) : List<&2, A>} 87 Equal.cong(List<&2, A>, List<&2, A>, zs => S.ins(~A, ~cmp, x, V.msort(~A, ~cmp, zs)), V.vals(~A, UPS.ulog(~A, t, i, x), i), V.vals(~A, AR.slots(Maybe<&2, A>, t), i), V.vals_above(~A, AR.slots(Maybe<&2, A>, t), i, Some{x}, i, N.le_refl(i))) 88 89 # ---- one sift-up at the fresh leaf ---- 90 91 def PushOK(~A: Data, ~cmp: A -> A -> Cmp, sh: ST.Shadow, x: A) -> Type: 92 Sigma<&1, &1, ST.Shadow, sh2 => {H.push(~A, ~cmp, ST.real(~A, sh), x) == ST.real(~A, sh2) : H.Heap} & ({ST.good(~A, ~cmp, sh2) == True{} : Bool} & ({ST.model(~A, ~cmp, sh2) == S.ins(~A, ~cmp, x, ST.model(~A, ~cmp, sh)) : List<&2, A>} & {Nat.is_le(ST.sh_depth(~A, sh2), 1n+ST.sh_depth(~A, sh)) == True{} : Bool}))> 93 94 # The sift-up result, packaged as the new shadow. `d` is the depth of the 95 # block the element is written into (the grown depth if the block was full). 96 def push_from(~A: Data, ~cmp: A -> A -> Cmp, +sh0: ST.Shadow, +size: Nat, +d: Nat, +t: AR.Tree>, +x: A, +tgt: List<&2, A>, +hd: {Nat.is_le(d, 31n) == True{} : Bool}, +hs: {Nat.is_le(1n+size, SC.pow2(d)) == True{} : Bool}, +hdd: {Nat.is_le(d, 1n+ST.sh_depth(~A, sh0)) == True{} : Bool}, +eq0: {H.push(~A, ~cmp, ST.real(~A, sh0), x) == H.BH{1n+size, U32.from_nat(1n+size), d, U.pow2u(d), H.sift_up(~A, ~cmp, d, U32.from_nat(size), x, AR.thaw(Maybe<&2, A>, t))} : H.Heap}, r: UPS.SiftOK(~A, ~cmp, d, 1n+size, tgt, d, t, size, x)) -> Sigma<&1, &1, ST.Shadow, sh2 => {H.push(~A, ~cmp, ST.real(~A, sh0), x) == ST.real(~A, sh2) : H.Heap} & ({ST.good(~A, ~cmp, sh2) == True{} : Bool} & ({ST.model(~A, ~cmp, sh2) == tgt : List<&2, A>} & {Nat.is_le(ST.sh_depth(~A, sh2), 1n+ST.sh_depth(~A, sh0)) == True{} : Bool}))>: 97 match r: 98 case Tuple{+t2, Tuple{esift, Tuple{pf2, Tuple{hho2, Tuple{hlay2, hms2}}}}}: 99 (ST.Sh{1n+size, d, t2}, 100 (Equal.trans(H.Heap, H.push(~A, ~cmp, ST.real(~A, sh0), x), H.BH{1n+size, U32.from_nat(1n+size), d, U.pow2u(d), H.sift_up(~A, ~cmp, d, U32.from_nat(size), x, AR.thaw(Maybe<&2, A>, t))}, ST.real(~A, ST.Sh{1n+size, d, t2}), eq0, 101 Equal.cong(Array>, H.Heap, a => H.BH{1n+size, U32.from_nat(1n+size), d, U.pow2u(d), a}, H.sift_up(~A, ~cmp, d, U32.from_nat(size), x, AR.thaw(Maybe<&2, A>, t)), AR.thaw(Maybe<&2, A>, t2), esift)), 102 (ST.good_intro(~A, ~cmp, 1n+size, d, t2, hd, pf2, hlay2, hho2, hs), 103 (hms2, hdd)))) 104 105 # ---- the capacity decision, in Nat ---- 106 107 def room_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_lt(U32.from_nat(size), U.pow2u(depth)) == Nat.is_lt(size, SC.pow2(depth)) : Bool}: 108 +hk = N.le_lt_trans(size, SC.pow2(depth), SC.pow2(1n+depth), hs, N.pow2_lt_succ(depth)) 109 Equal.sym(Bool, Nat.is_lt(size, SC.pow2(depth)), U32.is_lt(U32.from_nat(size), U.pow2u(depth)), 110 %UX.nat_round(size, 1n+depth, hd, hk) : {Nat.is_lt(_, SC.pow2(depth)) == U32.is_lt(U32.from_nat(size), U.pow2u(depth)) : Bool} 111 AR.lt_bridge(U32.from_nat(size), depth, ST.depth_lt32(depth, hd), U32.is_lt(U32.from_nat(size), U.pow2u(depth)), {==})) 112 113 def succ_le_double(+p: Nat, +h: {Nat.is_le(1n, p) == True{} : Bool}) -> {Nat.is_le(1n+p, Nat.double(p)) == True{} : Bool}: 114 match p: 115 case 0n: 116 Empty.absurd({Nat.is_le(1n, Nat.double(0n)) == True{} : Bool}, L.true_not_false(Nat.is_le(1n, 0n), h, {==})) 117 case 1n+ +k: 118 IX.double_le(k) 119 120 # ---- push into a block with room ---- 121 122 def push_room_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}, +hlt: {Nat.is_lt(size, SC.pow2(depth)) == True{} : Bool}) -> PushOK(~A, ~cmp, ST.Sh{size, depth, t}, x): 123 +hd = ST.g_depth(~A, ~cmp, size, depth, t, g) 124 +pf = ST.g_perfect(~A, ~cmp, size, depth, t, g) 125 push_from(~A, ~cmp, ST.Sh{size, depth, t}, size, depth, t, x, S.ins(~A, ~cmp, x, ST.model(~A, ~cmp, ST.Sh{size, depth, t})), hd, 126 N.lt_succ_le_succ(size, SC.pow2(depth), hlt), N.le_succ(depth), 127 %Equal.sym(Bool, U32.is_lt(U32.from_nat(size), U.pow2u(depth)), Nat.is_lt(size, SC.pow2(depth)), room_bridge(size, depth, hd, ST.g_size(~A, ~cmp, size, depth, t, g))) : {H.push_room(~A, ~cmp, size, U32.from_nat(size), depth, U.pow2u(depth), AR.thaw(Maybe<&2, A>, t), x, _) == H.BH{1n+size, U32.from_nat(1n+size), depth, U.pow2u(depth), H.sift_up(~A, ~cmp, depth, U32.from_nat(size), x, AR.thaw(Maybe<&2, A>, t))} : H.Heap} 128 %Equal.sym(Bool, Nat.is_lt(size, SC.pow2(depth)), True{}, hlt) : {H.push_room(~A, ~cmp, size, U32.from_nat(size), depth, U.pow2u(depth), AR.thaw(Maybe<&2, A>, t), x, _) == H.BH{1n+size, U32.from_nat(1n+size), depth, U.pow2u(depth), H.sift_up(~A, ~cmp, depth, U32.from_nat(size), x, AR.thaw(Maybe<&2, A>, t))} : H.Heap} 129 {==}, 130 UPS.sift_up_ok(~A, ~cmp, ~o, depth, depth, 1n+size, S.ins(~A, ~cmp, x, ST.model(~A, ~cmp, ST.Sh{size, depth, t})), t, size, x, 131 ST.depth_lt32(depth, hd), hlt, N.lt_succ(size), hlt, pf, 132 exc_up(~A, ~cmp, t, size, x, 1n+size, N.le_refl(1n+size), ST.g_ho(~A, ~cmp, size, depth, t, g)), 133 kids_leaf(~A, ~cmp, UPS.ulog(~A, t, size, x), IX.par(size), size), 134 lay_push(~A, depth, t, size, x, hlt, pf, ST.g_lay(~A, ~cmp, size, depth, t, g)), 135 ms_push(~A, ~cmp, depth, t, size, x, hlt, pf))) 136 137 # ---- push into a full block: double it first ---- 138 139 def push_grow_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}, +hfull: {Nat.is_lt(size, SC.pow2(depth)) == False{} : Bool}, +hroom: {Nat.is_lt(depth, 31n) == True{} : Bool}) -> PushOK(~A, ~cmp, ST.Sh{size, depth, t}, x): 140 +hd = ST.g_depth(~A, ~cmp, size, depth, t, g) 141 +pf = ST.g_perfect(~A, ~cmp, size, depth, t, g) 142 +hs = ST.g_size(~A, ~cmp, size, depth, t, g) 143 +t2 = GR.gtree(~A, depth, t) 144 +pf2 = GR.gtree_perfect(~A, depth, t, pf) 145 +hi2 = N.le_lt_trans(size, SC.pow2(depth), SC.pow2(1n+depth), hs, N.pow2_lt_succ(depth)) 146 +hs2 = N.le_trans(1n+size, 1n+SC.pow2(depth), SC.pow2(1n+depth), hs, succ_le_double(SC.pow2(depth), N.pow2_pos(depth))) 147 push_from(~A, ~cmp, ST.Sh{size, depth, t}, size, 1n+depth, t2, x, S.ins(~A, ~cmp, x, ST.model(~A, ~cmp, ST.Sh{size, depth, t})), N.lt_succ_le_succ(depth, 31n, hroom), hs2, N.le_refl(1n+depth), 148 %AR.new(Maybe<&2, A>, depth, None{}) : {H.push_room(~A, ~cmp, size, U32.from_nat(size), depth, U.pow2u(depth), AR.thaw(Maybe<&2, A>, t), x, U32.is_lt(U32.from_nat(size), U.pow2u(depth))) == H.BH{1n+size, U32.from_nat(1n+size), 1n+depth, U.pow2u(1n+depth), H.sift_up(~A, ~cmp, 1n+depth, U32.from_nat(size), x, ANode{AR.thaw(Maybe<&2, A>, t), _})} : H.Heap} 149 %Equal.sym(Bool, U32.is_lt(U32.from_nat(size), U.pow2u(depth)), Nat.is_lt(size, SC.pow2(depth)), room_bridge(size, depth, hd, hs)) : {H.push_room(~A, ~cmp, size, U32.from_nat(size), depth, U.pow2u(depth), AR.thaw(Maybe<&2, A>, t), x, _) == H.BH{1n+size, U32.from_nat(1n+size), 1n+depth, U.pow2u(1n+depth), H.sift_up(~A, ~cmp, 1n+depth, U32.from_nat(size), x, H.grown(~A, depth, AR.thaw(Maybe<&2, A>, t)))} : H.Heap} 150 %Equal.sym(Bool, Nat.is_lt(size, SC.pow2(depth)), False{}, hfull) : {H.push_room(~A, ~cmp, size, U32.from_nat(size), depth, U.pow2u(depth), AR.thaw(Maybe<&2, A>, t), x, _) == H.BH{1n+size, U32.from_nat(1n+size), 1n+depth, U.pow2u(1n+depth), H.sift_up(~A, ~cmp, 1n+depth, U32.from_nat(size), x, H.grown(~A, depth, AR.thaw(Maybe<&2, A>, t)))} : H.Heap} 151 {==}, 152 L.subst(List<&2, A>, zs => UPS.SiftOK(~A, ~cmp, 1n+depth, 1n+size, S.ins(~A, ~cmp, x, V.msort(~A, ~cmp, zs)), 1n+depth, t2, size, x), V.vals(~A, AR.slots(Maybe<&2, A>, t2), size), V.vals(~A, AR.slots(Maybe<&2, A>, t), size), GR.gtree_vals(~A, depth, t, size, pf, hs), 153 UPS.sift_up_ok(~A, ~cmp, ~o, 1n+depth, 1n+depth, 1n+size, S.ins(~A, ~cmp, x, V.msort(~A, ~cmp, V.vals(~A, AR.slots(Maybe<&2, A>, t2), size))), t2, size, x, 154 ST.depth_lt32(1n+depth, N.lt_succ_le_succ(depth, 31n, hroom)), hi2, N.lt_succ(size), hi2, pf2, 155 exc_up(~A, ~cmp, t2, size, x, 1n+size, N.le_refl(1n+size), GR.gtree_ho(~A, ~cmp, depth, t, size, pf, hs, ST.g_ho(~A, ~cmp, size, depth, t, g))), 156 kids_leaf(~A, ~cmp, UPS.ulog(~A, t2, size, x), IX.par(size), size), 157 lay_push(~A, 1n+depth, t2, size, x, hi2, pf2, GR.gtree_lay(~A, depth, t, size, pf, hs, ST.g_lay(~A, ~cmp, size, depth, t, g))), 158 ms_push(~A, ~cmp, 1n+depth, t2, size, x, hi2, pf2)))) 159 160 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}, +hroom: {Bool.or(Nat.is_lt(size, SC.pow2(depth)), Nat.is_lt(depth, 31n)) == True{} : Bool}, b: Bool, +eb: {Nat.is_lt(size, SC.pow2(depth)) == b : Bool}) -> PushOK(~A, ~cmp, ST.Sh{size, depth, t}, x): 161 match b: 162 case True{}: 163 push_room_ok(~A, ~cmp, ~o, size, depth, t, x, g, eb) 164 case False{}: 165 push_grow_ok(~A, ~cmp, ~o, size, depth, t, x, g, eb, 166 L.subst(Bool, c => {Bool.or(c, Nat.is_lt(depth, 31n)) == True{} : Bool}, Nat.is_lt(size, SC.pow2(depth)), False{}, eb, hroom))