additional transmute and transmute_unchecked harnesses

[AlexLB99]

Toward solving #19

This pr adds some additional harnesses for transmute_unchecked and transmute.

With this, we suspect that the main harnesses for part 1 of challenge 1 (verifying the transmute intrinsics directly) are there (besides adding more of the same kinds of harnesses, like the 2-way harnesses for more types). We go into more detail about what needs to be done for part 1, as well as what has been done and what can't be done here: https://docs.google.com/document/d/1zFGANNMx8mZ8fucKrN--ELwKASUPeP20THH6M_fQ7jg/edit?usp=sharing

Just one note: transmute has far fewer harnesses than transmute_unchecked here -- this is because it is not currently possible to write a wrapper for transmute, and it is thus not possible to write a function contract. A lot of the harnesses for transmute_unchecked test the function contract's validity clause, rather than the function itself, explaining this disparity.

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[AlexLB99]

Would be to happy hear your thoughts on this (@celinval, @feliperodri, or anyone else interested in this challenge). In particular, we would like to hear what you think about the completeness of part 1 of challenge 1 (i.e., is there anything major that Kani can do that isn't currently being verified here?). For our own thoughts on this, we refer to the above linked completeness document. Thank you!

[AlexLB99]

The new commit adds some harnesses for transmute/transmute_unchecked. In particular, it adds "2-way" harnesses for additional primitives (including floats), as well as for references, pointers, and slices. It also introduces a macro that generates these 2-way harnesses between more complex types (currently arrays, tuples, and structs).

As always, any feedback is greatly appreciated! I'm especially wondering if there are other properties we want to verify in this "part 1" (i.e., harnesses for the transmute intrinsics directly), or if it makes sense to do the rest of the verification at the part 2/3/4 level. In any case, thanks in advance!

[AlexLB99]

Hi @thanhnguyen-aws, I've updated the PR to reflect your previous comments. Happy to hear your thoughts whenever you get a chance -- thanks!

[thanhnguyen-aws]

Hi @thanhnguyen-aws, I've updated the PR to reflect your previous comments. Happy to hear your thoughts whenever you get a chance -- thanks!

Hello, thanks for your hard work. I have some comments:

1. We should change the name of the marco: transmute_unchecked_should_succeed! into ``proof_of_contract_for_transmute_unchecked` as it generates the proof_of_contract harness.
2. For transmute_unchecked_should_fail, you don't need #[kani::stub_verified(transmute_unchecked_wrapper)].
3. For the corresponding transmute_unchecked_should_succeed! harnesses, the attribute should be just #[kani::proof], but inside the harness body, you should add a kani::assume(some condition) such that the harness will be verified successfully. The condition should be something more expressive (based on the knowledge of the types encoding, see my example, and I don't think you can use macro here), not your generic require clause: ub_checks::can_dereference(&input as *const T as *const U)). The purpose of those harnesses is to confirm that your require clause can cover all the cases where transmute_unchecked is safe (as Kani will assert your require clause after you assume the specific condition).

[AlexLB99]

Thanks for the reply @thanhnguyen-aws! I was just getting back to work on this, and I just wanted to check a few things with you:

• For point 3, if I'm understanding correctly, the suggestion is to have harnesses that show that the specific preconditions imply our generic precondition. Since we're asserting rather than assuming the generic precondition, would you suggest stubbing (or manually asserting the precondition, or something else)? For instance, a harness could look like:

#[kani::proof]
#[kani::stub_verified(transmute_unchecked_wrapper)]
fn should_succeed_u32_to_char() {
    let src: u32 = kani::any_where(|x| core::char::from_u32(*x).is_some());
    let dst: char = unsafe { transmute_unchecked_wrapper(src) };
}

• If that is what we're trying to do for the should_succeed cases, then I suppose the should_fail ones should show that when the specific precondition doesn't hold, our generic precondition also doesn't hold (e.g., we assume the negation of the specific precondition, and we assert the generic precondition). In this case as well, stubbing seems like it might be a natural solution, although this would differ from your suggestion in point 2 to remove the stubbing, so I was just hoping to check with you if this solution is still aligned what you had in mind, or if you were thinking of another direction entirely for the should_fail harnesses. Just to visualize with an example, I was thinking maybe something like this:

#[kani::proof]
#[kani::stub_verified(transmute_unchecked_wrapper)]
#[kani::should_panic]
fn should_fail_u32_to_char() {
    let src: u32 = kani::any_where(|x| !core::char::from_u32(*x).is_some());
    let dst: char = unsafe { transmute_unchecked_wrapper(src) };
}

• For point 1, that makes sense -- just to clarify though, these proof_for_contract harnesses would be different from the ones in point 3 right? In other words, we'd have the proof_of_contract_for_transmute_unchecked macro that does a kani::proof_for_contract(transmute_unchecked_wrapper), and we'd have type-specific should_succeed harnesses that show that specific preconditions imply our generic precondition (and so they'd be asserting the generic precondition rather than assuming it like in proof_of_contract_for_transmute_unchecked). Just to make sure, is this what you had in mind?

Happy to hear your thoughts whenever you get a chance, and thank you as always for your suggestions!

[AlexLB99]

I've added a new commit that demonstrates more completely what my last comment discusses (e.g., the modified should_succeed and should_fail harnesses). Please feel free to let me know if this is closer to what you were thinking, and if I might be misunderstanding anything (e.g., like my above comment discusses, this still uses stubbing, which does differ from one of your suggestions). Thanks!

[thanhnguyen-aws]

I've added a new commit that demonstrates more completely what my last comment discusses (e.g., the modified should_succeed and should_fail harnesses). Please feel free to let me know if this is closer to what you were thinking, and if I might be misunderstanding anything (e.g., like my above comment discusses, this still uses stubbing, which does differ from one of your suggestions). Thanks!

Hello,
Sorry for my late response, I have just finished my 2-week vacation.
I am really happy to see your work and it is even better than my expectation.

[patricklam]

can we ping on a review here @tautschnig @qinheping @carolynzech ? thanks.