def pk.diff_fill

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

import Base
import bend-osdev-bytes@0.1.1.0/bytes.bend as B
import bend-osdev-pkcs7@0.1.0.0/pkcs7.bend as P

234# the padding's difference from its own byte is 0
235def pk.diff_fill(+n: Nat, +u: U32) -> {P.pkcs7.diff(P.pkcs7.fill(n, B.byte(u)), B.byte(u), 0) == 0 : U32}:
236  match n:
237    case 0n:
238      {==}
239    case 1n+p:
240      %Equal.sym(U32, B.byte(B.byte(u)), B.byte(u), pk.bb(u)) : {P.pkcs7.diff(P.pkcs7.fill(p, B.byte(u)), B.byte(u), U32.or(0, U32.xor(_, B.byte(u)))) == 0 : U32}
241      %Equal.sym(U32, U32.xor(B.byte(u), B.byte(u)), 0, pk.xor_self(B.byte(u))) : {P.pkcs7.diff(P.pkcs7.fill(p, B.byte(u)), B.byte(u), U32.or(0, _)) == 0 : U32}
242      pk.diff_fill(p, u)