def partial

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

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

296# Fewer than 2^g chaining values pushed on a stack with g empty low slots,
297# then folded into the pending output o: the specification's tree of height
298# g over the outputs and o, folded into the rest of the stack.
299def partial(+g: Nat, +fs: List<&2,T.Out>, +o: T.Out, +t: K.Stack, +hl: {Nat.is_lt(SC.length(T.Out,fs),SC.pow2(g)) == True{} : Bool}) -> {K.finish(push_all(E(g,t),cvs(fs)),o) == K.finish(t,S.tree(g,SC.append(T.Out,fs,Con{o,Nil{}}))) : T.Out}:
300  match g:
301    case 0n: partial_zero(fs,o,t,hl)
302    case 1n+p:
303      partial_split(p,fs,o,t,hl,Nat.is_lt(SC.length(T.Out,fs),SC.pow2(p)),{==},f2 => t2 => h2 => partial(p,f2,o,t2,h2))