def get_go

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/array.bend:234

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32.bend as U
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/list.bend as LL
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as SC

234# Base 2.0.32 passes each descent step its branch decision z; eb names it as
235# U32.is_lt(i, U32.shr(2^d)), the value Base computes, so callers pass {==}.
236def get_go(-T: Data, +d: Nat, +t: Tree<T>, +i: U32, +x: T, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +hi: {Nat.is_lt(U32.to_nat(i), SC.pow2(d)) == True{} : Bool}, +hx: {SC.nth(T, slots(T, t), U32.to_nat(i)) == Some{x} : Maybe<&2, T>}, +b: Bool, +eb: {U32.is_lt(i, U32.shr(U.pow2u(d))) == b : Bool}, +pf: {perfect(T, d, t) == True{} : Bool}) -> {Array.get.go(T, thaw(T, t), U.pow2u(d), i, b) == (thaw(T, t), x) : Array<T> & T}:
237  match d t b:
238    case 0n TLeaf{+y} _:
239      %leaf_value(T, y, U32.to_nat(i), x, hi, hx) : {(ALeaf{y}, y) == (ALeaf{y}, _) : Array<T> & T}
240      {==}
241    case 0n TNode{l, r} _:
242      Empty.absurd({Array.get.go(T, thaw(T, TNode{l, r}), 1, i, b) == (thaw(T, TNode{l, r}), x) : Array<T> & T}, L.false_true(pf))
243    case 1n+p TLeaf{y} _:
244      Empty.absurd({Array.get.go(T, ALeaf{y}, U.pow2u(1n+p), i, b) == (ALeaf{y}, x) : Array<T> & T}, L.false_true(pf))
245    case 1n+ +p TNode{+l, +r} True{}:
246      +hp = N.lt_trans(p, 1n+p, 32n, N.lt_succ(p), hd)
247      +pl = pf_left(T, p, l, r, pf)
248      +hil = lt_bridge(i, p, hp, True{}, L.subst(U32, w => {U32.is_lt(i, w) == True{} : Bool}, U32.shr(U.pow2u(1n+p)), U.pow2u(p), U.shr_pow2u(p, hd), eb))
249      %Equal.sym(U32, U32.shr(U.pow2u(1n+p)), U.pow2u(p), U.shr_pow2u(p, hd)) : {Array.swap.lo(T, thaw(T, r), Array.get.go(T, thaw(T, l), _, i, U32.is_lt(i, U32.shr(_)))) == (ANode{thaw(T, l), thaw(T, r)}, x) : Array<T> & T}
250      %Equal.sym(Array<T> & T, Array.get.go(T, thaw(T, l), U.pow2u(p), i, U32.is_lt(i, U32.shr(U.pow2u(p)))), (thaw(T, l), x), get_go(T, p, l, i, x, hp, hil, Equal.trans(Maybe<&2, T>, SC.nth(T, slots(T, l), U32.to_nat(i)), SC.nth(T, SC.append(T, slots(T, l), slots(T, r)), U32.to_nat(i)), Some{x}, Equal.sym(Maybe<&2, T>, SC.nth(T, SC.append(T, slots(T, l), slots(T, r)), U32.to_nat(i)), SC.nth(T, slots(T, l), U32.to_nat(i)), LL.nth_append_left(T, slots(T, l), slots(T, r), U32.to_nat(i), len_lt(T, p, l, U32.to_nat(i), pl, hil))), hx), U32.is_lt(i, U32.shr(U.pow2u(p))), {==}, pl)) : {Array.swap.lo(T, thaw(T, r), _) == (ANode{thaw(T, l), thaw(T, r)}, x) : Array<T> & T}
251      {==}
252    case 1n+ +p TNode{+l, +r} False{}:
253      +hp = N.lt_trans(p, 1n+p, 32n, N.lt_succ(p), hd)
254      +pl = pf_left(T, p, l, r, pf)
255      +le = N.not_lt_le(U32.to_nat(i), SC.pow2(p), lt_bridge(i, p, hp, False{}, L.subst(U32, w => {U32.is_lt(i, w) == False{} : Bool}, U32.shr(U.pow2u(1n+p)), U.pow2u(p), U.shr_pow2u(p, hd), eb)))
256      +j = U32.sub(i, U.pow2u(p))
257      +ej = sub_bridge(i, p, hp, le)
258      +hir = L.subst(Nat, n => {Nat.is_lt(n, SC.pow2(p)) == True{} : Bool}, Nat.sub(U32.to_nat(i), SC.pow2(p)), U32.to_nat(j), Equal.sym(Nat, U32.to_nat(j), Nat.sub(U32.to_nat(i), SC.pow2(p)), ej), upper_lt(U32.to_nat(i), p, hi, le))
259      +hxr = L.subst(Nat, n => {SC.nth(T, slots(T, r), n) == Some{x} : Maybe<&2, T>}, Nat.sub(U32.to_nat(i), SC.pow2(p)), U32.to_nat(j), Equal.sym(Nat, U32.to_nat(j), Nat.sub(U32.to_nat(i), SC.pow2(p)), ej), Equal.trans(Maybe<&2, T>, SC.nth(T, slots(T, r), Nat.sub(U32.to_nat(i), SC.pow2(p))), SC.nth(T, SC.append(T, slots(T, l), slots(T, r)), U32.to_nat(i)), Some{x}, Equal.sym(Maybe<&2, T>, SC.nth(T, SC.append(T, slots(T, l), slots(T, r)), U32.to_nat(i)), SC.nth(T, slots(T, r), Nat.sub(U32.to_nat(i), SC.pow2(p))), right_nth(T, p, l, r, U32.to_nat(i), pl, le)), hx))
260      %Equal.sym(U32, U32.shr(U.pow2u(1n+p)), U.pow2u(p), U.shr_pow2u(p, hd)) : {Array.swap.hi(T, thaw(T, l), Array.get.go(T, thaw(T, r), _, U32.sub(i, _), U32.is_lt(U32.sub(i, _), U32.shr(_)))) == (ANode{thaw(T, l), thaw(T, r)}, x) : Array<T> & T}
261      %Equal.sym(Array<T> & T, Array.get.go(T, thaw(T, r), U.pow2u(p), j, U32.is_lt(j, U32.shr(U.pow2u(p)))), (thaw(T, r), x), get_go(T, p, r, j, x, hp, hir, hxr, U32.is_lt(j, U32.shr(U.pow2u(p))), {==}, pf_right(T, p, l, r, pf))) : {Array.swap.hi(T, thaw(T, l), _) == (ANode{thaw(T, l), thaw(T, r)}, x) : Array<T> & T}
262      {==}