def pk.main

bend-osdev-pkcs7@0.1.0.0 · PROOF.bend:1375

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

1375def 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>}:
1376  +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)))
1377  # the padding is 1 + (q - L mod (1 + q)) bytes
1378  %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>}
1379  # the block size is one the padding takes
1380  %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>}
1381  # and the padded length is a multiple of it (pk.hm)
1382  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))