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, 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 literally met. This is left as a committee question open across the sentence-pair challenges, and is disclosed under Known limitations.

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 — the double-drop the body's ptr.add(1)-before-f ordering exists to prevent. 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 via a mirroring kani::assume (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. Each body is written once for arbitrary T and instantiated per shape, mirroring its _u8 counterpart.

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). Added CI cost ≈57 s total at the pinned Kani 0.67 / CBMC 6.10.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 (12 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, and Drop of a both-ends-consumed DropToken vector. forget_allocation_drop_remaining shares the remaining-range drop path; __iterator_get_unchecked remains the assume-mirror noted above.

Upstream Kani contributions

proof_for_contract can't resolve generic trait-impl methods at the pinned Kani, which is why __iterator_get_unchecked is verified through a mirror rather than a contract. We fixed that upstream in model-checking/kani#4865 (merged; not yet in this pin).

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). This is the acceptance question open across the sentence-pair challenges; deferring to the committee on whether representative-type coverage satisfies the clause, and 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 (+977 / −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.

Add mod verify harnesses for all 22 Challenge 24 targets in IntoIter and the spec_extend / spec_from_iter / spec_from_elem / extract_if helpers. Harnesses exercise the real shipped bodies (no cfg(kani) rewrites) over symbolic-length inputs, with every kani::assume paired with a satisfied kani::cover. Unbounded and generic-T are not literally met (committee gate) and are disclosed. Additive only.

…y, drop) Add harnesses instantiating the IntoIter / spec_* move and index paths over element shapes the existing u8/i8/() harnesses do not exercise: an over-aligned type, an odd-stride type, a validity-niche type, and a destructor type across the move/consume paths. Existing harnesses are unchanged; additive only.

…r states

… states

…le iterator states

…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.

…harnesses

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

kasimte mentioned this pull request Sep 25, 2026

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

Merged

kasimte added 3 commits September 28, 2026 12:39

Challenge 24: verify IntoIter safety from arbitrary reachable iterato…

56cabac

…r states

Challenge 24: verify IntoIter::fold from arbitrary reachable iterator…

8fe1f3a

… states

Challenge 24: verify try_fold, next_chunk, into_vecdeque from reachab…

25d1371

…le iterator states

kasimte mentioned this pull request Sep 30, 2026

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: add non-vacuity covers to the three symbolic-length u8 …

f7fa1f1

…harnesses

Navigation Menu

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 6 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