def pd.dc

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

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-pkcs7@0.1.0.0/pkcs7.bend as P
import bend-osdev-cbc@0.1.0.0/cbc.bend as C

121# from the ciphertext c, decrypting gives M' and unpadding M' gives m
122def pd.dc(~K: Data, ~dec: K -> M.CmBlock -> M.CmBlock, +k: K, +iv: B.Octets, +mp: B.Octets, +m: B.Octets, e2: {P.Pkcs7.unpad(16n, mp) == Done{m} : Result<&2, &2, M.CmError, B.Octets>}, +c: B.Octets, ok: Bool) -> {Nat.is_lt(0n, B.Octets.len(c)) == ok : Bool} -> {C.Cbc.decrypt(~K, ~dec, k, iv, c) == Done{mp} : Result<&2, &2, M.CmError, B.Octets>} -> {C.Cbc.decrypt_padded(~K, ~dec, k, iv, c) == Done{m} : Result<&2, &2, M.CmError, B.Octets>}:
123  match ok:
124    case True{}:
125      eo => e1 => %Equal.sym(Bool, Nat.is_lt(0n, B.Octets.len(c)), True{}, eo) : {pd.dpx(~K, ~dec, k, iv, c, _) == Done{m} : Result<&2, &2, M.CmError, B.Octets>}
126        %Equal.sym(Result<&2, &2, M.CmError, B.Octets>, C.Cbc.decrypt(~K, ~dec, k, iv, c), Done{mp}, e1) : {Result.bind(&2, &2, M.CmError, B.Octets, B.Octets, _, padded => P.Pkcs7.unpad(16n, padded)) == Done{m} : Result<&2, &2, M.CmError, B.Octets>}
127        e2
128    case False{}:
129      eo => e1 => pd.dc0(~K, ~dec, k, iv, mp, m, e2, c, eo, e1)