def pk.rt

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

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

1384def pk.rt(ok: Bool, +bs: Nat, +m: B.Octets) -> {P.pkcs7.size_ok(bs) == ok : Bool} -> {Result.bind(&2, &2, M.CmError, B.Octets, B.Octets, P.Pkcs7.pad.go(ok, bs, m), c => P.Pkcs7.unpad(bs, c)) == Result.map(&2, &2, M.CmError, B.Octets, B.Octets, c => m, P.Pkcs7.pad.go(ok, bs, m)) : Result<&2, &2, M.CmError, B.Octets>}:
1385  match ok:
1386    case False{}:
1387      e => {==}
1388    case True{}:
1389      match bs:
1390        case 0n:
1391          e => pk.absurd({P.Pkcs7.unpad(0n, P.pkcs7.pad.oct(0n, m)) == Done{m} : Result<&2, &2, M.CmError, B.Octets>}, e)
1392        case 1n+q:
1393          e => pk.main(q, m, e)