Core-models compatibility tool

[maximebuyse]

This PR introduces a tool that given a crate, checks if it can be verified using the core-models aeneas library.

The basic idea is to compare the core/alloc items that the crate uses to the ones we provide. charon exports a list of external names used by a crate which can be convenient for that. I tried 3 approaches:

• Compare at the rust level using the llbc. This is wrong because it misses the hand-written lean, and some names don't match well because of the tricks we use.
• List the names in our lean library (lean level), take the external names used by the crate in hte llbc, convert these names to lean names using the aeneas naming conventions. Then compare the lists. This approach gives a lot of false positives (crate for which the tool says some core items are not covered by our lib even though our lib covers what is needed) because aeneas simplifies between llbc and lean, so a lot of external names form core that appear in the llbc are not in the lean produced by aeneas.
• Compare at the lean level. This is the approach in this PR which avoids the issues of the other approaches. I am not entirely satisfied though because it relies on a custom python extraction of the names in the lean file as no standard lean tool seems to be able to do what we need here. Also this approach doesn't have a lot of added value compared to just trying to extract the lean and then to type-check it, the main advantage is de-duplication of missing definition errors.