Challenge 24: verify Vec IntoIter and spec_* function safety with Kani by kasimte · Pull Request #689 · model-checking/verify-rust-std

kasimte · 2026-09-18T17:45:03Z

Towards #285.

Kani harnesses for Challenge 24: Verify the safety of Vec functions part 2 — Vec::IntoIter and the specialization helpers it routes through (spec_extend, spec_from_iter, spec_from_iter_nested, spec_from_elem, from_elem, extract_if). 47 harnesses across all 22 listed functions. Each runs the function's real shipped body — no #[cfg(kani)] rewrite, no kani::assume(false) on a real branch — at symbolic length where tractable, fixed small sizes where noted, and asserts the observable effect rather than just absence of UB. All pass via scripts/run-kani.sh.

Unbounded length and generic T are not met; both are disclosed under Limitations. Whether representative-type, bounded coverage satisfies these clauses is a judgment we defer to the reviewers.

What the harnesses check

Real bodies at symbolic length. Vecs are built with kani::slice::any_slice_of_array + to_vec, so the pointer-walking loops (next/next_back, fold/try_fold, advance_by/advance_back_by) run a symbolic number of iterations up to the backing size (64 for IntoIter, smaller where noted).
Functional postconditions, not just non-UB. For example: next/next_back return the exact first/last element and shrink length by one; advance_by(k) returns Ok iff k <= len; fold visits exactly len elements; from_elem(e, n) yields length n with every v[j] == e; size_hint == (len, Some(len)).
Drop and early-exit paths are hit, not assumed. try_fold short-circuits (Err) in both a u8 and a Drop-carrying variant, exercising IntoIter's real Drop, so a double-drop on the short-circuit path would be caught. extract_if::next writes through the real vec.as_mut_ptr().add(i).
ZST arm. The separate T::IS_ZST branch (byte-walking end, fixed ptr) is verified on Vec<()> at symbolic length.
__iterator_get_unchecked. Already ships #[requires(i < self.len())] + kani::modifies(self) on main with no exercising harness. Verified here directly as a proof_for_contract at two instantiations — u8 (from arbitrary reachable states up to the backing bound) and the odd-stride [u8; 3] (see Upstream Kani contributions).
Non-vacuity. 29 kani::cover reachability witnesses across the suite.

Element-type coverage (+8 harnesses)

These reach properties of T the u8/() instantiations don't. Most share one generic body instantiated per shape, mirroring its _u8 counterpart; the [u8; 3] get_unchecked row is a second proof_for_contract (see Upstream Kani contributions).

harness	method	property
`check_into_iter_next_al16`	`next`	over-alignment (`#[repr(align(16))]`): 16-byte stride
`check_into_iter_next_bool`	`next`	validity niche
`check_into_iter_next_droptoken`	`next`	forward move-out of a `Drop` type
`check_into_iter_next_back_droptoken`	`next_back`	backward move-out drop (distinct geometry)
`check_into_iter_get_unchecked_arr3`	`__iterator_get_unchecked`	odd (non-power-of-two) stride `add(i)`
`check_spec_extend_intoiter_droptoken`	`spec_extend` (IntoIter)	bulk-move + `forget_remaining_elements`, no double-drop
`check_from_iter_intoiter_droptoken`	`SpecFromIter` (IntoIter)	`ManuallyDrop` + `from_parts` ownership transfer
`check_extract_if_next_droptoken`	`ExtractIf::next`	leak-amplification backshift-on-drop

