1	import Base
2	import ../lib/common.bend as C
3	
4	# Specification of the Poly1305 one-time authenticator (RFC 8439 section
5	# 2.5), transcribed from the RFC's pseudocode over natural numbers. Nothing
6	# is shared with the implementation (src/crypto/poly1305/): the accumulator
7	# is one Nat reduced mod p = 2^130 - 5 after every block, as in HACL*'s
8	# Spec.Poly1305. Numbers are little-endian byte strings; a byte is the low 8
9	# bits of a U32. Multiplication by 256 is written C.shift(8n, x) (eight
10	# doublings, spec/lib/common.bend).
11	#
12	# The proof checker expands a closed Nat in unary, so 2^130 is never formed
13	# (as spec/math/w64.bend never forms 2^64): "x mod p" is modp(x) below, which
14	# uses only 2^130 = p + 5 through C.low / C.high (k halvings). That modp(x)
15	# is Nat.mod(x, 2^130 - 5) is proved for every x in
16	# proofs/crypto/poly1305/modp.bend (law modp_mod, stated with 2^130 written
17	# C.shift(130n, one) for a variable one = 1). p() below is the constant,
18	# for the reader; no proof unfolds it.
19	#
20	# Bend's native runtime keeps a Nat below 2^48, so this specification is a
21	# proof object; tools/check_poly1305.py runs a line-by-line mirror of it.
22	
23	# p = 2^130 - 5
24	def p() -> Nat:
25	  Nat.sub(C.pow2(130n), 5n)
26	
27	# x = lo + 2^130 hi is congruent to lo + 5 hi mod p (2^130 = p + 5); the fold
28	# strictly decreases x while hi > 0, so x folds bring x below 2^130.
29	def fold(+x: Nat) -> Nat:
30	  Nat.add(C.low(130n, x), Nat.mul(C.high(130n, x), 5n))
31	
32	def folds(n: Nat, x: Nat) -> Nat:
33	  match n:
34	    case 0n: x
35	    case 1n+k: folds(k, fold(x))
36	
37	def pick(b: Bool, x: Nat, y: Nat) -> Nat:
38	  match b:
39	    case True{}: x
40	    case False{}: y
41	
42	# y < 2^130: y itself when y < p, else y - p = (y + 5) - 2^130.
43	def canon(+y: Nat) -> Nat:
44	  match y:
45	    case 0n: 0n
46	    case 1n+z: pick(C.fits(130n, Nat.add(1n+z, 5n)), 1n+z, C.low(130n, Nat.add(1n+z, 5n)))
47	
48	# x mod p
49	def modp(+x: Nat) -> Nat:
50	  canon(folds(x, x))
51	
52	# le_bytes_to_num
53	def le_num(bytes: List<&2, U32>) -> Nat:
54	  match bytes:
55	    case Nil{}: 0n
56	    case b <> rest: Nat.add(U32.to_nat(U32.and(b, 255)), C.shift(8n, le_num(rest)))
57	
58	# num_to_n_le_bytes: the low n bytes of x.
59	def le_bytes(n: Nat, +x: Nat) -> List<&2, U32>:
60	  match n:
61	    case 0n: Nil{}
62	    case 1n+k: U32.from_nat(C.low(8n, x)) <> le_bytes(k, C.high(8n, x))
63	
64	def prefix(n: Nat, xs: List<&2, U32>) -> List<&2, U32>:
65	  match n xs:
66	    case 0n _: Nil{}
67	    case 1n+k Nil{}: Nil{}
68	    case 1n+k x <> rest: x <> prefix(k, rest)
69	
70	def suffix(n: Nat, xs: List<&2, U32>) -> List<&2, U32>:
71	  match n xs:
72	    case 0n _: xs
73	    case 1n+k Nil{}: Nil{}
74	    case 1n+k x <> rest: suffix(k, rest)
75	
76	# clamp(r): r &= 0x0ffffffc0ffffffc0ffffffc0fffffff, i.e. r[3], r[7], r[11]
77	# and r[15] keep their low four bits, r[4], r[8] and r[12] lose their low two.
78	def clamp_mask(i: Nat) -> U32:
79	  match i:
80	    case 3n: 15
81	    case 7n: 15
82	    case 11n: 15
83	    case 15n: 15
84	    case 4n: 252
85	    case 8n: 252
86	    case 12n: 252
87	    case _: 255
88	
89	def clamp_from(r: List<&2, U32>, +i: Nat) -> List<&2, U32>:
90	  match r:
91	    case Nil{}: Nil{}
92	    case b <> rest: U32.and(b, clamp_mask(i)) <> clamp_from(rest, 1n+i)
93	
94	def clamp(r: List<&2, U32>) -> List<&2, U32>:
95	  clamp_from(r, 0n)
96	
97	# The message cut into 16-byte blocks, the last one possibly shorter; fuel
98	# bounds the number of blocks (the length of the message is enough).
99	def blocks(fuel: Nat, +msg: List<&2, U32>) -> List<&2, List<&2, U32>>:
100	  match fuel msg:
101	    case 0n _: Nil{}
102	    case 1n+k Nil{}: Nil{}
103	    case 1n+k b <> rest: prefix(16n, b <> rest) <> blocks(k, suffix(16n, b <> rest))
104	
105	# for each block: n = le_bytes_to_num(block | [0x01]); a += n; a = (r * a) % p
106	def absorb(bs: List<&2, List<&2, U32>>, +r: Nat, a: Nat) -> Nat:
107	  match bs:
108	    case Nil{}: a
109	    case b <> rest:
110	      +n = le_num(List.append(&2, U32, b, [1]))
111	      absorb(rest, r, modp(Nat.mul(r, Nat.add(a, n))))
112	
113	# poly1305_mac(msg, key): r = clamp(key[0..16]), s = key[16..32];
114	# a = 0, absorb every block, a += s; the tag is num_to_16_le_bytes(a).
115	def poly1305_mac(+key: List<&2, U32>, +msg: List<&2, U32>) -> List<&2, U32>:
116	  +r = le_num(clamp(prefix(16n, key)))
117	  +s = le_num(prefix(16n, suffix(16n, key)))
118	  le_bytes(16n, Nat.add(absorb(blocks(List.length(&2, U32, msg), msg), r, 0n), s))
119	
120	# The same function, split on the message first so that a proof about an
121	# unknown message does not unfold it.
122	def mac(+key: List<&2, U32>, +msg: List<&2, U32>) -> List<&2, U32>:
123	  match msg:
124	    case Nil{}: poly1305_mac(key, [])
125	    case b <> rest: poly1305_mac(key, b <> rest)
126	
127	# ---------------------------------------------------------------- the polynomial
128	
129	# RFC 8439 2.5 describes the accumulator as the evaluation, at r and
130	# modulo p, of the polynomial whose coefficients are the blocks (each with
131	# its 0x01 byte): with q blocks n_1 .. n_q,
132	#   poly(r) = n_1 r^q + n_2 r^(q-1) + ... + n_q r
133	# (as Spec.Poly1305 in HACL* and the field statements of Mathlib's ZMod p).
134	# Clause absorb_poly (proofs/crypto/poly1305/poly.bend) proves
135	# absorb(blocks, r, 0) == poly(blocks, r) mod (2^130 - 5).
136	def coeff(b: List<&2, U32>) -> Nat:
137	  le_num(List.append(&2, U32, b, [1]))
138	
139	def poly(+bs: List<&2, List<&2, U32>>, +r: Nat) -> Nat:
140	  match bs:
141	    case Nil{}: 0n
142	    case b <> rest: Nat.add(Nat.mul(coeff(b), Nat.pow(r, 1n+List.length(&2, List<&2, U32>, rest))), poly(rest, r))