def ba.adv

bend-osdev-algo@0.1.0.0 · PROOF.bend:1326

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 AR
import bend-osdev-algo@0.1.0.0/proof_u32.bend as U
import bend-osdev-algo@0.1.0.0/proof_bsearch.bend as Q

1326# one halving of [lo, hi): active when lo < hi (c)
1327def ba.adv(c: Bool, +g: Nat, +d: Nat, +l: List<&2, U32>, +hl: {List.length(&2, U32, l) == AR.Arrays.slots(d) : Nat}, +key: U32, +n: U32, +hN: {Nat.is_le(U32.to_nat(n), AR.Arrays.slots(d)) == True{} : Bool}, +hs: {S.bsearch.sorted(Q.bq.pre(l, n)) == True{} : Bool}, +lo: U32, +hi: U32, +ec: {U32.is_lt(lo, hi) == c : Bool}, +i1: {Nat.is_le(U32.to_nat(lo), Q.bq.lb(l, n, key)) == True{} : Bool}, +i2: {Nat.is_le(Q.bq.lb(l, n, key), U32.to_nat(hi)) == True{} : Bool}, +i3: {Nat.is_le(U32.to_nat(hi), U32.to_nat(n)) == True{} : Bool}, +hz: {Nat.is_lt(Q.bq.s(lo, hi), U.uq.pw(1n+g)) == True{} : Bool}, ih: @lo2: U32 -> @hi2: U32 -> @j1: {Nat.is_le(U32.to_nat(lo2), Q.bq.lb(l, n, key)) == True{} : Bool} -> @j2: {Nat.is_le(Q.bq.lb(l, n, key), U32.to_nat(hi2)) == True{} : Bool} -> @j3: {Nat.is_le(U32.to_nat(hi2), U32.to_nat(n)) == True{} : Bool} -> @jz: {Nat.is_lt(Q.bq.s(lo2, hi2), U.uq.pw(g)) == True{} : Bool} -> {U32.to_nat(Q.bq.run(g, d, l, lo2, hi2, key)) == Q.bq.lb(l, n, key) : Nat}) -> {U32.to_nat(Q.bq.run(g, d, l, Q.bq.nlo.a(c, U32.is_lt(Q.bq.x(d, l, lo, hi), key), lo, Q.bq.mid(lo, hi)), Q.bq.nhi.a(c, U32.is_lt(Q.bq.x(d, l, lo, hi), key), hi, Q.bq.mid(lo, hi)), key)) == Q.bq.lb(l, n, key) : Nat}:
1328  match c:
1329    case False{}:
1330      +h0 = U32.to_nat(hi)
1331      +l0 = U32.to_nat(lo)
1332      +e0 = Q.bq.sub_le0(h0, l0, Q.bq.not_lt(l0, h0, u32.mv_lt(lo, hi, False{}, ec)))
1333      ih(lo, hi, i1, i2, i3, Q.bq.lt_rw(0n, U.uq.pw(g), Q.bq.s(lo, hi), U.uq.pw(g), Equal.sym(Nat, Q.bq.s(lo, hi), 0n, e0), {==}, Q.bq.pw_pos(g)))
1334    case True{}:
1335      +h0 = U32.to_nat(hi)
1336      +l0 = U32.to_nat(lo)
1337      +s = Q.bq.s(lo, hi)
1338      +m = Q.bq.m(lo, hi)
1339      +mid = Q.bq.mid(lo, hi)
1340      +lb = Q.bq.lb(l, n, key)
1341      +sh = U32.to_nat(U32.shr(U32.sub(hi, lo)))
1342      +hlt = u32.mv_lt(lo, hi, True{}, ec)
1343      +hle = Q.bq.lt_le(l0, h0, hlt)
1344      +eD = U.uq.u32_sub(hi, lo, hle)
1345      +eE = Equal.trans(Nat, sh, U.uq.half(U32.to_nat(U32.sub(hi, lo))), U.uq.half(s), U.uq.u32_shr(U32.sub(hi, lo)), Equal.cong(Nat, Nat, z => U.uq.half(z), U32.to_nat(U32.sub(hi, lo)), s, eD))
1346      +ehs = Q.bq.add_sub(l0, h0, hle)
1347      +hmh = Q.bq.lt_rw(Nat.add(l0, U.uq.half(s)), Nat.add(l0, s), m, h0, {==}, ehs, Equal.trans(Bool, Nat.is_lt(Nat.add(l0, U.uq.half(s)), Nat.add(l0, s)), Nat.is_lt(U.uq.half(s), s), True{}, Q.bq.lt_cancel(l0, U.uq.half(s), s), Q.bq.half_lt(s, Q.bq.sub_pos(l0, h0, hlt))))
1348      +hadd = Q.bq.le_rw(m, h0, Nat.add(l0, sh), h0, Equal.cong(Nat, Nat, z => Nat.add(l0, z), U.uq.half(s), sh, Equal.sym(Nat, sh, U.uq.half(s), eE)), {==}, Q.bq.lt_le(m, h0, hmh))
1349      +eM = Equal.trans(Nat, U32.to_nat(mid), Nat.add(l0, sh), m, U.uq.u32_add(lo, U32.shr(U32.sub(hi, lo)), hi, hadd), Equal.cong(Nat, Nat, z => Nat.add(l0, z), sh, U.uq.half(s), eE))
1350      +hmN = Q.bq.lt_le_trans(m, h0, U32.to_nat(n), hmh, i3)
1351      %Equal.sym(Bool, U32.is_lt(Q.bq.x(d, l, lo, hi), key), Nat.is_lt(m, lb), ba.key_cmp(d, l, hl, key, n, hN, hs, mid, m, eM, hmN)) : {U32.to_nat(Q.bq.run(g, d, l, Q.bq.lo_b(_, lo, mid), Q.bq.hi_b(_, hi, mid), key)) == lb : Nat}
1352      ba.adv2(Nat.is_lt(m, lb), g, d, l, key, n, lo, hi, {==}, i1, i2, i3, hz, eM, ehs, hmh, ih)