1	import Base
2	import ./limbs.bend as L
3	import ../subtle.bend as Subtle
4	
5	# Poly1305 (RFC 8439 section 2.5) over byte lists, on radix-2^8 limbs
6	# (src/crypto/poly1305/limbs.bend). A byte is the low 8 bits of a U32. The
7	# key is r || s (32 bytes); mac reads missing key bytes as absent (zero), the
8	# checked poly1305 returns None unless the key has exactly 32 bytes.
9	# proofs/crypto/poly1305/ proves mac equal to spec/crypto/poly1305.bend for
10	# every key and message.
11	
12	def mask(xs: List<&2, U32>) -> List<&2, U32>:
13	  match xs:
14	    case Nil{}: Nil{}
15	    case x <> t: U32.and(x, 255) <> mask(t)
16	
17	# r &= 0x0ffffffc0ffffffc0ffffffc0fffffff, byte by byte.
18	def clamp_mask(i: Nat) -> U32:
19	  match i:
20	    case 3n: 15
21	    case 7n: 15
22	    case 11n: 15
23	    case 15n: 15
24	    case 4n: 252
25	    case 8n: 252
26	    case 12n: 252
27	    case _: 255
28	
29	def clamp(r: List<&2, U32>, +i: Nat) -> List<&2, U32>:
30	  match r:
31	    case Nil{}: Nil{}
32	    case b <> rest: U32.and(b, clamp_mask(i)) <> clamp(rest, 1n+i)
33	
34	# A message block as limbs: its bytes, then the 0x01 byte.
35	def load(b: List<&2, U32>) -> List<&2, U32>:
36	  mask(List.append(&2, U32, b, [1]))
37	
38	# The accumulator over 16-byte blocks (the last one possibly shorter); fuel
39	# bounds the number of blocks. (A one-byte message is its own case only so
40	# that a proof about a message b <> rest with rest unknown stays small.)
41	def absorb(fuel: Nat, +msg: List<&2, U32>, +r: List<&2, U32>, h: List<&2, U32>) -> List<&2, U32>:
42	  match fuel msg:
43	    case 0n _: h
44	    case 1n+k Nil{}: h
45	    case 1n+k b <> Nil{}:
46	      absorb(k, L.skip(16n, [b]), r, L.block(r, h, load(L.take(16n, [b]))))
47	    case 1n+k b <> c <> rest:
48	      absorb(k, L.skip(16n, b <> c <> rest), r, L.block(r, h, load(L.take(16n, b <> c <> rest))))
49	
50	def zero() -> List<&2, U32>:
51	  [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
52	
53	# r = clamp(key[0..16]) and s = key[16..32], as limbs.
54	def r_key(+key: List<&2, U32>) -> List<&2, U32>:
55	  L.fit(16n, mask(clamp(L.take(16n, key), 0n)))
56	
57	def s_key(+key: List<&2, U32>) -> List<&2, U32>:
58	  mask(L.take(16n, L.skip(16n, key)))
59	
60	def tag(+key: List<&2, U32>, +msg: List<&2, U32>) -> List<&2, U32>:
61	  +r = r_key(key)
62	  +s = s_key(key)
63	  +h = absorb(List.length(&2, U32, msg), msg, r, zero())
64	  L.fin(h, s)
65	
66	# The 16-byte tag of msg under key = r || s. (The match on msg only keeps a
67	# proof's goal small while msg is unknown; both arms are the same.)
68	def mac(+key: List<&2, U32>, +msg: List<&2, U32>) -> List<&2, U32>:
69	  match msg:
70	    case Nil{}: tag(key, [])
71	    case b <> rest: tag(key, b <> rest)
72	
73	def has_key(+key: List<&2, U32>) -> Bool:
74	  Nat.is_eq(List.length(&2, U32, key), 32n)
75	
76	def when(ok: Bool, x: List<&2, U32>) -> Maybe<&2, List<&2, U32>>:
77	  match ok:
78	    case True{}: Some{x}
79	    case False{}: None{}
80	
81	# The tag, or None unless the key has 32 bytes.
82	def poly1305(+key: List<&2, U32>, +msg: List<&2, U32>) -> Maybe<&2, List<&2, U32>>:
83	  when(has_key(key), mac(key, msg))
84	
85	# True exactly when the key has 32 bytes and tag is the tag of msg; the tags
86	# are compared in constant time (src/crypto/subtle.bend).
87	def verify(+key: List<&2, U32>, +msg: List<&2, U32>, +tag: List<&2, U32>) -> Bool:
88	  Bool.and(has_key(key), Subtle.eq(mac(key, msg), tag))