def tree

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/argon2/memory.bend:85

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as SC
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/array.bend as AR

85# The perfect tree of depth d holding ws (padded by zeros, truncated at 2^d).
86def tree(d: Nat, +ws: List<&2, U32>) -> AR.Tree<U32>:
87  match d:
88    case 0n:
89      AR.TLeaf{nthv(ws, 0n)}
90    case 1n+ +p:
91      AR.TNode{tree(p, SC.take(U32, ws, SC.pow2(p))), tree(p, SC.drop(U32, ws, SC.pow2(p)))}