~/jendhub

def push_split

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

import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/tree.bend as Tree
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

130# Pushing the chaining values of xs ++ ys.
131def push_split(+s: K.Stack, +xs: List<&2,T.Out>, +ys: List<&2,T.Out>) -> {push_all(s,cvs(SC.append(T.Out,xs,ys))) == push_all(push_all(s,cvs(xs)),cvs(ys)) : K.Stack}:
132  %Equal.sym(List<&2,T.CV>,cvs(SC.append(T.Out,xs,ys)),SC.append(T.CV,cvs(xs),cvs(ys)),cvs_append(xs,ys)) : {push_all(s,_) == push_all(push_all(s,cvs(xs)),cvs(ys)) : K.Stack}
133  push_all_append(s,cvs(xs),cvs(ys))

Uses (10)

Used by (2)