1 import Base 2 import ./types/binary_heap.bend as E 3 4 # Min-heap in a PACKED native array: the elements live in slots [0, size) of a 5 # `Base.Array` of 2^depth slots, element i having children 2i+1 and 2i+2 and 6 # parent (i-1)/2. No node is allocated per element and no link is stored: the 7 # heap shape is the index arithmetic (docs/ARCHITECTURE.md). 8 # 9 # push writes the element at slot `size` and SIFTS IT UP while its parent 10 # is larger (early exit: the loop stops at the first parent that is 11 # not larger, which is what makes a random push O(1) on average), 12 # pop takes slot 0, moves the last element to the root and SIFTS IT DOWN 13 # through the smaller child, 14 # peek reads slot 0, length is the cached size, 15 # to_sorted_list clones the array and drains the clone (the heap itself is 16 # returned unchanged), 17 # from_list is repeated push. 18 # 19 # Index arithmetic uses `U32.shl` (doubling), `U32.inc` (+1) and `U32.shr` 20 # (halving) rather than `U32.add`, because those are exactly the operations 21 # whose Nat meaning the proofs can bridge without ever naming 2^32 -- a 22 # literal the checker would have to expand as a unary Nat 23 # (proofs/binary_heap/u32idx.bend). 24 # 25 # The record caches what would otherwise be recomputed per operation: `n` is 26 # the size as a U32 (the index the next push writes), `cap` = 2^depth as a 27 # U32, and `depth` bounds every sift loop. Indices are U32 throughout, so no 28 # index arithmetic walks a unary Nat; `size` stays a Nat because that is what 29 # the specification's `length` is. 30 # 31 # The order is a static comparator ~cmp : A -> A -> Cmp (a template 32 # parameter); its total-order laws are proof obligations of each instance 33 # (proofs/lib/order.bend: U32 and String). Elements equal under cmp are 34 # identical under the laws, so multiplicities are exact. 35 # 36 # Cost (n = size): push O(log n) worst case and O(1) expected, pop O(log n), 37 # peek/length O(1), from_list O(n log n), to_sorted_list O(n log n) plus one 38 # O(n) array clone. Capacity doubles when a push finds the block full; depth 39 # is bounded by 31, so every slot index is a representable U32. 40 # Errors: peek/pop on an empty heap -> Fail{EmptyHeap}, heap unchanged. 41 42 type Heap<-A: Data> is Type: 43 BH{size: Nat, n: U32, depth: Nat, cap: U32, slots: Array>} 44 45 def max_depth() -> Nat: 46 31n 47 48 def le(~A: Data, ~cmp: A -> A -> Cmp, x: A, y: A) -> Bool: 49 Cmp.is_le(cmp(x, y)) 50 51 def empty_slots(~A: Data, +depth: Nat) -> Array>: 52 Array.new(Maybe<&2, A>, depth, None{}) 53 54 def new(~A: Data) -> Heap: 55 BH{0n, 0, 0n, 1, empty_slots(~A, 0n)} 56 57 def length(~A: Data, h: Heap) -> Heap & Nat: 58 BH{+size, n, depth, cap, arr} = h 59 (BH{size, n, depth, cap, arr}, size) 60 61 # ---- reading a slot ---- 62 63 # The slot value, with a default that a well-formed heap never needs (every 64 # index a sift loop reads is inside [0, size), where the slot is Some). 65 def slot_or(~A: Data, d: A, m: Maybe<&2, A>) -> A: 66 match m: 67 case None{}: 68 d 69 case Some{v}: 70 v 71 72 def item_of(~A: Data, m: Maybe<&2, A>) -> Result<&2, &2, E.Error, A>: 73 match m: 74 case None{}: 75 Fail{E.EmptyHeap{}} 76 case Some{v}: 77 Done{v} 78 79 # ---- sift up ---- 80 # 81 # A sift loop cannot be written as one recursive function with an early exit 82 # in Bend: `match` only scrutinises a parameter, and definitions may not be 83 # mutually recursive. The loop therefore carries its decision in a state that 84 # an earlier (non-recursive) probe builds: `UStop{arr, i}` means the sifted 85 # value belongs at slot i, `UMove{arr, i, pv, p}` means the parent value pv 86 # moves down into slot i and the sift goes on at p. 87 88 type Up<-A: Data> is Type: 89 UStop{arr: Array>, i: U32} 90 UMove{arr: Array>, i: U32, pv: A, p: U32} 91 92 # The parent index of i (i > 0). For i = 0 the probe never reads it. 93 def parent(+i: U32) -> U32: 94 U32.shr(U32.sub(i, 1)) 95 96 def up_dec(~A: Data, arr: Array>, i: U32, pv: A, p: U32, ok: Bool) -> Up: 97 match ok: 98 case True{}: 99 UStop{arr, i} 100 case False{}: 101 UMove{arr, i, pv, p} 102 103 def up_mb(~A: Data, ~cmp: A -> A -> Cmp, arr: Array>, i: U32, +x: A, p: U32, m: Maybe<&2, A>) -> Up: 104 match m: 105 case None{}: 106 UStop{arr, i} 107 case Some{+pv}: 108 up_dec(~A, arr, i, pv, p, le(~A, ~cmp, pv, x)) 109 110 def up_slot(~A: Data, ~cmp: A -> A -> Cmp, i: U32, x: A, p: U32, r: Array> & Maybe<&2, A>) -> Up: 111 (arr, m) = r 112 up_mb(~A, ~cmp, arr, i, x, p, m) 113 114 def up_root(~A: Data, ~cmp: A -> A -> Cmp, +i: U32, x: A, arr: Array>, root: Bool) -> Up: 115 match root: 116 case True{}: 117 UStop{arr, i} 118 case False{}: 119 up_slot(~A, ~cmp, i, x, parent(i), Array.get(Maybe<&2, A>, arr, parent(i))) 120 121 # Where the value x, currently destined for slot i, must go next. 122 def up_probe(~A: Data, ~cmp: A -> A -> Cmp, +i: U32, +x: A, arr: Array>) -> Up: 123 up_root(~A, ~cmp, i, x, arr, U32.is_eq(i, 0)) 124 125 def up_go(~A: Data, ~cmp: A -> A -> Cmp, fuel: Nat, +x: A, st: Up) -> Array>: 126 match fuel st: 127 case 0n UStop{arr, i}: 128 Array.set(Maybe<&2, A>, arr, i, Some{x}) 129 case 0n UMove{arr, i, pv, p}: 130 Array.set(Maybe<&2, A>, arr, i, Some{x}) 131 case 1n+f UStop{arr, i}: 132 Array.set(Maybe<&2, A>, arr, i, Some{x}) 133 case 1n+f UMove{arr, i, +pv, +p}: 134 up_go(~A, ~cmp, f, x, up_probe(~A, ~cmp, p, x, Array.set(Maybe<&2, A>, arr, i, Some{pv}))) 135 136 # Place x at slot i and restore heap order upwards (fuel bounds the climb). 137 def sift_up(~A: Data, ~cmp: A -> A -> Cmp, fuel: Nat, i: U32, +x: A, arr: Array>) -> Array>: 138 up_go(~A, ~cmp, fuel, x, up_probe(~A, ~cmp, i, x, arr)) 139 140 # ---- sift down ---- 141 142 type Down<-A: Data> is Type: 143 DStop{arr: Array>, i: U32} 144 DMove{arr: Array>, i: U32, cv: A, ci: U32} 145 146 def down_dec(~A: Data, arr: Array>, i: U32, cv: A, ci: U32, ok: Bool) -> Down: 147 match ok: 148 case True{}: 149 DStop{arr, i} 150 case False{}: 151 DMove{arr, i, cv, ci} 152 153 def down_two(~A: Data, ~cmp: A -> A -> Cmp, arr: Array>, i: U32, +x: A, l: U32, +lv: A, r: U32, +rv: A, left: Bool) -> Down: 154 match left: 155 case True{}: 156 down_dec(~A, arr, i, lv, l, le(~A, ~cmp, x, lv)) 157 case False{}: 158 down_dec(~A, arr, i, rv, r, le(~A, ~cmp, x, rv)) 159 160 def down_rmb(~A: Data, ~cmp: A -> A -> Cmp, arr: Array>, i: U32, +x: A, l: U32, +lv: A, r: U32, m: Maybe<&2, A>) -> Down: 161 match m: 162 case None{}: 163 down_dec(~A, arr, i, lv, l, le(~A, ~cmp, x, lv)) 164 case Some{+rv}: 165 down_two(~A, ~cmp, arr, i, x, l, lv, r, rv, le(~A, ~cmp, lv, rv)) 166 167 def down_rslot(~A: Data, ~cmp: A -> A -> Cmp, i: U32, x: A, l: U32, +lv: A, r: U32, rr: Array> & Maybe<&2, A>) -> Down: 168 (arr, m) = rr 169 down_rmb(~A, ~cmp, arr, i, x, l, lv, r, m) 170 171 def down_lmb(~A: Data, ~cmp: A -> A -> Cmp, arr: Array>, i: U32, +x: A, +l: U32, two: Bool, m: Maybe<&2, A>) -> Down: 172 match two m: 173 case _ None{}: 174 DStop{arr, i} 175 case True{} Some{+lv}: 176 down_rslot(~A, ~cmp, i, x, l, lv, U32.inc(l), Array.get(Maybe<&2, A>, arr, U32.inc(l))) 177 case False{} Some{+lv}: 178 down_dec(~A, arr, i, lv, l, le(~A, ~cmp, x, lv)) 179 180 def down_lslot(~A: Data, ~cmp: A -> A -> Cmp, i: U32, +x: A, +l: U32, two: Bool, r: Array> & Maybe<&2, A>) -> Down: 181 (arr, m) = r 182 down_lmb(~A, ~cmp, arr, i, x, l, two, m) 183 184 def down_has(~A: Data, ~cmp: A -> A -> Cmp, +size: U32, i: U32, x: A, arr: Array>, +l: U32, has_left: Bool) -> Down: 185 match has_left: 186 case True{}: 187 down_lslot(~A, ~cmp, i, x, l, U32.is_lt(l, U32.sub(size, 1)), Array.get(Maybe<&2, A>, arr, l)) 188 case False{}: 189 DStop{arr, i} 190 191 # Where the value x, currently destined for slot i of a heap of `size` 192 # elements, must go next. 193 def down_probe(~A: Data, ~cmp: A -> A -> Cmp, +size: U32, +i: U32, x: A, arr: Array>) -> Down: 194 down_has(~A, ~cmp, size, i, x, arr, U32.inc(U32.shl(i)), U32.is_lt(U32.inc(U32.shl(i)), size)) 195 196 def down_go(~A: Data, ~cmp: A -> A -> Cmp, fuel: Nat, +size: U32, +x: A, st: Down) -> Array>: 197 match fuel st: 198 case 0n DStop{arr, i}: 199 Array.set(Maybe<&2, A>, arr, i, Some{x}) 200 case 0n DMove{arr, i, cv, ci}: 201 Array.set(Maybe<&2, A>, arr, i, Some{x}) 202 case 1n+f DStop{arr, i}: 203 Array.set(Maybe<&2, A>, arr, i, Some{x}) 204 case 1n+f DMove{arr, i, +cv, +ci}: 205 down_go(~A, ~cmp, f, size, x, down_probe(~A, ~cmp, size, ci, x, Array.set(Maybe<&2, A>, arr, i, Some{cv}))) 206 207 # Place x at slot i of a heap of `size` elements and restore heap order down. 208 def sift_down(~A: Data, ~cmp: A -> A -> Cmp, fuel: Nat, +size: U32, i: U32, +x: A, arr: Array>) -> Array>: 209 down_go(~A, ~cmp, fuel, size, x, down_probe(~A, ~cmp, size, i, x, arr)) 210 211 # ---- push ---- 212 213 # Doubling: the old block becomes the lower half of a block one level deeper, 214 # so every element keeps its index. 215 def grown(~A: Data, +depth: Nat, arr: Array>) -> Array>: 216 ANode{arr, empty_slots(~A, depth)} 217 218 def push_room(~A: Data, ~cmp: A -> A -> Cmp, size: Nat, +n: U32, +depth: Nat, +cap: U32, arr: Array>, x: A, room: Bool) -> Heap: 219 match room: 220 case True{}: 221 BH{1n+size, U32.inc(n), depth, cap, sift_up(~A, ~cmp, depth, n, x, arr)} 222 case False{}: 223 BH{1n+size, U32.inc(n), 1n+depth, U32.shl(cap), sift_up(~A, ~cmp, 1n+depth, n, x, grown(~A, depth, arr))} 224 225 def push(~A: Data, ~cmp: A -> A -> Cmp, h: Heap, x: A) -> Heap: 226 BH{size, +n, +depth, +cap, arr} = h 227 push_room(~A, ~cmp, size, n, depth, cap, arr, x, U32.is_lt(n, cap)) 228 229 # ---- peek ---- 230 231 def peek_found(~A: Data, size: Nat, n: U32, depth: Nat, cap: U32, r: Array> & Maybe<&2, A>) -> Heap & Result<&2, &2, E.Error, A>: 232 (arr, m) = r 233 (BH{size, n, depth, cap, arr}, item_of(~A, m)) 234 235 def peek_go(~A: Data, size: Nat, +n: U32, depth: Nat, cap: U32, arr: Array>, empty: Bool) -> Heap & Result<&2, &2, E.Error, A>: 236 match empty: 237 case True{}: 238 (BH{size, n, depth, cap, arr}, Fail{E.EmptyHeap{}}) 239 case False{}: 240 peek_found(~A, size, n, depth, cap, Array.get(Maybe<&2, A>, arr, 0)) 241 242 def peek(~A: Data, h: Heap) -> Heap & Result<&2, &2, E.Error, A>: 243 BH{size, +n, depth, cap, arr} = h 244 peek_go(~A, size, n, depth, cap, arr, U32.is_eq(n, 0)) 245 246 # ---- pop ---- 247 248 # The last element has been taken out of slot m = n - 1; put it at the root 249 # and sift it down over the remaining m elements. 250 def pop_move(~A: Data, ~cmp: A -> A -> Cmp, size: Nat, +m: U32, +depth: Nat, cap: U32, root: A, last: A, arr: Array>, empty: Bool) -> Heap & Result<&2, &2, E.Error, A>: 251 match empty: 252 case True{}: 253 (BH{size, m, depth, cap, arr}, Done{root}) 254 case False{}: 255 (BH{size, m, depth, cap, sift_down(~A, ~cmp, depth, m, 0, last, arr)}, Done{root}) 256 257 def pop_last(~A: Data, ~cmp: A -> A -> Cmp, size: Nat, +m: U32, depth: Nat, cap: U32, +root: A, rl: Array> & Maybe<&2, A>) -> Heap & Result<&2, &2, E.Error, A>: 258 (arr, ml) = rl 259 pop_move(~A, ~cmp, size, m, depth, cap, root, slot_or(~A, root, ml), arr, U32.is_eq(m, 0)) 260 261 # The last element is READ, not cleared: the invariant says nothing about the 262 # slots above the size, so clearing it would be one array write per pop that 263 # the algorithm does not need (the C reference does not do it either). 264 # 265 # The root slot of a nonempty heap is Some; the None case cannot be reached 266 # from a well-formed heap and returns the state unchanged. 267 def pop_with(~A: Data, ~cmp: A -> A -> Cmp, size: Nat, +n: U32, depth: Nat, cap: U32, arr: Array>, mr: Maybe<&2, A>) -> Heap & Result<&2, &2, E.Error, A>: 268 match mr: 269 case None{}: 270 (BH{size, n, depth, cap, arr}, Fail{E.EmptyHeap{}}) 271 case Some{+root}: 272 pop_last(~A, ~cmp, Nat.sub(size, 1n), U32.sub(n, 1), depth, cap, root, Array.get(Maybe<&2, A>, arr, U32.sub(n, 1))) 273 274 def pop_root(~A: Data, ~cmp: A -> A -> Cmp, size: Nat, +n: U32, depth: Nat, cap: U32, rr: Array> & Maybe<&2, A>) -> Heap & Result<&2, &2, E.Error, A>: 275 (arr, mr) = rr 276 pop_with(~A, ~cmp, size, n, depth, cap, arr, mr) 277 278 def pop_go(~A: Data, ~cmp: A -> A -> Cmp, size: Nat, +n: U32, depth: Nat, cap: U32, arr: Array>, empty: Bool) -> Heap & Result<&2, &2, E.Error, A>: 279 match empty: 280 case True{}: 281 (BH{size, n, depth, cap, arr}, Fail{E.EmptyHeap{}}) 282 case False{}: 283 pop_root(~A, ~cmp, size, n, depth, cap, Array.get(Maybe<&2, A>, arr, 0)) 284 285 def pop(~A: Data, ~cmp: A -> A -> Cmp, h: Heap) -> Heap & Result<&2, &2, E.Error, A>: 286 BH{size, +n, depth, cap, arr} = h 287 pop_go(~A, ~cmp, size, n, depth, cap, arr, U32.is_eq(n, 0)) 288 289 # ---- from_list ---- 290 291 def from_list_go(~A: Data, ~cmp: A -> A -> Cmp, xs: List<&2, A>, h: Heap) -> Heap: 292 match xs: 293 case Nil{}: 294 h 295 case Con{x, rest}: 296 from_list_go(~A, ~cmp, rest, push(~A, ~cmp, h, x)) 297 298 def from_list(~A: Data, ~cmp: A -> A -> Cmp, xs: List<&2, A>) -> Heap: 299 from_list_go(~A, ~cmp, xs, new(~A)) 300 301 # ---- to_sorted_list ---- 302 303 # Repeated root removal on a COPY of the block: the heap itself is unchanged. 304 # The loop carries its state for the same reason the sift loops do. 305 # DrDone the copy is exhausted 306 # DrLast the root was the last element 307 # DrMore the root is out, `m` elements remain and `last` has to sift down 308 309 type Drain<-A: Data> is Type: 310 DrDone{arr: Array>} 311 DrLast{arr: Array>, root: A} 312 DrMore{arr: Array>, root: A, m: U32, last: A} 313 314 # Dropping the (linear) block is O(1): the runtime erases it. 315 def burn(~A: Data, arr: Array>) -> List<&2, A>: 316 Nil{} 317 318 def burn_cons(~A: Data, root: A, arr: Array>) -> List<&2, A>: 319 Con{root, Nil{}} 320 321 def drain_mb(~A: Data, arr: Array>, root: A, +m: U32, ml: Maybe<&2, A>, empty: Bool) -> Drain: 322 match ml empty: 323 case None{} _: 324 DrLast{arr, root} 325 case Some{last} True{}: 326 DrLast{arr, root} 327 case Some{last} False{}: 328 DrMore{arr, root, m, last} 329 330 def drain_last(~A: Data, root: A, +m: U32, empty: Bool, rl: Array> & Maybe<&2, A>) -> Drain: 331 (arr, ml) = rl 332 drain_mb(~A, arr, root, m, ml, empty) 333 334 def drain_root(~A: Data, arr: Array>, +m: U32, mr: Maybe<&2, A>) -> Drain: 335 match mr: 336 case None{}: 337 DrDone{arr} 338 case Some{root}: 339 drain_last(~A, root, m, U32.is_eq(m, 0), Array.get(Maybe<&2, A>, arr, m)) 340 341 def drain_take(~A: Data, +m: U32, r: Array> & Maybe<&2, A>) -> Drain: 342 (arr, mr) = r 343 drain_root(~A, arr, m, mr) 344 345 # Take the root out of a copy holding `n` elements. Emptiness is decided by 346 # the count, not by reading slot 0: the drain must stop at `n = 0` whatever 347 # the slots above the heap hold (and it saves one array read per element). 348 def drain_take_go(~A: Data, +n: U32, arr: Array>, empty: Bool) -> Drain: 349 match empty: 350 case True{}: 351 DrDone{arr} 352 case False{}: 353 drain_take(~A, U32.sub(n, 1), Array.get(Maybe<&2, A>, arr, 0)) 354 355 def drain_probe(~A: Data, +n: U32, arr: Array>) -> Drain: 356 drain_take_go(~A, n, arr, U32.is_eq(n, 0)) 357 358 def drain_go(~A: Data, ~cmp: A -> A -> Cmp, fuel: Nat, +depth: Nat, st: Drain) -> List<&2, A>: 359 match fuel st: 360 case _ DrDone{arr}: 361 burn(~A, arr) 362 case _ DrLast{arr, root}: 363 burn_cons(~A, root, arr) 364 case 0n DrMore{arr, root, m, last}: 365 burn_cons(~A, root, arr) 366 case 1n+f DrMore{arr, root, +m, last}: 367 Con{root, drain_go(~A, ~cmp, f, depth, drain_probe(~A, m, sift_down(~A, ~cmp, depth, m, 0, last, arr)))} 368 369 def sorted_of(~A: Data, ~cmp: A -> A -> Cmp, +size: Nat, +n: U32, +depth: Nat, cap: U32, c: Array> & Array>) -> Heap & List<&2, A>: 370 (arr, copy) = c 371 (BH{size, n, depth, cap, arr}, drain_go(~A, ~cmp, size, depth, drain_probe(~A, n, copy))) 372 373 def to_sorted_list(~A: Data, ~cmp: A -> A -> Cmp, h: Heap) -> Heap & List<&2, A>: 374 BH{+size, +n, +depth, +cap, arr} = h 375 sorted_of(~A, ~cmp, size, n, depth, cap, Array.clone(Maybe<&2, A>, arr)) 376 377 # ---- operation traces ---- 378 379 def obs_nat(~A: Data, r: Heap & Nat) -> Heap & E.Obs: 380 (h, n) = r 381 (h, E.ONat{n}) 382 383 def obs_item(~A: Data, r: Heap & Result<&2, &2, E.Error, A>) -> Heap & E.Obs: 384 (h, x) = r 385 (h, E.OItem{x}) 386 387 def obs_list(~A: Data, r: Heap & List<&2, A>) -> Heap & E.Obs: 388 (h, xs) = r 389 (h, E.OList{xs}) 390 391 def drop_heap(~A: Data, h: Heap, v: Heap & E.Obs) -> Heap & E.Obs: 392 v 393 394 # FromList replaces the heap: the old block is dropped (O(1) erasure). 395 def replace(~A: Data, ~cmp: A -> A -> Cmp, h: Heap, xs: List<&2, A>) -> Heap & E.Obs: 396 BH{size, n, depth, cap, arr} = h 397 (from_list(~A, ~cmp, xs), E.OUnit{}) 398 399 def step(~A: Data, ~cmp: A -> A -> Cmp, h: Heap, op: E.Op) -> Heap & E.Obs: 400 match op: 401 case E.Length{}: 402 obs_nat(~A, length(~A, h)) 403 case E.Push{x}: 404 (push(~A, ~cmp, h, x), E.OUnit{}) 405 case E.Peek{}: 406 obs_item(~A, peek(~A, h)) 407 case E.Pop{}: 408 obs_item(~A, pop(~A, ~cmp, h)) 409 case E.FromList{xs}: 410 replace(~A, ~cmp, h, xs) 411 case E.ToSortedList{}: 412 obs_list(~A, to_sorted_list(~A, ~cmp, h)) 413 414 def record(~A: Data, acc: List<&2, E.Obs>, r: Heap & E.Obs) -> Heap & List<&2, E.Obs>: 415 (h, o) = r 416 (h, Con{o, acc}) 417 418 def step_acc(~A: Data, ~cmp: A -> A -> Cmp, op: E.Op, st: Heap & List<&2, E.Obs>) -> Heap & List<&2, E.Obs>: 419 (h, acc) = st 420 record(~A, acc, step(~A, ~cmp, h, op)) 421 422 def run_acc(~A: Data, ~cmp: A -> A -> Cmp, ops: List<&2, E.Op>, st: Heap & List<&2, E.Obs>) -> Heap & List<&2, E.Obs>: 423 match ops: 424 case Nil{}: 425 st 426 case Con{op, rest}: 427 run_acc(~A, ~cmp, rest, step_acc(~A, ~cmp, op, st)) 428 429 def finish(~A: Data, st: Heap & List<&2, E.Obs>) -> Heap & List<&2, E.Obs>: 430 (h, acc) = st 431 (h, List.reverse(&2, E.Obs, acc)) 432 433 def run(~A: Data, ~cmp: A -> A -> Cmp, ops: List<&2, E.Op>, h: Heap) -> Heap & List<&2, E.Obs>: 434 finish(~A, run_acc(~A, ~cmp, ops, (h, Nil{}))) 435 436 # ---- checked instances (proofs/binary_heap.bend) ---- 437 438 def run_u32(ops: List<&2, E.Op>, h: Heap) -> Heap & List<&2, E.Obs>: 439 run(~U32, ~U32.cmp, ops, h) 440 441 def run_string(ops: List<&2, E.Op>, h: Heap) -> Heap & List<&2, E.Obs>: 442 run(~String, ~String.order, ops, h)