Update the Charon pin to latest and delete scripts/charon-patch.diff #4834

Summary

The pinned Charon (b250680a, the commit #4714 landed as v0.1.91) is 2,151 commits behind upstream. Bringing it current would let us delete scripts/charon-patch.diff and the "Patch Charon" CI step entirely — the endgame #4714 described — but the Charon AST has been reorganised underneath kani-compiler/src/codegen_aeneas_llbc, so the bump is a real migration rather than a pointer change.

I measured all of this on top of the nightly-2026-09-22 toolchain bump (#4833).

What "latest" is

Charon retired the v0.1.x tags and now tags per release date. There are 133 such tags:

So there is no gentle increment left: the smallest available checkpoint is 1,414 commits away, and the newest is 2,151. The incremental strategy used for v0.1.68 → v0.1.91 (#4657, #4660, #4669, #4684, #4686, #4696, #4699, #4702, #4714) is no longer available, which argues for going straight to the newest tag.

Note that every recent Charon, main included, pins rustc nightly-2026-09-17 for itself — the tag dates are release dates, not the rustc nightly they track.

The patch file can go

With the submodule checked out at nightly-2026.09.23 and no patch applied, Charon compiles clean against nightly-2026-09-22:

• it no longer uses box_patterns (the only thing Update toolchain to nightly-2026-09-22 #4833 had to add to the patch)
• Bug: Dependency resolution fails for annotate-snippets AeneasVerif/charon#806, the dependency-resolution bug the llbc-regression workflow comment names as the blocker, was closed on 2025-09-08

So this bump should delete scripts/charon-patch.diff, drop the "Patch Charon" step from .github/workflows/kani.yml, and remove the stale comment above it.

What the migration costs

All 136 build errors are on Kani's side, in the 2,525 lines of codegen_aeneas_llbc (mir_to_ullbc/mod.rs alone is 2,064). Not a scattering of fixups — the AST moved:

• ast/ split into bodies/, items/, krate.rs, meta/, type_level/; most of our import paths no longer resolve
• ids::Vector → ids::IndexVec
• RawStatement → StatementKind, RawTerminator → TerminatorKind
• 37 enum variants renamed or re-shaped (E0599), 34 struct fields renamed (E0560), 15 constructor arity changes (E0061), 10 initializers missing new fields (E0063)
• TranslateOptions fields (monomorphize, no_ops_to_function_calls, no_merge_goto_chains, remove_associated_types) gone
• TraitDecl lost parent_clauses, type_clauses, const_defaults
• the pass registry changed: no ULLBC_PASSES, LLBC_PASSES, or transform::reorder_decls
• errors::Level variants renamed again

Expect the count to grow as imports are fixed and later errors stop being masked.

The risk worth planning around: mir_to_ullbc translates MIR into Charon's ULLBC, and a mechanical rename can silently change meaning. Only the 10 tests in tests/llbc would notice, so each chunk wants its own reasoning about semantics rather than a compile-clean signal.

Suggested shape of the work

1. Bump the submodule to nightly-2026.09.23, delete scripts/charon-patch.diff, drop the CI patch step, refresh Cargo.lock.
2. Imports and pure renames (IndexVec, StatementKind/TerminatorKind, module paths) — mechanical, gets the error count down to the genuine redesigns.
3. The redesigns: TranslateOptions, TraitDecl's clause/const layout, the pass registry. These need reading Charon's new intent, not pattern-matching on the old code.
4. tests/llbc green (10 tests), then scripts/kani-llbc-regression.sh.

Worth keeping each step a separate commit — the diff will be large and otherwise unreviewable.