Lean verification code generator

[yoavseginer]

When a libfunc test is run and the Lean generator is turned on, Lean code is generated which can be used to verify the correctness (soundness and completeness) of the libfunc. The Lean code is generated into files in a separate verification directory.

All code for the Lean generator is behind the 'lean' compilation feature. Moreover, having compiled the cairo compiler with the 'lean' feature, one must also set the CAIRO_GEN_LEAN environment flag to generate the Lean code (this may be redundant and can easily be removed).

The Lean generator code has two main components: one (mainly inside the Casm builder) collects auxiliary information during the build process, which is later needed by the Lean generator. The generation of the Lean code then takes place after the test was completed, and is implemented in a separate crate. Some small changes had to be introduced to the compiler and test code to allow the auxiliary information collected in the builder to reach the Lean generator.

Finally, a few libfunc tests were added (in u256 and u512). The tests modify existing tests by not destroying the U128MulGuarantees returned by the core libfunc. In this way the Lean proof only verifies the core functionality.

[reviewable-StarkWare]

This change is 

[yoavseginer]

I see that some checks fail, something about a mismatch between the command number and crate number. I indeed added a new crate, so I probably should have added something additional somewhere, but I don't know where.