feat(lean): preliminary core model extraction

[abentkamp]

This PR adds an option to core-models/hax.sh to extract Lean code from Core models. It is able to generate a Lean file that compiles.

To make the extraction work, I currently must exclude some functions and do some text replacements using sed (see hax.sh). This is due to the following issues:

• [Lean] Extend support for associated types #1710
• [Lean] Items in recursive modules do not get ordered correctly #1823
• [Lean] Ensure that generated spec lemmas are communicated to mvcgen #1818
• [Lean] self_ vs self #1852
• Rust Engine: Name Rendering: support GlobalId suffixes #1646
• [Lean] Reserved keywords get escaped only sometimes #1853

Moreover, the following points should be improved in future PRs:

• The types i128 and u128 should get a proper implementation ([Lean] Create u128 and i128 types #1854)
• I have deactivated spec generation for opaque definitions here, but they should instead get an axiomatized spec. ([Lean] Axiomatize spec when using hax_lib::opaque #1847)
• == should be rendered == ([Lean] Render Rust's == as == in Lean #1845)

This PR lets us produce a compiling Lean file, but the file is not part of this PR. This is because the generated items are all in the namespace Core_models, whereas extracted Code references Core. So we cannot use the file just yet. In a future PR, I plan to make extraction generate references to the Core_models namespace whenever extracting something that is not Core models itself. (#1855)

[skip changelog]