Conversation
68e2629 to
c1620b6
Compare
74 harnesses proving safety of all 10 unsafe functions and 17 safe abstractions listed in Challenge 16, across 13 iterator adapter files. Unbounded verification via large symbolic arrays, loop contracts, and inductive decomposition. 4 representative types (u8, (), char, (char,u8)) cover all behavioral axes of the generic code.
There was a problem hiding this comment.
Pull request overview
Adds Kani-based formal verification coverage for iterator adapter implementations in library/core/src/iter/adapters/, including harnesses and contract/invariant annotations to justify the safety of unsafe internals and safe abstractions.
Changes:
- Add
#[cfg(kani)]verification modules with Kani harnesses across multiple iterator adapters. - Add/extend safety contracts (
#[requires(...)]) and Kani loop-invariant annotations (#[cfg_attr(kani, ...)]) to enable (mostly) unbounded verification. - Document verification assumptions/limitations inline (e.g., bounded unwind in some harnesses).
Reviewed changes
Copilot reviewed 13 out of 13 changed files in this pull request and generated 6 comments.
Show a summary per file
| File | Description |
|---|---|
| library/core/src/iter/adapters/zip.rs | Adds contracts/loop-invariant annotations and extensive Kani harnesses for Zip unsafe/specialized paths. |
| library/core/src/iter/adapters/take.rs | Adds loop-invariant annotations and Kani harnesses for Take specialized paths. |
| library/core/src/iter/adapters/step_by.rs | Adds Kani harnesses exercising original_step via multiple entry points. |
| library/core/src/iter/adapters/skip.rs | Adds Kani harnesses for Skip::__iterator_get_unchecked. |
| library/core/src/iter/adapters/map.rs | Adds Kani harnesses for Map unsafe methods. |
| library/core/src/iter/adapters/map_windows.rs | Adds Kani harnesses targeting buffer initialization/wrap, clone paths, and drop safety. |
| library/core/src/iter/adapters/fuse.rs | Adds Kani harnesses for Fuse::__iterator_get_unchecked. |
| library/core/src/iter/adapters/filter.rs | Adds bounded + inductive-step Kani harnesses for next_chunk-related unsafe operations. |
| library/core/src/iter/adapters/filter_map.rs | Adds bounded + inductive-step Kani harnesses for next_chunk-related unsafe operations. |
| library/core/src/iter/adapters/enumerate.rs | Adds Kani harnesses for Enumerate::__iterator_get_unchecked. |
| library/core/src/iter/adapters/copied.rs | Adds Kani harnesses for Copied::__iterator_get_unchecked and next_chunk specialization. |
| library/core/src/iter/adapters/cloned.rs | Adds a safety contract for next_unchecked and Kani harnesses for unsafe methods. |
| library/core/src/iter/adapters/array_chunks.rs | Adds comments about loop reasoning and Kani harnesses for next_back and bounded fold. |
- Remove unused `loop_invariant` import in take.rs and zip.rs (#[cfg_attr(kani, kani::loop_invariant(...))] does not require it) - Rewrite `Zip::get_unchecked` `#[requires(...)]` to avoid `self.index + idx` overflow, using subtraction-based bounds - Clarify "vacuous loop invariant" comments in take.rs and zip.rs — note that `true` is intentional and only enables loop-contract mode - Reword "Loop invariant:" to "Safety argument:" in array_chunks.rs to avoid implying a verified invariant where there is none (bounded harness) Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
- Remove unused `loop_invariant` import in take.rs and zip.rs (#[cfg_attr(kani, kani::loop_invariant(...))] does not require it) - Rewrite `Zip::get_unchecked` `#[requires(...)]` to avoid `self.index + idx` overflow, using subtraction-based bounds - Clarify "vacuous loop invariant" comments in take.rs and zip.rs — note that `true` is intentional and only enables loop-contract mode - Reword "Loop invariant:" to "Safety argument:" in array_chunks.rs to avoid implying a verified invariant where there is none (bounded harness)
|
Hi @feliperodri — addressed the Copilot review in commit e80e689:
All CI green on the fork test PR kasimte#2 (identical tree). Ready for another look when you have a moment. |
|
Thanks for bringing the branch up to date with |
There was a problem hiding this comment.
@kasimte This is strong, honest work — thank you for the transparent write-up of every limitation. To be clear up front about what's good: the source code is verified directly (no #[cfg(not(kani))] body substitution), and the unsafe trait-method harnesses are sound and non-circular — e.g. check_copied_get_unchecked_u8 does kani::assume(idx < iter.size_hint().0) (the documented precondition, not the safety conclusion), then lets CBMC check the real __iterator_get_unchecked(idx) for UB and asserts result == slice[idx]. That's a legitimate manual stand-in for proof_for_contract, and the #[requires] clauses faithfully match the assumed preconditions.
I'm requesting changes on two points.
1. The 5 loop_invariant(true) annotations (take.rs, zip.rs)
All five added loop invariants are #[cfg_attr(kani, kani::loop_invariant(true))], and the code comments call them "intentionally vacuous ... only to enable loop-contract mode." The concern: these loops perform get_unchecked(i) / __iterator_get_unchecked(i), whose safety depends on the induction variable staying < len. A true invariant does not establish that inductive bound, which leaves two possibilities that need to be resolved:
- If loop-contract mode genuinely abstracts the loop, the havoc'd
iis constrained only bytrue, so the indexed access is exercised at an arbitrary index — the proof should then either fail or be relying on something else to re-derive the bound. Please explain why it's sound. - If instead the loop is effectively still being unwound (bounded by
MAX_LEN), then these functions are bounded, not "unbounded via loop contracts" as the summary states — in which case the claim should be corrected.
Either way, please provide a meaningful loop invariant that captures the bound the get_unchecked relies on (e.g. i <= len / self.index <= self.len), as you did locally for array_chunks::fold, or a concrete justification that true is sufficient and the coverage is genuinely unbounded. (This is the same trivial-invariant issue that #327's loop_invariant(true) and the discussion on #544 ran into.)
2. Decorative safety contracts (9 of 10 #[requires])
9 of the 10 #[requires(...)] (the __iterator_get_unchecked / get_unchecked trait methods) have no #[kani::proof_for_contract], so Kani never checks them as contracts — a plain #[kani::proof] that calls the method ignores its contract. I understand proof_for_contract doesn't support trait-impl methods today, and that you mirror each precondition with a kani::assume in a real harness (which is what actually does the verification). That's reasonable, but as written the annotation and the assumed precondition are independent and can silently drift. Please either:
- add a brief note in the code that these
#[requires]are documentation-only (verification is via the mirroredassumeinmod verify), and/or - keep a single source of truth so the contract and the harness precondition can't diverge.
Minor / for the committee
The disclosed limitations — bounded array_chunks::fold, Range<u8> substitution for next_back_remainder, and 4 concrete types standing in for a generic T — are reasonable and clearly documented; I'll defer to the maintainers on whether they satisfy the "unbounded" and "generic" wording of the challenge.
Overall this is close, and the verification approach is sound where it counts. Resolving the loop-invariant question (item 1) is the main blocker.
|
Thanks for the thorough review, @feliperodri — working through both items now (meaningful invariants + the requires notes); will push updates and a full response shortly. |
Replace the five vacuous #[kani::loop_invariant(true)] annotations with real inductive bounds that capture the indexed-access bound (take spec_fold / spec_for_each: kani::index <= end; zip fold: kani::index <= len; nth: self.index <= end; super_nth: self.index <= self.len). Each verifies with base and step checks. Document each trait-impl #[requires] as precondition documentation, verified via the mirrored kani::assume in mod verify. Add a checked #[ensures] with a proof_for_contract harness for the inherent StepBy::original_step, and rewrite Skip::__iterator_get_unchecked's precondition in overflow-safe subtraction form. Correct the bounded-vs-unbounded wording in the harness comments to match what the harnesses verify.
|
Thanks for the detailed review, @feliperodri. Both items are addressed in the pushed commits; details below. 1. Loop invariants (the 5
|
| Site | Invariant now |
|---|---|
take.rs spec_fold / spec_for_each |
kani::index <= end |
zip.rs TRANC fold |
kani::index <= len |
zip.rs TRA nth |
self.index <= end |
zip.rs super_nth |
self.index <= self.len |
(kani::index is Kani's handle for a for loop's iteration count, per the loop-contracts reference; the loop's own pattern variable is not in scope in the invariant position.)
On your question of why the abstracted loop with true was sound rather than failing at an arbitrary index: the loops are genuinely abstracted, not unwound — the loop_invariant base/step checks appear in the verification output — and Kani retains the loop guard around the abstracted body (loop-contracts reference), so the havoc'd index stays < end and get_unchecked(i) was only ever checked under that bound. The explicit invariants now state that bound directly, so it is visible in the annotation and any drift is checkable.
2. Trait-impl #[requires]
Most of these #[requires] are already upstream (#435); because they sit on trait-impl methods, proof_for_contract cannot check them there, so they remain unchecked in main. This PR's harnesses are what exercise them: each #[requires] now carries a note that it documents the precondition and is verified via the mirrored kani::assume in the named verify:: harness, with the two to be kept in sync. I re-checked each assume against its contract expression and found them consistent.
Where proof_for_contract can resolve the method — the inherent StepBy::original_step — this push adds #[ensures(|result| result.get() - 1 == old(self).step_minus_one)] with a proof_for_contract harness. Skip::__iterator_get_unchecked's precondition is also rewritten in the overflow-safe subtraction form, matching the Zip::get_unchecked fix.
Claim corrections
The PR body and the harness comments now separate the two axes: loop contracts remove the unwinding bounds on the annotated loops, while harness input arrays remain bounded at MAX_LEN (5000/u8, 50/char+tuple; ZST at isize::MAX; the spec_fold inductive step is the arbitrary-length case). "unbounded" now appears only where it is literally true, and the requirements table leaves the criterion judgment to the committee.
Also in this push
- Merged current
main(nightly-2025-11-25 subtree update); no runtime-logic changes to the 27 target functions. - CI on the updated branch: green — all
Verify stdpartitions,autoharness, andupstream_test(rustfmt) passing.
The remaining gaps — input-domain bounds and concrete types for T — are disclosed in the body; glad to track them however the committee prefers.
The functional asserts force CBMC to bit-blast the input array ("array too
large for flattening" at u32::MAX), so asserted harnesses keep their proven
bounds and assert-free companions carry the length axis. Accessor harnesses
that already had no functional assert are raised in place. char keeps its
bounded harness: per-element validity constraints cap both tiers far lower.
…-harness scope notes The Zip harness havocs index across its full valid range and pins the returned pair to both source slices. The side-effecting Map source is exercised on Zip (measured: the same layer through Skip's n arithmetic times out at every tried bound). The filter/filter_map notes record the N >= 1 scope of the write-index SAFETY argument.
|
The latest commits extend the harness coverage in three ways:
|
One cover per assume-bearing harness (55 across 11 adapter modules), after the last assume: each run's property report now witnesses that every assumption set is satisfiable. Pattern from model-checking#637.
|
Pushed 9a8654f: every |
feliperodri
left a comment
There was a problem hiding this comment.
Thanks @kasimte. Reviewed against all three open Challenge 16 solutions (#549/#602/#632) with our vacuity tooling + local Kani (pinned Kani 0.67.0 / CBMC 6.8.0). Of the three, we're prioritizing this one — it's the soundest: the earlier loop_invariant(true) issue (T2b) is fully resolved (0 occurrences; the 5 invariants are now real inductive bounds like kani::index <= end / self.index <= len), no cfg(kani) body swaps, no assume-the-conclusion, symbolic inputs, and a representative local run passed (step_by original_step proof_for_contract, cloned get_unchecked, zip nth, take spec_fold, zip spec_fold_unbounded — all VERIFICATION SUCCESSFUL).
Requesting changes because it does not yet meet the challenge's stated success criteria:
- Generic-
Tnot met (hard requirement). Every harness is monomorphized to concrete element types (u8/char/unit/tuple/DropToken). The challenge requires the proofs to hold for genericTwith no monomorphization. - Unbounded not met for several targets.
array_chunks::fold,filter::next_chunk_dropless,filter_map::next_chunk,zip::spec_foldare unwind-capped (unwind(9), MAX_LEN≈8),map_windowsis exercised with only 2next()calls, andzip::get_uncheckedis bounded to MAX_LEN=64. The challenge requires arbitrary length. - The three
*_unboundedharnesses re-implement the loop body (hand-written inductive fragments doingget_unchecked_mut/copy_nonoverlapping) rather than proving the real function — so they don't actually verify the shipping code's unbounded behavior. - Contracts largely unproven as contracts. Only
step_by::original_stephas a#[kani::proof_for_contract]; the other ~10#[requires]are mirrored viakani::assumein plain proofs (understood given Kani can't target trait-impl methods, but the criterion says "write and prove the contract").
To be accepted this needs generic-T proofs (or a documented, committee-accepted rationale for the Kani limitation) and genuinely unbounded proofs of the real functions. Great progress — this is the front-runner.
# Conflicts: # library/core/src/iter/adapters/filter.rs
… allows - array_chunks::fold: source-level loop contract (real invariant + explicit loop_modifies) replaces the unwind cap; backing symbolic at MAX_LEN 5000 - zip::get_unchecked arbitrary-state harness raised from MAX_LEN 64 to 5000 - map_windows: arbitrary-state push/accessor/drop proofs over the full documented Buffer invariant range (any prior push count), u8 and drop-glue - delete the three *_unbounded loop-body re-implementations; real-function proofs and precisely documented walls replace them - zip::spec_fold: the TrustedLen loop-contract route is tool-walled at the pin (loop_invariant method-call lowering defect); wall stated at the harness - filter/filter_map: structural wall stated (traversal loop lives in the generic try_for_each default behind a capturing closure) - cite kani#1997 at every trait-impl contract note; fix stale comments
…oofs The arbitrary-state harnesses proved UB-absence and invariant preservation but did not pin the operation's effect. Both now assert that push advances start by one (or wraps it to the front at the boundary) and that the pushed element becomes the back of the window, for the Copy and drop-glue variants.
|
Thanks for the detailed review. Head
|
…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.
…cking#4916) A contract target whose type arguments include a fn-pointer type (`<Wrap<fn(u8) -> u8> as Probe>::probe`, or the standard adapters' `<std::iter::Map<std::slice::Iter<u8>, fn(&u8) -> u8> as Iterator>::__iterator_get_unchecked`) failed to resolve: `resolve_ty`'s `Type::BareFn` arm returned `unsupported`, so the fn-pointer argument was dropped and the concrete impl could not match. This PR builds the fn-pointer type in that arm (Rust ABI, non-variadic; inputs and output resolved recursively; lifetimes erased like every other path argument; safety carried through), so these targets resolve. ## Verification | test (`-Zfunction-contracts`) | expect | |---|---| | `tests/kani/FunctionContracts/generic_fn_pointer_argument.rs` | **3 targets verify.** A plain fn-pointer argument (`fn(u8) -> u8`); a reference-carrying fn pointer (`fn(&u8) -> u8`) whose impl type is late-bound (`for<'a> fn(&'a u8) -> u8`), where the erased argument still matches; and an `unsafe` fn pointer (safety carried through the built signature). The three impls have distinct postconditions, so each harness verifies only if resolution picks its own fn-pointer instantiation. | | `tests/expected/function-contract/generic_fn_pointer_cabi.rs` | **still fails to resolve** *(expected-output test; the diagnostic is the pass)*. A non-Rust-ABI fn pointer (`extern "C" fn(u8) -> u8`) is not built by the arm and keeps the uninstantiated type. | Confirmed locally: `generic_fn_pointer_argument` verifies 3/3; `generic_fn_pointer_cabi` fails to resolve (the expected diagnostic); the resolver suites are unchanged (`generic_argument_instantiation` 6, `cross_module_multiple_impls` 7, `multiple_inherent_impls` 3). The std target `<std::iter::Map<std::slice::Iter<u8>, fn(&u8) -> u8> as std::iter::Iterator>::__iterator_get_unchecked` resolves, failing only on the absent contract (`__iterator_get_unchecked` has no contract). CI runs the full suite on the pinned toolchain. Mechanism: fn-pointer types were the last commonly-written argument shape `resolve_ty` rejected outright. Building the signature (Rust ABI only, non-variadic, arguments resolved through the same `resolve_ty` recursion, lifetimes erased, `unsafe` safety carried) makes the argument concrete, and the existing full resolution then matches the impl. Anything the arm does not build (a non-Rust ABI, or a variadic fn pointer) keeps the old uninstantiated type, so nothing that resolved before changes. Resolves model-checking#4909. That issue reports this wall for the standard iterator adapters: `Map` and `Filter` carry a mapping or predicate function argument whose fn-pointer instantiation could not be named. The Challenge 16 submission (`model-checking/verify-rust-std#549`) falls back to a `kani::assume` mirror harness for `Map`'s `__iterator_get_unchecked` for this reason; with the arm, `Map<Iter<u8>, fn(&u8) -> u8>` resolves as a `proof_for_contract` target. As model-checking#4909 notes, closure instantiations stay out of reach for any resolver change (a closure's type cannot be written in path syntax), so only the fn-pointer instantiations are addressed here. `BareFn` is also one of the two argument kinds model-checking#4830 names as prerequisites for the semantic-resolution rewrite; it lands here on its own, ahead of that refactor. Scope: lifetimes are erased, so a higher-ranked fn pointer resolves against an erased signature; if a `fn(&'static u8) -> u8` sibling impl also exists, the higher-ranked target resolves to it instead. The `generic_fn_pointer_higher_ranked.rs` fixme test documents this, and binding the late-bound regions is tracked as a follow-up (model-checking#4933). By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
Towards #280 (Challenge 16: Verify the safety of Iterator functions).
83 Kani harnesses covering all 10 unsafe functions and all 17 safe abstractions across 13 iterator adapter files in
library/core/src/iter/adapters/. Most unsafe-method#[requires]preconditions already exist upstream (#435);mainhas no harnesses for these adapters, so this PR adds the verification layer — the harnesses that exercise each precondition and check the guardedget_unchecked/next_uncheckedfor UB.Unbounded length and generic
Tare not literally met. This is left as a committee question open across the sentence-pair challenges, and is disclosed under Known limitations.Requirements checklist
Zip::get_uncheckedproven directly over arbitrary reachable state, and transitively vianext/nth/fold). Of the 10#[requires], 7 are upstream (#435); this PR adds 2 and rewritesSkip's overflow-safe.#[ensures]onoriginal_step(proof_for_contract), arbitrary-state proofs onmap_windows, and drop-glue/panicking-drop variants.array_chunks::foldand the annotatedtake/ziploops verify via source-level loop contracts (no unwind bounds);map_windowsis proven from arbitrary buffer state; u8/ZST accessor companions run atu32::MAX/isize::MAX.zip::spec_foldand thefilter/filter_mapchunk functions stay bounded at documented tool/structural walls. Deferred to the committee.Tu8,()(ZST),char(validity niche),(char,u8)(padding), and Clone types with real drop glue incl. a panicking destructor. Sibling challenges 0026/0029 waive this to primitive types. Deferred to the committee.pointer_dereferenceclass; invalid value — checked where raw bytes become typed; uninitialized reads — no check class at the repo's CI flags (Kani's uninit checking is opt-in, not inrun-kani.sh); mutating immutable bytes — no Kani check class (repo-wide tool scope, surfaced on #582).#[requires](7 from #435, 2 added, 1 rewritten overflow-safe) are precondition documentation, each mirrored by akani::assumein the harness that exercises it —proof_for_contractcan't resolve generic trait-impl methods at the pinned Kani (see Upstream Kani contributions). The inherentoriginal_stepcarries a checked#[ensures]viaproof_for_contract. Every harnesskani::assumeis paired with akani::covernon-vacuity witness.Known limitations
u32::MAX; char, whose per-element validity dominates, hits it earlier). Assertion-free UB companions verify the same unchecked accesses atu32::MAX(u8) andisize::MAX(ZST). Slice length is fully symbolic within each bound.filter/filter_mapchunk harnesses coverN >= 1; the SAFETY argument for the unchecked write (idx < Nwhenever the closure runs) requiresN >= 1.zip::spec_fold(tool wall). Its only sound loop invariant is the TrustedLen exactness relation, which needs asize_hintcall — and method calls insidekani::loop_invariantmis-lower at the pinned Kani (#[kani::loop_invariant]with a method call lowers the call with "not enough arguments", substituting a non-deterministic value kani#4796), so the loop can't carry a source-level contract. Verified by a bounded end-to-end harness.filter/filter_mapchunk functions (structural). The traversal loop lives in the genericIterator::try_for_eachdefault behind a capturing closure, so no adapter-level loop contract can attach, and contracting the shared default would route every std proof through the loop-contract transform (Loop contracts have no attach site for loops inside called iterator combinators (fold/try_for_each/collect) kani#4893). Verified by bounded end-to-end harnesses.next_back_remainder. UsesRange<u8>instead ofslice::Iterbecause CBMC exhausts resources on the pointer-heavy adapter chain; exercises the sameunwrap_err_uncheckedpath.T. Kani needs concrete types (CBMC operates on concrete GOTO programs), so a single generic proof isn't possible with this tool. The unsafe operations depend onsize_of/align_of/drop glue, not type identity; the type menu covers those axes. Deferred to the committee.Source code modifications
Six loop-contract invariants via
#[cfg_attr(kani, kani::loop_invariant(...))], all verified inductive (base + step), plus one explicit assigns clause:take.rsspec_fold/spec_for_each:kani::index <= endzip.rsfold:kani::index <= len;nth:self.index <= end;super_nth:self.index <= self.lenarray_chunks.rsfold:i <= inner_len, withkani::loop_modifies(&i, &accum)supplying the assigns clause CBMC can't inferZero impact on non-Kani builds. Contract changes vs
main: 7 of the 10#[requires]are upstream (#435, unchanged); this PR adds 2 (Cloned::next_unchecked,Zip::get_unchecked), rewritesSkip::__iterator_get_uncheckedin overflow-safe subtraction form, and adds 1 checked#[ensures]onoriginal_step.Upstream Kani contributions
These preconditions are checked through mirrored
kani::assumes becauseproof_for_contractcan't resolve generic trait-impl methods at the pinned Kani; we fixed that upstream in model-checking/kani#4865 (merged; not yet in this pin). TheMaptargets additionally need fn-pointer type arguments resolved in contract target paths; we fixed that in model-checking/kani#4916 (merged; not yet in this pin).Verification details (click to expand)
Quick verification
Expected:
Complete - 83 successfully verified harnesses, 0 failures, 83 total.Each assume-bearing harness also reports** 1 of 1 cover properties satisfied.Verification techniques
any_slice_of_array): asserted harnesses at 5000 (u8) / 50 (char, tuple), where the assertion forces array bit-blasting; assertion-free UB companions atu32::MAX(u8) /isize::MAX(ZST). Length fully symbolic within each bound.kani::index <= end/len,i <= inner_len) on the annotated loops intake.rs/zip.rs/array_chunks.rs, so Kani abstracts them without per-harness unwind bounds;array_chunks::foldadds an explicitkani::loop_modifies.Zip::get_uncheckedover its full valid state (indexhavoced0..=len, 5000 tier), andmap_windows'sBufferwithstarthavoced over its full invariant range (every state reachable after any number of pushes, hence any source length), for a Copy type and a drop-glue type.StepBy::original_step(inherent) —#[ensures]+#[kani::proof_for_contract].kani::assumesite is paired with akani::cover; each run's cover report surfaces any assumption that becomes unsatisfiable.Safety contracts
__iterator_get_unchecked#[requires(idx < self.it.size_hint().0)]next_unchecked#[requires(self.it.size_hint().0 > 0)]__iterator_get_unchecked#[requires(idx < self.it.size_hint().0)]__iterator_get_unchecked#[requires(idx < self.iter.size_hint().0)]__iterator_get_unchecked#[requires(self.iter.is_some() && idx < self.iter.as_ref().unwrap().size_hint().0)]__iterator_get_unchecked#[requires(idx < self.iter.size_hint().0)]next_unchecked#[requires(self.iter.size_hint().0 > 0)]__iterator_get_unchecked#[requires(self.n <= self.iter.size_hint().0 && idx < self.iter.size_hint().0 - self.n)]__iterator_get_unchecked#[requires(idx < self.size_hint().0)]get_unchecked#[requires(self.index <= self.a.size() && idx < self.a.size() - self.index && self.index <= self.b.size() && idx < self.b.size() - self.index)]original_step#[ensures(|result| result.get() - 1 == old(self).step_minus_one)]— checked viaproof_for_contractUnsafe functions (10/10)
__iterator_get_uncheckedu32::MAXcompanion)next_uncheckedu32::MAX, unit, char, tup)__iterator_get_uncheckedu32::MAXcompanion)__iterator_get_uncheckedu32::MAXcompanion)__iterator_get_uncheckedu32::MAX, unit, char, tup)__iterator_get_uncheckedu32::MAXcompanion)next_uncheckedu32::MAX, unit, char, tup)__iterator_get_uncheckedu32::MAX, unit, char, tup)__iterator_get_uncheckedMapsource)get_uncheckedindex <= lenstate at the 5000 tier, functional asserts) + transitive vianext/nth/foldSafe abstractions (17/17)
next_back_remainderfoldspec_next_chunknext_chunk_droplessnext_chunkas_array_refshould_panic, 2 arbitrary-state: u8 + drop-glue)as_uninit_array_mutpushstart <= Ninvariant range — both push branches at every reachable offset, with post-state effect assertions:startadvances or wraps, pushed element lands at the window's back)droporiginal_stepproof_for_contract)spec_foldspec_for_eachfoldnextnthnext_backspec_foldTest plan
tool_configpin (Kani 0.67.0 / CBMC 6.10.0) with the CI flag set incl.--no-assert-contracts: 83/83.diffblue/cbmcHomebrew tap, before any verification runs (a repo-wide macOS infra issue, not a verification failure); the ubuntu verify-std partitions and autoharness pass.By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.