Challenge 10: Kani contracts for String memory safety - #645
Challenge 10: Kani contracts for String memory safety#645sankalpsthakur wants to merge 1 commit into
Conversation
|
both ubuntu jobs die with a runner shutdown signal shortly after string::verify::check_from_utf16le_lossy starts, while the 3-thread macos jobs finish that same harness in 238s, so it was peaking the 16 gb runner's memory rather than failing a check. switched it to kissat, the same remedy core::ptr uses for check_align_offset_5; state space and check count are unchanged. |
7f81109 to
1d9ad25
Compare
Add safety contracts and proof harnesses covering String allocation and mutation. Runtime stdlib logic is unchanged: everything added here is either a contract attribute or lives behind cfg(kani). check_from_utf16le_lossy passes the whole 2-byte buffer instead of a symbolic sub-slice. On a little-endian target it is the only one of the four UTF-16 harnesses that keeps the align_to::<u16> arms of from_utf16le_lossy live, and any_slice_of_array picks a symbolic start as well as a symbolic end, which left the slice's base pointer alignment symbolic on top of that. Both bytes are still symbolic; only the slice bounds are now fixed. This also drops the earlier solver(kissat) selection. kissat did not stop the ubuntu runner being reclaimed mid-solve, and it made the harness slower on macOS, where it then ran past the 10m autoharness timeout. Fixes rust-lang#61
1d9ad25 to
1ce502d
Compare
|
dropped solver(kissat); ubuntu was still getting reclaimed with it in place, and it pushed the macos autoharness run past the 10m cap. check_from_utf16le_lossy now takes the whole 2-byte buffer rather than a symbolic sub-slice, so the bytes stay symbolic but the base pointer alignment feeding align_to:: doesn't. |
|
Withdrawing this; no maintainer signal and we are cutting the queue. |
2 participants
Summary
Kani safety contracts and proof harnesses for this challenge. Runtime stdlib logic is unchanged; annotations are cfg(kani) / contract attributes.
String allocation/mutation safety contracts.
Validation
challenge/10-stringscripts/run-kani.sh)Fixes #61
AI/LLM disclosure