LAWS.fcrypt_spec: law of bend-osdev-legacy-ciphers@0.1.0.0
Import: import bend-osdev-legacy-ciphers@0.1.0.0/LAWS.bend as LAWS
Lines 322-325 of bend-osdev-legacy-ciphers@0.1.0.0/LAWS.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/LAWS.bend&start_line=322&end_line=325

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/fcrypt.bend as FC

# the FCrypt specification's second vector: key 114477AADD003366,
# plaintext 123456789ABCDEF0, ciphertext D8ED787477EC0680
law fcrypt_spec:
  {Result.map(&2, &2, L.LcError, FC.LcFcryptKey, L.LcBlock64, k => FC.LcFcrypt.encrypt(k, L.LcBlock64{305419896, 2596069104}), FC.LcFcrypt.key(B.Octets.of_list([17, 68, 119, 170, 221, 0, 51, 102]))) == Done{L.LcBlock64{3639441524, 2011956864}} : Result<&2, &2, L.LcError, L.LcBlock64>}

Uses (9):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Result
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Result.map
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=Octets.of_list
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/fcrypt.bend&name=LcFcrypt.encrypt
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/fcrypt.bend&name=LcFcrypt.key
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/fcrypt.bend&name=LcFcryptKey
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/legacy_ciphers.bend&name=LcBlock64
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/legacy_ciphers.bend&name=LcError