def run_tree_go
bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/blake/blake3/loop.bend:53
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/loop.bend as Loop
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/tree.bend as TR
53def run_tree_go(+x: T.Out, +r: List<&2,T.Out>) -> {K.finish(TR.push_all(K.StkNil{},TR.cvs(init2(r,x))),last2(r,x)) == S.tree(1n+SC.length(T.Out,r),Con{x,r}) : T.Out}:
54 %snoc2(r,x) : {K.finish(TR.push_all(K.StkNil{},TR.cvs(init2(r,x))),last2(r,x)) == S.tree(1n+SC.length(T.Out,r),_) : T.Out}
55 %len_init2(r,x) : {K.finish(TR.push_all(K.StkNil{},TR.cvs(init2(r,x))),last2(r,x)) == S.tree(1n+_,SC.append(T.Out,init2(r,x),Con{last2(r,x),Nil{}})) : T.Out}
56 TR.tree_stack(init2(r,x),last2(r,x))