law blocks64_octets_round_trip

bend-osdev-cipher-core@0.1.0.0 · LAWS.bend:23

import bend-osdev-cipher-core@0.1.0.0/LAWS.bend as LAWS
import Base
import bend-osdev-cipher-core@0.1.0.0/cipher_core.bend as L
import bend-osdev-cipher-core@0.1.0.0/modes64.bend as X

23law blocks64_octets_round_trip:
24  for +bs: List<&2, L.LcBlock64>
25  {X.Lc64.blocks_of(X.Lc64.octets_of(bs)) == Done{bs} : Result<&2, &2, L.LcError, List<&2, L.LcBlock64>>}

Uses (21)

Used by (4)