law des_cbc_round_trip
bend-osdev-legacy-ciphers@0.1.0.0 · LAWS.bend:233
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
233law des_cbc_round_trip:
234 for +k: D.LcDesKey
235 for +iv: L.LcBlock64
236 for +bs: List<&2, L.LcBlock64>
237 {X.Lc64.cbc_decrypt_blocks(~D.LcDesKey, ~D.LcDes.decrypt, k, iv, X.Lc64.cbc_encrypt_blocks(~D.LcDesKey, ~D.LcDes.encrypt, k, iv, bs)) == bs : List<&2, L.LcBlock64>}