law modes64_not_whole_blocks

bend-osdev-legacy-ciphers@0.1.0.0 · LAWS.bend:359

import Base
import bend-osdev-bytes@0.1.0.0/bytes.bend as B
import bend-osdev-legacy-ciphers@0.1.0.0/legacy_ciphers.bend as L
import bend-osdev-legacy-ciphers@0.1.0.0/modes64.bend as X

359# the 64-bit modes refuse a message that is not whole blocks
360law modes64_not_whole_blocks:
361  {Result.map(&2, &2, L.LcError, List<&2, L.LcBlock64>, Unit, bs => Unit{}, X.Lc64.blocks_of(B.Octets.zeros(12n))) == Fail{L.LcNotBlockMultiple{12n}} : Result<&2, &2, L.LcError, Unit>}