PROOF.cbcp.iv: def of bend-osdev-cbc@0.1.0.0
Import: import bend-osdev-cbc@0.1.0.0/PROOF.bend as PROOF
Lines 216-219 of bend-osdev-cbc@0.1.0.0/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-cbc@0.1.0.0/PROOF.bend&start_line=216&end_line=219

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

# a 16-byte IV is the block of its bytes
def cbcp.iv(+iv: B.Octets, h: {B.Octets.len(iv) == 16n : Nat}) -> {C.cbc.iv(iv) == Done{M.cm.block_of(B.Octets.to_list(iv))} : Result<&2, &2, M.CmError, M.CmBlock>}:
  %Equal.sym(Nat, B.len(B.Octets.to_list(iv)), 16n, oc.len(iv, 16n, h)) : {M.cm.need_block.pick(Nat.is_eq(_, 16n), B.Octets.to_list(iv), M.CmBadIvLength{B.len(B.Octets.to_list(iv))}) == Done{M.cm.block_of(B.Octets.to_list(iv))} : Result<&2, &2, M.CmError, M.CmBlock>}
  {==}

Uses (14):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_eq
  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.to_list
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=len
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/PROOF.bend&name=oc.len
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cbc@0.1.0.0/cbc.bend&name=cbc.iv
  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
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/mode_core.bend&name=cm.block_of
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/mode_core.bend&name=cm.need_block.pick