Memory.tree_slots: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/memory.bend as Memory
Lines 116-130 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/memory.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/memory.bend&start_line=116&end_line=130

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/list.bend as LL
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L

# The words of tree(d, ws) are ws, for 2^d words.
def tree_slots(+d: Nat, +ws: List<&2, U32>, +h: {SC.length(U32, ws) == SC.pow2(d) : Nat}) -> {AR.slots(U32, tree(d, ws)) == ws : List<&2, U32>}:
  match d:
    case 0n:
      leaf_slots(ws, h)
    case 1n+ +p:
      +k = SC.pow2(p)
      +ht = LL.sc_length_take(U32, ws, k, L.subst(Nat, z => {Nat.is_le(k, z) == True{} : Bool}, SC.pow2(1n+p), SC.length(U32, ws), Equal.sym(Nat, SC.length(U32, ws), SC.pow2(1n+p), h), pow2_le_succ(p)))
      +hd = Equal.trans(Nat, SC.length(U32, SC.drop(U32, ws, k)), Nat.sub(SC.length(U32, ws), k), k, length_drop(ws, k),
        Equal.trans(Nat, Nat.sub(SC.length(U32, ws), k), Nat.sub(Nat.double(k), k), k, Equal.cong(Nat, Nat, z => Nat.sub(z, k), SC.length(U32, ws), Nat.double(k), h), double_sub(k)))
      Equal.trans(List<&2, U32>, SC.append(U32, AR.slots(U32, tree(p, SC.take(U32, ws, k))), AR.slots(U32, tree(p, SC.drop(U32, ws, k)))), SC.append(U32, SC.take(U32, ws, k), SC.drop(U32, ws, k)), ws,
        Equal.trans(List<&2, U32>, SC.append(U32, AR.slots(U32, tree(p, SC.take(U32, ws, k))), AR.slots(U32, tree(p, SC.drop(U32, ws, k)))), SC.append(U32, SC.take(U32, ws, k), AR.slots(U32, tree(p, SC.drop(U32, ws, k)))), SC.append(U32, SC.take(U32, ws, k), SC.drop(U32, ws, k)),
          Equal.cong(List<&2, U32>, List<&2, U32>, z => SC.append(U32, z, AR.slots(U32, tree(p, SC.drop(U32, ws, k)))), AR.slots(U32, tree(p, SC.take(U32, ws, k))), SC.take(U32, ws, k), tree_slots(p, SC.take(U32, ws, k), ht)),
          Equal.cong(List<&2, U32>, List<&2, U32>, z => SC.append(U32, SC.take(U32, ws, k), z), AR.slots(U32, tree(p, SC.drop(U32, ws, k))), SC.drop(U32, ws, k), tree_slots(p, SC.drop(U32, ws, k), hd))),
        take_drop(ws, k))

Uses (24):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.double
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_le
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.sub
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/memory.bend&name=double_sub
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/memory.bend&name=leaf_slots
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/memory.bend&name=length_drop
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/memory.bend&name=pow2_le_succ
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/memory.bend&name=take_drop
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/memory.bend&name=tree
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/array.bend&name=slots
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/list.bend&name=sc_length_take
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend&name=subst
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend&name=append
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend&name=drop
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend&name=length
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend&name=pow2
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend&name=take