From: "Gary Guo" <gary@garyguo.net>
To: "Miguel Ojeda" <miguel.ojeda.sandonis@gmail.com>,
"Lorenzo Delgado" <lnsdev@proton.me>
Cc: "Miguel Ojeda" <ojeda@kernel.org>,
"Boqun Feng" <boqun@kernel.org>, "Gary Guo" <gary@garyguo.net>,
"Björn Roy Baron" <bjorn3_gh@protonmail.com>,
"Benno Lossin" <lossin@kernel.org>,
"Andreas Hindborg" <a.hindborg@kernel.org>,
"Alice Ryhl" <aliceryhl@google.com>,
"Trevor Gross" <tmgross@umich.edu>,
"Danilo Krummrich" <dakr@kernel.org>,
"Daniel Almeida" <daniel.almeida@collabora.com>,
"Tamir Duberstein" <tamird@kernel.org>,
"Alexandre Courbot" <acourbot@nvidia.com>,
"Onur Özkan" <work@onurozkan.dev>,
linux-kernel@vger.kernel.org, rust-for-linux@vger.kernel.org,
"Thorsten Blum" <blum@kernel.org>,
"Francis Laniel" <laniel_francis@npnm.eu>
Subject: Re: [PATCH v3 1/2] rust: non_empty: add NonEmpty
Date: Wed, 14 Oct 2026 15:25:31 +0100 [thread overview]
Message-ID: <DM4MPF17NSQL.2IOMXIQEVINKR@garyguo.net> (raw)
In-Reply-To: <CANiq72nok4xoA6j1SXVdWKLEKAqj3MfzCa-Sse7NNbkrn2MXiw@mail.gmail.com>
On Wed Oct 14, 2026 at 12:55 PM BST, Miguel Ojeda wrote:
> On Wed, Oct 14, 2026 at 10:30 AM Lorenzo Delgado <lnsdev@proton.me> wrote:
>>
>> +/// A container that can report whether it holds any element.
>> +///
>> +/// The result must not change while the container is only reachable through a shared reference.
>> +///
>> +/// Unsafe code may only rely on the result for a container type whose implementation it trusts,
>> +/// such as the ones in this module, since a safe implementation can return anything.
>> +pub trait IsEmpty {
>> + /// Returns `true` if the container holds no element.
>> + fn is_empty(&self) -> bool;
>> +}
>
> Do we need this to be a safe trait? If it is unsafe, then we can
> simplify the invariant and more easily think about the type, like
> other `Non*`s, no?
I think in this case the meaning of "empty" depends on the container itself.
Unsafe code that relies on "is_empty" would be the `NonEmpty<Container>` itself,
so it just needs to trust itself (as boundary of unsafe is module level).
I think of almost all of the text above can be removed. The invariant of
`NonEmpty` can just be "`IsEmpty::is_empty` has returned true" and how it is
interpreted is up to the container type.
Best,
Gary
next prev parent reply other threads:[~2026-10-14 14:25 UTC|newest]
Thread overview: 5+ messages / expand[flat|nested] mbox.gz Atom feed top
2026-10-14 8:30 [PATCH v3 0/2] rust: add NonEmpty Lorenzo Delgado
2026-10-14 8:30 ` [PATCH v3 1/2] rust: non_empty: " Lorenzo Delgado
2026-10-14 11:55 ` Miguel Ojeda
2026-10-14 14:25 ` Gary Guo [this message]
2026-10-14 8:30 ` [PATCH v3 2/2] rust: uaccess: use NonEmpty in strcpy_into_buf() Lorenzo Delgado
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=DM4MPF17NSQL.2IOMXIQEVINKR@garyguo.net \
--to=gary@garyguo.net \
--cc=a.hindborg@kernel.org \
--cc=acourbot@nvidia.com \
--cc=aliceryhl@google.com \
--cc=bjorn3_gh@protonmail.com \
--cc=blum@kernel.org \
--cc=boqun@kernel.org \
--cc=dakr@kernel.org \
--cc=daniel.almeida@collabora.com \
--cc=laniel_francis@npnm.eu \
--cc=linux-kernel@vger.kernel.org \
--cc=lnsdev@proton.me \
--cc=lossin@kernel.org \
--cc=miguel.ojeda.sandonis@gmail.com \
--cc=ojeda@kernel.org \
--cc=rust-for-linux@vger.kernel.org \
--cc=tamird@kernel.org \
--cc=tmgross@umich.edu \
--cc=work@onurozkan.dev \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is an external index of several public inboxes,
see mirroring instructions on how to clone and mirror
all data and code used by this external index.