Challenge 29: Verify safety of Box functions#573
Challenge 29: Verify safety of Box functions#573Samuelsills wants to merge 3 commits intomodel-checking:mainfrom
Conversation
Add Kani proof harnesses for Box functions specified in Challenge model-checking#29: 9 unsafe functions (assume_init, from_raw, from_non_null, from_raw_in, from_non_null_in, downcast_unchecked x3) and 34 safe functions covering allocation, conversion, cloning, downcasting, and trait implementations. Exceeds the 75% safe function threshold (34/43 = 79%). Resolves model-checking#526 Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Verification Coverage ReportUnsafe Functions (9/9 — 100% ✅)
Safe Functions with Unsafe Code (34/43 — 79%, exceeds 75% threshold ✅)Allocation: Total: 43 harnesses (9 unsafe + 34 safe) UBs Checked
Verification Approach
|
There was a problem hiding this comment.
Pull request overview
Adds Kani proof harnesses to alloc::boxed to model-check safety contracts and key behaviors of Box APIs as part of Challenge #29 (“Safety of boxed”), including required unsafe APIs and a threshold of safe APIs.
Changes:
- Introduces a
#[cfg(kani)]verifymodule containing Kani proof harnesses for 9 required unsafeBoxfunctions. - Adds Kani proof harnesses for 34 safe
Boxfunctions across allocation, slice utilities, conversions, traits, and downcasting. - Includes downcast proofs for
Any/Errortrait objects and theirSend/Syncvariants.
| let r: Result<Box<[i32; 3]>, _> = b.try_into(); | ||
| assert!(r.is_ok()); |
There was a problem hiding this comment.
verify_into_array is currently exercising TryInto (b.try_into()) rather than the Box<[T]>::into_array API (which returns Option<Box<[T; N]>>). This means the into_array method isn’t actually being verified here and the proof largely duplicates verify_try_from_slice_to_array. Update this harness to call b.into_array::<3>() (and assert is_some() / contents) so it covers the intended function.
| let r: Result<Box<[i32; 3]>, _> = b.try_into(); | |
| assert!(r.is_ok()); | |
| let r = b.into_array::<3>(); | |
| assert!(r.is_some()); | |
| let r = r.unwrap(); | |
| assert!(r[0] == 1 && r[1] == 2 && r[2] == 3); |
| #[cfg(kani)] | ||
| #[unstable(feature = "kani", issue = "none")] | ||
| mod verify { | ||
| use core::any::Any; | ||
| use core::kani; | ||
| use core::mem::MaybeUninit; | ||
|
|
||
| use crate::alloc::Global; | ||
| use crate::boxed::Box; |
There was a problem hiding this comment.
This #[cfg(kani)] verification module calls APIs like Box::new, Box::new_uninit, and Box::new_uninit_slice, which are all #[cfg(not(no_global_oom_handling))] in this file. As written, enabling cfg(kani) alongside no_global_oom_handling will fail to compile. Consider gating the module (or the affected proofs) with #[cfg(not(no_global_oom_handling))], or rewriting the harnesses to only use fallible/allocator-based constructors that are available under no_global_oom_handling.
| fn verify_downcast_error() { | ||
| use core::fmt; | ||
| #[derive(Debug)] | ||
| struct MyError; | ||
| impl fmt::Display for MyError { | ||
| fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { | ||
| write!(f, "MyError") | ||
| } | ||
| } | ||
| impl super::error::Error for MyError {} | ||
| let e: Box<dyn super::error::Error> = Box::new(MyError); | ||
| let d = e.downcast::<MyError>(); | ||
| assert!(d.is_ok()); |
There was a problem hiding this comment.
MyError (and its Display/Error impls) is duplicated across the three verify_downcast_error* proofs. To reduce repetition and keep these harnesses easier to maintain, consider defining MyError once in the module (or a small helper) and reusing it in all three proofs.
The previous body called b.try_into(), which goes through the TryFrom<Box<[T]>> for Box<[T;N]> impl (which uses boxed_slice_as_array_unchecked, not into_array). The TryFrom path is already covered separately by verify_try_from_slice_to_array. Now the harness calls b.into_array() directly and asserts on the recovered array contents, providing direct coverage of the Box::<[T]>::into_array spec function (Challenge 29).
Summary
Add Kani proof harnesses for Box functions specified in Challenge #29:
Unsafe (9/9 — all required):
assume_init(single + slice),from_raw,from_non_null,from_raw_in,from_non_null_in,downcast_unchecked(Any, Any+Send, Any+Send+Sync)Safe (34/43 — 79%, exceeds 75% threshold):
new_in,try_new_in,try_new_uninit_in,try_new_zeroed_innew_uninit_slice,new_zeroed_slice,try_new_uninit_slice,try_new_zeroed_slice,into_arrayinto_boxed_slice,write,into_non_null,into_raw_with_allocator,into_non_null_with_allocator,into_unique,leak,into_pindrop,default(i32, str),clone(T, str),from_slice,from(&str),from(Box->Box<[u8]>),try_from(slice->array)downcast(Any x3, Error x3)All harnesses verified locally with Kani.
Resolves #526