1	import Base
2	import ../../../spec/lib/common.bend as C
3	import ../../../src/crypto/poly1305/poly1305.bend as P
4	import ../../../spec/crypto/poly1305.bend as R
5	
6	# The Poly1305 clauses (proved in proof.bend).
7	
8	# The implementation's tag is the RFC 8439 tag, for every key and message
9	# (keys of other lengths than 32 included: both read missing bytes as absent).
10	law mac_correct:
11	  for +key: List<&2, U32>
12	  for +msg: List<&2, U32>
13	  {P.mac(key, msg) == R.mac(key, msg) : List<&2, U32>}
14	
15	# The tag has 16 bytes.
16	law mac_length:
17	  for +key: List<&2, U32>
18	  for +msg: List<&2, U32>
19	  {List.length(&2, U32, R.mac(key, msg)) == 16n : Nat}
20	
21	# The specification's reduction is x mod (2^130 - 5), for every x
22	# (2^130 written C.shift(130n, one) with one == 1, as the checker would
23	# expand a closed 2^130 in unary).
24	law modp_mod:
25	  for +one: Nat
26	  for +h1: {one == 1n : Nat}
27	  for +x: Nat
28	  {R.modp(x) == Nat.mod(x, Nat.sub(C.shift(130n, one), 5n)) : Nat}
29	
30	# The checked API: the tag for a 32-byte key, None for any other length.
31	law poly1305_valid:
32	  for +key: List<&2, U32>
33	  for +msg: List<&2, U32>
34	  for +h: {Nat.is_eq(List.length(&2, U32, key), 32n) == True{} : Bool}
35	  {P.poly1305(key, msg) == Some{R.mac(key, msg)} : Maybe<&2, List<&2, U32>>}
36	
37	law poly1305_invalid:
38	  for +key: List<&2, U32>
39	  for +msg: List<&2, U32>
40	  for +h: {Nat.is_eq(List.length(&2, U32, key), 32n) == False{} : Bool}
41	  {P.poly1305(key, msg) == None{} : Maybe<&2, List<&2, U32>>}
42	
43	# verify accepts the RFC tag under a 32-byte key ...
44	law verify_accepts:
45	  for +key: List<&2, U32>
46	  for +msg: List<&2, U32>
47	  for +h: {Nat.is_eq(List.length(&2, U32, key), 32n) == True{} : Bool}
48	  {P.verify(key, msg, R.mac(key, msg)) == True{} : Bool}
49	
50	# ... and rejects every other tag.
51	law verify_rejects:
52	  for +key: List<&2, U32>
53	  for +msg: List<&2, U32>
54	  for +tag: List<&2, U32>
55	  for h: {tag != R.mac(key, msg) : List<&2, U32>}
56	  {P.verify(key, msg, tag) == False{} : Bool}
57	
58	# The RFC's polynomial reading of the accumulator: absorbing the blocks
59	# (reducing after every block) is evaluating the polynomial of the blocks at
60	# r and reducing once mod 2^130 - 5 (2^130 written C.shift(130n, one)).
61	law absorb_poly:
62	  for +one: Nat
63	  for +h1: {one == 1n : Nat}
64	  for +bs: List<&2, List<&2, U32>>
65	  for +r: Nat
66	  {R.absorb(bs, r, 0n) == Nat.mod(R.poly(bs, r), Nat.sub(C.shift(130n, one), 5n)) : Nat}
67	
68	# Hence the tag: ((poly(blocks, r) mod p) + s) mod 2^128, as 16 little-endian
69	# bytes, with r the clamped first half of the key and s the second half.
70	law mac_poly:
71	  for +one: Nat
72	  for +h1: {one == 1n : Nat}
73	  for +key: List<&2, U32>
74	  for +msg: List<&2, U32>
75	  {R.poly1305_mac(key, msg) == R.le_bytes(16n, Nat.add(Nat.mod(R.poly(R.blocks(List.length(&2, U32, msg), msg), R.le_num(R.clamp(R.prefix(16n, key)))), Nat.sub(C.shift(130n, one), 5n)), R.le_num(R.prefix(16n, R.suffix(16n, key))))) : List<&2, U32>}