secp256k1: Add field64 proofs.

[davecgh]

This adds formal verification proofs of the arithmetic in the new field64 implementation using the Z3 theorem prover along with a new directory to house all such proofs and an associated README.md to describe its contents.

It includes formal proofs for the following:

• 512-bit multiplication with saturated 64-bit limbs
• 512-bit squaring with saturated 64-bit limbs
• 512-bit modular reduction over the field prime saturated 64-bit limbs

---

Theorem prover output:

$ python internal/proofs/mul512_4x64_prover.py
discarded carry 0 != 0: unsat
discarded carry 1 != 0: unsat
discarded carry 2 != 0: unsat
discarded carry 3 != 0: unsat
discarded carry 4 != 0: unsat
discarded carry 5 != 0: unsat
discarded carry 6 != 0: unsat
top limb after row 0 > 2**64-2: unsat
limb 5 after row 1 > 2**64-2: unsat
limb 5 after row 2 > 2**64-2: unsat
limb 5 after row 3 > 2**64-2: unsat

$ python internal/proofs/square512_4x64_prover.py
discarded carry 0 != 0: unsat
discarded carry 1 != 0: unsat
discarded carry 2 != 0: unsat
discarded carry 3 != 0: unsat

$ python internal/proofs/field_4x64_reduce_prover.py
discarded carry 0 != 0: unsat
discarded carry 1 != 0: unsat
discarded carry 2 != 0: unsat
top limb after 1st reduction > complement: unsat
value after 2nd reduction >= 2p: unsat
fully reduced result >= prime: unsat