PROOF.pk.main: def of bend-osdev-pkcs7@0.1.0.0
Import: import bend-osdev-pkcs7@0.1.0.0/PROOF.bend as PROOF
Lines 1375-1382 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=1375&end_line=1382

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-u32@0.1.0.0/LAWS.bend as UL

def pk.main(+q: Nat, +m: B.Octets, +e: {Nat.is_lt(1n+q, 256n) == True{} : Bool}) -> {P.Pkcs7.unpad(1n+q, P.pkcs7.pad.oct(1n+q, m)) == Done{m} : Result<&2, &2, M.CmError, B.Octets>}:
  +hs = pk.sub_succ(Nat.mod(B.Octets.len(m), 1n+q), q)(pk.mod_le(B.Octets.len(m), q, 0n, 0n, q)(UL.nat_add_zero(q)))
  # the padding is 1 + (q - L mod (1 + q)) bytes
  %Equal.sym(Nat, Nat.sub(1n+q, Nat.mod(B.Octets.len(m), 1n+q)), 1n+Nat.sub(q, Nat.mod(B.Octets.len(m), 1n+q)), hs) : {P.Pkcs7.unpad(1n+q, B.Octets.append(m, B.Octets.of_list(P.pkcs7.fill(_, U32.from_nat(_))))) == Done{m} : Result<&2, &2, M.CmError, B.Octets>}
  # the block size is one the padding takes
  %Equal.sym(Bool, Nat.is_lt(1n+q, 256n), True{}, e) : {P.Pkcs7.unpad.go(_, 1n+q, B.Octets.append(m, pk.pad(Nat.sub(q, Nat.mod(B.Octets.len(m), 1n+q))))) == Done{m} : Result<&2, &2, M.CmError, B.Octets>}
  # and the padded length is a multiple of it (pk.hm)
  pk.main2(q, m, Nat.sub(q, Nat.mod(B.Octets.len(m), 1n+q)), pk.le_sub(q, Nat.mod(B.Octets.len(m), 1n+q)), pk.lt_le(1n+q, 255n)(e), pk.hm(q, m))

Uses (25):
  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=Nat
  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.mod
  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.from_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.append
  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-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.hm
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-pkcs7@0.1.0.0/PROOF.bend&name=pk.le_sub
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-pkcs7@0.1.0.0/PROOF.bend&name=pk.lt_le
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-pkcs7@0.1.0.0/PROOF.bend&name=pk.main2
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-pkcs7@0.1.0.0/PROOF.bend&name=pk.mod_le
  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_succ
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-pkcs7@0.1.0.0/pkcs7.bend&name=Pkcs7.unpad
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-pkcs7@0.1.0.0/pkcs7.bend&name=Pkcs7.unpad.go
  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.pad.oct
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=nat_add_zero