Verify iter adapter unsafe methods + safe abstractions (challenge #16)#602
Verify iter adapter unsafe methods + safe abstractions (challenge #16)#602MavenRain wants to merge 4 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
Challenge 16: Verify the safety of
core::iteradaptersTowards challenge #16 (tracking issue #280). Adds Kani harnesses for the unsafe
methods and safe abstractions in
library/core/src/iter/adapters/.Unsafe methods (proven free of UB)
cloned__iterator_get_unchecked,next_uncheckedcopied__iterator_get_uncheckedenumerate__iterator_get_uncheckedfuse__iterator_get_uncheckedmap__iterator_get_unchecked,next_uncheckedskip__iterator_get_uncheckedzip__iterator_get_uncheckedThe
__iterator_get_uncheckedharnesses read at a symbolic in-bounds index(
kani::any_where(|i| i < size_hint().0)) over akani::any()backing array;the
next_uncheckedharnesses establish the non-empty precondition byconstruction.
Safe abstractions (proven free of UB)
array_chunks::next_back_remainderandarray_chunks::fold,copied::spec_next_chunk,filter::next_chunk_dropless,filter_map::next_chunk, themap_windowsBufferoperations (as_array_ref,as_uninit_array_mut,push,drop),step_by::original_step,take::spec_foldandtake::spec_for_each, andzip::next/next_back/nth/fold/spec_fold.Approach
#[cfg(kani)] mod verifyat the end of each adapter file.proof_for_contractto a generic trait method(kani#1997), each generic method is instantiated at representative concrete
element types via macros, with the caller precondition established by
construction rather than as a
#[requires].u8(1-byte),char(4-byte,validity-constrained), and compound tuples with padding such as
(char, u8)and
(u32, i16);zipharnesses pair two of them. These exercise the distinctmemory-layout classes, since the unsafe operations depend on
size_of::<T>()and
align_of::<T>()rather than onT's identity.Honest caveats (please review)
Two points where this encoding does not literally match the challenge's success
criteria, written out so the committee can weigh them:
T.These harnesses instead prove the property at the representative concrete
instantiations above. The soundness argument is the size-and-align one
described (the unsafe accesses do not branch on
T's identity, and therepresentative types cover ZST, single-byte, 4-byte validity-constrained,
and
padded-compound layouts), but this is representative-type coverage rather
than
a single universal-over-
Tproof. The reason is architectural: CBMCmonomorphizes and Kani has no generic contracts (kani#1997). Glad to switch
encodings if the committee prefers a different form.
cloned,copied,enumerate,fuse,map,skip), the__iterator_get_uncheckedproof iseffectively unbounded in the ZST and
u8cases: the backing length ranges upto the type's representable maximum (
isize::MAX/u32::MAXelements) with asymbolic index. The
charand padded-tuple cases of those harnesses use afixed backing length of 50, and
zip's__iterator_get_uncheckeduses a fixedlength of 50 for every element-type pair except
u8/u8(which isu32::MAX). The iterating abstractions (zipnext/nth/fold/spec_fold,takespec_fold/spec_for_each,filter,filter_map,array_chunks::fold,step_by) use a bounded length (5 to 16) with anexplicit
#[kani::unwind], because CBMC must unroll the loop. The per-elementsafety obligation is structurally identical at every position, so a modest
bound exercises it, but coverage there is bounded rather than arbitrary-length.
AI-assisted (Claude); disclosed per repo policy.