def tree_stack

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/blake/blake3/tree.bend:305

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake3/types.bend as T
import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake3/blake3.bend as K
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as SC
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/blake/blake3.bend as S
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/lists.bend as LS

305# The whole message: the stack starts empty and the height is the chunk count.
306def tree_stack(+fs: List<&2,T.Out>, +o: T.Out) -> {K.finish(push_all(K.StkNil{},cvs(fs)),o) == S.tree(1n+SC.length(T.Out,fs),SC.append(T.Out,fs,Con{o,Nil{}})) : T.Out}:
307  partial(1n+SC.length(T.Out,fs),fs,o,K.StkNil{},LS.lt_pow2_succ(SC.length(T.Out,fs)))