def bq.go

bend-osdev-algo@0.1.0.0 · proof_bsearch.bend:105

import Base
import bend-osdev-algo@0.1.0.0/bsearch.bend as S
import bend-osdev-array@0.1.0.0/array.bend as A
import bend-osdev-array@0.1.0.0/LAWS.bend as AL

105def bq.go(f: Nat, +d: Nat, +l: List<&2, U32>, +hl: {List.length(&2, U32, l) == A.Arrays.slots(d) : Nat}, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +lo: U32, +hi: U32, +key: U32) -> {S.bsearch.array.go(f, S.BsearchState{bq.ol(d, l), lo, hi}, key) == (bq.ol(d, l), bq.run(f, d, l, lo, hi, key)) : Array<U32> & U32}:
106  match f:
107    case 0n:
108      {==}
109    case 1n+ +g:
110      -a0 = bq.ol(d, l)
111      +mid = bq.mid(lo, hi)
112      +x = bq.x(d, l, lo, hi)
113      %Equal.sym(Array<U32> & U32, Array.get(U32, a0, mid), (a0, x), AL.of_list_get(U32, d, l, 0, hl, hd, mid)) : {S.bsearch.array.go(g, S.bsearch.array.step(U32.is_lt(lo, hi), _, key, lo, hi, mid), key) == (a0, bq.run(1n+g, d, l, lo, hi, key)) : Array<U32> & U32}
114      %Equal.sym(S.BsearchState, S.bsearch.array.step(U32.is_lt(lo, hi), (a0, x), key, lo, hi, mid), S.BsearchState{a0, bq.nlo(d, l, lo, hi, key), bq.nhi(d, l, lo, hi, key)}, bq.step_eq(U32.is_lt(lo, hi), a0, x, key, lo, hi, mid)) : {S.bsearch.array.go(g, _, key) == (a0, bq.run(1n+g, d, l, lo, hi, key)) : Array<U32> & U32}
115      bq.go(g, d, l, hl, hd, bq.nlo(d, l, lo, hi, key), bq.nhi(d, l, lo, hi, key), key)