Pkcs7.pkcs7.unpad.oct: def of bend-osdev-cipher-modes@0.1.0.0
Import: import bend-osdev-cipher-modes@0.1.0.0/pkcs7.bend as Pkcs7
Lines 65-71 of bend-osdev-cipher-modes@0.1.0.0/pkcs7.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-cipher-modes@0.1.0.0/pkcs7.bend&start_line=65&end_line=71

import Base
import bend-osdev-bytes@0.1.0.0/bytes.bend as B
import bend-osdev-cipher-modes@0.1.0.0/cipher_modes.bend as M

# the value p of the last byte must be 1 to bs, and the last p bytes all p
# (on Octets of n bytes, so that only those p bytes become a list)
def pkcs7.unpad.oct(+bs: Nat, +m: B.Octets, +n: Nat) -> Result<&2, &2, M.CmError, B.Octets>:
  +v = pkcs7.last(B.Octets.at(m, Nat.sub(n, 1n)), 0)
  +p = U32.to_nat(v)
  +good = Bool.and(Nat.is_lt(0n, p), Bool.and(Nat.is_le(p, bs), U32.is_eq(pkcs7.diff(B.Octets.to_list(B.Octets.drop(Nat.sub(n, p), m)), v, 0), 0)))
  pkcs7.strip(good, n, p, m)

Uses (16):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.and
  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_le
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.sub
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Result
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_eq
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat
  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.at
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=Octets.drop
  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-cipher-modes@0.1.0.0/cipher_modes.bend&name=CmError
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/pkcs7.bend&name=pkcs7.diff
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/pkcs7.bend&name=pkcs7.last
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/pkcs7.bend&name=pkcs7.strip