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

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

def pk.blocks(ok: Bool, +bs: Nat, +m: B.Octets) -> {P.pkcs7.size_ok(bs) == ok : Bool} -> {Result.map(&2, &2, M.CmError, B.Octets, Nat, c => Nat.mod(B.Octets.len(c), bs), P.Pkcs7.pad.go(ok, bs, m)) == Result.map(&2, &2, M.CmError, B.Octets, Nat, c => 0n, P.Pkcs7.pad.go(ok, bs, m)) : Result<&2, &2, M.CmError, Nat>}:
  match ok:
    case False{}:
      e => {==}
    case True{}:
      match bs:
        case 0n:
          e => pk.absurd({Done{Nat.mod(B.Octets.len(P.pkcs7.pad.oct(0n, m)), 0n)} == Done{0n} : Result<&2, &2, M.CmError, Nat>}, e)
        case 1n+q:
          e => %Equal.sym(Nat, B.Octets.len(P.pkcs7.pad.oct(1n+q, m)), Nat.add(B.Octets.len(m), B.Octets.len(B.Octets.of_list(P.pkcs7.fill(Nat.sub(1n+q, Nat.mod(B.Octets.len(m), 1n+q)), U32.from_nat(Nat.sub(1n+q, Nat.mod(B.Octets.len(m), 1n+q))))))), BL.octets_len_append(m, B.Octets.of_list(P.pkcs7.fill(Nat.sub(1n+q, Nat.mod(B.Octets.len(m), 1n+q)), U32.from_nat(Nat.sub(1n+q, Nat.mod(B.Octets.len(m), 1n+q))))))) : {Done{Nat.mod(_, 1n+q)} == Done{0n} : Result<&2, &2, M.CmError, Nat>}
            %Equal.sym(Nat, B.Octets.len(B.Octets.of_list(P.pkcs7.fill(Nat.sub(1n+q, Nat.mod(B.Octets.len(m), 1n+q)), U32.from_nat(Nat.sub(1n+q, Nat.mod(B.Octets.len(m), 1n+q)))))), B.len(P.pkcs7.fill(Nat.sub(1n+q, Nat.mod(B.Octets.len(m), 1n+q)), U32.from_nat(Nat.sub(1n+q, Nat.mod(B.Octets.len(m), 1n+q))))), BL.octets_len_of_list(P.pkcs7.fill(Nat.sub(1n+q, Nat.mod(B.Octets.len(m), 1n+q)), U32.from_nat(Nat.sub(1n+q, Nat.mod(B.Octets.len(m), 1n+q)))))) : {Done{Nat.mod(Nat.add(B.Octets.len(m), _), 1n+q)} == Done{0n} : Result<&2, &2, M.CmError, Nat>}
            %Equal.sym(Nat, B.len(P.pkcs7.fill(Nat.sub(1n+q, Nat.mod(B.Octets.len(m), 1n+q)), U32.from_nat(Nat.sub(1n+q, Nat.mod(B.Octets.len(m), 1n+q))))), Nat.sub(1n+q, Nat.mod(B.Octets.len(m), 1n+q)), pk.fill_len(Nat.sub(1n+q, Nat.mod(B.Octets.len(m), 1n+q)), U32.from_nat(Nat.sub(1n+q, Nat.mod(B.Octets.len(m), 1n+q))))) : {Done{Nat.mod(Nat.add(B.Octets.len(m), _), 1n+q)} == Done{0n} : Result<&2, &2, M.CmError, Nat>}
            %Equal.sym(Nat, Nat.mod(Nat.add(B.Octets.len(m), Nat.sub(1n+q, Nat.mod(B.Octets.len(m), 1n+q))), 1n+q), 0n, pk.mod_pad(B.Octets.len(m), q, 0n, 0n, q)(UL.nat_add_zero(q))) : {Done{_} == Done{0n} : Result<&2, &2, M.CmError, Nat>}
            {==}

Uses (24):
  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.add
  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=Result.map
  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/LAWS.bend&name=octets_len_append
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=octets_len_of_list
  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.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-bytes@0.1.1.0/bytes.bend&name=len
  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.absurd
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-pkcs7@0.1.0.0/PROOF.bend&name=pk.fill_len
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-pkcs7@0.1.0.0/PROOF.bend&name=pk.mod_pad
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-pkcs7@0.1.0.0/pkcs7.bend&name=Pkcs7.pad.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-pkcs7@0.1.0.0/pkcs7.bend&name=pkcs7.size_ok
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=nat_add_zero