Re: [PATCH 2/5] rust: alloc: add Vec::pop

[Benno Lossin]

On Fri Mar 21, 2025 at 8:44 AM CET, Alice Ryhl wrote:
> On Thu, Mar 20, 2025 at 10:11:09PM +0000, Benno Lossin wrote:
>> On Thu Mar 20, 2025 at 2:52 PM CET, Alice Ryhl wrote:
>> > +
>> > +        // INVARIANT: If the first `len` elements are valid, then the first `len-1` elements are
>> 
>> Please add spaces around `-`.
>
> I can do that, but does it really read better?

That's how rustfmt would format it and I do think it improves
readability for me.

>> > +        // valid.
>> > +        self.len = len_sub_1;
>> > +
>> > +        // INVARIANT: This invalidates a value in this vector's allocation, but the Vec invariants
>> > +        // do not require it to be valid because `self.len <= len_sub_1`.
>> 
>> I don't think this should be an `INVARIANT` comment. Maybe we don't even
>> need it.
>
> I can drop the INVARIANT: prefix.

Sounds good.

---
Cheers,
Benno