Lean core-lib tests

[maximebuyse]

This PR adds a new test framework allowing to check that the lean core library behaves like it is supposed to.

The tests are defined in rust, checking that a call to a core function's result with concrete params gives the expected concrete value. The rust is tested to validate that the expected values correspond to the behaviour of rust core. The tests are also translated to lean with aeneas, and checked in lean.

This should validate:

• That the core models defined in Rust are correctly translated by Aeneas
• That the manual lean definitions are correct (for primitives or temporary workarounds when aeneas can't extract some rust models)

[abentkamp]

This is great! Do we still need the client_test? Doesn't the new test cover both clean extraction and equivalence to Rust?

[abentkamp]

And what's going wrong with closure extraction? Sometimes move || ... instead of || ... works better for Aeneas.

[maximebuyse]

This is great! Do we still need the client_test? Doesn't the new test cover both clean extraction and equivalence to Rust?

I like the idea of testing in the same conditions as a user of the library, but it is true that for now the equivalence tests probably covers everything (and more) that the client-test covers. Anyway more tests is not a bad thing, and in the future we might want to add some proofs in client-test which would make it different. So I'd say we keep it.

[maximebuyse]

And what's going wrong with closure extraction? Sometimes move || ... instead of || ... works better for Aeneas.

I re-activated some of these tests, and added more precise reasons for those that still need to be de-activated.

[abentkamp]

Cool, thanks!