def tree_perfect
bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/argon2/memory.bend:93
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/memory.bend as Memory
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
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
93def tree_perfect(+d: Nat, +ws: List<&2, U32>) -> {AR.perfect(U32, d, tree(d, ws)) == True{} : Bool}:
94 match d:
95 case 0n:
96 {==}
97 case 1n+ +p:
98 L.and_intro(AR.perfect(U32, p, tree(p, SC.take(U32, ws, SC.pow2(p)))), AR.perfect(U32, p, tree(p, SC.drop(U32, ws, SC.pow2(p)))), tree_perfect(p, SC.take(U32, ws, SC.pow2(p))), tree_perfect(p, SC.drop(U32, ws, SC.pow2(p))))