From aa4b14529885d840cc4ee78d73d1c8d4b61b3d75 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 3 Aug 2026 16:40:03 +0000 Subject: [PATCH] Respect new_unchecked precondition in IndexRange proof harnesses The proof_for_contract harnesses for IndexRange::next_unchecked and IndexRange::next_back_unchecked, introduced in commit a0fca1cc2f8b03f559d2fb9c09df97d5089e7ddf ("A bunch of LLM-generated contracts (#451)"), construct their IndexRange via `IndexRange::new_unchecked(start, end)` with entirely unconstrained `start` and `end`. That violates new_unchecked's documented safety precondition (and #[requires] contract) `start <= end`: the assumption provided by the contract under verification only takes effect at the call to next_unchecked / next_back_unchecked, after the UB of the unchecked constructor call has already happened. The violation is currently invisible in CI because run-kani.sh passes --no-assert-contracts; with dependency contracts asserted (the Kani default since model-checking/kani#3802), proof_for_index_range_next_back_unchecked fails on the asserted `start <= end` clause. Constrain both harnesses with `kani::assume(start <= end)`. The stronger `start < end` required by the functions under verification continues to be assumed from their own contracts, preserving the intent of the harnesses. Verified (Kani 152c6a8c + CBMC 6.10.0) that all three ops::index_range::verify harnesses pass both with and without --no-assert-contracts. Co-authored-by: Kiro --- library/core/src/ops/index_range.rs | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/library/core/src/ops/index_range.rs b/library/core/src/ops/index_range.rs index bf8083194391a..1fc721b3a9e2e 100644 --- a/library/core/src/ops/index_range.rs +++ b/library/core/src/ops/index_range.rs @@ -250,6 +250,10 @@ mod verify { fn proof_for_index_range_next_unchecked() { let start = kani::any::(); let end = kani::any::(); + // Respect new_unchecked's safety precondition (start <= end); the + // stronger requirement of next_unchecked (start < end) is assumed + // from its contract. + kani::assume(start <= end); let mut range = unsafe { IndexRange::new_unchecked(start, end) }; @@ -260,6 +264,10 @@ mod verify { fn proof_for_index_range_next_back_unchecked() { let start = kani::any::(); let end = kani::any::(); + // Respect new_unchecked's safety precondition (start <= end); the + // stronger requirement of next_back_unchecked (start < end) is + // assumed from its contract. + kani::assume(start <= end); let mut range = unsafe { IndexRange::new_unchecked(start, end) };