law pkcs7_pad_empty

bend-osdev-pkcs7@0.1.0.0 · LAWS.bend:25

import Base
import bend-osdev-bytes@0.1.1.0/bytes.bend as B
import bend-osdev-mode-core@0.1.0.0/mode_core.bend as M
import bend-osdev-pkcs7@0.1.0.0/pkcs7.bend as P

25# PKCS #7 (RFC 5652, 6.3): the empty message becomes a whole block of 16s; 15 bytes gain one 1
26law pkcs7_pad_empty:
27  {P.Pkcs7.pad(16n, B.Octets.empty()) == Done{B.Octets.of_list([16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16])} : Result<&2, &2, M.CmError, B.Octets>}