From e6b72df11898cbf8b18c6bb358e6c876e4826782 Mon Sep 17 00:00:00 2001 From: Jack Wrenn Date: Mon, 23 Dec 2024 11:04:09 -0500 Subject: [PATCH] Apply suggestions from code review Co-authored-by: Joshua Liebow-Feeser --- src/next_array.rs | 31 +++++++++++++++++++++++-------- 1 file changed, 23 insertions(+), 8 deletions(-) diff --git a/src/next_array.rs b/src/next_array.rs index 5e3a30928..86480b197 100644 --- a/src/next_array.rs +++ b/src/next_array.rs @@ -38,13 +38,28 @@ impl ArrayBuilder { // 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 Drop for ArrayBuilder { // 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