LAWS.block64_octets_dual: law of bend-osdev-cipher-core@0.1.0.0
Import: import bend-osdev-cipher-core@0.1.0.0/LAWS.bend as LAWS
Lines 17-21 of bend-osdev-cipher-core@0.1.0.0/LAWS.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-cipher-core@0.1.0.0/LAWS.bend&start_line=17&end_line=21

import Base
import bend-osdev-bytes@0.1.1.0/bytes.bend as B
import bend-osdev-cipher-core@0.1.0.0/cipher_core.bend as L

law block64_octets_dual:
  for +o: B.Octets
  for +b: L.LcBlock64
  for e: {L.LcBlock64.of_octets(o) == Some{b} : Maybe<&2, L.LcBlock64>}
  {L.LcBlock64.to_octets(b) == o : B.Octets}

Uses (6):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.1/bytes.bend&name=Octets
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/PROOF.bend&name=b64.dual
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/cipher_core.bend&name=LcBlock64
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/cipher_core.bend&name=LcBlock64.of_octets
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/cipher_core.bend&name=LcBlock64.to_octets