Chacha20poly1305.pad16: def of bend-collections@1.0.0.0
Import: import bend-collections@1.0.0.0/spec/crypto/chacha20poly1305.bend as Chacha20poly1305
Lines 18-21 of bend-collections@1.0.0.0/spec/crypto/chacha20poly1305.bend: https://jend.leeeet.dev/read.txt?path=bend-collections@1.0.0.0/spec/crypto/chacha20poly1305.bend&start_line=18&end_line=21

import Base

# pad16(x): zero bytes up to a multiple of 16, i.e. (16 - len(x) % 16) % 16
# of them ("if (len(x) % 16) == 0 then NULL else copies(0, 16 - len % 16)").
def pad16(+xs: List<&2, U32>) -> List<&2, U32>:
  List.replicate(U32, Nat.mod(Nat.sub(16n, Nat.mod(List.length(&2, U32, xs), 16n)), 16n), 0)

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.length
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.replicate
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mod
  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