Sha3.padding_bytes: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/spec/crypto/sha3.bend as Sha3
Lines 21-32 of bend-collections-laws-crypto@1.0.0.0/spec/crypto/sha3.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/sha3.bend&start_line=21&end_line=32

import Base

# M || 01 || pad10*1(r, |M| + 2) at the byte level, for q = 1..136 bytes to
# the end of the block: the suffix bits 0, 1 and the first pad bit 1 are the
# byte 0x06; the last pad bit is the top bit, 0x80, of the block's last byte;
# with one byte left both fall in it: 0x86.
def padding_bytes(q: Nat) -> List<&2, U32>:
  match q:
    case 0n:
      Nil{}
    case 1n:
      [U32.or(6, 128)]
    case 2n+k:
      6 <> List.append(&2, U32, List.replicate(U32, k, 0), [128])

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.append
  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
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.or