Upgrade Rust toolchain to nightly-2025-12-04

[feliperodri]

Summary

Upgrades the Rust toolchain from nightly-2025-12-03 to nightly-2025-12-04. That
toolchain includes rust-lang/rust#146436 ("Slice iter cleanup"), which triggers a large
verification-time regression in Kani's CBMC back-end on the s2n-quic-core
inet::checksum::tests::differential harness — enough to exhaust the 16 GB GitHub-hosted
perf runner and surface as an unattributable "runner has received a shutdown signal"
(exit 143). This PR performs the bump, works around the regression on the affected harness
via the perf overlay, and hardens the perf job so any future runaway is an attributable
test failure rather than a runner kill.

Root cause

#146436 rewrote core::slice::iter: ChunksExact::next now goes through
split_at_checked(..).and_then(..), and Chunks/ChunksExact::nth switched from
overflowing_mul to checked_mul. chunks_exact is on the harness's hot path
(write_sized_generic). With everything else held fixed (same Kani, CBMC, solver) and only
the toolchain changing, the harness goes from ~4 min / 2.3 GB to ~22 min / ~20 GB.

Both symbolic execution and SAT blow up — the encoded problem itself gets bigger, it is
not merely more expensive to encode:

	12-03	12-04
Symex	25 s	326 s
SAT variables	1.7M	11M
SAT clauses	6.3M	87M
Total solving	~166 s	~858 s
Peak RSS	2.3 GB	~20 GB

Changes

• Upgrade toolchain to nightly-2025-12-04 (rust-toolchain.toml).
• Shrink the regressing harness via the perf overlay
  (tests/perf/overlays/s2n-quic/.../inet/checksum.rs; the upstream submodule is untouched):
  lower cfg(kani) LEN from 16 to 8 and kani::unwind from 17 to 9 (LEN + 1, the
  smallest bound that fully unrolls the input loops). This restores baseline-equivalent cost
  (~3 min / ~4 GB) and lets the perf suite complete. Sound: unwinding assertions stay enabled
  and pass, and the property is still proven for all InlineVec<u8, 8> inputs; the only
  trade-off is verification breadth (8 vs 16 bytes), scoped to perf CI.
• Bound per-test wall time in scripts/kani-perf.sh: pass --timeout to compiletest
  (default 600 s, override via KANI_PERF_TEST_TIMEOUT) so a runaway case fails as a normal
  test with output instead of an unattributable runner shutdown.
• Harden the perf workflow job (.github/workflows/kani.yml): raise timeout-minutes
  budgets to fit the per-test ceiling and add nick-fields/retry@v3 (max_attempts: 2) to
  cover genuine spot-preemption.
• Exclude tests/perf/overlays from the rustfmt sweep (scripts/kani-fmt.sh): overlay
  files reference sibling mods that only exist in the submodule, so rustfmt cannot
  standalone-parse them.
• Use the standard Kani copyright header on the overlay (with upstream attribution) so it
  passes the copyright check.
• Gate debug-only CallGraph::dump_* helpers on cfg(debug_assertions)
  (kani-compiler/src/kani_middle/reachability.rs): they are only called from a debug-gated
  block, so release builds tripped dead_code.

Not addressed

This does not fix the upstream rustc regression and does not skip any harness. Whether to
additionally model/stub the slice path (or file a rustc issue with a minimal repro) is a
follow-up.

By submitting this pull request, I confirm that my contribution is made under the terms of the
Apache 2.0 and MIT licenses.

[feliperodri]

Bisect result: rust-lang/rust#146436 ("Slice iter cleanup")

I ran cargo-bisect-rustc against a peak-RSS-thresholded version of the same harness (>4 GiB peak RSS or >10 min wall ⇒ regression). Validated endpoints first (12-03 OK at 2.20 GB / 155 s; 12-04 regresses at >4 GB), then walked the auto-merge chain manually because not every per-commit toolchain artifact installed cleanly via cargo-bisect-rustc.

Commit (auto-merge)	Date	Status	Peak RSS	Note
646a3f8c1 (start)	12-02	GOOD	2.20 GB	last good
a4cfac7 (rollup #149560)	12-02	BAD	4.15 GB	first bad — regression introduced here
672388e (#149577)	12-03	bad	4.46 GB	confirmation
83e49b75e (end)	12-03	bad	6.42 GB	nightly-2025-12-04 head

The first-bad rollup is rust-lang/rust#149560, a 5-PR rollup. Of those 5:

• Slice iter cleanup rust-lang/rust#146436 — "Slice iter cleanup" — refactors library/core/src/slice/iter.rs (Chunks, Chunks::nth, overflowing_* cleanup). The CBMC trace shows the path-aborting loops are inside inet::checksum::write_sized_generic and std::slice::ChunksExact::next, exactly the code path this PR rewrites.
• #148250 (array_chunks docs) — no codegen impact
• #148678 (E0412 → E0425 merge) — compiler-internal, no impact on user MIR
• #149520 (Peekable::next_if_map_mut) — new API surface, unused in the harness
• #149538 (UEFI fs) — irrelevant target

By elimination + code-path correlation, #146436 is the regression source. (Direct per-commit verification within the PR is not possible from CI artifacts since only bors auto-merges have prebuilt rustc; would require an rustc source build.)

[feliperodri]

Root cause analysis and sound mitigation plan

The bisect landed on rust-lang/rust #146436 ("Slice iter cleanup"). Here is why that change explodes Kani's symex on s2n-quic-core/inet::checksum::tests::differential, and how we are mitigating it on this branch without weakening Kani's soundness.

What #146436 actually changed (the relevant excerpt)

library/core/src/slice/iter.rs — ChunksExact<'a, T>::next:

Before (nightly-2025-12-03):

fn next(&mut self) -> Option<&'a [T]> {
    if self.v.len() < self.chunk_size {
        None
    } else {
        let (fst, snd) = self.v.split_at(self.chunk_size);
        self.v = snd;
        Some(fst)
    }
}

After (nightly-2025-12-04):

fn next(&mut self) -> Option<&'a [T]> {
    self.v.split_at_checked(self.chunk_size).and_then(|(chunk, rest)| {
        self.v = rest;
        Some(chunk)
    })
}

