Argon2.hp_go: def of bend-collections@1.0.0.0
Import: import bend-collections@1.0.0.0/src/crypto/argon2/argon2.bend as Argon2
Lines 27-38 of bend-collections@1.0.0.0/src/crypto/argon2/argon2.bend: https://jend.leeeet.dev/read.txt?path=bend-collections@1.0.0.0/src/crypto/argon2/argon2.bend&start_line=27&end_line=38

import Base
import bend-collections@1.0.0.0/src/crypto/blake/blake2b/sized.bend as H

# H' for T > 64 (RFC 9106 section 3.3): W1 || .. || Wr || V_{r+1}, where
# Wi is the first 32 bytes of Vi, V_{i+1} = H^64(Vi) and V_{r+1} = H^{T-32r}(Vr).
# (V_i is a 64-byte digest, never empty; it is inspected first so that proofs
# keep the chain of hashes folded.)
def hp_go(n: Nat, v: List<&2, U32>, +last: Nat) -> List<&2, U32>:
  match n v:
    case _ Nil{}:
      Nil{}
    case 0n +x <> +r:
      cat(List.take(&2, U32, x <> r, 32n), H.hash(last, x <> r))
    case 1n+p +x <> +r:
      cat(List.take(&2, U32, x <> r, 32n), hp_go(p, H.hash(64n, x <> r), last))

Uses (6):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  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=U32
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/src/crypto/argon2/argon2.bend&name=cat
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/src/crypto/blake/blake2b/sized.bend&name=hash