PROOFPadded.pd.e0: def of bend-osdev-cbc@0.1.0.0
Import: import bend-osdev-cbc@0.1.0.0/PROOF_padded.bend as PROOFPadded
Lines 93-99 of bend-osdev-cbc@0.1.0.0/PROOF_padded.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-cbc@0.1.0.0/PROOF_padded.bend&start_line=93&end_line=99

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

# CBC decryption of no bytes, under any IV, is no bytes
def 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}:
  match r:
    case Fail{e}:
      h => Empty.absurd({B.Octets.len(mp) == 0n : Nat}, pd.fd(B.Octets, e, mp, h))
    case Done{v}:
      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)))

Uses (14):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Result
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=Octets
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=Octets.len
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=Octets.of_list
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/PROOF_padded.bend&name=pd.fd
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/PROOF_padded.bend&name=pd.inj
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/cbc.bend&name=cbc.d1.fast
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/mode_core.bend&name=CmBlock
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/mode_core.bend&name=CmError