bend-osdev-pkcs7 Releases (1): 0.1.0.0 0x17768ee6992327a9e94940296270eb23 indexed https://jend.leeeet.dev/files.txt?path=bend-osdev-pkcs7@0.1.0.0 Definitions (68): LAWS.pkcs7_round_trip (https://jend.leeeet.dev/definition.txt?path=bend-osdev-pkcs7@0.1.0.0/LAWS.bend&name=pkcs7_round_trip) # Unpadding undoes padding, for every block size bs and message m: when bs # is one the padding takes (1 to 255), unpad(pad(m)) is m; when it is not, # both refuse alike (CmBadBlockSize) law pkcs7_round_trip: for +bs: Nat for +m: B.Octets {Result.bind(&2, &2, M.CmError, B.Octets, B.Octets, P.Pkcs7.pad(bs, m), c => P.Pkcs7.unpad(bs, c)) == Result.map(&2, &2, M.CmError, B.Octets, B.Octets, c => m, P.Pkcs7.pad(bs, m)) : Result<&2, &2, M.CmError, B.Octets>} LAWS.pkcs7_pad_blocks (https://jend.leeeet.dev/definition.txt?path=bend-osdev-pkcs7@0.1.0.0/LAWS.bend&name=pkcs7_pad_blocks) # A padded message is a whole number of blocks, for every block size and # message law pkcs7_pad_blocks: for +bs: Nat for +m: B.Octets {Result.map(&2, &2, M.CmError, B.Octets, Nat, c => Nat.mod(B.Octets.len(c), bs), P.Pkcs7.pad(bs, m)) == Result.map(&2, &2, M.CmError, B.Octets, Nat, c => 0n, P.Pkcs7.pad(bs, m)) : Result<&2, &2, M.CmError, Nat>} LAWS.pkcs7_pad_empty (https://jend.leeeet.dev/definition.txt?path=bend-osdev-pkcs7@0.1.0.0/LAWS.bend&name=pkcs7_pad_empty) # PKCS #7 (RFC 5652, 6.3): the empty message becomes a whole block of 16s; 15 bytes gain one 1 law pkcs7_pad_empty: {P.Pkcs7.pad(16n, B.Octets.empty()) == Done{B.Octets.of_list([16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16])} : Result<&2, &2, M.CmError, B.Octets>} LAWS.pkcs7_pad_15 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-pkcs7@0.1.0.0/LAWS.bend&name=pkcs7_pad_15) law pkcs7_pad_15: {P.Pkcs7.pad(16n, B.Octets.of_list([107, 193, 190, 226, 46, 64, 159, 150, 233, 61, 126, 17, 115, 147, 23])) == Done{B.Octets.of_list([107, 193, 190, 226, 46, 64, 159, 150, 233, 61, 126, 17, 115, 147, 23, 1])} : Result<&2, &2, M.CmError, B.Octets>} LAWS.pkcs7_unpad_15 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-pkcs7@0.1.0.0/LAWS.bend&name=pkcs7_unpad_15) law pkcs7_unpad_15: {P.Pkcs7.unpad(16n, B.Octets.of_list([107, 193, 190, 226, 46, 64, 159, 150, 233, 61, 126, 17, 115, 147, 23, 1])) == Done{B.Octets.of_list([107, 193, 190, 226, 46, 64, 159, 150, 233, 61, 126, 17, 115, 147, 23])} : Result<&2, &2, M.CmError, B.Octets>} LAWS.pkcs7_unpad_zero (https://jend.leeeet.dev/definition.txt?path=bend-osdev-pkcs7@0.1.0.0/LAWS.bend&name=pkcs7_unpad_zero) # a last byte of 0, or one the bytes before it contradict, is bad padding law pkcs7_unpad_zero: {P.Pkcs7.unpad(16n, B.Octets.of_list([107, 193, 190, 226, 46, 64, 159, 150, 233, 61, 126, 17, 115, 147, 23, 0])) == Fail{M.CmBadPadding{}} : Result<&2, &2, M.CmError, B.Octets>} LAWS.pkcs7_unpad_mixed (https://jend.leeeet.dev/definition.txt?path=bend-osdev-pkcs7@0.1.0.0/LAWS.bend&name=pkcs7_unpad_mixed) law pkcs7_unpad_mixed: {P.Pkcs7.unpad(16n, B.Octets.of_list([107, 193, 190, 226, 46, 64, 159, 150, 233, 61, 126, 17, 115, 2, 3, 3])) == Fail{M.CmBadPadding{}} : Result<&2, &2, M.CmError, B.Octets>} PROOF.pk.disc (https://jend.leeeet.dev/definition.txt?path=bend-osdev-pkcs7@0.1.0.0/PROOF.bend&name=pk.disc) def pk.disc(b: Bool) -> Type: PROOF.pk.empty (https://jend.leeeet.dev/definition.txt?path=bend-osdev-pkcs7@0.1.0.0/PROOF.bend&name=pk.empty) def pk.empty(h: {False{} == True{} : Bool}) -> Empty: PROOF.pk.absurd (https://jend.leeeet.dev/definition.txt?path=bend-osdev-pkcs7@0.1.0.0/PROOF.bend&name=pk.absurd) def pk.absurd(-A: Type, h: {False{} == True{} : Bool}) -> A: PROOF.pk.sub_zero (https://jend.leeeet.dev/definition.txt?path=bend-osdev-pkcs7@0.1.0.0/PROOF.bend&name=pk.sub_zero) def pk.sub_zero(+a: Nat) -> {Nat.sub(a, 0n) == a : Nat}: PROOF.pk.add_sub (https://jend.leeeet.dev/definition.txt?path=bend-osdev-pkcs7@0.1.0.0/PROOF.bend&name=pk.add_sub) # (L + k) - k is L def pk.add_sub(+l: Nat, +k: Nat) -> {Nat.sub(Nat.add(l, k), k) == l : Nat}: PROOF.pk.le_step (https://jend.leeeet.dev/definition.txt?path=bend-osdev-pkcs7@0.1.0.0/PROOF.bend&name=pk.le_step) def pk.le_step(+x: Nat, +y: Nat) -> {Nat.is_le(x, y) == True{} : Bool} -> {Nat.is_le(x, 1n+y) == True{} : Bool}: PROOF.pk.le_sub (https://jend.leeeet.dev/definition.txt?path=bend-osdev-pkcs7@0.1.0.0/PROOF.bend&name=pk.le_sub) # q - r <= q def pk.le_sub(+q: Nat, +r: Nat) -> {Nat.is_le(Nat.sub(q, r), q) == True{} : Bool}: PROOF.pk.sub_succ (https://jend.leeeet.dev/definition.txt?path=bend-osdev-pkcs7@0.1.0.0/PROOF.bend&name=pk.sub_succ) # r <= q gives (1 + q) - r = 1 + (q - r) def pk.sub_succ(+r: Nat, +q: Nat) -> {Nat.is_le(r, q) == True{} : Bool} -> {Nat.sub(1n+q, r) == 1n+Nat.sub(q, r) : Nat}: PROOF.pk.le_trans (https://jend.leeeet.dev/definition.txt?path=bend-osdev-pkcs7@0.1.0.0/PROOF.bend&name=pk.le_trans) def pk.le_trans(+a: Nat, +b: Nat, +c: Nat) -> {Nat.is_le(a, b) == True{} : Bool} -> {Nat.is_le(b, c) == True{} : Bool} -> {Nat.is_le(a, c) == True{} : Bool}: PROOF.pk.le0 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-pkcs7@0.1.0.0/PROOF.bend&name=pk.le0) def pk.le0(+y: Nat) -> {Nat.is_le(0n, y) == True{} : Bool}: PROOF.pk.lt0 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-pkcs7@0.1.0.0/PROOF.bend&name=pk.lt0) def pk.lt0(+x: Nat) -> {Nat.is_lt(x, 0n) == True{} : Bool} -> {False{} == True{} : Bool}: PROOF.pk.lt_le (https://jend.leeeet.dev/definition.txt?path=bend-osdev-pkcs7@0.1.0.0/PROOF.bend&name=pk.lt_le) def pk.lt_le(+x: Nat, +y: Nat) -> {Nat.is_lt(x, 1n+y) == True{} : Bool} -> {Nat.is_le(x, y) == True{} : Bool}: PROOF.pk.go_skip (https://jend.leeeet.dev/definition.txt?path=bend-osdev-pkcs7@0.1.0.0/PROOF.bend&name=pk.go_skip) # 1 + m + x steps from (m, d, r) take one wrap and leave x def pk.go_skip(+m: Nat, +x: Nat, +d: Nat, +r: Nat) -> {Nat.divmod.go(1n+Nat.add(m, x), m, d, r) == Nat.divmod.go(x, Nat.add(m, r), 1n+d, 0n) : Nat & Nat}: PROOF.pk.sub_add_r (https://jend.leeeet.dev/definition.txt?path=bend-osdev-pkcs7@0.1.0.0/PROOF.bend&name=pk.sub_add_r) # (1 + m + r) - r = 1 + m def pk.sub_add_r(+m: Nat, +r: Nat) -> {Nat.sub(1n+Nat.add(m, r), r) == 1n+m : Nat}: PROOF.pk.mod_le (https://jend.leeeet.dev/definition.txt?path=bend-osdev-pkcs7@0.1.0.0/PROOF.bend&name=pk.mod_le) # the remainder is at most q def pk.mod_le(+a: Nat, +m: Nat, +d: Nat, +r: Nat, +q: Nat) -> {Nat.add(m, r) == q : Nat} -> {Nat.is_le(Pair.snd(Nat, Nat, Nat.divmod.go(a, m, d, r)), q) == True{} : Bool}: PROOF.pk.mod_pad (https://jend.leeeet.dev/definition.txt?path=bend-osdev-pkcs7@0.1.0.0/PROOF.bend&name=pk.mod_pad) # a + (1 + q - (a mod (1 + q))) is a multiple of 1 + q def pk.mod_pad(+a: Nat, +m: Nat, +d: Nat, +r: Nat, +q: Nat) -> {Nat.add(m, r) == q : Nat} -> {Pair.snd(Nat, Nat, Nat.divmod.go(Nat.add(a, Nat.sub(1n+q, Pair.snd(Nat, Nat, Nat.divmod.go(a, m, d, r)))), m, d, r)) == 0n : Nat}: PROOF.pk.fill_len (https://jend.leeeet.dev/definition.txt?path=bend-osdev-pkcs7@0.1.0.0/PROOF.bend&name=pk.fill_len) def pk.fill_len(+n: Nat, +v: U32) -> {B.len(P.pkcs7.fill(n, v)) == n : Nat}: PROOF.pk.mask_fill (https://jend.leeeet.dev/definition.txt?path=bend-osdev-pkcs7@0.1.0.0/PROOF.bend&name=pk.mask_fill) def pk.mask_fill(+n: Nat, +v: U32) -> {B.mask(P.pkcs7.fill(n, v)) == P.pkcs7.fill(n, B.byte(v)) : List<&2, U32>}: PROOF.pk.drop_fill (https://jend.leeeet.dev/definition.txt?path=bend-osdev-pkcs7@0.1.0.0/PROOF.bend&name=pk.drop_fill) def pk.drop_fill(+k: Nat, +v: U32) -> {B.drop(k, P.pkcs7.fill(1n+k, v)) == Con{v, Nil{}} : List<&2, U32>}: PROOF.pk.bb (https://jend.leeeet.dev/definition.txt?path=bend-osdev-pkcs7@0.1.0.0/PROOF.bend&name=pk.bb) # BEGIN GENERATED by gen/pkcs7_proof.py: bits # a byte's byte is itself def pk.bb(u: U32) -> {B.byte(B.byte(u)) == B.byte(u) : U32}: PROOF.pk.wself (https://jend.leeeet.dev/definition.txt?path=bend-osdev-pkcs7@0.1.0.0/PROOF.bend&name=pk.wself) # a word XOR itself is zero, bit by bit def pk.wself(+n: Nat, w: Word(n)) -> {Word.xor(n, w, w) == Word.zero(n) : Word(n)}: PROOF.pk.xor_self (https://jend.leeeet.dev/definition.txt?path=bend-osdev-pkcs7@0.1.0.0/PROOF.bend&name=pk.xor_self) def pk.xor_self(+a: U32) -> {U32.xor(a, a) == 0 : U32}: PROOF.pk.diff_fill (https://jend.leeeet.dev/definition.txt?path=bend-osdev-pkcs7@0.1.0.0/PROOF.bend&name=pk.diff_fill) # the padding's difference from its own byte is 0 def pk.diff_fill(+n: Nat, +u: U32) -> {P.pkcs7.diff(P.pkcs7.fill(n, B.byte(u)), B.byte(u), 0) == 0 : U32}: PROOF.pk.u8.c7 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-pkcs7@0.1.0.0/PROOF.bend&name=pk.u8.c7) # BEGIN GENERATED by gen/pkcs7_proof.py: u8 # the values 224 to 255 def pk.u8.c7(r: Nat) -> {Nat.is_le(224n+r, 255n) == True{} : Bool} -> {U32.to_nat(B.byte(U32.from_nat(224n+r))) == 224n+r : Nat}: PROOF.pk.u8.c6 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-pkcs7@0.1.0.0/PROOF.bend&name=pk.u8.c6) # the values 192 to 223 def pk.u8.c6(r: Nat) -> {Nat.is_le(192n+r, 255n) == True{} : Bool} -> {U32.to_nat(B.byte(U32.from_nat(192n+r))) == 192n+r : Nat}: PROOF.pk.u8.c5 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-pkcs7@0.1.0.0/PROOF.bend&name=pk.u8.c5) # the values 160 to 191 def pk.u8.c5(r: Nat) -> {Nat.is_le(160n+r, 255n) == True{} : Bool} -> {U32.to_nat(B.byte(U32.from_nat(160n+r))) == 160n+r : Nat}: PROOF.pk.u8.c4 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-pkcs7@0.1.0.0/PROOF.bend&name=pk.u8.c4) # the values 128 to 159 def pk.u8.c4(r: Nat) -> {Nat.is_le(128n+r, 255n) == True{} : Bool} -> {U32.to_nat(B.byte(U32.from_nat(128n+r))) == 128n+r : Nat}: PROOF.pk.u8.c3 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-pkcs7@0.1.0.0/PROOF.bend&name=pk.u8.c3) # the values 96 to 127 def pk.u8.c3(r: Nat) -> {Nat.is_le(96n+r, 255n) == True{} : Bool} -> {U32.to_nat(B.byte(U32.from_nat(96n+r))) == 96n+r : Nat}: PROOF.pk.u8.c2 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-pkcs7@0.1.0.0/PROOF.bend&name=pk.u8.c2) # the values 64 to 95 def pk.u8.c2(r: Nat) -> {Nat.is_le(64n+r, 255n) == True{} : Bool} -> {U32.to_nat(B.byte(U32.from_nat(64n+r))) == 64n+r : Nat}: PROOF.pk.u8.c1 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-pkcs7@0.1.0.0/PROOF.bend&name=pk.u8.c1) # the values 32 to 63 def pk.u8.c1(r: Nat) -> {Nat.is_le(32n+r, 255n) == True{} : Bool} -> {U32.to_nat(B.byte(U32.from_nat(32n+r))) == 32n+r : Nat}: PROOF.pk.u8 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-pkcs7@0.1.0.0/PROOF.bend&name=pk.u8) # the values 0 to 31 def pk.u8(r: Nat) -> {Nat.is_le(r, 255n) == True{} : Bool} -> {U32.to_nat(B.byte(U32.from_nat(r))) == r : Nat}: PROOF.pk.ug (https://jend.leeeet.dev/definition.txt?path=bend-osdev-pkcs7@0.1.0.0/PROOF.bend&name=pk.ug) # Pkcs7.unpad's checks and its unpad.oct, with what they compute as # arguments, so that each can be rewritten on its own def pk.ug(+bs: Nat, +m: B.Octets, +n: Nat, +md: Nat) -> Result<&2, &2, M.CmError, B.Octets>: PROOF.pk.k2 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-pkcs7@0.1.0.0/PROOF.bend&name=pk.k2) def pk.k2(+bs: Nat, +m: B.Octets, +n: Nat, +p: Nat, le: Bool, +d: U32) -> Result<&2, &2, M.CmError, B.Octets>: PROOF.pk.k (https://jend.leeeet.dev/definition.txt?path=bend-osdev-pkcs7@0.1.0.0/PROOF.bend&name=pk.k) def pk.k(+bs: Nat, +m: B.Octets, +n: Nat, +v: U32, +p: Nat) -> Result<&2, &2, M.CmError, B.Octets>: PROOF.pk.pad (https://jend.leeeet.dev/definition.txt?path=bend-osdev-pkcs7@0.1.0.0/PROOF.bend&name=pk.pad) # the padding of 1 + p1 bytes def pk.pad(+p1: Nat) -> B.Octets: PROOF.pk.at (https://jend.leeeet.dev/definition.txt?path=bend-osdev-pkcs7@0.1.0.0/PROOF.bend&name=pk.at) # its last byte, at L + p1 of m and it def pk.at(+m: B.Octets, +p1: Nat) -> {B.Octets.at(B.Octets.append(m, pk.pad(p1)), Nat.add(B.Octets.len(m), p1)) == Some{B.byte(U32.from_nat(1n+p1))} : Maybe<&2, U32>}: PROOF.pk.len (https://jend.leeeet.dev/definition.txt?path=bend-osdev-pkcs7@0.1.0.0/PROOF.bend&name=pk.len) # the padded message's length def pk.len(+m: B.Octets, +p1: Nat) -> {B.Octets.len(B.Octets.append(m, pk.pad(p1))) == 1n+Nat.add(B.Octets.len(m), p1) : Nat}: PROOF.pk.oct (https://jend.leeeet.dev/definition.txt?path=bend-osdev-pkcs7@0.1.0.0/PROOF.bend&name=pk.oct) # unpad.oct on m and a padding of 1 + p1 bytes (p1 below 255) gives m def pk.oct(+bs: Nat, +m: B.Octets, +p1: Nat, hle: {Nat.is_le(1n+p1, bs) == True{} : Bool}, hb: {Nat.is_le(1n+p1, 255n) == True{} : Bool}) -> {P.pkcs7.unpad.oct(bs, B.Octets.append(m, pk.pad(p1)), 1n+Nat.add(B.Octets.len(m), p1)) == Done{m} : Result<&2, &2, M.CmError, B.Octets>}: PROOF.pk.main2 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-pkcs7@0.1.0.0/PROOF.bend&name=pk.main2) # the round trip for a block size 1 + q (q below 255) and a padding of # 1 + p1 bytes, p1 <= q, that makes whole blocks def pk.main2(+q: Nat, +m: B.Octets, +p1: Nat, +hle: {Nat.is_le(p1, q) == True{} : Bool}, hb: {Nat.is_le(1n+q, 255n) == True{} : Bool}, hm: {Nat.mod(1n+Nat.add(B.Octets.len(m), p1), 1n+q) == 0n : Nat}) -> {P.Pkcs7.unpad.go(True{}, 1n+q, B.Octets.append(m, pk.pad(p1))) == Done{m} : Result<&2, &2, M.CmError, B.Octets>}: PROOF.pk.hm (https://jend.leeeet.dev/definition.txt?path=bend-osdev-pkcs7@0.1.0.0/PROOF.bend&name=pk.hm) # 1 + L + (q - L mod (1 + q)) is a multiple of 1 + q def pk.hm(+q: Nat, +m: B.Octets) -> {Nat.mod(1n+Nat.add(B.Octets.len(m), Nat.sub(q, Nat.mod(B.Octets.len(m), 1n+q))), 1n+q) == 0n : Nat}: PROOF.pk.main (https://jend.leeeet.dev/definition.txt?path=bend-osdev-pkcs7@0.1.0.0/PROOF.bend&name=pk.main) def 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>}: PROOF.pk.rt (https://jend.leeeet.dev/definition.txt?path=bend-osdev-pkcs7@0.1.0.0/PROOF.bend&name=pk.rt) def 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>}: PROOF.pk.blocks (https://jend.leeeet.dev/definition.txt?path=bend-osdev-pkcs7@0.1.0.0/PROOF.bend&name=pk.blocks) 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>}: Check.err (https://jend.leeeet.dev/definition.txt?path=bend-osdev-pkcs7@0.1.0.0/check.bend&name=err) def err(e: M.CmError) -> String: Check.res (https://jend.leeeet.dev/definition.txt?path=bend-osdev-pkcs7@0.1.0.0/check.bend&name=res) def res(r: Result<&2, &2, M.CmError, B.Octets>) -> String: Check.back (https://jend.leeeet.dev/definition.txt?path=bend-osdev-pkcs7@0.1.0.0/check.bend&name=back) # whether r is m def back(r: Result<&2, &2, M.CmError, B.Octets>, +m: B.Octets) -> String: Check.bytes.go (https://jend.leeeet.dev/definition.txt?path=bend-osdev-pkcs7@0.1.0.0/check.bend&name=bytes.go) # n pseudo-random bytes (a linear congruential generator) def bytes.go(n: Nat, +s: U32, acc: List<&2, U32>) -> List<&2, U32>: Check.msg (https://jend.leeeet.dev/definition.txt?path=bend-osdev-pkcs7@0.1.0.0/check.bend&name=msg) def msg(n: Nat) -> B.Octets: Check.iv (https://jend.leeeet.dev/definition.txt?path=bend-osdev-pkcs7@0.1.0.0/check.bend&name=iv) def iv() -> B.Octets: Check.main (https://jend.leeeet.dev/definition.txt?path=bend-osdev-pkcs7@0.1.0.0/check.bend&name=main) def main() -> IO(Unit): Pkcs7.pkcs7.fill (https://jend.leeeet.dev/definition.txt?path=bend-osdev-pkcs7@0.1.0.0/pkcs7.bend&name=pkcs7.fill) # n bytes of value v def pkcs7.fill(n: Nat, +v: U32) -> List<&2, U32>: Pkcs7.pkcs7.size_ok (https://jend.leeeet.dev/definition.txt?path=bend-osdev-pkcs7@0.1.0.0/pkcs7.bend&name=pkcs7.size_ok) def pkcs7.size_ok(+bs: Nat) -> Bool: Pkcs7.pkcs7.pad.oct (https://jend.leeeet.dev/definition.txt?path=bend-osdev-pkcs7@0.1.0.0/pkcs7.bend&name=pkcs7.pad.oct) # m and its padding (on Octets, so that a long message is not walked as a # list: Bend 2.0.37's runtime overflows its stack on deep structural # recursion) def pkcs7.pad.oct(+bs: Nat, +m: B.Octets) -> B.Octets: Pkcs7.Pkcs7.pad.go (https://jend.leeeet.dev/definition.txt?path=bend-osdev-pkcs7@0.1.0.0/pkcs7.bend&name=Pkcs7.pad.go) def Pkcs7.pad.go(ok: Bool, +bs: Nat, m: B.Octets) -> Result<&2, &2, M.CmError, B.Octets>: Pkcs7.Pkcs7.pad (https://jend.leeeet.dev/definition.txt?path=bend-osdev-pkcs7@0.1.0.0/pkcs7.bend&name=Pkcs7.pad) # m padded to a whole number of bs-byte blocks def Pkcs7.pad(+bs: Nat, m: B.Octets) -> Result<&2, &2, M.CmError, B.Octets>: Pkcs7.pkcs7.diff (https://jend.leeeet.dev/definition.txt?path=bend-osdev-pkcs7@0.1.0.0/pkcs7.bend&name=pkcs7.diff) # 0 when every byte of xs is v def pkcs7.diff(xs: List<&2, U32>, +v: U32, acc: U32) -> U32: Pkcs7.pkcs7.last (https://jend.leeeet.dev/definition.txt?path=bend-osdev-pkcs7@0.1.0.0/pkcs7.bend&name=pkcs7.last) # the last byte, or d if there is none def pkcs7.last(m: Maybe<&2, U32>, d: U32) -> U32: Pkcs7.pkcs7.strip (https://jend.leeeet.dev/definition.txt?path=bend-osdev-pkcs7@0.1.0.0/pkcs7.bend&name=pkcs7.strip) def pkcs7.strip(ok: Bool, +n: Nat, +p: Nat, m: B.Octets) -> Result<&2, &2, M.CmError, B.Octets>: Pkcs7.pkcs7.unpad.oct (https://jend.leeeet.dev/definition.txt?path=bend-osdev-pkcs7@0.1.0.0/pkcs7.bend&name=pkcs7.unpad.oct) # the value p of the last byte must be 1 to bs, and the last p bytes all p # (on Octets of n bytes, so that only those p bytes become a list) def pkcs7.unpad.oct(+bs: Nat, +m: B.Octets, +n: Nat) -> Result<&2, &2, M.CmError, B.Octets>: Pkcs7.Pkcs7.unpad.go (https://jend.leeeet.dev/definition.txt?path=bend-osdev-pkcs7@0.1.0.0/pkcs7.bend&name=Pkcs7.unpad.go) def Pkcs7.unpad.go(ok: Bool, +bs: Nat, +m: B.Octets) -> Result<&2, &2, M.CmError, B.Octets>: Pkcs7.Pkcs7.unpad (https://jend.leeeet.dev/definition.txt?path=bend-osdev-pkcs7@0.1.0.0/pkcs7.bend&name=Pkcs7.unpad) # m without its padding; m must be a non-empty whole number of blocks def Pkcs7.unpad(+bs: Nat, m: B.Octets) -> Result<&2, &2, M.CmError, B.Octets>: