Run.init_len: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/run.bend as Run
Lines 34-45 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/run.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/run.bend&start_line=34&end_line=45

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/list.bend as LL
import bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/types.bend as A
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/argon2/argon2.bend as SA

def init_len(+n: Nat, +l: Nat, +q: Nat, +hh: List<&2, U32>, +mem: List<&2, A.Block>) -> {SC.length(A.Block, SA.init_go(n, l, q, hh, mem)) == SC.length(A.Block, mem) : Nat}:
  match n:
    case 0n:
      {==}
    case 1n+ +rest:
      +b0 = SA.block_of(SA.hprime(1024n, SA.cat(hh, SA.cat(SA.le32(0n), SA.le32(l)))))
      +b1 = SA.block_of(SA.hprime(1024n, SA.cat(hh, SA.cat(SA.le32(1n), SA.le32(l)))))
      +m1 = SA.set(mem, Nat.mul(l, q), b0)
      +m2 = SA.set(m1, Nat.add(Nat.mul(l, q), 1n), b1)
      Equal.trans(Nat, SC.length(A.Block, SA.init_go(rest, Nat.add(l, 1n), q, hh, m2)), SC.length(A.Block, m2), SC.length(A.Block, mem),
        init_len(rest, Nat.add(l, 1n), q, hh, m2),
        Equal.trans(Nat, SC.length(A.Block, m2), SC.length(A.Block, m1), SC.length(A.Block, mem), LL.length_update(A.Block, m1, Nat.add(Nat.mul(l, q), 1n), b1), LL.length_update(A.Block, mem, Nat.mul(l, q), b0)))

Uses (15):
  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.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul
  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/lib/list.bend&name=length_update
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/argon2/argon2.bend&name=block_of
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/argon2/argon2.bend&name=cat
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/argon2/argon2.bend&name=hprime
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/argon2/argon2.bend&name=init_go
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/argon2/argon2.bend&name=le32
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/argon2/argon2.bend&name=set
  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/src/crypto/argon2/types.bend&name=Block