Password.hp_go_len: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/password.bend as Password
Lines 58-73 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/password.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/password.bend&start_line=58&end_line=73

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2b/sized.bend as H
import bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/argon2.bend as A2

# W1 || .. : 32 bytes per chained digest, then the last digest.
def hp_go_len(+n: Nat, +v: List<&2, U32>, +last: Nat, +hv: {len(v) == 64n : Nat}, +hl: {Nat.is_le(last, 64n) == True{} : Bool}) -> {len(A2.hp_go(n, v, last)) == Nat.add(Nat.mul(1n+n, 32n), last) : Nat}:
  match n v:
    case _ Nil{}:
      Empty.absurd({len(Nil{}) == Nat.add(Nat.mul(1n+n, 32n), last) : Nat}, N.zero_succ(63n, hv))
    case 0n +x <> +r:
      %Equal.sym(Nat, len(List.append(&2, U32, List.take(&2, U32, x <> r, 32n), H.hash(last, x <> r))), Nat.add(len(List.take(&2, U32, x <> r, 32n)), len(H.hash(last, x <> r))), len_append(List.take(&2, U32, x <> r, 32n), H.hash(last, x <> r))) : {_ == Nat.add(32n, last) : Nat}
      %Equal.sym(Nat, len(List.take(&2, U32, x <> r, 32n)), 32n, len_take(x <> r, 32n, L.subst(Nat, z => {Nat.is_le(32n, z) == True{} : Bool}, 64n, len(x <> r), Equal.sym(Nat, len(x <> r), 64n, hv), {==}))) : {Nat.add(_, len(H.hash(last, x <> r))) == Nat.add(32n, last) : Nat}
      %Equal.sym(Nat, len(H.hash(last, x <> r)), last, hash_len(last, x <> r, hl)) : {Nat.add(32n, _) == Nat.add(32n, last) : Nat}
      {==}
    case 1n+ +p +x <> +r:
      +w = H.hash(64n, x <> r)
      %Equal.sym(Nat, len(List.append(&2, U32, List.take(&2, U32, x <> r, 32n), A2.hp_go(p, w, last))), Nat.add(len(List.take(&2, U32, x <> r, 32n)), len(A2.hp_go(p, w, last))), len_append(List.take(&2, U32, x <> r, 32n), A2.hp_go(p, w, last))) : {_ == Nat.add(Nat.mul(2n+p, 32n), last) : Nat}
      %Equal.sym(Nat, len(List.take(&2, U32, x <> r, 32n)), 32n, len_take(x <> r, 32n, L.subst(Nat, z => {Nat.is_le(32n, z) == True{} : Bool}, 64n, len(x <> r), Equal.sym(Nat, len(x <> r), 64n, hv), {==}))) : {Nat.add(_, len(A2.hp_go(p, w, last))) == Nat.add(Nat.mul(2n+p, 32n), last) : Nat}
      %Equal.sym(Nat, len(A2.hp_go(p, w, last)), Nat.add(Nat.mul(1n+p, 32n), last), hp_go_len(p, w, last, hash_len(64n, x <> r, {==}), hl)) : {Nat.add(32n, _) == Nat.add(Nat.mul(2n+p, 32n), last) : Nat}
      Equal.sym(Nat, Nat.add(Nat.add(32n, Nat.mul(1n+p, 32n)), last), Nat.add(32n, Nat.add(Nat.mul(1n+p, 32n), last)), NA.add_assoc(32n, Nat.mul(1n+p, 32n), last))

Uses (20):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.append
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.take
  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.is_le
  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/crypto/argon2/password.bend&name=hash_len
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/password.bend&name=len
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/password.bend&name=len_append
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/password.bend&name=len_take
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=add_assoc
  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/proofs/lib/nat.bend&name=zero_succ
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/argon2.bend&name=hp_go
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2b/sized.bend&name=hash