1	# Laws of PKCS #7 padding (pkcs7.bend), for every block size and message:
2	# unpadding undoes padding, and padding gives a whole number of blocks; and
3	# RFC 5652's padding examples, with the refusals of bad padding. The proofs
4	# rest on bytes' and u32's laws only.
5	import Base
6	import bend-osdev-bytes@0.1.1.0/bytes.bend as B
7	import bend-osdev-mode-core@0.1.0.0/mode_core.bend as M
8	import ./pkcs7.bend as P
9	
10	# Unpadding undoes padding, for every block size bs and message m: when bs
11	# is one the padding takes (1 to 255), unpad(pad(m)) is m; when it is not,
12	# both refuse alike (CmBadBlockSize)
13	law pkcs7_round_trip:
14	  for +bs: Nat
15	  for +m: B.Octets
16	  {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>}
17	
18	# A padded message is a whole number of blocks, for every block size and
19	# message
20	law pkcs7_pad_blocks:
21	  for +bs: Nat
22	  for +m: B.Octets
23	  {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>}
24	
25	# PKCS #7 (RFC 5652, 6.3): the empty message becomes a whole block of 16s; 15 bytes gain one 1
26	law pkcs7_pad_empty:
27	  {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>}
28	
29	law pkcs7_pad_15:
30	  {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>}
31	
32	law pkcs7_unpad_15:
33	  {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>}
34	
35	# a last byte of 0, or one the bytes before it contradict, is bad padding
36	law pkcs7_unpad_zero:
37	  {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>}
38	
39	law pkcs7_unpad_mixed:
40	  {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>}