Lean version of Aeneas library

Stream: Program verification

[Oliver Butterley]

The Lean library of Aeneas is currently lean4:v4.21.0, I'm guessing there are plans to update it to a more recent version of Lean? Can I help with this process? I'm eager to verify Rust code taking advantage of some of the more recent additions to Lean. @Son Ho

[Son Ho]

Yes, I wanted to update it but have been busy with other things (I just came back from two weeks of vacations and I'm now focusing on on improving the subset supported by the translation). Don't hesitate to give it a try and open a PR: the only blocking thing that I will have to test on my side is whether the CI for SymCrypt still works (this is internal to Microsoft for now).

[Son Ho]

As a side note: working on the translation will keep me busy for a while, but after that I would like to update scalar_tac and progress to leverage grind - updating to a more recent version of Lean should definitely help in that regard.