Move the Charon pin to current and drop the patch machinery by feliperodri · Pull Request #4883 · model-checking/kani

feliperodri · 2026-09-27T19:17:54Z

Rebased onto main after #4881 and #4882 merged. Nine commits: five for the bump itself (from cbd1e83c7) and four follow-ups (see "Follow-ups" below). They're split so each can be read on its own.

Resolves #4834: Charon goes from a commit 2,176 commits old to nightly-2026.09.29, and scripts/charon-patch.diff, the CI step that applied it, and the workspace [patch] for its git dependency all go away. Charon itself builds unpatched on our toolchain.

Why it's shaped this way

Every past Charon bump broke Kani because we hand-copied Charon's option defaults and its list of passes. Charon now exposes both, so the LLBC backend configures Charon exactly as charon --preset aeneas does and runs run_transformation_passes after our own MIR-to-ULLBC step. That deletes about 90 lines, and the next bump should be mostly renames.

For the translation itself, wherever the AST was redesigned rather than renamed, I copied what Charon's own MIR translator emits instead of inventing a mapping — the arithmetic overflow modes, assert kinds, switches, builtin types, drops. The commit message lists each one.

What the review should focus on

The risk the issue called out is a port that compiles but changes meaning. #4881 pinned the old output first, and I reviewed every changed expected file against its old version. The expected-file commit lists what changed; in short: formatting, names instead of @Adt0, and two deliberate refinements — unchecked_add overflow is now ub.+ rather than a panic (the old AST couldn't say UB), and drops name their glue type.

Three things I'd especially like eyes on, because each was a silent bug waiting to happen:

TypeDeclId::UNIT must be (). Every tuple points at id 0, and Charon's driver reserves it before anything else. Kani didn't, so without that tuples would have silently named whichever ADT got registered first. The tuple and projection tests now print (i32, i32) where that would show.
Asserts need their check_kind. We dropped the MIR assert message; the new reconstruct_fallible_operations only folds an overflow check into panic.+ when it knows which check it is. Without it, arith_checked quietly stops folding.
Charon now type-checks the translation, and it caught a real mismatch the old pin never checked: calls didn't pass the late-bound regions the callee declares. Calls now pass them as erased, from the same helper the declaration uses. A follow-up (f5c3d5139) makes the declarations themselves match Charon's numbering; see below.

Things I'd like input on

deny.toml (its own commit): swap four stale MPL exceptions for ustr (BSD-2-Clause-Patent), and ignore two "unmaintained" advisories (paste, atomic-polyfill) that only Charon pulls in. They're not vulnerabilities and the LLBC backend isn't in releases, but ignoring advisories is a policy call — happy to handle it differently.
Drops point at the glue Instance::resolve_drop_in_place returns, the core::ptr::drop_glue instance that drop_in_place::<T> wraps. Upstream reaches the glue through a proof for a synthetic Destruct::drop_glue method, which Kani doesn't model. If Aeneas specifically wants the trait form, that's a bigger follow-up.

Not in this PR

Charon's {impl} path naming (LLBC: name methods with Charon's impl path elements instead of a type suffix #4884): it isn't needed for Update the Charon pin to latest and delete scripts/charon-patch.diff #4834 and renames every method, so it is in Build and lint the LLBC backend with warnings denied in its CI job #4886 instead.
Arrays, slices, str literals, Box, casts, const generics, supertraits and associated consts still stop at Kani's own todo!()s — same as before, independent of Charon. Listed with reproducers in LLBC backend: constructs that still abort translation #4885.
Trait-clause proofs stay placeholders, as they were. both_none's output also shows Tracking Issue: Address follow-up comments on #3514 (LLBC Backend) #3585's generic-vs-monomorphized mismatch more visibly now (a generic signature over a monomorphic body) — pre-existing, not introduced here.

Follow-ups

