Verify iter adapter unsafe methods + safe abstractions (challenge #16)#602
Verify iter adapter unsafe methods + safe abstractions (challenge #16)#602MavenRain wants to merge 3 commits into
Conversation
…del-checking#16) Kani harnesses for core::iter::adapters: - Unsafe (__iterator_get_unchecked / next_unchecked / get_unchecked): cloned, copied, enumerate, fuse, map, skip, zip. - Safe abstractions with internal unsafe: array_chunks::next_back_remainder, copied::spec_next_chunk, map_windows Buffer::{as_array_ref, as_uninit_array_mut, push, drop}, step_by::original_step, zip::{next, next_back}. Each harness takes a symbolic-length sub-slice of a fixed bounded array and is instantiated per representative element type ((), u8, char, (char, u8)) via macros. The generic unsafe trait methods use plain #[kani::proof] with the #[requires] precondition established by construction, since Kani cannot put contracts on generic trait methods (kani#1997). Signed-off-by: Onyeka Obi <softwareengineerasaservant@isurvivable.cv>
…ing#16) Adds Kani harnesses for the iterating / chunk-building iterator-adapter methods deferred from the initial model-checking#16 set for tractability: array_chunks::fold filter::next_chunk_dropless filter_map::next_chunk take::spec_fold / spec_for_each zip::nth / fold / spec_fold Each is instantiated over (), u8, char and a composite tuple type (32 harnesses total); all verify with 0 failures. These methods loop over a symbolic-length slice. Drafted without an explicit unwind bound, CBMC over-unwound the loop and timed out; adding assumption) plus a tightened MAX_LEN makes each verify in under a second.
upstream_test runs ./x fmt --check with rust-lang/rust's rustfmt.toml (style_edition 2024, use_small_heuristics = Max). Reflow the check_zip_safe! invocations and the Filter::new call one argument per line. Formatting only. Signed-off-by: Onyeka Obi <softwareengineerasaservant@isurvivable.cv>
|
Status update for reviewers: this PR is green on every check and mergeable It covers the complete unsafe surface of the iter adapters: all The one design decision worth a maintainer's eye is that kani#1997 workaround: The iterating adapters listed as deferred are already verified on a follow-up |
1 participant
Verify iter adapter unsafe methods + safe abstractions (challenge #16)
Towards challenge #16 (tracking issue #280). Adds Kani harnesses for
core::iter::adapters: all __iterator_get_unchecked / next_unchecked /
get_unchecked unsafe methods (cloned, copied, enumerate, fuse, map, skip, zip),
plus the safe abstractions array_chunks::next_back_remainder,
copied::spec_next_chunk, map_windows Buffer ops
(as_array_ref/as_uninit_array_mut/push/drop), step_by::original_step, and
zip::next/next_back. Each is instantiated per representative element type via
macros (no monomorphization), with the precondition established by construction
(Kani can't put contracts on generic trait methods, kani#1997). The remaining
iterating adapters (array_chunks::fold, filter::next_chunk_dropless,
filter_map::next_chunk, take::spec_fold/spec_for_each, zip::nth/fold/spec_fold)
are deferred to a follow-up. AI-assisted (Claude); disclosed per repo policy.