law block64_octets_round_trip

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

import Base
import bend-osdev-legacy-ciphers@0.1.0.0/legacy_ciphers.bend as L

214# 64-bit blocks as bytes: a block read back from its 8 bytes is itself, and
215# a list of blocks read back from its bytes is itself
216law block64_octets_round_trip:
217  for +b: L.LcBlock64
218  {L.LcBlock64.of_octets(L.LcBlock64.to_octets(b)) == Some{b} : Maybe<&2, L.LcBlock64>}