def get

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

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32.bend as U
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as SC

300# Public Base entry points. Premises: the tree is perfect of depth d < 32 and
301# the index is below 2^d; x is the value currently stored at that index.
302def get(-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>}, +pf: {perfect(T, d, t) == True{} : Bool}) -> {Array.get(T, thaw(T, t), i) == (thaw(T, t), x) : Array<T> & T}:
303  %Equal.sym(Array<T> & U32, Array.size(T, thaw(T, t)), (thaw(T, t), U.pow2u(d)), size_thaw(T, d, t, pf)) : {Array.get.at(T, i, _) == (thaw(T, t), x) : Array<T> & T}
304  %Equal.sym(U32, U32.and(i, U32.sub(U.pow2u(d), 1)), i, U.mask_pow2u(i, d, hd, hi)) : {Array.get.go(T, thaw(T, t), U.pow2u(d), _, U32.is_lt(_, U32.shr(U.pow2u(d)))) == (thaw(T, t), x) : Array<T> & T}
305  get_go(T, d, t, i, x, hd, hi, hx, U32.is_lt(i, U32.shr(U.pow2u(d))), {==}, pf)