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?