def pk.blocks

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

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

1401def 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>}:
1402  match ok:
1403    case False{}:
1404      e => {==}
1405    case True{}:
1406      match bs:
1407        case 0n:
1408          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)
1409        case 1n+q:
1410          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>}
1411            %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>}
1412            %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>}
1413            %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>}
1414            {==}