def fao.go

lawful-bytes@0.1.1.0 · proof_fast_append.bend:1419

import Base
import lawful-bytes@0.1.1.0/defs.bend as D
import lawful-bytes@0.1.1.0/fast.bend as FA
import lawful-bytes@0.1.1.0/proof_core.bend as C
import lawful-arrays@0.1.0.0/proof_base.bend as AB
import lawful-arrays@0.1.0.0/proof_tree.bend as P

1419def fao.go(+ld: U32, +td: P.Tree<U32>, +ls: U32, +ts: P.Tree<U32>, +d: Nat, +s: U32, +n: U32,
1420  +hd: {D.ok(C.BT(ld, td), d) == True{} : Bool},
1421  +hc: {Nat.is_le(Nat.add(D.size(C.BT(ld, td)), U32.to_nat(n)), D.cap(C.BT(ld, td))) == True{} : Bool},
1422  m: C.BMirror(D1(ld, td, ls, ts, s, n))) ->
1423  {D.ok(Pair.fst(D.Bytes, D.Bytes, FA.append(C.BT(ld, td), C.BT(ls, ts), s, n)), d) == True{} : Bool}:
1424  (+l1, m2) = m
1425  (+t1, +e1) = m2
1426  +q = QQ(ld, s, n)
1427  +hk1 = ok1(ld, td, ls, ts, d, s, n, l1, t1, e1, hd, hc)
1428  +el = el1(ld, td, ls, ts, d, s, n, l1, t1, e1, hd, hc)
1429  +hdd = C.ok_d(ld, td, d, hd)
1430  +hl0 = hlen0(ld, td, l1, d, n, el, hd, hc)
1431  %Equal.sym(D.Bytes & D.Bytes, FA.append(C.BT(ld, td), C.BT(ls, ts), s, n), (C.BT(U32.add(l1, NPw(ld, n)), TF(ld, ts, s, n, l1, t1)), C.BT(ls, ts)),
1432    fa_eq(ld, td, ls, ts, s, n, l1, t1, e1)) :
1433    {D.ok(Pair.fst(D.Bytes, D.Bytes, _), d) == True{} : Bool}
1434  C.ok_mk(U32.add(l1, NPw(ld, n)), TF(ld, ts, s, n, l1, t1), d,
1435    aw_full(NW(ld, n), ts, U32.add(U32.shrn(q, 2n), 1), C.WD(ts, U32.shrn(q, 2n)), t1, U32.shrn(q, 2n), U32.shrn(l1, 2n), SH(q), d, C.ok_full(l1, t1, d, hk1)),
1436    hdd,
1437    AB.subst(Nat, y => {Nat.is_le(y, Nat.mul(4n, Nat.pow(2n, d))) == True{} : Bool}, Nat.add(U32.to_nat(l1), U32.to_nat(NPw(ld, n))), U32.to_nat(U32.add(l1, NPw(ld, n))),
1438      Equal.sym(Nat, U32.to_nat(U32.add(l1, NPw(ld, n))), Nat.add(U32.to_nat(l1), U32.to_nat(NPw(ld, n))), C.add_fits(l1, NPw(ld, n), d, hdd, hl0)), hl0))