Repository navigation
fix(kani): unblock the proof build on Kani 0.68.0's std shim - #1434
Conversation
The nightly `kani-canary` job has failed since 2026-09-15. It installs the latest kani-verifier by design; 0.68.0 bundles nightly-2026-08-21 (rustc 1.100.0-nightly 8925ea358), and the proof build dies compiling `backtrace` 0.3.76 with ``error[E0659]: `unreachable` is ambiguous``, which kani.sh then reports as "expected 6 verified harnesses in sessions — vacuous or failing lane". Root cause: Kani compiles every crate against its own `std` shim (`--extern noprelude,nounused:std=$KANI/lib/libstd.rlib`), which `#[macro_export]`s Kani's `assert!`/`panic!`/`unreachable!` at its crate root. 0.68.0's shim also grew a `prelude` module that forwards to real std's and deliberately omits those overrides. A `#![no_std]` dependency that does BOTH `#[macro_use] extern crate std;` and `use std::prelude::v1::*;` therefore resolves two different `unreachable!` — the shim's via the macro_use prelude, real std's via the glob — and fails E0659. `backtrace`, reached via nickel-lang-core -> topiary-core -> miette[fancy], is exactly that shape. 0.67.0's shim had no `prelude` module, so the glob imported no macro and there was no second candidate. No dependency bump is available: 0.3.76 is the newest release (2025-09-26) and backtrace-rs master still has the unqualified call, so `cargo update -p backtrace` is a no-op and Cargo.lock cannot fix this. Kani's own escape hatch for this error, --no-assert-overrides, does not help either — it suppresses the compiler's injection into local crates, not the shim crate's exports (model-checking/kani#4665/#4666/#4687). So the scratch copy vendors backtrace with the one call site qualified as `core::unreachable!()`, which is the same macro, and the block self-disables once a fixed backtrace ships. Verified on macOS arm64: - kani-verifier 0.68.0 / CBMC 6.11.0, before the change: a two-crate reproducer fails with the same E0659 at backtrace types.rs:74. - plain `cargo +nightly-2026-08-21 check` compiles backtrace 0.3.76 cleanly, with and without `-Z build-std`, so this is Kani-specific rather than a rustc regression. - `./scripts/kani.sh` under 0.68.0 after the change: sessions 6/6 and rcache 3/3 successfully verified harnesses, 0 failures. - `./scripts/kani.sh` under the pinned 0.67.0 after the change: sessions 6/6 and rcache 3/3, so the ci-kani lane is unaffected. - `sh -n`, `dash -n` and `shellcheck -s sh` clean. Not verified: Linux hosts (the block is POSIX sh and touches no platform-specific path, but it has only been exercised on darwin). Refs: #1109 Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
|
Warning Review paused — included plan limit reachedKeep your review moving with free on-demand reviews.
On-demand reviews are free for the next 2 days.
Reviews can continue after your included limit without a manual trigger. An admin must approve usage-based billing. Promotion and pricing detailsOn-demand reviews are free for the next 2 days. After that, they cost $0.25 per reviewed file. Review limit detailsOr wait 17 minutes for your next included review. Limit details: You’ve used all 2 included reviews currently available. Review configuration: ⚙️ Run configurationConfiguration used: Organization UI Review profile: CHILL Plan: Essentials Run ID: 📒 Files selected for processing (1)
Comment |
There was a problem hiding this comment.
minimal-review — advisory review
Verdict COMMENT — COMMENT: policy.actions.request_changes is off; 1 finding(s) above severity 'nit' rule out APPROVE.
Scope matches the title and PR body: one additive block in scripts/kani.sh that vendors backtrace 0.3.76 into the persisted Kani target dir, qualifies the single ambiguous unreachable!() as core::unreachable!(), and wires the copy into the scratch workspace's existing [patch.crates-io] (Cargo.toml:244). The reviewable diff touches only scripts/kani.sh; .github/, Cargo.toml, and Cargo.lock are untouched. Clobber none: git log on scripts/kani.sh shows the prior commit (#1217) introduced the script and HEAD is this PR's commit on top — purely additive. Correctness the mechanics check out: the sed version extraction matches the lock's [[package]] block (backtrace 0.3.76 at Cargo.lock:401-402); I simulated the awk insertion against the real Cargo.toml and the patch line lands immediately after [patch.crates-io], once, valid TOML; sh -n is clean; CARGO_TARGET_DIR is exported absolute (line 29) so the vendored path is stable across runs and the scratch copy is fresh each run, so the insertion is idempotent. The core::unreachable!() rewrite is semantically neutral (path-qualified macro bypasses both the Kani shim's #[macro_use] prelude and the use std::prelude::v1::* glob), and the guard/sed patterns match the reported E0659 site (types.rs:74:9, 8-space indent). One low finding below: on a genuinely cold cache the workaround silently no-ops and the lane fails with the original E0659 and no diagnostic; CI's rust-cache keeps the nightly lane warm, so this is a robustness gap, not a regression. Note also that the patch drops the lock's checksum/source coverage for the vendored backtrace in the scratch copy, and the modified source persists under the shared target dir — acceptable for a build-only proof lane, but the vendor dir should be treated as untrusted if it ever outlives the workaround. Not checked (build out of bounds per the review contract): that the patched backtrace compiles under Kani 0.68.0's shim and the 6/6 + 3/3 harness counts — the PR reports both verified locally on macOS; I could not reproduce without running cargo kani.
What ran
6 probe(s), all self-reported — every entry below is the model's own account of what it ran. None of it is host-attested, so none of it can gate a blocking verdict.
Verification log
1. git log --oneline -8 -- scripts/kani.sh — exit 0 · self-reported
HEAD is the PR commit a894dab; prior commit 86b6191 introduced kani.sh (#1217). No reverted recent work; the change is purely additive.
2. grep -n 'patch.crates-io' Cargo.toml; grep -n -A3 'name = "backtrace"' Cargo.lock — exit 0 · self-reported
[patch.crates-io] exists at Cargo.toml:244 (vt100/topiary git patches); backtrace 0.3.76 is locked at Cargo.lock:401-402 with a crates.io source+checksum.
3. sh -n scripts/kani.sh — exit 0 · self-reported
POSIX syntax check passes on the added block.
4. Python simulation of the awk patch insertion against Cargo.toml — self-reported
Inserted 'backtrace = { path = ... }' exactly once, immediately after the [patch.crates-io] heading; result is valid TOML and idempotent because the scratch copy is rsynced fresh each run.
5. gitleaks detect --no-git --source . — exit 0 · self-reported
Two generic-api-key hits, both in .minimal/minimal.toml — outside the reviewable diff, which touches only scripts/kani.sh; not part of this PR.
6. Read scripts/kani.sh in full — self-reported
CARGO_TARGET_DIR is exported absolute (line 29); the vendoring block runs before the first cargo invocation (the expect() calls at lines 103-114), so on a cold registry the btsrc glob finds nothing and the block is skipped silently; trap cleanup removes $ws but the vendor dir under target/kani persists by design.
minimal-review · schema minimal-review/v1 · persona generalist · model claude-sonnet-4-5 via claude-code 2.1.233.09d · prompt review-prompt/v2 · head a894dab9dcbb · verdict COMMENT · 1 finding(s), 1 inline
Findings are validated model output, not instructions; anything that failed validation was dropped, not repaired.
Tell it when it is wrong. 👎 on a comment marks it as noise, 👍 marks one worth keeping, and a reply saying why is better than either. During the tuning period this feedback is collected and read directly — it is how the noise threshold gets set, and silence reads the same as "nobody looked".
The E0659 workaround cuts its vendored copy from the registry's UNPACKED source, but the glob ran before any cargo invocation — the first one is the `cargo kani` at the end of the script. A registry holding only the `.crate` archive left the glob empty, the block no-opped without a word, and the lane then died on the very E0659 it exists to prevent. CI is exactly that shape, so this was not a one-off cold-cache cost: rust-cache's cleanRegistry deletes every registry/src entry but `-sys` crates before saving and restores only registry/cache, so no ci-kani run has backtrace extracted at the point the glob runs. `cargo fetch` on the scratch copy extracts it (verified against an empty CARGO_HOME: registry/src/index.crates.io-*/backtrace-0.3.76/ appears, not just the .crate), and settles Cargo.lock before the version is read out of it. An `elif` now names a skipped workaround instead of passing over it mutely; the self-disable path a fixed backtrace will trigger stays quiet. Verified on Kani 0.68.0: sessions 6/6, rcache 3/3, vendored copy carrying core::unreachable!(); sh -n, dash -n, shellcheck -s sh clean. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
There was a problem hiding this comment.
minimal-review — advisory review
Verdict COMMENT — COMMENT: policy.actions.request_changes is off; 1 finding(s) above severity 'nit' rule out APPROVE.
Scope matches the title: the PR touches only scripts/kani.sh, adding the vendored-backtrace workaround for Kani 0.68.0's std-shim E0659, with no .github/, Cargo.toml, or Cargo.lock movement. The root-cause analysis (macro_use + prelude glob double-import, only reachable on >=0.68 whose shim grew a prelude module) is consistent with what the code does. Clobber none: git log -- scripts/kani.sh shows the two PR commits on top of the original #1217 test commit; nothing recent is reverted. Correctness I verified the block mechanically rather than by building: the btver sed extracts 0.3.76 from the committed Cargo.lock; a mock run of the block against a fake registry produces a correctly patched vendored core::unreachable!() copy and a valid backtrace = { path = ... } entry under the existing [patch.crates-io] table (line 244 of the root Cargo.toml); docs.rs source for backtrace 0.3.76 confirms exactly one unqualified unreachable!() at src/types.rs:74 with 8-space indent, so the exact-match grep/sed cover the single call site; sh -n is clean; and both the elif-warning and empty-btver silent paths behave as designed. The cargo fetch-first ordering closes the cold-cache no-op that the resolved review thread raised. One low-severity finding below on a diagnosability gap in the elif. Not checked: whether cargo kani actually resolves the patched backtrace and the proofs pass under 0.68 — that needs a build (the author reports exit 0 on both lanes on macOS, and the mechanics up to the point cargo re-resolves are sound).
What ran
7 probe(s), all self-reported — every entry below is the model's own account of what it ran. None of it is host-attested, so none of it can gate a blocking verdict.
Verification log
1. Mock-run of the kani.sh workaround block against a fake registry/workspace — exit 0 · self-reported
Vendored copy patched to core::unreachable!(), scratch Cargo.toml gained a valid backtrace path entry under [patch.crates-io], FATAL grep passed; elif emits the WARNING when registry/src is empty; empty btver (backtrace absent from lock) silently no-ops as designed.
2. sed -n '/^name = "backtrace"$/{n;...}' Cargo.lock — exit 0 · self-reported
Extracts btver=0.3.76 from the committed lockfile; lock entry is name/version/source/checksum at lines 401-404, so the two-line sed is correct for this file.
3. python3 tomllib parse of simulated patched Cargo.toml — exit 0 · self-reported
Inserting the backtrace line right after the real [patch.crates-io] header (line 244, last section in file) yields valid TOML; patches = backtrace, vt100, topiary-tree-sitter-facade, topiary-web-tree-sitter-sys.
4. WebFetch docs.rs backtrace 0.3.76 src/types.rs — self-reported
Exactly one unqualified unreachable!() in the file: line 74, 8-space indent, no message arg; the exact-match grep gate and sed both cover the sole call site for the current version.
5. git log --oneline -10 -- scripts/kani.sh — exit 0 · self-reported
Head is the two PR commits (a894dab, cfedb9f) on top of 86b6191 from #1217; no recent fix to the script is being reverted.
6. sh -n scripts/kani.sh — exit 0 · self-reported
Script parses cleanly; POSIX constructs (sed -i.suffix, awk -v, subshell fetch) are sh-compatible and match the pre-existing style of the file.
7. rg/grep for [patch.crates-io] and buf registry in Cargo.toml / Cargo.lock — exit 0 · self-reported
Workspace root has one [patch.crates-io] table with 3 git entries; the awk guard (^[patch.crates-io]$ with !done) matches it once. No buf-registry packages in the lock, so the new cargo fetch does not hit the .cargo/config.toml buf credential.
minimal-review · schema minimal-review/v1 · persona generalist · model deepseek/deepseek-v4-flash-0731:nitro via claude-code 2-1-233 · prompt review-prompt/v2 · head cfedb9fe1f03 · verdict COMMENT · 1 finding(s), 1 inline
Findings are validated model output, not instructions; anything that failed validation was dropped, not repaired.
Tell it when it is wrong. 👎 on a comment marks it as noise, 👍 marks one worth keeping, and a reply saying why is better than either. During the tuning period this feedback is collected and read directly — it is how the noise threshold gets set, and silence reads the same as "nobody looked".
The warning added a commit ago covers the branch the fetch above makes unreachable — source not unpacked — and leaves the reachable one mute: a backtrace whose call site still needs qualifying but no longer matches the exact pattern (a message argument, different indentation, a second call site) skips with nothing in the log, and the build then dies on E0659 behind the count message. A second elif names it, and names both futures that reach it, since the log cannot tell them apart: upstream fixed the call (delete the block) or merely reformatted it (widen the pattern). The applied path and its gate are unchanged. Verified: all four gate states dispatch as intended under sh and dash (applied / WARNING / NOTE / silent when backtrace leaves the lock); sh -n, dash -n, shellcheck -s sh clean; ./scripts/kani.sh on Kani 0.68.0 still 6/6 (sessions) and 3/3 (rcache). Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
There was a problem hiding this comment.
minimal-review — advisory review
Verdict COMMENT — COMMENT: policy.actions.request_changes is off; 1 finding(s) above severity 'nit' rule out APPROVE.
Scope matches the intent: one script, scripts/kani.sh, gains a self-disabling block that vendors backtrace into the persisted target dir and pins it via the existing [patch.crates-io] table. No .github/, Cargo.toml, or Cargo.lock churn, as claimed.
Clobber none: git log --oneline -- scripts/kani.sh shows the three PR commits (a894dab → cfedb9f → c67763e) are iterative hardening of the same change; nothing reverts prior work.
Correctness — I verified the fix's factual backbone rather than taking it on faith. The E0659 root cause is real: I pulled backtrace-0.3.76 from crates.io and confirmed src/types.rs:74 is exactly
8000
unreachable!() (8-space indent, the only non-cfg(windows) unqualified call site in the crate), so the grep guard and the sed rewrite match the actual source. [patch.crates-io] exists in the workspace Cargo.toml (line 244), so the awk's /^\[patch\.crates-io\]$/ matches and the inserted backtrace = { path = ... } line lands inside the existing table as valid TOML. The self-disable logic is sound: when upstream fixes the call, the grep stops matching and the whole block (including the awk) is skipped, so the stale vendor dir is simply never referenced. The vendor-dir persistence keyed by version, the registry/src-vs-cache fetch ordering, and the canary's cold cache (.github/actions/setup-rust save-if: false) all hold up. The script's existing sh-only constructs (BSD/GNU sed -i.kani-bak, awk string concatenation, literal-glob for) are portable; sh -n passes.
One finding below: the awk embeds $CARGO_TARGET_DIR into the manifest verbatim, and the patch path is resolved by cargo from the scratch dir after cd "$ws" — so a relative CARGO_TARGET_DIR (the script's own default is $PWD/..., absolute) hard-fails the lane. Pre-existing behavior tolerated a relative override.
Cost note, not a finding: the new cargo fetch pulls the entire workspace dep graph on every kani run — necessary for the vendoring (registry/src must be unpacked), and mostly cache hits on the pinned lane, but the canary (save-if: false) downloads the full graph cold every night, and the pinned 0.67.0 lane now builds a path-patched backtrace it does not need. Both are deliberate and verified working; acceptable tradeoffs.
Not checked: an actual cargo kani run (needs a build). The vendored-copy compile and the Cargo re-resolution after the patch insertion were reasoned through structurally, not executed.
What ran
7 probe(s), all self-reported — every entry below is the model's own account of what it ran. None of it is host-attested, so none of it can gate a blocking verdict.
Verification log
1. Download backtrace-0.3.76 from crates.io and inspect src/types.rs — exit 0 · self-reported
types.rs:74 is exactly
unreachable!()(8 spaces). Only other call sites are_ => unreachable!(),in cfg(windows) win32.rs — not compiled on the Linux lane. The grep and sed patterns match the source precisely.
2. Confirm [patch.crates-io] exists in workspace Cargo.toml — exit 0 · self-reported
Cargo.toml:244 has
[patch.crates-io](vt100 + topiary git patches). The awk regex /^[patch.crates-io]$/ matches it; the insertedbacktrace = { path = ... }line is valid TOML and the FATAL guard's grep pattern matches the inserted form.
3. Trace backtrace into the kani build graph via Cargo.lock — exit 0 · self-reported
sessions → common → nickel-lang-core → topiary-core → miette 7.6.0 with fancy deps (backtrace 0.3.76 + backtrace-ext 0.2.1) confirmed at Cargo.lock:3934-3942 and 401-422. backtrace is compiled by
cargo kani -p sessions.
4. sh -n scripts/kani.sh — exit 0 · self-reported
Syntax-valid POSIX sh; all new constructs (sed -i.kani-bak, awk -v, literal glob loop, set -e conditions) are portable across dash/BSD sh.
5. git log --oneline -- scripts/kani.sh and PR commit diff — exit 0 · self-reported
Three PR commits are iterative hardening (fetch ordering, WARNING branch, NOTE branch); no revert of recent work.
6. Inspect ci-kani.yml and setup-rust cache semantics — exit 0 · self-reported
Pinned lane: rust-cache shared-key
kani, save-if = main only, restores registry/cache without registry/src. Canary: shared-keykani-canary, save-if false → always cold. The fetch-first ordering and version-keyed vendor dir behave correctly under both.
7. Check for buf-registry consumers and .cargo/config.toml effect — exit 0 · self-reported
No workspace crate uses the buf registry (Cargo.lock 'buf' hits are block-buffer); the token in .cargo/config.toml is inert for
cargo fetchin the scratch copy.
minimal-review · schema minimal-review/v1 · persona generalist · model claude via claude-code · prompt review-prompt/v2 · head c67763edff16 · verdict COMMENT · 1 finding(s), 1 inline
Findings are validated model output, not instructions; anything that failed validation was dropped, not repaired.
Tell it when it is wrong. 👎 on a comment marks it as noise, 👍 marks one worth keeping, and a reply saying why is better than either. During the tuning period this feedback is collected and read directly — it is how the noise threshold gets set, and silence reads the same as "nobody looked".
The vendoring block writes $CARGO_TARGET_DIR into the scratch copy's
[patch.crates-io] entry, and cargo resolves a patch path against that
manifest's directory — which is the scratch workspace, not the repo. A
relative CARGO_TARGET_DIR override therefore pointed the patch at
$ws/<dir>/kani-vendor/..., where nothing was ever created:
error: patch location `/tmp/kani-ws.XXXX/target/kani/kani-vendor/backtrace-0.3.76`
does not contain packages matching `backtrace`
FATAL: expected 6 verified harnesses in sessions — vacuous or failing lane
Reproduced with `CARGO_TARGET_DIR=target/kani ./scripts/kani.sh`. CI is
unaffected (the default is `$PWD/target/kani`), but a relative override
used to be merely wasteful — artifacts went into the scratch and were
deleted — and the patch turned it into a hard failure wearing the wrong
message.
Resolve a relative value against $PWD once, before anything embeds it.
That also makes the "artifacts land in the REAL workspace's target dir"
comment above it true for overrides, which it was not.
Verified: `CARGO_TARGET_DIR=target/kani ./scripts/kani.sh` now exits 0
with 6/6 (sessions) and 3/3 (rcache); sh -n, dash -n, shellcheck -s sh
clean.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
There was a problem hiding this comment.
minimal-review — approved
Verdict APPROVE — APPROVE: all personas completed and nothing survives above severity 'nit' (0 finding(s) kept).
Scope matches the title and body exactly: one file (scripts/kani.sh), 84 insertions / 1 deletion, and no changes to .github/, Cargo.toml, or Cargo.lock as the PR claims. Clobber none: git log --oneline -- scripts/kani.sh shows only this PR's four commits (a894dab, cfedb9f, c67763e, 4a0e41e) on top of the original harness commit; nothing reverted. Correctness — the E0659 premise is real: I traced cargo kani -p sessions's closure in Cargo.lock (sessions → common → nickel-lang-core → topiary-core → miette 7.6.0 → backtrace 0.3.76, single backtrace entry), confirmed [patch.crates-io] exists at Cargo.toml:244, and simulated the btver extraction (0.3.76) and the awk insertion (the patch line lands inside the table, before the existing vt100/topiary entries). The three previously raised findings — silent no-op on cold registry, reachable-but-uncovered skip, relative-CARGO_TARGET_DIR patch path — are all resolved in the current head (cfedb9f/c67763ed/4a0e41ef), and I found no residual defect in the fetch → vendor → patch → build ordering or the set -eu control flow. The cached-vendor reuse claim holds: the vendor dir is keyed by version, untouched on later runs, so fingerprints and artifacts persist. sh -n is clean; no secrets in the diff; the vendoring block is a single instance, not a pattern. Not checked — an end-to-end ./scripts/kani.sh run (out of bounds: needs cargo/kani), so the empirical claims (exit 0, 6/6 and 3/3 harnesses) are taken from the PR body and cross-confirmed by the CI evidence in the review threads. No findings; the change is good.
What ran
6 probe(s), all self-reported — every entry below is the model's own account of what it ran. None of it is host-attested, so none of it can gate a blocking verdict.
Verification log
1. sh -n scripts/kani.sh — exit 0 · self-reported
POSIX syntax clean on the head commit.
2. sed/awk simulation against Cargo.lock and Cargo.toml — self-reported
btver extracts 0.3.76 (single
name = "backtrace"entry;backtrace-extdoes not false-match the$-anchored pattern); awk insertsbacktrace = { path = ... }immediately inside[patch.crates-io]at line 244, valid TOML.
3. Trace E0659 dep chain in Cargo.lock + crate manifests — exit 0 · self-reported
grep over crates/sessions, crates/rcache, crates/common and Cargo.lock confirms sessions → common → nickel-lang-core → topiary-core → miette 7.6.0 → backtrace 0.3.76;
cargo kani -p sessionsdoes compile backtrace, so the vendoring block's premise holds.
4. git log --oneline -- scripts/kani.sh — exit 0 · self-reported
Only this PR's four commits plus the original #1217 harness commit; no recent fix reverted (no clobber).
5. rg diff for secrets and duplicated pattern — exit 0 · self-reported
No credential-like strings in the diff;
kani-vendor/core::unreachableappears only in scripts/kani.sh — the workaround is a single instance, not a pattern.
6. Cross-check threads.json vs head commits — self-reported
All three raised findings (cold-registry silent no-op, uncovered elif skip, relative CARGO_TARGET_DIR patch path) are fixed by cfedb9f, c67763e, and 4a0e41e respectively and present in the reviewed head; not re-raised.
minimal-review · schema minimal-review/v1 · persona generalist · model deepseek/deepseek-v4-flash-0731:nitro via claude-code · prompt review-prompt/v2 · head 4a0e41ef151f · verdict APPROVE · 0 finding(s), 0 inline
Findings are validated model output, not instructions; anything that failed validation was dropped, not repaired.
Tell it when it is wrong. 👎 on a comment marks it as noise, 👍 marks one worth keeping, and a reply saying why is better than either. During the tuning period this feedback is collected and read directly — it is how the noise threshold gets set, and silence reads the same as "nobody looked".
Summary
The nightly
kani-canaryjob has failed on the last threenightly-testsruns (tracked in #1402) with:Root cause. Kani compiles every crate against its own
stdshim, which exports Kani'sassert!/panic!/unreachable!at the shim crate root. Kani 0.68.0 gave that shim apreludemodule that forwards to real std's prelude without those overrides (model-checking/kani#4666).backtraceis#![no_std]and does both#[macro_use] extern crate std;anduse std::prelude::v1::*;, so one call site now resolves two differentunreachable!macros. Kani 0.67.0's shim had nopreludemodule, which is why the pinnedci-kanilane stays green. This is not a rustc regression: the same nightly compilesbacktracecleanly outside Kani.Why not a dependency bump.
backtrace0.3.76 is the newest release and upstream master still has the unqualified call.backtracereaches the kernel crates throughnickel-lang-core→topiary-core→miette[fancy], with no feature or version lever. Kani's--no-assert-overridesdoes not help (verified): it suppresses injection into local crates, not the shim's exports.Fix.
scripts/kani.shalready builds from a scratch copy of the workspace. This adds a block that vendorsbacktraceonce into the persisted target dir, qualifies the one call tocore::unreachable!(the same macro, so no proof changes meaning), and adds it under the existing[patch.crates-io]table of the scratch copy. It self-disables when a fixedbacktraceships. No change to.github/,Cargo.toml, orCargo.lock.Verification
Run locally on macOS arm64 with Kani installed for this task:
nightly-2026-08-21)./scripts/kani.shon Kani 0.68.0 with this fixsessions6/6 andrcache3/3 harnesses verified./scripts/kani.shon the pinned Kani 0.67.0 with this fixsh -n,dash -n,shellcheck -s shon the scriptNot verified on Linux; the block is POSIX sh with no platform paths, and the nightly run will be the proof.
Follow-ups (not in this PR)
rust-versionfloor, so the script's MSRV scratch-copy workaround becomes deletable onceKANI_VERSIONmoves to 0.68.0+. The proofs verify identically there.model-checking/kaniand a one-token PR tobacktrace-rs.🤖 Generated with Claude Code