def padding_bytes

bend-collections-laws-crypto@1.0.0.0 · spec/crypto/sha3.bend:21

import Base

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