HOL-Light/Autogen: Autogenerate zeta tables inside HOL-Light specs

[hanno-becker]

The HOL-Light specs for NTT, invNTT, and the mulcache computation all embed large arrays of constants into their specifications.

We should autogenerate those constants through autogen -- ideally in such a way that there's only a single core routine generating an array of integers, and multiple formatting routines exporting them to .ml / .c. This way, it's most apparent that the tables are indeed the same in spec and code.