Factor generated code by module

Currently we generate one huge blob of code and specs for a crate. It would be better to factor this by Rust module, so that we don't have to regenerate/reprove everything when we change one function.

TODO:

• check if we can easily manage interdependencies. Are Rust rules on dependencies between modules compatible with Coq's rules?