Document the invariant that the vector's length is always less than or
equal to its capacity. This is already implied by these other
invariants:

- `self.len` always represents the exact number of elements stored in
  the vector.
- `self.layout` represents the absolute number of elements that can be
  stored within the vector without re-allocation.

but it doesn't hurt to spell it out. Note that the language references
`self.capacity` rather than `self.layout.len` as the latter is zero for
a vector of ZSTs.

Update a safety comment touched by this patch to correctly reference
`realloc` rather than `alloc` and replace "leaves" with "leave" to
improve grammar.

Signed-off-by: Tamir Duberstein <tamird@gmail.com>
---
 rust/kernel/alloc/kvec.rs | 19 +++++++++++--------
 1 file changed, 11 insertions(+), 8 deletions(-)

diff --git a/rust/kernel/alloc/kvec.rs b/rust/kernel/alloc/kvec.rs
index 7ebec5c4a277..f8045b6c8976 100644
--- a/rust/kernel/alloc/kvec.rs
+++ b/rust/kernel/alloc/kvec.rs
@@ -90,6 +90,8 @@ macro_rules! kvec {
 ///   without re-allocation. For ZSTs `self.layout`'s capacity is zero. However, it is legal for the
 ///   backing buffer to be larger than `layout`.
 ///
+/// - `self.len()` is always less than or equal to `self.capacity()`.
+///
 /// - The `Allocator` type `A` of the vector is the exact same `Allocator` type the backing buffer
 ///   was allocated with (and must be freed with).
 pub struct Vec<T, A: Allocator> {
@@ -262,8 +264,8 @@ pub const fn new() -> Self {
     /// Returns a slice of `MaybeUninit<T>` for the remaining spare capacity of the vector.
     pub fn spare_capacity_mut(&mut self) -> &mut [MaybeUninit<T>] {
         // SAFETY:
-        // - `self.len` is smaller than `self.capacity` and hence, the resulting pointer is
-        //   guaranteed to be part of the same allocated object.
+        // - `self.len` is smaller than `self.capacity` by the type invariant and hence, the
+        //   resulting pointer is guaranteed to be part of the same allocated object.
         // - `self.len` can not overflow `isize`.
         let ptr = unsafe { self.as_mut_ptr().add(self.len) } as *mut MaybeUninit<T>;
 
@@ -289,8 +291,8 @@ pub fn push(&mut self, v: T, flags: Flags) -> Result<(), AllocError> {
         self.reserve(1, flags)?;
 
         // SAFETY:
-        // - `self.len` is smaller than `self.capacity` and hence, the resulting pointer is
-        //   guaranteed to be part of the same allocated object.
+        // - `self.len` is smaller than `self.capacity` by the type invariant and hence, the
+        //   resulting pointer is guaranteed to be part of the same allocated object.
         // - `self.len` can not overflow `isize`.
         let ptr = unsafe { self.as_mut_ptr().add(self.len) };
 
@@ -822,12 +824,13 @@ pub fn collect(self, flags: Flags) -> Vec<T, A> {
             unsafe { ptr::copy(ptr, buf.as_ptr(), len) };
             ptr = buf.as_ptr();
 
-            // SAFETY: `len` is guaranteed to be smaller than `self.layout.len()`.
+            // SAFETY: `len` is guaranteed to be smaller than `self.layout.len()` by the type
+            // invariant.
             let layout = unsafe { ArrayLayout::<T>::new_unchecked(len) };
 
-            // SAFETY: `buf` points to the start of the backing buffer and `len` is guaranteed to be
-            // smaller than `cap`. Depending on `alloc` this operation may shrink the buffer or leaves
-            // it as it is.
+            // SAFETY: `buf` points to the start of the backing buffer and `len` is guaranteed by
+            // the type invariant to be smaller than `cap`. Depending on `realloc` this operation
+            // may shrink the buffer or leave it as it is.
             ptr = match unsafe {
                 A::realloc(Some(buf.cast()), layout.into(), old_layout.into(), flags)
             } {

-- 
2.49.0

On Mon, Apr 7, 2025 at 4:52 PM Tamir Duberstein <tamird@gmail.com> wrote:
>
> Document the invariant that the vector's length is always less than or
> equal to its capacity. This is already implied by these other
> invariants:
>
> - `self.len` always represents the exact number of elements stored in
>   the vector.
> - `self.layout` represents the absolute number of elements that can be
>   stored within the vector without re-allocation.
>
> but it doesn't hurt to spell it out. Note that the language references
> `self.capacity` rather than `self.layout.len` as the latter is zero for
> a vector of ZSTs.
>
> Update a safety comment touched by this patch to correctly reference
> `realloc` rather than `alloc` and replace "leaves" with "leave" to
> improve grammar.
>
> Signed-off-by: Tamir Duberstein <tamird@gmail.com>

This change has a conflict with the spare_capacity_mut patch in alloc-next.

Alice

On Wed, Apr 16, 2025 at 10:41 AM Alice Ryhl <aliceryhl@google.com> wrote:
>
> On Mon, Apr 7, 2025 at 4:52 PM Tamir Duberstein <tamird@gmail.com> wrote:
> >
> > Document the invariant that the vector's length is always less than or
> > equal to its capacity. This is already implied by these other
> > invariants:
> >
> > - `self.len` always represents the exact number of elements stored in
> >   the vector.
> > - `self.layout` represents the absolute number of elements that can be
> >   stored within the vector without re-allocation.
> >
> > but it doesn't hurt to spell it out. Note that the language references
> > `self.capacity` rather than `self.layout.len` as the latter is zero for
> > a vector of ZSTs.
> >
> > Update a safety comment touched by this patch to correctly reference
> > `realloc` rather than `alloc` and replace "leaves" with "leave" to
> > improve grammar.
> >
> > Signed-off-by: Tamir Duberstein <tamird@gmail.com>
>
> This change has a conflict with the spare_capacity_mut patch in alloc-next.

Indeed. I have resolved it locally but was holding off until some
reviews arrived. I guess I'll respin now.