PROOF.pk.oct: def of bend-osdev-pkcs7@0.1.0.0
Import: import bend-osdev-pkcs7@0.1.0.0/PROOF.bend as PROOF
Lines 1339-1359 of bend-osdev-pkcs7@0.1.0.0/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-pkcs7@0.1.0.0/PROOF.bend&start_line=1339&end_line=1359

import Base
import bend-osdev-bytes@0.1.1.0/bytes.bend as B
import bend-osdev-bytes@0.1.1.0/LAWS.bend as BL
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

# unpad.oct on m and a padding of 1 + p1 bytes (p1 below 255) gives m
def pk.oct(+bs: Nat, +m: B.Octets, +p1: Nat, hle: {Nat.is_le(1n+p1, bs) == True{} : Bool}, hb: {Nat.is_le(1n+p1, 255n) == True{} : Bool}) -> {P.pkcs7.unpad.oct(bs, B.Octets.append(m, pk.pad(p1)), 1n+Nat.add(B.Octets.len(m), p1)) == Done{m} : Result<&2, &2, M.CmError, B.Octets>}:
  +el = pk.add_sub(B.Octets.len(m), p1)
  # the last byte is the byte of 1 + p1
  %Equal.sym(Nat, Nat.sub(Nat.add(B.Octets.len(m), p1), 0n), Nat.add(B.Octets.len(m), p1), pk.sub_zero(Nat.add(B.Octets.len(m), p1))) : {pk.k(bs, B.Octets.append(m, pk.pad(p1)), 1n+Nat.add(B.Octets.len(m), p1), P.pkcs7.last(B.Octets.at(B.Octets.append(m, pk.pad(p1)), _), 0), U32.to_nat(P.pkcs7.last(B.Octets.at(B.Octets.append(m, pk.pad(p1)), _), 0))) == Done{m} : Result<&2, &2, M.CmError, B.Octets>}
  %Equal.sym(Maybe<&2, U32>, B.Octets.at(B.Octets.append(m, pk.pad(p1)), Nat.add(B.Octets.len(m), p1)), Some{B.byte(U32.from_nat(1n+p1))}, pk.at(m, p1)) : {pk.k(bs, B.Octets.append(m, pk.pad(p1)), 1n+Nat.add(B.Octets.len(m), p1), P.pkcs7.last(_, 0), U32.to_nat(P.pkcs7.last(_, 0))) == Done{m} : Result<&2, &2, M.CmError, B.Octets>}
  # whose value is 1 + p1
  %Equal.sym(Nat, U32.to_nat(B.byte(U32.from_nat(1n+p1))), 1n+p1, pk.u8(1n+p1)(hb)) : {pk.k(bs, B.Octets.append(m, pk.pad(p1)), 1n+Nat.add(B.Octets.len(m), p1), B.byte(U32.from_nat(1n+p1)), _) == Done{m} : Result<&2, &2, M.CmError, B.Octets>}
  # at most the block size
  %Equal.sym(Bool, Nat.is_le(1n+p1, bs), True{}, hle) : {pk.k2(bs, B.Octets.append(m, pk.pad(p1)), 1n+Nat.add(B.Octets.len(m), p1), 1n+p1, _, P.pkcs7.diff(B.Octets.to_list(B.Octets.drop(Nat.sub(Nat.add(B.Octets.len(m), p1), p1), B.Octets.append(m, pk.pad(p1)))), B.byte(U32.from_nat(1n+p1)), 0)) == Done{m} : Result<&2, &2, M.CmError, B.Octets>}
  # the last 1 + p1 bytes are the padding
  %Equal.sym(Nat, Nat.sub(Nat.add(B.Octets.len(m), p1), p1), B.Octets.len(m), el) : {pk.k2(bs, B.Octets.append(m, pk.pad(p1)), 1n+Nat.add(B.Octets.len(m), p1), 1n+p1, True{}, P.pkcs7.diff(B.Octets.to_list(B.Octets.drop(_, B.Octets.append(m, pk.pad(p1)))), B.byte(U32.from_nat(1n+p1)), 0)) == Done{m} : Result<&2, &2, M.CmError, B.Octets>}
  %Equal.sym(B.Octets, B.Octets.drop(B.Octets.len(m), B.Octets.append(m, pk.pad(p1))), pk.pad(p1), BL.octets_drop_append(m, pk.pad(p1))) : {pk.k2(bs, B.Octets.append(m, pk.pad(p1)), 1n+Nat.add(B.Octets.len(m), p1), 1n+p1, True{}, P.pkcs7.diff(B.Octets.to_list(_), B.byte(U32.from_nat(1n+p1)), 0)) == Done{m} : Result<&2, &2, M.CmError, B.Octets>}
  %Equal.sym(List<&2, U32>, B.Octets.to_list(pk.pad(p1)), B.mask(P.pkcs7.fill(1n+p1, U32.from_nat(1n+p1))), BL.octets_to_of(P.pkcs7.fill(1n+p1, U32.from_nat(1n+p1)))) : {pk.k2(bs, B.Octets.append(m, pk.pad(p1)), 1n+Nat.add(B.Octets.len(m), p1), 1n+p1, True{}, P.pkcs7.diff(_, B.byte(U32.from_nat(1n+p1)), 0)) == Done{m} : Result<&2, &2, M.CmError, B.Octets>}
  %Equal.sym(List<&2, U32>, B.mask(P.pkcs7.fill(1n+p1, U32.from_nat(1n+p1))), P.pkcs7.fill(1n+p1, B.byte(U32.from_nat(1n+p1))), pk.mask_fill(1n+p1, U32.from_nat(1n+p1))) : {pk.k2(bs, B.Octets.append(m, pk.pad(p1)), 1n+Nat.add(B.Octets.len(m), p1), 1n+p1, True{}, P.pkcs7.diff(_, B.byte(U32.from_nat(1n+p1)), 0)) == Done{m} : Result<&2, &2, M.CmError, B.Octets>}
  # all of them the byte
  %Equal.sym(U32, P.pkcs7.diff(P.pkcs7.fill(1n+p1, B.byte(U32.from_nat(1n+p1))), B.byte(U32.from_nat(1n+p1)), 0), 0, pk.diff_fill(1n+p1, U32.from_nat(1n+p1))) : {pk.k2(bs, B.Octets.append(m, pk.pad(p1)), 1n+Nat.add(B.Octets.len(m), p1), 1n+p1, True{}, _) == Done{m} : Result<&2, &2, M.CmError, B.Octets>}
  # so the first L bytes are kept
  %Equal.sym(Nat, Nat.sub(Nat.add(B.Octets.len(m), p1), p1), B.Octets.len(m), el) : {Done{B.Octets.take(_, B.Octets.append(m, pk.pad(p1)))} == Done{m} : Result<&2, &2, M.CmError, B.Octets>}
  %Equal.sym(B.Octets, B.Octets.take(B.Octets.len(m), B.Octets.append(m, pk.pad(p1))), m, BL.octets_take_append(m, pk.pad(p1))) : {Done{_} == Done{m} : Result<&2, &2, M.CmError, B.Octets>}
  {==}

