Loop.run_tree: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/loop.bend as Loop
Lines 58-62 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/loop.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/loop.bend&start_line=58&end_line=62

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

# A nonempty list of outputs: the stack run is the tree of height |list|.
def run_tree(+x: T.Out, +r: List<&2,T.Out>) -> {run(K.StkNil{},Con{x,r}) == S.tree(SC.length(T.Out,Con{x,r}),Con{x,r}) : T.Out}:
  Equal.trans(T.Out,run2(r,K.StkNil{},x),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}),
    run2_split(r,K.StkNil{},x),
    run_tree_go(x,r))

Uses (16):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/loop.bend&name=init2
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/loop.bend&name=last2
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/loop.bend&name=run
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/loop.bend&name=run2
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/loop.bend&name=run2_split
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/loop.bend&name=run_tree_go
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/tree.bend&name=cvs
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/tree.bend&name=push_all
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/blake/blake3.bend&name=tree
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend&name=length
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake3/blake3.bend&name=Stack
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake3/blake3.bend&name=finish
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake3/types.bend&name=Out