refactor(deque): clarify proof contracts

Author: peter-jerry-ye

deque/index_ops.mbt

@@ -16,15 +16,13 @@
 /// The deque representation invariant guarantees these indices are in bounds.
 /// Keep these private so callers cannot bypass bounds checks.
 #inline
-#proof_import("moonbit_builtin_prelude.FixedArray")
 fn[T] UninitializedArray::unsafe_get(
   self : UninitializedArray[T],
   index : Int,
 ) -> T = "%fixedarray.unsafe_get"
 
 ///|
 #inline
-#proof_import("moonbit_builtin_prelude.FixedArray")
 fn[T] UninitializedArray::unsafe_set(
   self : UninitializedArray[T],
   index : Int,
@@ -40,11 +38,12 @@ fn wrap_index(
   offset : Int,
   capacity : Int,
 ) -> Int where {
-  proof_require: wrap_index_pre(head, offset, capacity),
+  proof_require: buffer_index_in_bounds(head, capacity),
+  proof_require: valid_wrap_offset(offset, capacity),
   proof_ensure: result => wrap_index_post(head, offset, capacity, result),
-  proof_ensure: result => wrap_index_mod_equiv(head, offset, capacity, result),
 } {
-  proof_assert single_wrap_range(head, offset, capacity)
+  proof_assert head + offset >= 0
+  proof_assert head + offset < capacity * 2
   let contiguous = capacity - head
   if offset < contiguous {
     proof_assert (head + offset) % capacity == head + offset
@@ -62,22 +61,23 @@ fn decrement_index(
   index : Int,
   capacity : Int,
 ) -> Int where {
-  proof_require: decrement_index_pre(index, capacity),
+  proof_require: buffer_index_in_bounds(index, capacity),
   proof_ensure: result => decrement_index_post(index, capacity, result),
-  proof_ensure: result => decrement_index_mod_equiv(index, capacity, result),
 } {
   if index == 0 {
+    proof_assert buffer_index_in_bounds(capacity - 1, capacity)
     proof_assert (index + capacity - 1) % capacity == capacity - 1
     capacity - 1
   } else {
+    proof_assert buffer_index_in_bounds(index - 1, capacity)
     proof_assert (index + capacity - 1) % capacity == index - 1
     index - 1
   }
 }
 
 ///|
 /// Computes the capacity used by `realloc` after its runtime overflow check.
-/// The contract proves the index invariant restored after a successful growth.
+/// The contract proves the layout invariant restored after a successful growth.
 #warnings("-unused_value")
 #inline
 fn deque_realloc_capacity(
@@ -101,10 +101,9 @@ fn deque_tail_index(
   len : Int,
   capacity : Int,
 ) -> Int where {
-  proof_require: deque_index_inv(capacity, head, len),
+  proof_require: deque_layout_inv(capacity, head, len),
   proof_require: len > 0,
   proof_ensure: result => wrap_index_post(head, len - 1, capacity, result),
-  proof_ensure: result => buffer_index_in_bounds(result, capacity),
 } {
   wrap_index(head, len - 1, capacity)
 }
@@ -118,11 +117,10 @@ fn deque_element_index(
   capacity : Int,
   index : Int,
 ) -> Int where {
-  proof_require: deque_index_inv(capacity, head, len),
+  proof_require: deque_layout_inv(capacity, head, len),
   proof_require: index >= 0,
   proof_require: index < len,
   proof_ensure: result => wrap_index_post(head, index, capacity, result),
-  proof_ensure: result => buffer_index_in_bounds(result, capacity),
 } {
   wrap_index(head, index, capacity)
 }
@@ -134,9 +132,11 @@ fn deque_push_back_core(
   len : Int,
   capacity : Int,
 ) -> Int where {
-  proof_require: deque_index_inv(capacity, head, len),
+  proof_require: deque_layout_inv(capacity, head, len),
   proof_require: len < capacity,
-  proof_ensure: result => deque_push_back_post(capacity, head, len, result),
+  proof_ensure: result => {
+    deque_push_back_index_post(capacity, head, len, result)
+  },
 } {
   wrap_index(head, len, capacity)
 }
@@ -149,9 +149,11 @@ fn deque_push_front_core(
   len : Int,
   capacity : Int,
 ) -> Int where {
-  proof_require: deque_index_inv(capacity, head, len),
+  proof_require: deque_layout_inv(capacity, head, len),
   proof_require: len < capacity,
-  proof_ensure: result => deque_push_front_post(capacity, head, len, result),
+  proof_ensure: result => {
+    deque_push_front_index_post(capacity, head, len, result)
+  },
 } {
   decrement_index(head, capacity)
 }
@@ -164,9 +166,11 @@ fn deque_pop_front_core(
   len : Int,
   capacity : Int,
 ) -> Int where {
-  proof_require: deque_index_inv(capacity, head, len),
+  proof_require: deque_layout_inv(capacity, head, len),
   proof_require: len > 0,
-  proof_ensure: result => deque_pop_front_post(capacity, head, len, result),
+  proof_ensure: result => {
+    deque_pop_front_index_post(capacity, head, len, result)
+  },
 } {
   wrap_index(head, 1, capacity)
 }
@@ -178,9 +182,9 @@ fn deque_pop_back_core(
   len : Int,
   capacity : Int,
 ) -> Int where {
-  proof_require: deque_index_inv(capacity, head, len),
+  proof_require: deque_layout_inv(capacity, head, len),
   proof_require: len > 0,
-  proof_ensure: result => deque_pop_back_post(capacity, head, len, result),
+  proof_ensure: result => deque_pop_back_index_post(capacity, head, len, result),
 } {
   wrap_index(head, len - 1, capacity)
 }

deque/index_ops.mbtp

@@ -13,98 +13,60 @@
 // limitations under the License.
 
 ///|
-/// Contracts for the private circular-buffer index operations.
-/// `offset` may reach `capacity` for the next free slot, but never exceeds it.
-predicate wrap_index_pre(head : Int, offset : Int, capacity : Int) {
-  capacity > 0 &&
-  head >= 0 &&
-  head < capacity &&
-  offset >= 0 &&
-  offset <= capacity
+/// A physical index into a buffer of `capacity` elements.
+predicate buffer_index_in_bounds(index : Int, capacity : Int) {
+  index >= 0 && index < capacity
 }
 
 ///|
-/// A valid deque offset can cross the end of the buffer at most once.
-predicate single_wrap_range(head : Int, offset : Int, capacity : Int) {
-  head + offset >= 0 && head + offset < capacity * 2
+/// An offset accepted by a single-wrap operation. The upper bound is inclusive
+/// because advancing one position in a capacity-one buffer uses `offset == 1`.
+predicate valid_wrap_offset(offset : Int, capacity : Int) {
+  offset >= 0 && offset <= capacity
 }
 
 ///|
-/// The branch form is also the machine-integer safety argument: every
-/// subtraction is non-negative, and the addition branch stays below capacity.
+/// The result is in bounds, follows the branch implementation, and is equal to
+/// the remainder expression in the mathematical-integer proof model.
 predicate wrap_index_post(
   head : Int,
   offset : Int,
   capacity : Int,
   result : Int,
 ) {
-  result >= 0 &&
-  result < capacity &&
+  buffer_index_in_bounds(result, capacity) &&
   (if offset < capacity - head {
     result == head + offset
   } else {
     result == offset - (capacity - head)
-  })
-}
-
-///|
-/// In the mathematical-integer proof model, the branch form is exactly the
-/// remainder expression it replaces.
-predicate wrap_index_mod_equiv(
-  head : Int,
-  offset : Int,
-  capacity : Int,
-  result : Int,
-) {
+  }) &&
   result == (head + offset) % capacity
 }
 
-///|
-predicate decrement_index_pre(index : Int, capacity : Int) {
-  capacity > 0 && index >= 0 && index < capacity
-}
-
 ///|
 predicate decrement_index_post(
   index : Int,
   capacity : Int,
   result : Int,
 ) {
-  result >= 0 &&
-  result < capacity &&
-  (if index == 0 { result == capacity - 1 } else { result == index - 1 })
-}
-
-///|
-predicate decrement_index_mod_equiv(
-  index : Int,
-  capacity : Int,
-  result : Int,
-) {
+  buffer_index_in_bounds(result, capacity) &&
+  (if index == 0 { result == capacity - 1 } else { result == index - 1 }) &&
   result == (index + capacity - 1) % capacity
 }
 
 ///|
 /// The arithmetic part of the private `Deque` representation invariant.
-predicate deque_index_inv(capacity : Int, head : Int, len : Int) {
+predicate deque_layout_inv(capacity : Int, head : Int, len : Int) {
   (capacity == 0 && head == 0 && len == 0) ||
-  (capacity > 0 &&
-    head >= 0 &&
-    head < capacity &&
+  (buffer_index_in_bounds(head, capacity) &&
     len >= 0 &&
     len <= capacity)
 }
 
-///|
-predicate buffer_index_in_bounds(index : Int, capacity : Int) {
-  index >= 0 && index < capacity
-}
-
 ///|
 /// The numerical part of the deque invariant needed by reallocation. Element
 /// initialization and logical order are deliberately outside this proof slice.
 predicate deque_realloc_pre(capacity : Int, len : Int) {
-  capacity >= 0 &&
   capacity <= 0x3fff_ffff &&
   len >= 0 &&
   len <= capacity
@@ -121,63 +83,50 @@ predicate deque_realloc_post(
   new_capacity > capacity &&
   new_capacity <= 0x7fff_ffff &&
   len < new_capacity &&
-  deque_index_inv(new_capacity, 0, len)
+  deque_layout_inv(new_capacity, 0, len)
 }
 
 ///|
-predicate deque_push_back_post(
+predicate deque_push_back_index_post(
   capacity : Int,
   head : Int,
   len : Int,
   write_index : Int,
 ) {
-  buffer_index_in_bounds(write_index, capacity) &&
-  deque_index_inv(capacity, head, len + 1)
+  wrap_index_post(head, len, capacity, write_index) &&
+  deque_layout_inv(capacity, head, len + 1)
 }
 
 ///|
-predicate deque_push_front_post(
+predicate deque_push_front_index_post(
   capacity : Int,
   head : Int,
   len : Int,
   new_head : Int,
 ) {
   decrement_index_post(head, capacity, new_head) &&
-  buffer_index_in_bounds(new_head, capacity) &&
-  deque_index_inv(capacity, new_head, len + 1)
+  deque_layout_inv(capacity, new_head, len + 1)
 }
 
 ///|
-predicate deque_pop_front_post(
+predicate deque_pop_front_index_post(
   capacity : Int,
   head : Int,
   len : Int,
   new_head : Int,
 ) {
   buffer_index_in_bounds(head, capacity) &&
   wrap_index_post(head, 1, capacity, new_head) &&
-  deque_index_inv(capacity, new_head, len - 1)
+  deque_layout_inv(capacity, new_head, len - 1)
 }
 
 ///|
-predicate deque_pop_back_post(
+predicate deque_pop_back_index_post(
   capacity : Int,
   head : Int,
   len : Int,
   tail : Int,
 ) {
   wrap_index_post(head, len - 1, capacity, tail) &&
-  buffer_index_in_bounds(tail, capacity) &&
-  deque_index_inv(capacity, head, len - 1)
-}
-
-///|
-lemma wrap_index_pre_has_single_wrap(
-  head : Int,
-  offset : Int,
-  capacity : Int,
-) where {
-  proof_require: wrap_index_pre(head, offset, capacity),
-  proof_ensure: single_wrap_range(head, offset, capacity),
-} {
+  deque_layout_inv(capacity, head, len - 1)
 }