def cbc_enc_ok

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

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

8699def cbc_enc_ok(~K: Data, ~enc: K -> L.LcBlock64 -> L.LcBlock64, +k: K, +iv: L.LcBlock64, +bs: List<&2, L.LcBlock64>) -> {X.Lc64.cbc_encrypt(~K, ~enc, k, L.LcBlock64.to_octets(iv), X.Lc64.octets_of(bs)) == Done{X.Lc64.octets_of(X.Lc64.cbc_encrypt_blocks(~K, ~enc, k, iv, bs))} : Result<&2, &2, L.LcError, B.Octets>}:
8700  %Equal.sym(Maybe<&2, L.LcBlock64>, L.LcBlock64.of_octets(L.LcBlock64.to_octets(iv)), Some{iv}, Laws.block64_octets_round_trip(iv)) : {X.m64.cbc.e1(~K, ~enc, k, X.m64.iv(_, B.Octets.len(L.LcBlock64.to_octets(iv))), X.Lc64.octets_of(bs)) == Done{X.Lc64.octets_of(X.Lc64.cbc_encrypt_blocks(~K, ~enc, k, iv, bs))} : Result<&2, &2, L.LcError, B.Octets>}
8701  %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)) : {X.m64.cbc.e2(~K, ~enc, k, iv, _) == Done{X.Lc64.octets_of(X.Lc64.cbc_encrypt_blocks(~K, ~enc, k, iv, bs))} : Result<&2, &2, L.LcError, B.Octets>}
8702  {==}