~/jendhub

def run_tree

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/blake/blake3/loop.bend:58

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

58# A nonempty list of outputs: the stack run is the tree of height |list|.
59def 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}:
60  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}),
61    run2_split(r,K.StkNil{},x),
62    run_tree_go(x,r))

Uses (16)

Used by (1)