;;; -*-conf-windows-*-
;;;
;;; Primality proof for Poly1305.
;;;
;;; This is exactly the proof of Theorem 3.1 from Daniel J. Bernstein, `The
;;; Poly1305-AES message-authentication code'.

sievebits 32

small a = 37003
small b = 221101

pock p2 = 2, 245965590, [a, b]
pock p1 = 2, 111445310351, [p2]
pock 2p130m5 = 2, 758657323, [p1]
check 2p130m5, 130, 1361129467683753853853498429727072845819