def pd.e0

bend-osdev-cbc@0.1.0.0 · PROOF_padded.bend:93

import Base
import bend-osdev-bytes@0.1.1.0/bytes.bend as B
import bend-osdev-mode-core@0.1.0.0/mode_core.bend as M
import bend-osdev-cbc@0.1.0.0/cbc.bend as C

93# CBC decryption of no bytes, under any IV, is no bytes
94def pd.e0(~K: Data, ~dec: K -> M.CmBlock -> M.CmBlock, +k: K, r: Result<&2, &2, M.CmError, M.CmBlock>, +mp: B.Octets) -> {C.cbc.d1.fast(~K, ~dec, k, r, Nil{}) == Done{mp} : Result<&2, &2, M.CmError, B.Octets>} -> {B.Octets.len(mp) == 0n : Nat}:
95  match r:
96    case Fail{e}:
97      h => Empty.absurd({B.Octets.len(mp) == 0n : Nat}, pd.fd(B.Octets, e, mp, h))
98    case Done{v}:
99      h => Equal.sym(Nat, B.Octets.len(B.Octets.of_list(Nil{})), B.Octets.len(mp), Equal.cong(B.Octets, Nat, o => B.Octets.len(o), B.Octets.of_list(Nil{}), mp, pd.inj(B.Octets, B.Octets.of_list(Nil{}), mp, h)))