law des_ecb_round_trip
bend-osdev-legacy-ciphers@0.1.0.0 · LAWS.bend:228
import bend-osdev-legacy-ciphers@0.1.0.0/LAWS.bend as LAWS
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/des.bend as D
import bend-osdev-legacy-ciphers@0.1.0.0/modes64.bend as X
228law des_ecb_round_trip:
229 for +k: D.LcDesKey
230 for +bs: List<&2, L.LcBlock64>
231 {X.Lc64.ecb_decrypt_blocks(~D.LcDesKey, ~D.LcDes.decrypt, k, X.Lc64.ecb_encrypt_blocks(~D.LcDesKey, ~D.LcDes.encrypt, k, bs)) == bs : List<&2, L.LcBlock64>}