law block_octets_round_trip

bend-osdev-cipher-modes@0.1.0.0 · LAWS.bend:97

import bend-osdev-cipher-modes@0.1.0.0/LAWS.bend as LAWS
import Base
import bend-osdev-cipher-modes@0.1.0.0/cipher_modes.bend as M

97# A block written as Octets reads back as the same block, for every block
98law block_octets_round_trip:
99  for +b: M.CmBlock
100  {M.CmBlock.of_octets(M.CmBlock.to_octets(b)) == Some{b} : Maybe<&2, M.CmBlock>}

Uses (19)

Used by (0)

No other definition uses this definition.