Proofs for String::remove, Vec::swap_remove, Option::as_slice, and VecDeque::swap
#212
Conversation
Added unit type proofs for mut ptr
implemented integer type proof for contract for fn add, sub and offset
Verify/ptr mut composite
Combines macros for different types.
…allocation api, modified their proof for harness accordingly
Verify/ptr mut refactor harness
Verify String::remove in alloc::string
Proof for VecDeque::swap
Added updated proof for Vec::swap_remove
|
@stogaru Update the description of the PR to close the issue, update the goal's document stating the challenge is completed, and list the previous PRs that need to be merged before we can evaluate this PR and complete the goal. |
|
@feliperodri, I made the required changes. |
| // Ensure other elements remain unchanged | ||
| for k in 0..len { | ||
| if k != i && k != j { | ||
| assert_eq!(deque[k], arr[k]); | ||
| } | ||
| } |
There was a problem hiding this comment.
We don't need a loop here, this assertion could be done symbolically.
| // Ensure other elements remain unchanged | |
| for k in 0..len { | |
| if k != i && k != j { | |
| assert_eq!(deque[k], arr[k]); | |
| } | |
| } | |
| // Ensure other elements remain unchanged | |
| let k = kani::any_where(|&x: &usize| x < len); | |
| assert!(implies!(k != i && k !=j, deque[k] == arr[k])); |
There was a problem hiding this comment.
@feliperodri , how do I import implies macro?
use kani::{ensures, implies};The above code gives me the following error:
error[E0432]: unresolved import `kani::implies`
--> /Users/user/Documents/Education/CMU/Academics/2024Fall/14798/verify-rust-std/library/alloc/src/collections/vec_deque/mod.rs:3091:25
|
3091 | use kani::{ensures, implies};
| ^^^^^^^ no `implies` in `kani`
There was a problem hiding this comment.
I made a mistake when I wrote the implies! macro previously.
use kani::{implies}
...
assert!(implies!(k != i && k !=j => deque[k] == arr[k]));
...However, you don't need the implication here at all if that doesn't work. If it makes it more clear, you can just use an if statement. The main point here is to avoid the unnecessary loop.
| /// | ||
| /// The harness checks: | ||
| /// 1. The string length decreases by one after the `remove` operation. | ||
| /// 2. The removed character is valid ASCII. |
| /// 2. The removed character is valid ASCII. | ||
| /// 3. The removed character matches the character at the specified index in the original string. | ||
| /// | ||
| /// This ensures the `remove` function behaves as expected for constrained inputs. |
There was a problem hiding this comment.
What do you mean by that? This line might not be necessary.
| /// | ||
| /// This ensures the `remove` function behaves as expected for constrained inputs. | ||
| fn check_remove() { | ||
| // array size is chosen because it is small enough to be feasible to check exhaustively |
There was a problem hiding this comment.
Could you give us a insight of the verification performance here?
There was a problem hiding this comment.
@qinheping would we be possible to use your loop invariants for valid UTF-8 chars in this harness?
| // Convert byte array to a String directly (safe since all are ASCII) | ||
| let mut s = unsafe { String::from_utf8_unchecked(arr.to_vec()) }; |
There was a problem hiding this comment.
https://doc.rust-lang.org/book/ch08-02-strings.html
It should be UTF-8 encoded, not only ASCII.
| // Check that all other unaffected elements remain unchanged | ||
| for i in 0..vec.len() { | ||
| if i != index && i < original_len - 1 { | ||
| assert!(vec[i] == original_vec[i], "Unaffected elements should remain unchanged"); | ||
| } | ||
| } |
There was a problem hiding this comment.
This can be done symbolically. See previous comment.
Co-authored-by: Felipe R. Monteiro <[email protected]>
Closes #76
Changes
String::removeVec::swap_removeOption::as_sliceVecDeque::swapbyte_add,addandoffset, but stubbing cannot be done for these functions at this time due to Compilation Error When Stubbing Functions That Return Pointers Using Function Contracts kani#3732PoCs:
Vec::swap_remove: @MayureshJoshi25Option::as_slice,VecDeque::swap: @stogaruString::remove: @szlee118PRs that need to be merged before this PR:
core::ptr::byte_offset_from#186<dyn Trait>Proof for Contracts forbyte_add,byte_sub, andbyte_offset#188dyn Traitproof for contracts of byte_offset_from #196By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.