Tracking Issue: Address follow-up comments on #3514 (LLBC Backend)

[zhassan-aws]

This is a tracking issue for addressing the comments on #3514.

• [x] Use "Lean" instead of "Aeneas" for any user-visible feature
• [x] Upgrade Charon to a more recent commit
• [ ] Once we start calling Aeneas in the Kani driver, the driver should automatically delete the .llbc files
• [ ] Clean-up the handling of names
• [ ] Use "public functions" mode as opposed to "harness" mode
• [ ] Minimize code duplication between goto compiler interface and llbc compiler interface
• [ ] Generate generic code (using CrateItem) instead of monomorphized code (that uses Instance)

[ssyram]

Hi, I appreciate your work very much but am personally curious about what is the intended difference between your work and Charon? I think you are both converting / exporting Rust codes to LLBC?

[zhassan-aws]

Hi @ssyram. We wanted to add the ability to export LLBC in Kani to allow interaction with the CBMC backend, e.g. through function contracts (which Kani supports).

[ssyram]

Thanks for this! From my understanding, the codegen of LLBC is parallel to the GOTO format -- the codegen either generates GOTO to be put into CBMC or LLBC. Am I correct? And where will the interaction happen and how is it supposed to happen?

[zhassan-aws]

Correct. The plan was for the interaction to be via function contracts where the CBMC backend is used for lower-level functions (e.g with unsafe) and LLBC is used higher up.