Repository navigation
Challenge 1: Verify core transmuting methods #19
Description
Activity
Can we have an explicit link to the challenge...
- changed the title
[-]Tracking issue for Challenge 1: verify `core` transmuting methods[/-][+]Challenge 1: Verify `core` transmuting methods[/+]on Sep 5, 2024 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!
Reacted by Felipe R. MonteiroHi, I just had some questions about verifying the
transmutefunction 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!
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.Reacted by Alex Le BlancI was reading the description, and the definition of soundness.
A value-to-value transmutation is sound if:
- the source value is a bit-valid instance of the destination type;
- 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.
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
u8with same size asBar. Users need to ensure that the tag value corresponds to one of the existing variants:A,B, orC. IfB, the value of it's member must also be valid. TheOptiontag value maps to eitherSomeorNone, an so on.Reacted by Mohammad OmidvarAlso, 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.
Reacted by Mohammad OmidvarI would also highly recommend checking transmuting pointers, references, as well as structures with references.
- 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: ***@***.***>Reacted by Celina G. Val
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
transmuteis by using the unstableTransmutabilitytrait. We need to ensure that theDsttype implements theTransmuteFrom<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?- 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: ***@***.***>
- added a commit that references this issue
on Feb 4, 2025 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).
- added a commit that references this issue
on May 30, 2025 - added a commit that references this issue
on Jul 24, 2025 - added a commit that references this issue
on Sep 9, 2025 - added a commit that references this issue
on Apr 10, 2026
This issue is a tracking issue for Challenge 1: Verify
coretransmuting methods.Challenge link: https://model-checking.github.io/verify-rust-std/challenges/0001-core-transmutation.html