{
  "$type": "site.standard.document",
  "bskyPostRef": {
    "cid": "bafyreibqfaipfzfhuq3ngq6xep262aflmliswxbieyi7i2elgfk25np3w4",
    "uri": "at://did:plc:ivbknywyskln22er3nkssdhl/app.bsky.feed.post/3mk3b7vfc56l2"
  },
  "path": "/t/pre-rfc-a-tiny-internal-change-to-reverse-copy-from-slice-swap-with-slice/24189#post_1",
  "publishedAt": "2026-04-22T08:15:06.000Z",
  "site": "https://internals.rust-lang.org",
  "tags": [
    "source",
    "Creusot",
    "the Verify Rust std challenge",
    "Our verified version of swap_with_slice"
  ],
  "textContent": "tl;dr: I propose to rewrite, for example, `swap_with_slice` from this current version (source)\n\n\n    // Before (minimized)\n    pub const fn swap_with_slice(&mut self, other: &mut [T]) {\n        unsafe {\n            ptr::swap_nonoverlapping(self.as_mut_ptr(), other.as_mut_ptr(), self.len());\n        }\n    }\n\n\nto lift `self.len()` to the front as follows:\n\n\n    // After (minimized)\n    pub const fn swap_with_slice(&mut self, other: &mut [T]) {\n        let len = self.len();\n        unsafe {\n            ptr::swap_nonoverlapping(self.as_mut_ptr(), other.as_mut_ptr(), len);\n        }\n    }\n\n\nThe same idea applies to the implementation of `reverse` and `copy_from_slice`.\n\nAre there any downsides to such a rewrite?\n\n* * *\n\n### Motivation\n\nI'm working on formally verifying slice functions in core using Creusot (see also the Verify Rust std challenge).\n\nPart of the approach is to annotate functions with \"ghost code\" to enable formal reasoning using our tool Creusot with no impact to run-time. The goal being to verify fragments of core, there is an automated \"erasure check\" that if you remove this ghost code, the remaining code must match the original code in core. This check works for most functions, except the three in the title.\n\nIn the `swap_with_slice` example above, the method `as_mut_ptr` returns a raw pointer, and we extend its result with some \"ghost data\" that lets us record what the pointer is pointing to. Unfortunately for us, this \"ghost data\" carries the same lifetime as the input borrow, whereas previously `as_mut_ptr` only returned a raw pointer so there were no lifetimes in the result. Because of this, `self` is no longer available to call `self.len()`.\n\nHence our current solution is to rewrite this function to get `self.len()` first, and I'm wondering if it would make sense to upstream this single change to core, instead of extending our \"erasure check\" with an ad hoc rule for this case. (Our verified version of swap_with_slice for the curious.)\n\nIndeed, even outside of formal verification, one could argue that `self.as_mut_ptr()` \"morally borrows\" from `self`, so calling `self.len()` while the raw pointer `self.as_mut_ptr()` is still in use is kinda smelly.\n\nI'm curious to hear people's thoughts on this.",
  "title": "[Pre-RFC] A tiny internal change to `reverse`, `copy_from_slice`, `swap_with_slice`"
}