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

[zhassan-aws]

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

• Use "Lean" instead of "Aeneas" for any user-visible feature
• 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.

[feliperodri]

Status update from the Charon bump (#4834), which touched several of these. Nothing is merged yet, so I'm not ticking boxes:

• Upgrade Charon to a more recent commit — Move the Charon pin to current and drop the patch machinery #4883 moves the pin to current (nightly-2026.09.26) and drops charon-patch.diff. It's stacked on LLBC: translate wrapping arithmetic as wrapping, and cover what the Charon bump will touch #4881 (LLBC test coverage, plus a fix for wrapping arithmetic) and LLBC: name inherent methods instead of aborting, and deduplicate the name builders #4882, and Build and lint the LLBC backend with warnings denied in its CI job #4886 adds a lint gate so the backend can't quietly rot again.
• Clean up the handling of names — partly done in LLBC: name inherent methods instead of aborting, and deduplicate the name builders #4882: the three copies of the path-to-name walker are now one, and calling any inherent method no longer aborts the compiler. What's left is adopting Charon's {impl} path elements instead of the type-suffix scheme: LLBC: name methods with Charon's impl path elements instead of a type suffix #4884.
• Minimize duplication with the goto interface — Move the Charon pin to current and drop the patch machinery #4883 stops duplicating Charon (options and pass list now come from Charon itself). The duplication with the CBMC compiler_interface is unchanged.
• Public-functions mode — the compiler side already exists; the driver never selects it for -Zlean. Making it the default changes what -Zlean translates and means rewriting the tests/llbc harnesses, so I'd like a decision on that before sending a PR.
• Delete the .llbc files once the driver calls Aeneas — still blocked; the driver doesn't call Aeneas yet.
• Generic instead of monomorphized code — unchanged, and more visible now: Move the Charon pin to current and drop the patch machinery #4883's output shows a generic signature over a monomorphic body (e.g. drop glue types in option).

Separately, #4885 lists the constructs that still stop at the backend's own todo!()s (casts, arrays, slices, str, Box, …).