Uses (38):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  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=Maybe
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  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.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
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.from_nat
  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/LAWS.bend&name=octets_drop_append
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=octets_take_append
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=octets_to_of
  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.append
  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.len
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=Octets.take
  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=byte
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=mask
  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-pkcs7@0.1.0.0/PROOF.bend&name=pk.add_sub
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-pkcs7@0.1.0.0/PROOF.bend&name=pk.at
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-pkcs7@0.1.0.0/PROOF.bend&name=pk.diff_fill
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-pkcs7@0.1.0.0/PROOF.bend&name=pk.k
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-pkcs7@0.1.0.0/PROOF.bend&name=pk.k2
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-pkcs7@0.1.0.0/PROOF.bend&name=pk.mask_fill
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-pkcs7@0.1.0.0/PROOF.bend&name=pk.pad
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-pkcs7@0.1.0.0/PROOF.bend&name=pk.sub_zero
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-pkcs7@0.1.0.0/PROOF.bend&name=pk.u8
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-pkcs7@0.1.0.0/pkcs7.bend&name=pkcs7.diff
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-pkcs7@0.1.0.0/pkcs7.bend&name=pkcs7.fill
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-pkcs7@0.1.0.0/pkcs7.bend&name=pkcs7.last
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-pkcs7@0.1.0.0/pkcs7.bend&name=pkcs7.unpad.oct