def complete

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

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

220# A stack with g empty low slots absorbs the chaining values of 2^g outputs
221# as one complete subtree pushed at slot g.
222def complete(+g: Nat, +xs: List<&2,T.Out>, +t: K.Stack, +hl: {SC.length(T.Out,xs) == SC.pow2(g) : Nat}) -> {push_all(E(g,t),cvs(xs)) == E(g,K.push(t,S.cv(S.tree(g,xs)))) : K.Stack}:
223  match g:
224    case 0n: complete_zero(xs,t,hl)
225    case 1n+p:
226      complete_step(p,xs,t,pow_ne(xs,1n+p,hl),half_not_nil(xs,p,hl),
227        complete(p,SC.take(T.Out,xs,SC.pow2(p)),lift(t),half_len_take(xs,p,hl)),
228        complete(p,SC.drop(T.Out,xs,SC.pow2(p)),K.SFull{S.cv(S.tree(p,SC.take(T.Out,xs,SC.pow2(p)))),t},half_len_drop(xs,p,hl)))