Shapes: Al16 (#[repr(align(16))]), [u8; 3] (odd stride), bool (validity niche), DropToken (real Drop). Verified at the pinned Kani 0.68.0 / CBMC 6.11.0.

Arbitrary reachable iterator states (+13 harnesses)

The harnesses above start from a fresh iterator (ptr == buf). These re-check the surface from arbitrary reachable states: a symbolic number of elements consumed from each end, so ptr sits at any valid interior position. State is built through advance_by/advance_back_by (each verified by its own harness), reaching every state iteration can produce, and results are checked against a pre-conversion snapshot at the advanced offsets.

Covered from these states (13 of the 14 IntoIter targets): next, next_back, size_hint, as_slice, as_mut_slice (with a write-through check), advance_by, advance_back_by, fold, try_fold, next_chunk, into_vecdeque, __iterator_get_unchecked (its u8 proof_for_contract), and Drop of a both-ends-consumed DropToken vector. forget_allocation_drop_remaining shares the remaining-range drop path.

Upstream Kani contributions

__iterator_get_unchecked lives in a generic trait impl (Iterator for IntoIter). The harness names the allocator explicitly (<IntoIter<u8, Global> as core::iter::Iterator>::…) so it resolves as a proof_for_contract target. The enabling upstream fix is model-checking/kani#4865 (instantiate path generic arguments during type resolution), which we authored and which merged into this pin. The harnesses verify the method's shipped #[requires(i < self.len())] + kani::modifies(self) contract directly, at the u8/Global and [u8; 3]/Global instantiations.

How to verify

Scoped to these harnesses, from the repo root:

kani verify-std -Z unstable-options ./library -Z function-contracts -Z mem-predicates \
  -Z float-lib -Z c-ffi -Z loop-contracts -Z quantifiers -Z stubbing --no-assert-contracts \
  --harness vec::into_iter::verify --harness vec::extract_if::verify \
  --harness vec::spec_extend::verify --harness vec::spec_from_elem::verify \
  --harness vec::spec_from_iter::verify --harness vec::spec_from_iter_nested::verify \
  --cbmc-args --object-bits 12

Expected: Complete - 47 successfully verified harnesses, 0 failures, 47 total., every cover satisfied.

Limitations (disclosed)

Unbounded length: not met. All harnesses are length-bounded (64 for IntoIter, smaller where noted). A loop-contract route to genuine unboundedness was measured, but CBMC does not terminate on the kani::mem::same_allocation invariant the havoced IntoIter heap-pointer loops need; the same invariant over a stack array does verify, so the limit is specific to this heap-pointer shape, not the predicate.
Generic T: not met. Representative element types only (u8, (), a Drop token, and the over-aligned / odd-stride / niche shapes above). Whether representative-type coverage satisfies the clause is a judgment we defer to the reviewers; we will complete a single-generic-body conversion promptly on a favorable ruling.
Allocation-heavy bounds. extract_if::next and the default from_iter exceed the CI-standard --object-bits 12 budget at larger sizes; the Drop-token harnesses use a fixed size of 4 (drop obligations are per-element identical). Each bound is noted in-code.
Growth paths. spec_extend pre-sizes the destination, so its copy path is verified; element-by-element growth routes through extend_desugared, and SpecFromElem's T: Clone default through extend_with — both Challenge 23 targets, not claimed here.
Every changed line is additive (+976 / −0 across 7 files); no runtime logic is modified.

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

…king#4865) Contracts on a trait method whose type carries a concrete generic argument — `<CStr as Index<RangeFrom<usize>>>::index`, or a concrete instantiation of a generic self type — failed to resolve with `MissingTraitImpl`. `resolve_ty` returned the definition's identity type (`RangeFrom<usize>` came back as `RangeFrom<Idx>`), so the arguments written in the path were parsed but never applied. This PR applies them, in `resolve_ty`'s `Type::Path` arm, via the new `instantiate_path_args`. ## Verification The tests live in the standard `tests/kani` and `tests/expected` suites (CI runs them); each has a definite outcome: | test (`-Zfunction-contracts`) | expect | |---|---| | `tests/kani/FunctionContracts/generic_argument_instantiation.rs` | **6 targets verify.** A primitive argument resolved before (regression guard); the five generic shapes resolve *only* with this change — a generic argument, a generic self type (associated-type return, `where`-bounded method), a concrete DST self, a generic `impl` at a concrete instantiation, and a type with a lifetime parameter beside a type parameter (lifetime erased). | | `tests/expected/function-contract/generic_arg_unimplemented.rs` | **still fails `MissingTraitImpl`** *(expected-output test — this diagnostic is the pass)* — `<S as Generic<Wrap<u16>>>::generic` is genuinely not implemented, so valid targets resolve without over-resolving invalid ones. | | `tests/expected/function-contract/generic_method_unimplemented.rs` | **still fails `MissingTraitImpl`** *(expected-output test — this diagnostic is the pass)* — a trait method with its own generic parameter (`fn compute<T>`) is out of scope (see below). | Confirmed on nightly-2026-09-22 (Kani 0.68.0, CBMC 6.11.0): all six verify; with the fix reverted, the generic targets fail to resolve while the primitive resolves. The `cross_module_multiple_impls` (7/7), `multiple_inherent_impls` (3/3), and resolver unit (41/41) suites are unchanged. Mechanism: this is the "trait functions with generic parameters" limitation described in [model-checking#1997](model-checking#1997 (comment)). The trait's arguments already reach trait-impl resolution, but each came back uninstantiated from `resolve_ty`, and full `Instance::resolve` cannot match a concrete impl from a free parameter. Making the arguments concrete fixes that; any shape that cannot be resolved (const-generic arguments, omitted defaulted parameters) keeps the old uninstantiated type, so nothing that resolved before changes. No partial-resolution machinery is needed — with concrete arguments, the existing full resolution matches. These are not hypothetical. An iterator adapter's `__iterator_get_unchecked` (a generic self type) is another std-library method of this shape: the Challenge 16 and Challenge 24 submissions ([model-checking/verify-rust-std#549](model-checking/verify-rust-std#549), [model-checking/verify-rust-std#689](model-checking/verify-rust-std#689)) disclose it and fall back to `kani::assume` mirror harnesses. What this change reaches there: closure-free adapters resolve (`Cloned`, `Zip`); `Map`/`Filter` do not, since `fn`/closure types aren't supported by `resolve_ty`. Challenge 24's `<vec::IntoIter<u8> as Iterator>::__iterator_get_unchecked` resolves only with the allocator written out (`IntoIter<u8, std::alloc::Global>`, which needs `allocator_api`): omitted trailing parameters with declared defaults are not filled and keep the uninstantiated type. Related to model-checking#1997 — this handles a type carrying concrete generic arguments: a generic trait argument, or a generic self type instantiated to concrete types, against a concrete or generic `impl`. A trait method with its own generic parameter still fails to resolve — that parameter is not part of the path, so nothing here binds it. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

…el-checking#4915) A `proof_for_contract` target that omits a trailing generic parameter with a declared default failed to resolve with `MissingTraitImpl`. For example `<Vec<u8> as Trait>::m`, or the natural spelling of `<vec::IntoIter<u8> as Iterator>::__iterator_get_unchecked`, a target in the Challenge 24 submission (model-checking/verify-rust-std#689); both omit the allocator parameter. The parameter-count check kept the uninstantiated type instead of filling the default. This PR fills an omitted trailing parameter from its declared default, instantiated with the arguments so far, matching what rustc does for omitted arguments. The logic lives in `default_type_arg`, called from `instantiate_path_args`'s substitution loop. A path written with no generic arguments at all (a bare `Wrapper` for `struct Wrapper<T = u8>`) is treated as an empty argument list, so an all-defaulted type resolves too. Parenthesized arguments keep the uninstantiated type. ## Verification | test (`-Zfunction-contracts`) | expect | |---|---| | `tests/kani/FunctionContracts/generic_default_argument_fill.rs` | **5 targets verify.** A std container default (`Vec<u8>` fills `A = Global`); a sibling impl with a distinct postcondition (`Vec<u16>`), so each harness only verifies if resolution picks its own impl; a default referencing an earlier parameter (`Pair<T, U = T>` at `Pair<u8>` fills `U = u8`); the explicit spelling (`Vec<u16, std::alloc::Global>`) unchanged; and an all-defaulted type written with no argument list (`AllDefault` for `struct AllDefault<T = u8>`) fills `T = u8`. | | `tests/expected/function-contract/generic_default_missing_required.rs` | **still fails `MissingTraitImpl`** *(expected-output test; this diagnostic is the pass)*. `NoDefault<u8>` omits a parameter with no default, so only declared defaults are filled. | | `tests/expected/function-contract/generic_default_missing_bare.rs` | **still fails `MissingTraitImpl`** *(expected-output test; this diagnostic is the pass)*. `NoDefaultBare` written with no argument list omits a parameter with no default, so the no-arguments path still keeps the uninstantiated type. | | `tests/expected/function-contract/generic_default_const_param.rs` | **still fails `MissingTraitImpl`** *(expected-output test; this diagnostic is the pass)*. `WithConst<u8>` omits a defaulted **const** parameter; only defaulted type parameters are filled, so the const default is not filled and the target keeps the uninstantiated type. | The four original targets were confirmed locally when this PR was first submitted (`generic_default_argument_fill` 4/4, the two negatives failing `MissingTraitImpl`, resolver suites unchanged at `generic_argument_instantiation` 6, `cross_module_multiple_impls` 7, `multiple_inherent_impls` 3). This revision adds the no-arguments case (`check_all_parameters_defaulted`) and the `generic_default_missing_bare` negative; CI runs the full suite on the pinned toolchain. Scope: type parameters only. A const parameter (with or without a default), and any argument that cannot be resolved, keep the uninstantiated type, as before. Defaults are instantiated structurally (no normalization), matching how `resolve_ty` already hands `tcx.type_of` results forward. Resolves model-checking#4914. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

kasimte requested a review from a team as a code owner September 18, 2026 17:45

feliperodri added the Challenge Used to tag a challenge label Sep 20, 2026

This was referenced Sep 25, 2026

Instantiate path generic arguments during type resolution model-checking/kani#4865

Merged

Contract targets that omit defaulted generic parameters fail to resolve model-checking/kani#4914

Closed

kasimte mentioned this pull request Sep 30, 2026

Fill omitted defaulted generic parameters during type resolution model-checking/kani#4915

Merged

Challenge 24: IntoIter + spec_* harness suite (squashed)

815b42b

kasimte force-pushed the 24-build branch from f7fa1f1 to 497cba4 Compare October 7, 2026 00:23

Challenge 24: verify __iterator_get_unchecked via proof_for_contract

d5fa4f0

kasimte force-pushed the 24-build branch from 497cba4 to d5fa4f0 Compare October 7, 2026 04:32

Navigation Menu

Repository navigation

Challenge 24: verify Vec IntoIter and spec_* function safety with Kani - #689

Challenge 24: verify Vec IntoIter and spec_* function safety with Kani#689
kasimte wants to merge 2 commits into
model-checking:mainfrom
kasimte:24-build

kasimte commented Sep 18, 2026 •

edited

Loading

Uh oh!

This branch has not been deployed

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Conversation

kasimte commented Sep 18, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

What the harnesses check

Element-type coverage (+8 harnesses)

Arbitrary reachable iterator states (+13 harnesses)

Upstream Kani contributions

How to verify

Limitations (disclosed)

Uh oh!

This branch has not been deployed

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

kasimte commented Sep 18, 2026 •

edited

Loading