Re: [PATCH 2/2] rust: page: add method to copy data between safe pages

[Miguel Ojeda]

On Mon, Feb 16, 2026 at 12:42 AM Andreas Hindborg <a.hindborg@xxxxxxxxxx> wrote:
>
> Why?

If you mean why we don't do it everywhere, then it is because for many
functions it wouldn't add much value, but it would add substantial
verbosity, which has a cost for both readers and writers.

Originally, we picked the standard library style, because it seemed
like a good balance that both had shown good results (especially for
this language, where we have rich, strong types in signatures which
help reduce the need) and that would get others to write docs easily.

Sometimes it may be needed, e.g. there are many parameters with
details to explain that wouldn't read well otherwise, or there are
primitive integers parameters with constraints on them (instead of a
newtype that enforces them) and so on.

i.e. why do you think you need it here? When a reader sees the list,
they will need to pause to read it, thinking there is something
important/subtle there -- is there?

(I say this as someone that generally likes structured, "exhaustive"
documentation such as, say, the classic Win32 docs...)

> Writes require a mutable reference. There cannot be a mutable reference
> while we have a shared reference.

Ok, but I am trying to map what you wrote with what the callee
requires. In the second bullet point, you justify there are no races
for the read side, and the third one for the write side. But you refer
to the type invariant in the second one, for some reason, and that
type invariant already promises no data races for `SafePage`, and all
we have here are `SafePage`s on both sides, no?

So to me it sounds like either you could justify everything just by
invoking the type invariant (that is why I mentioned circular
reasoning, because the type invariant doesn't seem justified itself in
`// INVARIANT:`) or the type invariant is actually a different, weaker
one (which would explain why you need extra explanations in `//
SAFETY:` on top of the type invariant).

(By the way, if we use bullet points, then I think we should map each
to the callee's one, i.e. #2 and #3 would be together since #2 is the
one in the callee about data races).

Cheers,
Miguel