Apply suggestions from code review

Co-authored-by: Joshua Liebow-Feeser <[email protected]>

src/next_array.rs

@@ -38,13 +38,28 @@ impl<T, const N: usize> ArrayBuilder<T, N> {
         // invariant of `self.arr`. Even if this line panics, we have not
         // created any intermediate invalid state.
         *place = MaybeUninit::new(value);
-        // PANICS: This cannot panic, since `self.len < N <= usize::MAX`.
-        // `0..self.len` are valid. Due to the above write, the element at
-        // `self.len` is now also valid. Consequently, all elements at indicies
-        // `0..(self.len + 1)` are valid, and `self.len` can be safely
-        // incremented without violating `self.arr`'s invariant. It is fine if
-        // this increment panics, as we have not created any intermediate
-        // invalid state.
+        // Lemma: `self.len < N`. By invariant, `self.len <= N`. Above, we index
+        // into `self.arr`, which has size `N`, at index `self.len`. If `self.len == N`
+        // at that point, that index would be out-of-bounds, and the index
+        // operation would panic. Thus, `self.len != N`, and since `self.len <= N`,
+        // that means that `self.len < N`.
+        //
+        // PANICS: Since `self.len < N`, and since `N <= usize::MAX`,
+        // `self.len + 1 <= usize::MAX`, and so `self.len += 1` will not
+        // overflow. Overflow is the only panic condition of `+=`.
+        //
+        // SAFETY:
+        // - We are required to uphold the invariant that `self.len <= N`.
+        //   Since, by the preceding lemma, `self.len < N` at this point in the
+        //   code, `self.len += 1` results in `self.len <= N`.
+        // - We are required to uphold the invariant that `self.arr[..self.len]`
+        //   are valid instances of `T`. Since this invariant already held when
+        //   this method was called, and since we only increment `self.len`
+        //   by 1 here, we only need to prove that the element at
+        //   `self.arr[self.len]` (using the value of `self.len` before incrementing)
+        //   is valid. Above, we construct `place` to point to `self.arr[self.len]`,
+        //   and then initialize `*place` to `MaybeUninit::new(value)`, which is
+        //   a valid `T` by construction.
         self.len += 1;
     }
 
@@ -92,7 +107,7 @@ impl<T, const N: usize> Drop for ArrayBuilder<T, N> {
     // selectively run their destructors.
     fn drop(&mut self) {
         // SAFETY:
-        // - by invariant on `&[T]`, `self.as_mut()` is:
+        // - by invariant on `&mut [T]`, `self.as_mut()` is:
         //   - valid for reads and writes
         //   - properly aligned
         //   - non-null