Challenge 1: Verify core transmuting methods

[tautschnig]

This issue is a tracking issue for Challenge 1: Verify core transmuting methods.

Challenge link: https://model-checking.github.io/verify-rust-std/challenges/0001-core-transmutation.html

[rahulku]

Can we have an explicit link to the challenge...

[AlexLB99]

Hi all, I'll be working on this alongside professor Patrick Lam (@patricklam) from the University of Waterloo. Will keep you updated on progress, and happy to collaborate with anyone else working on this!

[AlexLB99]

Hi, I just had some questions about verifying the transmute function itself.

(1) Which combinations of input/output types specifically would we want to check for transmute? For instance, I saw another challenge (pointer manipulation proofs #100) was going with something like:

• All integer types.
• At least one dyn Trait.
• At least one slice.
• For unit type.
• At least one composite type with multiple non-ZST fields.

Does something like this seem reasonable for transmute (e.g., one dyn Trait to another dyn Trait)?

(2) Also, in the comments of #100, it's mentioned that it's better to have separate harnesses for different input types. In the case of transmute, is it better to have separate harnesses for each combination of input/output types we want to test? For instance: transmute_type1_to_type2_harness(), transmute_type2_to_type1_harness(), transmute_type1_to_type3_harness(), etc.

Thank you!

[celinval]

Hi @AlexLB99, answering your questions:

(1) For the transmute challenge, I would suggest that you try difference layout combinations. For example, transmuting types with different sizes, types with zero size type, types with different validity requirements, with different padding bytes, as well as types with the same layout.
(2) Yes, this is in fact a Kani limitation. When verifying contracts, you can only verify one instantiation of the target function. Thus, you need one harness per generic parameter combination.

[momvart]

I was reading the description, and the definition of soundness.

A value-to-value transmutation is sound if:

1. the source value is a bit-valid instance of the destination type;
2. violations of library safety invariants (e.g., invariants on a field's value) of the destination type are not violated by subsequent use of the transmuted value.

I was wondering if this definition includes the niche tag encoding for enums. Should it be interpreted as a case of bit-validity or as invariants on field's value?

While I think challenges #109 and #84 are related as the basic cases of it, you can imagine more complicated possible undefined behaviors when transmuting to enums like below (which also uses a niche encoding because of char):

enum Bar {
    A,
    B(Option<(u8, char)>),
    C,
}

---

BTW, we at SFU, would be happy to participate in these challenges under our project which is a tool performing concolic execution for MIR.

[celinval]

Hi @momvart, yes, this challenge does include niche tag encoding as part of the bit validity specification. Generating an invalid tag is UB, and generating an invalid variant value is also UB.

Let's say you transmute an array of u8 with same size as Bar. Users need to ensure that the tag value corresponds to one of the existing variants: A, B, or C. If B, the value of it's member must also be valid. The Option tag value maps to either Some or None, an so on.

[celinval]

Also, it's great to hear about SFU interest, @momvart. Please check the tool application process, and if you have further questions, please post them in the discussions.

[celinval]

I would also highly recommend checking transmuting pointers, references, as well as structures with references.

[patricklam]

Yes, this was just the first step to check that we're on the right track.

…

On Fri, Dec 6, 2024, 8:50 AM Celina G. Val ***@***.***> wrote: I would also highly recommend checking transmuting pointers, references, as well as structures with references. — Reply to this email directly, view it on GitHub <#19 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAOKE5WNLBQCJTPWQRU672D2ECU7HAVCNFSM6AAAAABJGDFVA6VHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDKMRRGI3DGNZYGU> . You are receiving this because you were mentioned.Message ID: ***@***.***>

[kynehc]

Hi, I am a PhD student at The Chinese University of Hong Kong, and I'm interested in addressing this challenge. After some research, I believe a straightforward way to annotate safety contracts for transmute is by using the unstable Transmutability trait. We need to ensure that the Dst type implements the TransmuteFrom<Src> trait. However, it seems there's no way to express this requirement with a predicate like #[requires(Dst: TransmuteFrom<Src>)]. Could Kani potentially offer a method to achieve this? Or is there something I might have overlooked?

[patricklam]

Hi, Interesting observation. It's hard for me to imagine being able to use experimental traits in a proof of these methods, since they don't exactly come with guarantees.

…

On Mon, Dec 9, 2024 at 10:31 PM Kynehc ***@***.***> wrote: Hi, I am a PhD student at The Chinese University of Hong Kong, and I'm interested in addressing this challenge. After some research, I believe a straightforward way to annotate safety contracts for transmute is by using the unstable Transmutability trait. We need to ensure that the Dst type implements the TransmuteFrom<Src> trait. However, it seems there's no way to express this requirement with a predicate like #[requires(Dst: TransmuteFrom<Src>)]. Could Kani potentially offer a method to achieve this? Or is there something I might have overlooked? — Reply to this email directly, view it on GitHub <#19 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAOKE5VZKAVFKLLT5OZJQNL2EVPPLAVCNFSM6AAAAABJGDFVA6VHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDKMRXGM4TCMZWGY> . You are receiving this because you were mentioned.Message ID: ***@***.***>

[AlexLB99]

Hello, so for part 1 of this challenge (annotating the transmute intrinsics), we've prepared a document going over potential sources of UB and discussing if we cover these, and if not, why we don't. The main idea is that if we're only concerned in part 1 with preventing immediate UB, then the main thing to watch out for is value validity. Most of the other types of UB occur once the value produced by the transmute is used in some way (e.g., an invalid pointer).

I was hoping to hear your thoughts on this -- do you believe that the transmute intrinsics should have function contracts that prevent/catch problematic cases but that aren't immediate UB (e.g., creating invalid pointers)? If not, do you see anything beyond value validity that can and should be encoded in a Kani function contract for transmute? If you have some time, please let me know what you think about this (@celinval, @feliperodri, or anyone else interested) -- thanks! 😃

Note: just to clarify, these questions are about the function annotations in particular-- as for harnesses, we definitely plan on adding some more in our next pr (e.g., for compound types and references).