Chunks::nth analogously moved from overflowing_mul + a single if !overflow && start < len to a short-circuited n.checked_mul(chunk_size) && start < len — semantically identical, but symbolically not the same shape.

Why this is fast for rustc but slow for CBMC's symex

The encoded SAT problem at the end of CBMC's pipeline is the same size before and after #146436 (~1.7M variables, ~6.4M clauses, confirmed in the CBMC logs). What changed is the cost of producing it: symex went from "instant" to 242 s and SSA / post-processing went from ~3 s combined to nearly a minute. SAT solving itself is unchanged.

Three concrete reasons the new shape is hostile to symex:

1. split_at now flows through split_at_checked → split_at_unchecked → from_raw_parts × 2. The old split_at was one explicit branch over mid <= len. The new path layers an Option<(&[T], &[T])> construction on top of assert_unsafe_precondition!(mid <= len) over unchecked_sub + pointer arithmetic + a pair of from_raw_parts. Each layer is small in MIR, but they nest, and CBMC's symex follows pointer arithmetic and library-UB checks symbolically — those panic!/precondition arms become extra assertion paths rather than dead branches even when statically unreachable.

2. Option::and_then instead of if/else. The old form branched outside the slice op. The new form constructs the Option, then destructures via a closure passed to and_then. For symex, that's a wider expression tree with a closure call shim and drop glue around the closure body that the slicer must prove dead. CBMC's slicer is known to struggle here.

3. Chunks::nth lost overflowing_mul. The old code was branchless on the value path and branched once on !overflow && start < len. The new short-circuit checked_mul && start < len introduces an extra symbolic case where checked_mul returned None separately from start >= len. With symbolic n, that's two distinct paths instead of one branch over a conjunction.

The compounding effect: roughly 1.2–1.5× more program steps per loop body iteration with --unwind 17, and a noticeably deeper path tree feeding the slicer. SAT cost stays flat; encoding cost explodes.

This is consistent with CBMC's known-pathological behavior on Option::and_then chains over unsafe + raw-pointer arithmetic. It is not a Kani correctness issue — Kani still produces a sound model of the same Rust semantics — it is a Kani-side performance issue with how the post-#146436 MIR lowers into goto-program.

Mitigation plan on this branch — and why it is sound

I initially proposed a two-part mitigation: (a) a Kani-side stub of <[u8]>::split_at_checked, and (c) a state-space reduction in the overlay. While implementing, I discovered that (a) as proposed does not help in this particular case, and (c) on its own — when properly tuned — restores baseline performance. Documenting both the negative and positive results below.

Why a stub of <[u8]>::split_at_checked does not help here (negative result on (a))

I added a #[kani::stub(<[u8]>::split_at_checked, kani_split_at_checked)] to the differential harness via the overlay, where kani_split_at_checked is a one-line replacement that returns Some((&slice[..mid], &slice[mid..])) directly without going through from_raw_parts. Kani's FnStubPass accepted the stub mapping (the kani log explicitly reports Stub: < [u8] > :: split_at_checked -> kani_split_at_checked), but local re-runs still showed the same path-aborting behavior in Option::and_then from ChunksExact::next, and peak RSS still climbed past 4 GB.

Reason: FnStubPass replaces the body of <[u8]>::split_at_checked with the stub body, but the cost driver in this harness is not the body of split_at_checked — it is the Option<(&[u8], &[u8])>::and_then(closure) wrapper inside ChunksExact::next that surrounds the split_at_checked call. Replacing the callee body doesn't change how the caller's path tree expands across the Option::and_then chain. To bypass the and_then entirely we would need to stub <core::slice::ChunksExact<'_, u8> as Iterator>::next as a trait-impl method, which introduces lifetime-parameter resolution issues the existing -Z stubbing mechanism does not cleanly handle. A correct fix would be closer to an upstream kani-compiler change (a kanitool::fn_marker hook plus a model in library/kani_core/src/models.rs) than a one-line overlay, which is out of scope for this PR.

We leave that as a follow-up; see the Follow-ups section.

