ir for multi-precision arithmetic

[mmcloughlin]

In order to support more elaborate optimizations for the underlying multi-precision arithmetic, it might help to introduce a simpler "generic assembly" precisely for this purpose. Rather than manipulating avo functions, this would instead be a small RTL (Register Transfer Language) with the smallest instruction set possible to implement routines like Montgomery Multiplication. Benefits:

• Simpler to manipulate and analyze than avo.
• Close to the machine, but still possible to generate other languages from, for example pure Go with math/bits intrinsics or even assembly for other architectures. #103
• Consider applying SMT techniques and z3 to verify correctness. #99 #101

Related #46 #95 #49

[mmcloughlin]

z3 bindings in Go:

• https://github.com/aclements/go-z3
• https://github.com/mitchellh/go-z3
• https://github.com/benbjohnson/glee/tree/master/z3
• https://github.com/skorobogatov/z3
• https://github.com/akreuzer/z3go/

Useful C API examples: https://github.com/Z3Prover/z3/blob/71d68b8fe082b5efb8cf9990e7275b3b97acbb62/examples/c/test_capi.c

Migrating to #99