def pk.oct

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

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

1339# unpad.oct on m and a padding of 1 + p1 bytes (p1 below 255) gives m
1340def 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>}:
1341  +el = pk.add_sub(B.Octets.len(m), p1)
1342  # the last byte is the byte of 1 + p1
1343  %Equal.sym(Nat, Nat.sub(Nat.add(B.Octets.len(m), p1), 0n), Nat.add(B.Octets.len(m), p1), pk.sub_zero(Nat.add(B.Octets.len(m), p1))) : {pk.k(bs, B.Octets.append(m, pk.pad(p1)), 1n+Nat.add(B.Octets.len(m), p1), P.pkcs7.last(B.Octets.at(B.Octets.append(m, pk.pad(p1)), _), 0), U32.to_nat(P.pkcs7.last(B.Octets.at(B.Octets.append(m, pk.pad(p1)), _), 0))) == Done{m} : Result<&2, &2, M.CmError, B.Octets>}
1344  %Equal.sym(Maybe<&2, U32>, 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))}, pk.at(m, p1)) : {pk.k(bs, B.Octets.append(m, pk.pad(p1)), 1n+Nat.add(B.Octets.len(m), p1), P.pkcs7.last(_, 0), U32.to_nat(P.pkcs7.last(_, 0))) == Done{m} : Result<&2, &2, M.CmError, B.Octets>}
1345  # whose value is 1 + p1
1346  %Equal.sym(Nat, U32.to_nat(B.byte(U32.from_nat(1n+p1))), 1n+p1, pk.u8(1n+p1)(hb)) : {pk.k(bs, B.Octets.append(m, pk.pad(p1)), 1n+Nat.add(B.Octets.len(m), p1), B.byte(U32.from_nat(1n+p1)), _) == Done{m} : Result<&2, &2, M.CmError, B.Octets>}
1347  # at most the block size
1348  %Equal.sym(Bool, Nat.is_le(1n+p1, bs), True{}, hle) : {pk.k2(bs, B.Octets.append(m, pk.pad(p1)), 1n+Nat.add(B.Octets.len(m), p1), 1n+p1, _, P.pkcs7.diff(B.Octets.to_list(B.Octets.drop(Nat.sub(Nat.add(B.Octets.len(m), p1), p1), B.Octets.append(m, pk.pad(p1)))), B.byte(U32.from_nat(1n+p1)), 0)) == Done{m} : Result<&2, &2, M.CmError, B.Octets>}
1349  # the last 1 + p1 bytes are the padding
1350  %Equal.sym(Nat, Nat.sub(Nat.add(B.Octets.len(m), p1), p1), B.Octets.len(m), el) : {pk.k2(bs, B.Octets.append(m, pk.pad(p1)), 1n+Nat.add(B.Octets.len(m), p1), 1n+p1, True{}, P.pkcs7.diff(B.Octets.to_list(B.Octets.drop(_, B.Octets.append(m, pk.pad(p1)))), B.byte(U32.from_nat(1n+p1)), 0)) == Done{m} : Result<&2, &2, M.CmError, B.Octets>}
1351  %Equal.sym(B.Octets, B.Octets.drop(B.Octets.len(m), B.Octets.append(m, pk.pad(p1))), pk.pad(p1), BL.octets_drop_append(m, pk.pad(p1))) : {pk.k2(bs, B.Octets.append(m, pk.pad(p1)), 1n+Nat.add(B.Octets.len(m), p1), 1n+p1, True{}, P.pkcs7.diff(B.Octets.to_list(_), B.byte(U32.from_nat(1n+p1)), 0)) == Done{m} : Result<&2, &2, M.CmError, B.Octets>}
1352  %Equal.sym(List<&2, U32>, B.Octets.to_list(pk.pad(p1)), B.mask(P.pkcs7.fill(1n+p1, U32.from_nat(1n+p1))), BL.octets_to_of(P.pkcs7.fill(1n+p1, U32.from_nat(1n+p1)))) : {pk.k2(bs, B.Octets.append(m, pk.pad(p1)), 1n+Nat.add(B.Octets.len(m), p1), 1n+p1, True{}, P.pkcs7.diff(_, B.byte(U32.from_nat(1n+p1)), 0)) == Done{m} : Result<&2, &2, M.CmError, B.Octets>}
1353  %Equal.sym(List<&2, U32>, B.mask(P.pkcs7.fill(1n+p1, U32.from_nat(1n+p1))), P.pkcs7.fill(1n+p1, B.byte(U32.from_nat(1n+p1))), pk.mask_fill(1n+p1, U32.from_nat(1n+p1))) : {pk.k2(bs, B.Octets.append(m, pk.pad(p1)), 1n+Nat.add(B.Octets.len(m), p1), 1n+p1, True{}, P.pkcs7.diff(_, B.byte(U32.from_nat(1n+p1)), 0)) == Done{m} : Result<&2, &2, M.CmError, B.Octets>}
1354  # all of them the byte
1355  %Equal.sym(U32, P.pkcs7.diff(P.pkcs7.fill(1n+p1, B.byte(U32.from_nat(1n+p1))), B.byte(U32.from_nat(1n+p1)), 0), 0, pk.diff_fill(1n+p1, U32.from_nat(1n+p1))) : {pk.k2(bs, B.Octets.append(m, pk.pad(p1)), 1n+Nat.add(B.Octets.len(m), p1), 1n+p1, True{}, _) == Done{m} : Result<&2, &2, M.CmError, B.Octets>}
1356  # so the first L bytes are kept
1357  %Equal.sym(Nat, Nat.sub(Nat.add(B.Octets.len(m), p1), p1), B.Octets.len(m), el) : {Done{B.Octets.take(_, B.Octets.append(m, pk.pad(p1)))} == Done{m} : Result<&2, &2, M.CmError, B.Octets>}
1358  %Equal.sym(B.Octets, B.Octets.take(B.Octets.len(m), B.Octets.append(m, pk.pad(p1))), m, BL.octets_take_append(m, pk.pad(p1))) : {Done{_} == Done{m} : Result<&2, &2, M.CmError, B.Octets>}
1359  {==}