f5c3d5139 declares generic parameters and regions the way Charon numbers them. Signatures with a reference that isn't a top-level &T input (Option<&u32>, &&u32, Holder<'_>), with a region used twice (pick<'a>(x: &'a u32, y: &'a u32)), with an early-bound region before a type parameter (fn f<'a, T: 'a>), or in an impl<'a> failed Charon's type check. Now all late-bound regions of the signature binder are declared once, after the early-bound ones; every parameter gets its per-kind position; the declared signature keeps its early-bound regions; and fn-pointer types bind their own regions. New test tests/llbc/regions.
817c2aa1f stops with an error ("Charon reported N error(s) while translating to LLBC") instead of the todo!() when Charon reports errors.
3a07dcfc0 fixes the drop-glue comment and removes an unused parameter.
c00ab4007 moves the pin to nightly-2026.09.29, which differs from nightly-2026.09.26 only in using the published serde_state_perfect_derive (Publish the serde_state fork to crates.io? AeneasVerif/charon#1486), so deny.toml no longer allows the serde_state git source.

tests/llbc 22/22, kani-llbc-regression.sh, kani 613, expected 478, ui 152, cargo-kani 71, unit tests with and without llbc, cargo deny --all-features, fmt, clippy.

feliperodri · 2026-09-28T18:43:47Z

Before merging: AeneasVerif/charon#1486 is resolved. The serde_state fork is now published as serde_state_perfect_derive (with a license field), and AeneasVerif/charon#1487 switches Charon to it. That change is a single commit (962e40b0) on top of the commit this PR pins (67da6d3b), with no API changes.

It isn't in a Charon tag yet — the latest, nightly-2026.09.28, still points at 67da6d3b. Once a tag includes it, this PR should move to that tag, which lets it:

drop the serde_state git allowlist entry from deny.toml (only tracing-tree stays), and the comment pointing at Clean up codegen_niche_literal #1486;
pick up the crates.io release in Cargo.lock;
lose the two no-license-field warnings from cargo deny.

No code change is needed on our side. I'll push that as one small commit and rerun cargo deny and the LLBC suite.

Charon at `nightly-2026.09.26` (67da6d3b, 2,176 commits past our pin) builds on our toolchain without any patch, so `scripts/charon-patch.diff`, the CI step that applied it, and the workspace `[patch]` that redirected Charon's `annotate-snippets` git dependency all go. That dependency is now a crates.io release. Charon picked up a new git dependency, `serde_state` (Nadrieril's fork, not the unrelated crates.io crate of that name), which `cargo deny` rejects; allow it next to `tracing-tree`. AeneasVerif/charon#1486 asks whether it can be published. The LLBC backend does not compile against this Charon yet; the following commits port it.

Kani kept its own copies of Charon's option defaults and of its list of transformation passes, and each Charon release changed both underneath it -- this Charon no longer has `ULLBC_PASSES`/`LLBC_PASSES`, a top-level `reorder_decls`, or most of the `TranslateOptions` fields we set. Charon now exposes the pieces its own driver uses. Build `CliOpts` with the `aeneas` preset (the configuration Aeneas consumes), derive `TranslateOptions` from it with `TranslateOptions::new`, and after Kani's own MIR-to-ULLBC translation run `run_transformation_passes`. That covers the opacity policy we hand-built -- `_` foreign, `crate` transparent, `Allocator` and its impls hidden -- and the LLBC printing the expected tests use, so all of it goes. The MIR level is no longer set: only Charon's own MIR fetcher reads it, and Kani translates the MIR it has already transformed.

The four MPL-2.0 exceptions (brownstone, colored, indent_write, nom-supreme) were for Charon dependencies that are gone; `ustr` (BSD-2-Clause-Patent) is new. Two new dependencies carry unmaintained-crate advisories: `paste` (RUSTSEC-2024-0436), used by Charon directly, and `atomic-polyfill` (RUSTSEC-2023-0089), via postcard -> heapless. Neither is a vulnerability, and both are only reached through the LLBC backend, which sits behind the `llbc` feature and is not part of Kani releases, so ignore them with that reason. `cargo deny --all-features --workspace check` passes.

Charon's AST was reorganised between our old pin and nightly-2026.09.26, and some of it was redesigned rather than renamed. The renames are mechanical; for every redesigned construct, this follows what Charon's own MIR translator (`bin/charon-driver/translate`) emits, since that is what the passes and Aeneas expect: - Arithmetic carries an overflow mode: MIR `Add`/`Sub`/`Mul`/shifts are `Wrap`, their `*Unchecked` forms and `Div`/`Rem` are `UB`, and `CheckedBinaryOp` is `AddChecked`/... (upstream's `translate_binaryop_kind`). - `Assert` is a terminator whose `check_kind` records the check. Kani dropped the MIR assert message; it is translated now, because `reconstruct_fallible_operations` only folds an overflow, bounds or division check into the operation it guards when it knows which check it is. - Constants are `ConstantExpr::new(kind, ty)`, with `Literal` and `ConstGeneric` merged into `ConstantExprKind`; integer values come from `IntegerValue::from_bits` instead of a hand-written table. - Switches are `SwitchData` plus a branch table, built as upstream does. - Builtin types are type declarations: tuples point at `TypeDeclId::UNIT`, `str` is the builtin `struct str { _0: [u8] }`, `Box` is tagged builtin. - Drops are terminators naming their drop glue. Upstream reaches it through a proof for its synthetic `Destruct::drop_glue`; Kani points at `drop_in_place::<T>`, which is that glue. - `TraitDecl` is built around associated items, `TraitRef` is hash-consed, and `FunDecl` holds the generics that used to be on the signature. Three things Charon's own driver sets up and Kani now does too: - `TypeDeclId::UNIT` must be the declaration of `()`. Every tuple points there, so without reserving it first, tuples silently named whichever ADT was registered first. - The target information, which `compute_layout_guarantees` requires. - `item_names`, which the printer and `compute_short_names` read; LLBC is now printed with item names instead of `@Adt0`/`@Fun1`. Charon now type-checks the translation, and it caught a mismatch that the old pin never checked: a function binds a region for each late-bound region of its reference inputs, but calls passed none. Calls now pass them as erased, as upstream does, from the same helper the declaration uses. Trait-clause proofs stay placeholders (`BuiltinOrAuto`), as they were, and trait objects become an explicit `TyKind::Error` instead of a placeholder predicate the new AST no longer has; neither is reachable from the tests.

Every expected file changed, and I reviewed each against its old version for meaning rather than format. What changed: - Formatting: `_0 = copy i == const 0i32` for `@0 := copy (i@1) == const (0 : i32)`, `storage_live`, and a `↳⚡` line for each call's unwind edge (Kani's existing abort block, now printed). - Items are printed by name (`is_zero(..)`, `(i32, i32)`, `Option<T>`) rather than by id, now that `item_names` is filled in. Since ids no longer appear, `main` is included again; `diverging_call`'s real check is the call in `main`. The `()` declaration is left out, as it is the same in every test. - Arithmetic spells its overflow mode: wrapping `wrap.+`, checked `panic.+` (was `+`, "fails on overflow"), and `/`, `%`, shifts and negation `panic.`, all as before. `unchecked_*` is now `ub.+` where it was `+`: its overflow is undefined behavior, which the old AST could not express. - Drops name their glue: `drop[drop_glue<'_, Option<i32>>] b`, with the types matching the values dropped. Nothing else changed meaning: literal values (negative ones at every width), switch arms, enum and tuple projections, trait impl and inherent method names are the same.

With Charon's type check now running on the translation, several common signatures made it reject Kani's output ("Found incorrect region var" / "Found incorrect type var") and the compiler then hit a `todo!()`: - `fn get(x: Option<&u32>)`, `fn deref2(x: &&u32)`, `fn read(h: Holder<'_>)`: only top-level `&T` inputs contributed late-bound regions, so a region nested in an ADT or another reference was undeclared. `fn pick<'a>(x: &'a u32, y: &'a u32)` declared `'a` twice, once per input. - `fn f<'a, T: 'a>(x: &'a T)`, `fn rd<'a, T>(x: R<'a, T>)`, methods of an `impl<'a>`: parameters were numbered with rustc's index, which counts all kinds together (and parent generics first), while Charon numbers each kind from zero. Late-bound regions also reused the ids of early-bound ones. - `FnDef::fn_sig` erases early-bound regions, so `f` above printed `x: &'_ T`. - Function-pointer types declared no regions for their own binder. Now, as in Charon's translation: - the late-bound regions are the signature binder's bound variables (all of them, each once, wherever they occur), numbered after the early-bound regions; - every generic parameter gets its position among parameters of the same kind, computed per item from `generics_of`, including parents; an `ItemGenerics` scope is active while translating a type, trait or function declaration (and a function's generic body, which mentions its parameters); - the declaration's signature comes from `tcx.fn_sig(..).instantiate_identity()`; - function-pointer types bind their regions, and item parameters inside them are referenced one binder further out. Elided regions (`'_`) stay unnamed, as Charon leaves them. `tests/llbc/regions` covers each case; it fails without this change. The llbc suite passes (22/22), and fmt and both CI clippy invocations are clean. `cargo clippy --features llbc` still reports the three pre-existing lints that model-checking#4886 fixes. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

…rrors Charon's pass pipeline type-checks the translation, so its error count is no longer zero in practice: on an input it rejects, Kani printed Charon's errors, then panicked with "not yet implemented" and reported an internal compiler error. Emit a fatal error that says Charon reported errors instead; Charon has already printed each of them, and no LLBC file is written. Checked by temporarily undoing the region declarations of the previous commit: `fn get(x: Option<&u32>)` now ends with "error: Charon reported 2 error(s) while translating to LLBC" and no `.llbc` file, instead of a panic. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

The comment on the `Drop` terminator said the glue for `T` is `drop_in_place::<T>`, but `Instance::resolve_drop_in_place` resolves to the `core::ptr::drop_glue` lang item (which `drop_in_place` wraps), and that is what the LLBC prints. `translate_generic_args_without_trait` took a `DefId` that it discarded; remove it. No change to the emitted LLBC. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

…git source Charon's nightly-2026.09.29 tag (962e40b0) differs from nightly-2026.09.26 only in depending on the published `serde_state_perfect_derive` 1.0.0 (MIT OR Apache-2.0) instead of the `serde_state` git fork (AeneasVerif/charon#1486, model-checking#1487). With no git source left besides `tracing-tree`, `deny.toml`'s `allow-git` is back to what main has. `cargo update -p charon` changes only the two `serde_state` entries in Cargo.lock. The llbc suite passes (22/22); `cargo deny check licenses sources bans` is ok. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

…odel-checking#4886) The rest of the Charon stack (model-checking#4881, model-checking#4882, model-checking#4883) has merged, and this is rebased onto `main`. Three commits: `ac73eb722` (the lint gate), `9fafffbb5` (method names, see the end), and `70806c417` (a comment noting that the `-D warnings` build also covers Charon). Last step of the Charon plan in model-checking#4834: make sure the LLBC backend can't quietly rot again. **Why.** Nothing in CI checked the LLBC backend for warnings or lints. The regression script's `-D warnings` build left out `llbc` because the old Charon had warnings of its own — its TODO said to revisit once the pin moved — and the clippy job only lints the default features. So the backend had accumulated 13 clippy errors that nobody could see (I found them while doing model-checking#4881). **What.** Charon now builds warning-free, and model-checking#4883 already removed ten of those errors; this fixes the last three. Then `kani-llbc-regression.sh` — which only the LLBC job runs, and which already builds with `llbc` — gains a `-D warnings` build and a `clippy -p kani-compiler --features llbc -- -D warnings`. The TODO in `kani-regression.sh` becomes a pointer to it. **The call I'd like checked:** I put the gate in the LLBC job rather than the main regression and clippy jobs, so that those don't have to build Charon on every PR. The trade-off is that a PR which breaks only the LLBC lints fails in the LLBC job rather than the clippy one — same signal, different place. Easy to move if you'd rather have it next to the other clippy run. Verified the gate actually gates: the script runs under `errexit`, and a planted `let_and_return` makes it exit 101. **Also: name methods the way Charon does.** The last commit replaces the implementing-type suffix on method names (`core::num::wrapping_addu8`, `test::getCounter`, `getWrapper<T>`) with Charon's `PathElem::Impl`: `{u8}` / `{Wrapper<T>}` for inherent impls, and `{impl T for A}` for trait impls. The trait-impl form refers to a trait impl declaration, which Kani now emits minimally, like trait declarations: the implemented trait and the generics, with no methods, associated items or vtable. The expected output of the four tests with methods changes accordingly, and `tests/llbc/impl_paths` covers generic inherent and trait impls. Resolves model-checking#4884 --------- Co-authored-by: Michael Tautschnig <tautschn@amazon.com> Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

…olchain job (model-checking#4920) Add a weekly job that tries to move the Charon pin to Charon's latest tag, and make the daily toolchain job also run the LLBC regression. **Context.** Charon tags `nightly-YYYY.MM.DD` almost every day, but nothing noticed the pin drifting: before model-checking#4883 it was 2,176 commits behind, and catching up needed a patch for `box` patterns (removed from nightly Rust) and skipping Charon versions that could no longer be built on current toolchains at all. A weekly attempt would have surfaced each of those changes when it happened. **The Charon job** (`.github/workflows/charon-update.yml`, Wednesdays 04:30 UTC and on demand) runs `scripts/charon_update.sh`, modelled on the CBMC and toolchain jobs: - move the `charon` submodule to the latest `nightly-*` tag and run `cargo update -p charon`; - run `kani-llbc-regression.sh`, which covers everything Charon affects (the LLBC build, the `-D warnings` build, llbc clippy and the llbc suite); the full `kani-regression.sh` doesn't build Charon, so it isn't needed here; - if that passes, open a `charon-<tag>` PR listing the merged Charon PRs since the current pin; the PR gets the full CI, including `cargo deny` for new licenses or git sources; - if it fails, file an "Automatic Charon upgrade failed" issue, or comment on it if one is open. Charon's tag changes nearly every day while a failure typically lasts for weeks, so this is one rolling issue rather than the one-issue-per-version scheme of the CBMC and toolchain jobs, which would file a new issue every week. A tag the open issue already mentions is not retried; an existing `charon-<tag>` branch also stops the job. Most failures will need a person (printer changes break expected files, AST renames need code changes), so in practice this is often an early-warning issue with the Charon log attached rather than a ready-to-merge PR. **The toolchain job** now runs `kani-llbc-regression.sh` after `kani-regression.sh`, since the latter does not build the LLBC backend: a toolchain that only breaks it (as the `box`-pattern removal did) went unnoticed until the PR's LLBC job. **Manual testing** (the workflow itself only runs on model-checking/kani, so I tested the script): - Pin already at the latest tag (`nightly-2026.09.29`): `next_step=none`. - Pin moved back to `nightly-2026.09.26` in a test commit: the script moved it to `nightly-2026.09.29`, `kani-llbc-regression.sh` passed (llbc 22/22), `next_step=create_pr`, and the log section lists the merged PR with a comparison link. - With a stubbed failing `kani-llbc-regression.sh` and a mocked `gh`: no open issue gives `create_issue`; an open issue that doesn't mention the tag gives `comment_issue`; one that does gives `none`. - Fetching the new tag into a depth-1 clone (as the setup action leaves the submodule) gives the full first-parent log and a working checkout. - The exact-title issue lookup finds a real issue (model-checking#4866) when given its title. - `shellcheck` is clean on the new script and `actionlint` on both workflows. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

feliperodri requested review from a team as code owners September 27, 2026 19:17

github-actions Bot added Z-EndToEndBenchCI Tag a PR to run benchmark CI Z-CompilerBenchCI Tag a PR to run benchmark CI labels Sep 27, 2026

feliperodri and others added 9 commits September 29, 2026 20:07

tautschnig force-pushed the charon-bump branch from eaad90b to c00ab40 Compare September 29, 2026 20:34

tautschnig approved these changes Sep 29, 2026

View reviewed changes

tautschnig enabled auto-merge September 29, 2026 20:37

tautschnig added this pull request to the merge queue Sep 29, 2026

github-merge-queue Bot removed this pull request from the merge queue due to failed status checks Sep 29, 2026

feliperodri added this pull request to the merge queue Sep 30, 2026

Merged via the queue into model-checking:main with commit 61ae23e Sep 30, 2026
33 of 34 checks passed

feliperodri deleted the charon-bump branch September 30, 2026 00:55

tautschnig mentioned this pull request Sep 30, 2026

Add a weekly Charon update job, and run the LLBC regression in the toolchain job #4920

Merged

Navigation Menu

Move the Charon pin to current and drop the patch machinery - #4883

Move the Charon pin to current and drop the patch machinery#4883
feliperodri merged 9 commits into
model-checking:mainfrom
feliperodri:charon-bump

feliperodri commented Sep 27, 2026 •

edited by tautschnig

Loading

Uh oh!

feliperodri commented Sep 28, 2026

Uh oh!

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Conversation

feliperodri commented Sep 27, 2026 • edited by tautschnig Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Why it's shaped this way

What the review should focus on

Things I'd like input on

Not in this PR

Follow-ups

Uh oh!

feliperodri commented Sep 28, 2026

Uh oh!

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

feliperodri commented Sep 27, 2026 •

edited by tautschnig

Loading