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

Open

kasimte wants to merge 6 commits into

model-checking:mainfrom

kasimte:24-build

Commits on Sep 18, 2026

Challenge 24: verify Vec IntoIter and spec_* function safety with Kani
kasimte
committed
18bdbe9

Commits on Sep 21, 2026

Challenge 24: add element-type shape coverage (align, stride, validity, drop)
kasimte
committed
dcc85d2

Commits on Sep 28, 2026

Challenge 24: verify IntoIter safety from arbitrary reachable iterator states
kasimte
committed
56cabac
Challenge 24: verify IntoIter::fold from arbitrary reachable iterator states
kasimte
committed
8fe1f3a
Challenge 24: verify try_fold, next_chunk, into_vecdeque from reachable iterator states
kasimte
committed
25d1371

Commits on Oct 2, 2026

Challenge 24: add non-vacuity covers to the three symbolic-length u8 harnesses
kasimte
committed
f7fa1f1