The prover, when run on recent sage versions, failed to prove some of its
goals due to a change in sage. This commit adapts our code accordingly.
The prover passes again after this commit.
Python 3 often returns iterable map objects where Python 2 returned
list. We can just them down to lists explicitly.
Overlooked in 13c88efed0005eb6745a222963ee74564054eafb.
This enables testing overflow is correctly encoded in the recid, and
likely triggers more edge cases.
Also introduce a Sage script to generate the parameters.
