Add simple limb overflow checker for Poly1305

Add simple limb overflow checker for Poly1305

Monocypher now grabs at the graal of Formal Verification.

It is very crude, but it works for Poly1305.  Just transliterate the C
program into Python, add some preconditions and asserts, and execute the
result as Python to prove the absence of overflow (provided the
preconditions are correct).

ECC code might be more difficult, we'll see.

See #246