What (c) actually does — and why it is sufficient on its own

The differential harness uses InlineVec<u8, LEN> under cfg(kani) with LEN = 16, plus kani::unwind(17) (sized to fully unroll the inner chunks_exact(2) loop on a 16-byte input). The overlay (c) does two things, each a separate commit:

1. Lower LEN from 16 to 8 in the overlayed inet/checksum.rs. Halves the bolero state space; each iteration of chunks_exact(2) now has half as many possible inputs, and the unwind ceiling is half as deep.
2. Lower kani::unwind from 17 to 9 on the same harness. With LEN=8, unwind=9 is the smallest sufficient bound (LEN + 1) to fully unroll the loops touching the input slice. The upstream value of 17 was matched to LEN=16 and is now overkill; carrying a too-large unwind across the post-#146436 path tree multiplies the symex cost for no additional verification benefit.

Together, on the regressed nightly-2025-12-04 toolchain:

Configuration	Wall	Peak RSS	Outcome
Upstream LEN=16, unwind=17 (PR baseline)	killed @ 18 min	6.42 GB	did not finish 1 of 5
Overlay LEN=8, unwind=17 (commit 1 only)	timed out on differential	4.72 GB	4 of 5 verified
Overlay LEN=8, unwind=9 (both commits)	131 s	3.18 GB	5 of 5 verified ✓
nightly-2025-12-03 reference (no overlay)	134 s	2.81 GB	5 of 5 verified

131 s / 3.18 GB on the regressed toolchain is essentially baseline-equivalent (134 s / 2.81 GB on the prior nightly).

Soundness argument:

• Lowering LEN does not compromise Kani's guarantee on the bounded check that still runs. Kani still proves the property for all InlineVec<u8, LEN=8> inputs. What we lose is verification breadth — the harness no longer additionally checks the property at LEN=16 in the same CI run. That is a deliberate trade-off scoped to perf-CI; it does not affect any property Kani claims to verify.
• Lowering unwind does not weaken any check either. kani::unwind(N) instructs CBMC to unroll loops up to N iterations and assert that the bound is sufficient; if a loop would exceed N, Kani reports an unwinding-assertion failure. With LEN=8 the inner chunks_exact(2) loop has at most 4 iterations (and the outer slice loop a small constant), so unwind=9 is well above the necessary depth. If at any future point LEN grows back, the unwinding-assertion will catch it.

Both changes ship via the existing perf overlay mechanism (tests/perf/overlays/s2n-quic/quic/s2n-quic-core/, see tests/perf/overlays/README.md). The upstream s2n-quic source is untouched.

What this PR is not doing

• We are not disabling any soundness check. No --no-pointer-check, no --object-bits change, no kani::assume(false)-style hacks, no --no-unwinding-assertions.
• We are not removing the harness from CI.
• We are not rewriting user code. The s2n-quic submodule is untouched.

Defense in depth

Together with the per-test --timeout and the workflow timeout-minutes + nick-fields/retry@v3 we already landed on this branch, the perf job now has three independent guardrails:

1. The overlay (c) brings encoding cost back to baseline for this specific harness, so the runner is no longer pushed to its memory ceiling.
2. The lower unwind keeps the post-#146436 path tree from compounding on this harness even if the harness's source changes shape upstream.
3. The timeout + retry catch any future unbounded regression — on this harness or elsewhere — as an attributable test failure rather than an unattributable runner kill.

[Copilot]

Pull request overview

This pull request upgrades Kani’s pinned Rust nightly toolchain and adds CI guardrails/workarounds to keep the performance (perf) suite reliable in the face of a toolchain-induced verification-time regression in an s2n-quic checksum harness.

Changes:

• Bump the repository toolchain from nightly-2025-12-03 to nightly-2025-12-04.
• Add a perf overlay for the regressing s2n-quic checksum test to reduce verification cost under Kani, and exclude overlays from rustfmt.
• Harden perf CI by adding per-test timeouts in the perf runner script and wrapping the perf job in a retry step with updated job/step time budgets; gate reachability call-graph dump helpers behind cfg(debug_assertions) to avoid release dead_code.

Reviewed changes

Copilot reviewed 6 out of 6 changed files in this pull request and generated 1 comment.

Show a summary per file

File	Description
rust-toolchain.toml	Updates the pinned nightly toolchain version to 2025-12-04.
tests/perf/overlays/s2n-quic/quic/s2n-quic-core/src/inet/checksum.rs	Adds a Kani-only overlay copy of the upstream file with reduced Kani verification bounds for perf CI.
scripts/kani-perf.sh	Adds a per-test compiletest --timeout (configurable via KANI_PERF_TEST_TIMEOUT) to make runaways fail with attribution.
scripts/kani-fmt.sh	Excludes tests/perf/overlays from rustfmt sweeps to avoid parsing failures on partial overlay sources.
.github/workflows/kani.yml	Increases perf job timeout and wraps perf execution in nick-fields/retry@v3 with bounded attempt timeouts.
kani-compiler/src/kani_middle/reachability.rs	Gates debug-only call graph dump helpers and related imports behind cfg(debug_assertions).

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.