def ecb_enc_ok

bend-osdev-legacy-ciphers@0.1.0.0 · PROOF.bend:8709

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/modes64.bend as X
import bend-osdev-legacy-ciphers@0.1.0.0/LAWS.bend as Laws

8709def ecb_enc_ok(~K: Data, ~f: K -> L.LcBlock64 -> L.LcBlock64, +k: K, +bs: List<&2, L.LcBlock64>) -> {Result.map(&2, &2, L.LcError, List<&2, L.LcBlock64>, B.Octets, xs => X.Lc64.octets_of(X.Lc64.ecb_encrypt_blocks(~K, ~f, k, xs)), X.Lc64.blocks_of(X.Lc64.octets_of(bs))) == Done{X.Lc64.octets_of(X.Lc64.ecb_encrypt_blocks(~K, ~f, k, bs))} : Result<&2, &2, L.LcError, B.Octets>}:
8710  %Equal.sym(Result<&2, &2, L.LcError, List<&2, L.LcBlock64>>, X.Lc64.blocks_of(X.Lc64.octets_of(bs)), Done{bs}, Laws.blocks64_octets_round_trip(bs)) : {Result.map(&2, &2, L.LcError, List<&2, L.LcBlock64>, B.Octets, xs => X.Lc64.octets_of(X.Lc64.ecb_encrypt_blocks(~K, ~f, k, xs)), _) == Done{X.Lc64.octets_of(X.Lc64.ecb_encrypt_blocks(~K, ~f, k, bs))} : Result<&2, &2, L.LcError, B.Octets>}
8711  {==}