From fc7bcf007b0ff0eedbacfc8d17a79ccc3d756269 Mon Sep 17 00:00:00 2001 From: Felix Klock Date: Mon, 10 Jun 2024 14:27:11 -0400 Subject: [PATCH 01/12] refined core transmutation challenge. --- doc/src/SUMMARY.md | 1 + doc/src/core-transmutation.md | 133 ++++++++++++++++++++++++++++++++++ 2 files changed, 134 insertions(+) create mode 100644 doc/src/core-transmutation.md diff --git a/doc/src/SUMMARY.md b/doc/src/SUMMARY.md index 29ec5d95fcda5..cee3011effbda 100644 --- a/doc/src/SUMMARY.md +++ b/doc/src/SUMMARY.md @@ -13,3 +13,4 @@ # Challenges - [Coming soon](./todo.md) +- [Core Transmutation](./core-transmutation.md) diff --git a/doc/src/core-transmutation.md b/doc/src/core-transmutation.md new file mode 100644 index 0000000000000..c6a5969feb5ec --- /dev/null +++ b/doc/src/core-transmutation.md @@ -0,0 +1,133 @@ +Challenge: Preconditions for core transmuting methods + +## Status + +\[Open | Resolved | Expired\]: Open + +## Dates + +Start date: + +End date: + +## Goal + +Confirm the correctness of value transmutations performed by libcore, including those transmutations exposed as public methods provided by libcore. + +To keep the goal somewhat manageable, it excludes some classes of code (e.g. utf8-validation, async tasks, and others); see the assumptions for the full list of excluded categories. + +## Details + +### Motivating Example + +There are several calls to these unsafe methods within the code of safe methods exported libcore itself, so having clear and verifiable safety contracts is critical for verifying the safety of the safe methods that invoke them. + +For example, `std::slice::align_to` (which unsafely converts any slice `&[T]` into a tuple `(&[T], &[U], &[T])` composed of a prefix, a maximal sequence of values of type `U`, and a suffix) just says for its safety that “all the usual caveats pertaining to `transmute::` also apply here”, but the documentation for `transmute` is frankly (and rightfully) scary. + +### Part 1: the two intrinsics + +The public unsafe intrinsic `transmute` takes a value of type `T` and reinterprets it to have type `U`, with the sole (statically-enforced) restriction being that the types `T` and `U` must have the same size. The unstable intrinsic `transmute_unchecked` is similar, except that it removes the static size restriction, treating violations of it as undefined behavior. + +What is the right way to encode the preconditions of the two transmutation intrinsics? + +If one is solely concerned about safety: The Rustonomicon lists several ways that transmutation can yield undefined behavior. Encoding a correct safety contract for transmute is crucial. + +If one is concerned about proving functional correctness, then reasoning about transmutation will require reasoning about the byte representation of values to justify that the reinterpretation of the value’s bytes for satisfying the pending proof obligation associated with the output value. + + +### Part 2: unsafe APIs with validity constraints + +There are unsafe methods (which are defined by libcore and reexported by libstd) have the effect of a transmutation between a (sequence of) T and a (sequence of) U. Come up with an appropriate safety contract for each of them; they should usually be something less arduous for callers than transmute itself (we hope). + + +### Part 3: unsafe APIs with richer constraints + +Similar to part 2, there are also unsafe methods, but now the safety condition is more complicated, such as “is valid ascii character” or "is valid unicode scalar value." + +### Part 4: safe APIs + +These are safe APIs that call into the unsafe API's from parts 1 through 3 above. Now our final goal is to prove that they actually are safe, despite calling transmute or transmute-related methods in their implementations. + +### Assumptions + +For this challenge, the following assumptions are acceptable: + +We are not attempting to validate all details of the memory model for this challenge; for example, you do not need to worry about whether we are using the Stacked Borrows or Tree Borrows aliasing models. Likewise, you do not need to validate the provenance-related API in `std::ptr`. + +You are allowed, but not required, to leverage the unstable `Transmutability` trait under development as part of your solution. This is a libstd-internal feature for auditing whether a given transmutation is safe. (It seems like something tools should try to leverage in some way; but it is also experimental.) Note that if you need to add new impls of `Transmutability`, then those new impl’s need to be accepted by (and landed in) the upstream Rust project before your solutiokn can be considered completed. See also https://github.com/rust-lang/rust/issues/99571 + +You do not need to verify the correctness of the transmute calls in the unit tests embedded in libcore, though it would be great to do so! + +To keep the goal somewhat manageable, we are omitting the following classes of code from the acceptance criteria for this challenge: + * utf8-validation (such as `str::from_utf8_unchecked`) + * the provenance-related API in `std::ptr` (such as `addr`, or `without_provenance`) + * the num methods (from modules like `core::num::f64`, `core::num::i32`, etc) + * pointer-metadata and vtable APIs (from modules like `core::ptr::metadata`) + * async rust runtime/task API (from `core::task`) + * core-internal specialization methods (such as traits like `RangeIteratorImpl` with methods prefixed with "spec_") + * core-internal `__iterator_get_unchecked` calls + * value output formatting machinery (from `std::fmt::rt`) + You do not need to verify those (potentially indirect) uses of transmute, unless you need to establish the safety/correctness of some of those methods in order to verify some other type in this list. (That is, you cannot assume them to be safe nor correct in your verification of other methods listed here.) We expect to issue future challenges tailored to each of the categories of transmutation uses listed above. + + +## Success Criteria + +A new entry to the specification book is created explaining the relevant patterns for verifying code that calls transmute. + +At least 35 of the following 47 intrinsics and functions (i.e. approximately 75%) have been annotated with contracts, and, for non-intrinsics, had their bodies verified. + + +| Function | Location | +|-----------------------|-------------------| +| `transmute_unchecked` | `core::intrinsics` | +| `transmute` | `core::intrinsics` | +| | | +| `MaybeUninit::array_assume_init` | `core::mem` | +| `MaybeUninit<[T; N]>::transpose` | `core::mem` | +| `<[MaybeUninit; N]>::transpose` | `core::mem` | +| `<[T; N] as IntoIterator>::into_iter` | `core::array::iter` | +| `BorrowedBuf::unfilled` | `core::io::borrowed_buf` | +| `BorrowedCursor::reborrow` | `core::io::borrowed_buf` | +| `str::as_bytes` | `core::str` | +| `from_u32_unchecked` | `core::char::convert` | +| `char_try_from_u32` | `core::char::convert` | +| `Ipv6Addr::new` | `core::net::ip_addr` | +| `Ipv6Addr::segments` | `core::net::ip_addr` | +| `align_offset` | `core::ptr` | +| `Alignment::new_unchecked` | `core::ptr::alignment` | +| `MaybeUninit::copy_from_slice` | `core::mem` | +| `str::as_bytes_mut` | `core::str` | +| | | +| ` as Iterator>::next_chunk` | `core::iter::adapters` | +| ` as Iterator>::next_chunk` | `core::iter::adapters` | +| `try_from_fn` | `core::array` | +| `iter_next_chunk` | `core::array` | +| `from_u32_unchecked` | `core::char` | +| `AsciiChar::from_u8_unchecked` | `core::ascii_char` | +| `memchr_aligned` | `core::slice::memchr` | +| `<[T]>::align_to_mut` | `core::slice` | +| `run_utf8_validation` | `core::str::validations` | +| `<[T]>::align_to` | `core::slice` | +| `is_aligned_to` | `core::const_ptr` | +| `is_aligned_to` | `core::mut_ptr` | +| `Alignment::new` | `core::ptr::alignment` | +| `Layout::from_size_align` | `core::alloc::layout` | +| `Layout::from_size_align_unchecked` | `core::alloc::layout` | +| `make_ascii_lowercase` | `core::str` | +| `make_ascii_uppercase` | `core::str` | +| | | +| `::forward_checked` | `core::iter::range` | +| `::next` | `core::str::iter` | +| `::next_back` | `core::str::iter` | +| `char::encode_utf16_raw` | `core::char` | +| `::backward_unchecked` | `core::iter::range` | +| `::forward_unchecked` | `core::iter::range` | +| `AsciiChar::from_u8` | `core::ascii_char` | +| `char::as_ascii` | `core::char` | +| `<[T]>::as_simd_mut` | `core::slice` | +| `<[T]>::as_simd` | `core::slice` | +| `memrchr` | `core::slice::memchr` | +| `do_count_chars` | `str::count` | + + +* All solutions to verification challenges need to satisfy the criteria established in the challenge book (TODO: Add link) in addition to the ones listed below From 929dd4af0fa7a92420f2284bd6da0a284970944d Mon Sep 17 00:00:00 2001 From: Felix Klock Date: Tue, 11 Jun 2024 09:27:24 -0400 Subject: [PATCH 02/12] clarify that full-functional correctness is not the specific point of this challenge, and that it suffices to focus on the transmutation-related safety invariants. --- doc/src/core-transmutation.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/doc/src/core-transmutation.md b/doc/src/core-transmutation.md index c6a5969feb5ec..8cdfeda838c70 100644 --- a/doc/src/core-transmutation.md +++ b/doc/src/core-transmutation.md @@ -76,6 +76,8 @@ A new entry to the specification book is created explaining the relevant pattern At least 35 of the following 47 intrinsics and functions (i.e. approximately 75%) have been annotated with contracts, and, for non-intrinsics, had their bodies verified. +For the safe functions, you do not need to provide a full-functional correctness specificatipn; it will suffice to add pre- and post-conditions (i.e. assumptions and assertions) around the relevant part of the code that calls the transmutation-related unsafe function or intrinsic. + | Function | Location | |-----------------------|-------------------| From 3e7249a1279f746112d984093a2057350282a7f1 Mon Sep 17 00:00:00 2001 From: Felix Klock Date: Tue, 11 Jun 2024 09:48:37 -0400 Subject: [PATCH 03/12] added appendix explaining how the list of methods was constructed. --- doc/src/core-transmutation.md | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/doc/src/core-transmutation.md b/doc/src/core-transmutation.md index 8cdfeda838c70..3537865d84993 100644 --- a/doc/src/core-transmutation.md +++ b/doc/src/core-transmutation.md @@ -133,3 +133,11 @@ For the safe functions, you do not need to provide a full-functional correctness * All solutions to verification challenges need to satisfy the criteria established in the challenge book (TODO: Add link) in addition to the ones listed below + +## Appendix A: The list construction + +The list of methods and intrinsics was gathered by surveying the call-graph (solely within the libcore source) of function bodies that could eventually invoke `transmute` or `transmute_unchecked`. For each caller: if the caller was itself `unsafe`, then its callers were then surveyed; if the caller was not `unsafe`, then it was treated as an end point for the survey. + +As mentioned in the assumptions, some (large) classes of methods were omitted from the challenge, either because 1. they encompassed a large API surface (e.g. `core::num`) that deserved separate treatment, 2. they had an enormous number of callers that would deserve separate treatment (e.g. `core::str::from_utf8_unchecked`), or 3. they interact with aspects of the Rust memory model that still need to be better understood by reasoning tools (e.g. the provenance APIs). + +You can see the [call graph produced by the survey here](https://hackmd.io/PYQNIL_aTxK0N6-AltxfbQ) From 3db5b5a8e1f85f81c0564b795ed30dae992ce943 Mon Sep 17 00:00:00 2001 From: "Felipe R. Monteiro" Date: Tue, 11 Jun 2024 18:19:22 -0400 Subject: [PATCH 04/12] Address comments from reviewers Signed-off-by: Felipe R. Monteiro --- doc/src/core-transmutation.md | 57 ++++++++++++++++++----------------- 1 file changed, 30 insertions(+), 27 deletions(-) diff --git a/doc/src/core-transmutation.md b/doc/src/core-transmutation.md index 3537865d84993..db568a7070121 100644 --- a/doc/src/core-transmutation.md +++ b/doc/src/core-transmutation.md @@ -1,50 +1,56 @@ -Challenge: Preconditions for core transmuting methods +# Challenge: Verify `core` transmuting methods -## Status +- **Status:** *One of the following: [Open | Resolved | Expired]* Open +- **Tracking Issue:** *Link to issue* +- **Start date:** *YY/MM/DD* +- **End date:** *YY/MM/DD* -\[Open | Resolved | Expired\]: Open - -## Dates - -Start date: - -End date: +------------------- ## Goal -Confirm the correctness of value transmutations performed by libcore, including those transmutations exposed as public methods provided by libcore. +Confirm the soundness of value transmutations performed by libcore, including those transmutations exposed as public methods provided by libcore. 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. + +If the context of the transmute is safe, these conditions should be proven with local reasoning. If the context of the transmute is unsafe, they may be discharged with a safety obligation on the caller. -To keep the goal somewhat manageable, it excludes some classes of code (e.g. utf8-validation, async tasks, and others); see the assumptions for the full list of excluded categories. +To keep the goal somewhat manageable, it excludes some classes of code (e.g. UTF8-validation, async tasks, and others); see the assumptions for the full list of excluded categories. ## Details ### Motivating Example -There are several calls to these unsafe methods within the code of safe methods exported libcore itself, so having clear and verifiable safety contracts is critical for verifying the safety of the safe methods that invoke them. +There are several calls to unsafe methods using transmute within the code of safe methods exported by libcore itself, so having clear and verifiable safety contracts is critical for verifying the safety of the safe methods that invoke them. + +For example, `std::slice::align_to` (which unsafely converts any slice `&[T]` into a tuple `(&[T], &[U], &[T])` composed of a prefix, a maximal sequence of values of type `U`, and a suffix) just says for its safety that “all the usual caveats pertaining to `transmute::` also apply here”, which might be an under specification. For more details, see the [documentation](https://doc.rust-lang.org/std/mem/fn.transmute.html) for `transmute`. + + +### Breaking-down the verification -For example, `std::slice::align_to` (which unsafely converts any slice `&[T]` into a tuple `(&[T], &[U], &[T])` composed of a prefix, a maximal sequence of values of type `U`, and a suffix) just says for its safety that “all the usual caveats pertaining to `transmute::` also apply here”, but the documentation for `transmute` is frankly (and rightfully) scary. +We lay out the verification challenge from the bottom up. Starting with the core implementation of `transmute` moving up to all unsafe and safe APIs that rely on it. -### Part 1: the two intrinsics +#### Part I - The Two Intrinsics -The public unsafe intrinsic `transmute` takes a value of type `T` and reinterprets it to have type `U`, with the sole (statically-enforced) restriction being that the types `T` and `U` must have the same size. The unstable intrinsic `transmute_unchecked` is similar, except that it removes the static size restriction, treating violations of it as undefined behavior. +The public unsafe intrinsic [`transmute`](https://doc.rust-lang.org/std/mem/fn.transmute.html) takes a value of type `T` and reinterprets it to have type `U`, with the sole (statically-enforced) restriction being that the types `T` and `U` must have the same size. The unstable intrinsic [`transmute_unchecked`](https://doc.rust-lang.org/core/intrinsics/fn.transmute_unchecked.html) is similar, except that it removes the static size restriction, treating violations of it as undefined behavior. -What is the right way to encode the preconditions of the two transmutation intrinsics? +_What is the right way to encode the preconditions of the two transmutation intrinsics?_ -If one is solely concerned about safety: The Rustonomicon lists several ways that transmutation can yield undefined behavior. Encoding a correct safety contract for transmute is crucial. +If one is solely concerned about safety: The [Rustonomicon](https://doc.rust-lang.org/nomicon/transmutes.html) lists several ways that transmutation can yield undefined behavior. Encoding a safety contract for transmute that captures all the relevant criteria laid out in the documentation is crucial. If one is concerned about proving functional correctness, then reasoning about transmutation will require reasoning about the byte representation of values to justify that the reinterpretation of the value’s bytes for satisfying the pending proof obligation associated with the output value. -### Part 2: unsafe APIs with validity constraints +#### Part II - `unsafe` APIs with Validity Constraints -There are unsafe methods (which are defined by libcore and reexported by libstd) have the effect of a transmutation between a (sequence of) T and a (sequence of) U. Come up with an appropriate safety contract for each of them; they should usually be something less arduous for callers than transmute itself (we hope). +There are unsafe methods (which are defined by libcore and reexported by libstd) that have the effect of a transmutation between a (sequence of) `T` and a (sequence of) `U`. Come up with an appropriate safety contract for each of them; they should usually be something simpler for callers than transmute itself (we hope). -### Part 3: unsafe APIs with richer constraints +#### Part III - `unsafe` APIs with Richer Constraints Similar to part 2, there are also unsafe methods, but now the safety condition is more complicated, such as “is valid ascii character” or "is valid unicode scalar value." -### Part 4: safe APIs +#### Part IV - `safe` APIs These are safe APIs that call into the unsafe API's from parts 1 through 3 above. Now our final goal is to prove that they actually are safe, despite calling transmute or transmute-related methods in their implementations. @@ -54,7 +60,7 @@ For this challenge, the following assumptions are acceptable: We are not attempting to validate all details of the memory model for this challenge; for example, you do not need to worry about whether we are using the Stacked Borrows or Tree Borrows aliasing models. Likewise, you do not need to validate the provenance-related API in `std::ptr`. -You are allowed, but not required, to leverage the unstable `Transmutability` trait under development as part of your solution. This is a libstd-internal feature for auditing whether a given transmutation is safe. (It seems like something tools should try to leverage in some way; but it is also experimental.) Note that if you need to add new impls of `Transmutability`, then those new impl’s need to be accepted by (and landed in) the upstream Rust project before your solutiokn can be considered completed. See also https://github.com/rust-lang/rust/issues/99571 +You are allowed, but not required, to leverage the unstable `Transmutability` trait under development as part of your solution. This is a libstd-internal feature for auditing whether a given transmutation is safe. (It seems like something tools should try to leverage in some way; but it is also experimental.) Note that if you need to add new impls of `Transmutability`, then those new impl’s need to be accepted by (and landed in) the upstream Rust project before your solution can be considered completed. See also https://github.com/rust-lang/rust/issues/99571 You do not need to verify the correctness of the transmute calls in the unit tests embedded in libcore, though it would be great to do so! @@ -76,14 +82,13 @@ A new entry to the specification book is created explaining the relevant pattern At least 35 of the following 47 intrinsics and functions (i.e. approximately 75%) have been annotated with contracts, and, for non-intrinsics, had their bodies verified. -For the safe functions, you do not need to provide a full-functional correctness specificatipn; it will suffice to add pre- and post-conditions (i.e. assumptions and assertions) around the relevant part of the code that calls the transmutation-related unsafe function or intrinsic. +For the safe functions, you do not need to provide a full-functional correctness specification; it will suffice to add pre- and post-conditions (i.e. assumptions and assertions) around the relevant part of the code that calls the transmutation-related unsafe function or intrinsic. | Function | Location | |-----------------------|-------------------| | `transmute_unchecked` | `core::intrinsics` | | `transmute` | `core::intrinsics` | -| | | | `MaybeUninit::array_assume_init` | `core::mem` | | `MaybeUninit<[T; N]>::transpose` | `core::mem` | | `<[MaybeUninit; N]>::transpose` | `core::mem` | @@ -99,7 +104,6 @@ For the safe functions, you do not need to provide a full-functional correctness | `Alignment::new_unchecked` | `core::ptr::alignment` | | `MaybeUninit::copy_from_slice` | `core::mem` | | `str::as_bytes_mut` | `core::str` | -| | | | ` as Iterator>::next_chunk` | `core::iter::adapters` | | ` as Iterator>::next_chunk` | `core::iter::adapters` | | `try_from_fn` | `core::array` | @@ -117,7 +121,6 @@ For the safe functions, you do not need to provide a full-functional correctness | `Layout::from_size_align_unchecked` | `core::alloc::layout` | | `make_ascii_lowercase` | `core::str` | | `make_ascii_uppercase` | `core::str` | -| | | | `::forward_checked` | `core::iter::range` | | `::next` | `core::str::iter` | | `::next_back` | `core::str::iter` | @@ -132,7 +135,7 @@ For the safe functions, you do not need to provide a full-functional correctness | `do_count_chars` | `str::count` | -* All solutions to verification challenges need to satisfy the criteria established in the challenge book (TODO: Add link) in addition to the ones listed below +* All solutions to verification challenges need to satisfy the criteria established in the [challenge book](https://model-checking.github.io/verify-rust-std/general-rules.html) in addition to the ones listed below ## Appendix A: The list construction From 38d03e022a86a6191effa5187ccc94e8561422b5 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 12 Jun 2024 15:10:52 +0200 Subject: [PATCH 05/12] Update doc/src/core-transmutation.md --- doc/src/core-transmutation.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/src/core-transmutation.md b/doc/src/core-transmutation.md index db568a7070121..5df267f322c62 100644 --- a/doc/src/core-transmutation.md +++ b/doc/src/core-transmutation.md @@ -1,6 +1,6 @@ # Challenge: Verify `core` transmuting methods -- **Status:** *One of the following: [Open | Resolved | Expired]* Open +- **Status:** Open - **Tracking Issue:** *Link to issue* - **Start date:** *YY/MM/DD* - **End date:** *YY/MM/DD* From d0fadd4e9c4ce963f0fcf7cf51822173998ce7e1 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 12 Jun 2024 15:11:01 +0200 Subject: [PATCH 06/12] Update doc/src/core-transmutation.md --- doc/src/core-transmutation.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/src/core-transmutation.md b/doc/src/core-transmutation.md index 5df267f322c62..40d0f55f37b97 100644 --- a/doc/src/core-transmutation.md +++ b/doc/src/core-transmutation.md @@ -1,7 +1,7 @@ # Challenge: Verify `core` transmuting methods - **Status:** Open -- **Tracking Issue:** *Link to issue* +- **Tracking Issue:** [Link to issue](https://github.com/model-checking/verify-rust-std/issues/19) - **Start date:** *YY/MM/DD* - **End date:** *YY/MM/DD* From e55b676ee314d710c554f541a85b1452b664fa62 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 12 Jun 2024 15:11:09 +0200 Subject: [PATCH 07/12] Update doc/src/core-transmutation.md --- doc/src/core-transmutation.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/src/core-transmutation.md b/doc/src/core-transmutation.md index 40d0f55f37b97..c4120314e5fb1 100644 --- a/doc/src/core-transmutation.md +++ b/doc/src/core-transmutation.md @@ -15,7 +15,7 @@ Confirm the soundness of value transmutations performed by libcore, including th If the context of the transmute is safe, these conditions should be proven with local reasoning. If the context of the transmute is unsafe, they may be discharged with a safety obligation on the caller. -To keep the goal somewhat manageable, it excludes some classes of code (e.g. UTF8-validation, async tasks, and others); see the assumptions for the full list of excluded categories. +To keep the goal somewhat manageable, it excludes some classes of code (e.g., UTF8-validation, async tasks, and others); see the assumptions listed below for the full list of excluded categories. ## Details From fbc02a33f0b8f461974c083c20f04e1310d71717 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 12 Jun 2024 15:11:20 +0200 Subject: [PATCH 08/12] Update doc/src/core-transmutation.md --- doc/src/core-transmutation.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/src/core-transmutation.md b/doc/src/core-transmutation.md index c4120314e5fb1..d22f21e6b9532 100644 --- a/doc/src/core-transmutation.md +++ b/doc/src/core-transmutation.md @@ -3,7 +3,7 @@ - **Status:** Open - **Tracking Issue:** [Link to issue](https://github.com/model-checking/verify-rust-std/issues/19) - **Start date:** *YY/MM/DD* -- **End date:** *YY/MM/DD* +- **End date:** 2024-12-10 ------------------- From 21099fe1fd4a16f1c7c79a738e6a85d5620484b1 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 12 Jun 2024 15:11:28 +0200 Subject: [PATCH 09/12] Update doc/src/core-transmutation.md --- doc/src/core-transmutation.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/src/core-transmutation.md b/doc/src/core-transmutation.md index d22f21e6b9532..f0ab0e1433eb5 100644 --- a/doc/src/core-transmutation.md +++ b/doc/src/core-transmutation.md @@ -43,7 +43,7 @@ If one is concerned about proving functional correctness, then reasoning about t #### Part II - `unsafe` APIs with Validity Constraints -There are unsafe methods (which are defined by libcore and reexported by libstd) that have the effect of a transmutation between a (sequence of) `T` and a (sequence of) `U`. Come up with an appropriate safety contract for each of them; they should usually be something simpler for callers than transmute itself (we hope). +There are unsafe methods (which are defined by libcore and reexported by libstd) that have the effect of a transmutation between a (sequence of) `T` and a (sequence of) `U`. Come up with an appropriate safety contract for each of them. #### Part III - `unsafe` APIs with Richer Constraints From ee50c83179ecb02e390dca7148b3631d7e77ac7c Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 12 Jun 2024 15:11:36 +0200 Subject: [PATCH 10/12] Update doc/src/core-transmutation.md --- doc/src/core-transmutation.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/src/core-transmutation.md b/doc/src/core-transmutation.md index f0ab0e1433eb5..1ccfe4065bfb7 100644 --- a/doc/src/core-transmutation.md +++ b/doc/src/core-transmutation.md @@ -2,7 +2,7 @@ - **Status:** Open - **Tracking Issue:** [Link to issue](https://github.com/model-checking/verify-rust-std/issues/19) -- **Start date:** *YY/MM/DD* +- **Start date:** 2024-06-12 - **End date:** 2024-12-10 ------------------- From 9a99cfcc4dfbca31401ca1d117a5e2dfde6bb353 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 12 Jun 2024 15:11:43 +0200 Subject: [PATCH 11/12] Update doc/src/core-transmutation.md --- doc/src/core-transmutation.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/src/core-transmutation.md b/doc/src/core-transmutation.md index 1ccfe4065bfb7..ba66c41be7e18 100644 --- a/doc/src/core-transmutation.md +++ b/doc/src/core-transmutation.md @@ -143,4 +143,4 @@ The list of methods and intrinsics was gathered by surveying the call-graph (sol As mentioned in the assumptions, some (large) classes of methods were omitted from the challenge, either because 1. they encompassed a large API surface (e.g. `core::num`) that deserved separate treatment, 2. they had an enormous number of callers that would deserve separate treatment (e.g. `core::str::from_utf8_unchecked`), or 3. they interact with aspects of the Rust memory model that still need to be better understood by reasoning tools (e.g. the provenance APIs). -You can see the [call graph produced by the survey here](https://hackmd.io/PYQNIL_aTxK0N6-AltxfbQ) +You can see the [call graph produced by the survey here](https://hackmd.io/PYQNIL_aTxK0N6-AltxfbQ). From e8fe674066993a2426b913007c3f04eafb3cf8bb Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 12 Jun 2024 15:14:06 +0200 Subject: [PATCH 12/12] Update doc/src/core-transmutation.md --- doc/src/core-transmutation.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/src/core-transmutation.md b/doc/src/core-transmutation.md index ba66c41be7e18..3a71c0c12ff29 100644 --- a/doc/src/core-transmutation.md +++ b/doc/src/core-transmutation.md @@ -1,4 +1,4 @@ -# Challenge: Verify `core` transmuting methods +# Challenge 1: Verify `core` transmuting methods - **Status:** Open - **Tracking Issue:** [Link to issue](https://github.com/model-checking/verify-rust-std/issues/19)