On Mon Sep 28, 2026 at 5:42 PM JST, Eliot Courtney wrote:
<...>
> +impl EncodedStream {
> + /// Creates an empty stream.
> + fn new() -> Self {
> + // INVARIANT: An empty stream's byte length is 0, a multiple of
> `size_of::<u64>()`.
> + Self(Vec::new())
> + }
> +
> + /// Appends a single `u64` to the stream.
> + fn push_u64(&mut self, value: u64) -> Result {
> + // INVARIANT: Appending `size_of::<u64>()` bytes keeps the byte
> length a multiple of
> + // `size_of::<u64>()`.
> + Ok(self.0.extend_from_slice(&value.to_ne_bytes(), GFP_KERNEL)?)
> + }
> +
> + /// Appends `data` as bytes to the stream, zero-padded to a `u64`
> boundary.
> + fn extend_with_padding<T: IntoBytes + Immutable + ?Sized>(&mut self,
> data: &T) -> Result {
> + let bytes = data.as_bytes();
> + let padded = bytes.len().next_multiple_of(size_of::<u64>());
> + // Reserve so that a failed allocation can't leave the invariant
> violated.
> + self.0.reserve(padded, GFP_KERNEL)?;
> + self.0.extend_from_slice(bytes, GFP_KERNEL)?;
> + // INVARIANT: The padding ensures the total length remains a
> multiple of
> + // `size_of::<u64>()`.
> + Ok(self.0.extend_with(padded - bytes.len(), 0u8, GFP_KERNEL)?)
> + }
> +}
> +
> +// The Deref to `&[u64]` relies on this alignment guarantee.
nit: `Deref`
... and that's all I could find on this patch. I particularly like how
the examples have turned out!