Program translation IR

[xldenis]

I'm introducing an IR in the translation of program code which is non-why3 specific. It serves a few purposes:

• Isolating the rest of Creusot from rustc's changes
• Making our translation independent from why3-isms
• It will allow us to push the whole cloning business down the pipeline and I have some ideas to dramatically simplify it
  • This should make the translation itself significantly simpler to understand both the MIR->IR one and the IR->MLCFG one.
• Opens the door to performing transformations and cleanup in Creusot to help out why3

This is far from finished but I'm already starting to see opportunities for clean up and simplification appearing.

[xldenis]

I'm moving towards merging this despite the work being unfinished, in particular constants still use the 'escape hatch', as this continually conflicts with any other change. There's also plenty further work to do cleaning up both the 'FMIR' (Functional MIR) and both the MIR -> FMIR and FMIR -> Creusot lowerings.