law fcrypt_round_trip

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

import Base
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

180law fcrypt_round_trip:
181  for k: FC.LcFcryptKey
182  for +b: L.LcBlock64
183  {FC.LcFcrypt.decrypt(k, FC.LcFcrypt.encrypt(k, b)) == b : L.LcBlock64}