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/memory regression in Kani's CBMC back-end on
the s2n-quic-core inet::checksum::tests::differential harness — originally
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, adds a regression test that captures the underlying issue, and
hardens the perf job (including fixing a latent compiletest deadlock) so any
future runaway is an attributable test failure rather than a runner kill.

Root cause

#146436 rewrote core::slice::iter: ChunksExact::next now decides Some/None
through split_at_checked(..).and_then(..), i.e. via the niche-encoded (null =
None) discriminant of Option<(&[T], &[T])>. On the harness's hot path
(write_sized_generic), a symbolic-index split_at makes the slice data
pointer a (cond ? base : NULL) select, so CBMC's symbolic execution can no
longer fold the loop-exit guard and chunks_exact unwinds to the --unwind
bound. With everything else fixed (same Kani, CBMC, solver) and only the
toolchain changing, both symex and SAT blow up — the encoded problem itself
grows, 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

• Toolchain bump to nightly-2025-12-04 (rust-toolchain.toml).
• Shrink the regressing harness via the perf overlay (submodule untouched):
  lower cfg(kani) LEN 16→8 and kani::unwind 17→9 (LEN + 1, the smallest
  bound that fully unrolls the loops). differential verifies in ~2–3 min again.
  Sound: unwinding assertions stay on and pass, the property still holds for all
  InlineVec<u8, 8> inputs; only verification breadth (8 vs 16 bytes) narrows.
• Add a regression test (tests/kani/Iterator/chunks_exact_split_at.rs): a
  freestanding minimal reproducer of the constant-propagation failure.
• Fix a latent compiletest --timeout deadlock (tools/compiletest): it
  waited on the child before draining stdout/stderr, so any test whose output
  exceeds the pipe buffer hung until the timeout — hanging every perf test once
  the suite passed --timeout. Now drains both pipes on dedicated threads
  (removes the unused read2 helper).
• Bound per-test wall time in scripts/kani-perf.sh (--timeout, default
  2400 s, override via KANI_PERF_TEST_TIMEOUT). Sized above the slowest
  legitimate test: s2n-quic-core runs 34 harnesses (~1250 s; the largest is
  sync::spsc::tests::alloc_test ~375 s, not differential) — not a regression,
  as it passes cap-free on main (~2650 s full suite, matching this branch).
• Harden the perf job (.github/workflows/kani.yml): fit the
  timeout-minutes budgets and add nick-fields/retry@v3 for spot-preemption.
• Skip tests/perf/overlays in the rustfmt sweep (scripts/kani-fmt.sh):
  overlay files reference submodule-only sibling mods, so rustfmt can't
  standalone-parse them.
• Kani copyright header on the overlay (with upstream attribution).
• Gate debug-only CallGraph::dump_* on cfg(debug_assertions)
  (kani-compiler/.../reachability.rs): otherwise release builds trip dead_code.

Not addressed

This does not fix the upstream rustc regression itself and does not skip any
harness. A deeper fix (a CBMC-side improvement to the niche/split_at
constant-propagation, or filing the reproducer upstream) is a follow-up; the
regression test added here documents the trigger.

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.