perf(deque): avoid modulo and redundant bounds checks

[peter-jerry-ye]

Why

Deque hot push, pop, and access paths repeatedly use remainder arithmetic to wrap circular-buffer indices, then perform bounds checks even when the private representation invariant establishes that the physical index is valid. This adds avoidable work to queue-heavy users such as async queues.

What changed

• Add private inline circular-index operations for logical offsets, successors, and predecessors, using branches instead of division.
• Use the branch-computed physical indices with private unchecked buffer access in simple push, pop, and element-access paths.
• Keep loop-heavy shifting, blitting, append, removal, and reversal paths on their existing remainder arithmetic and checked access.
• Route capacity growth through an inline arithmetic helper and reject capacities that cannot be doubled without overflowing Int.
• Add a regression test that compares Deque behavior with an Array model across wrap and growth boundaries.
• Add proof predicates and lemmas in index_ops.mbtp. Proof checking remains opt-in; the package does not enable proof mode.

Why this is correct

The scalar representation invariant covers both the zero-capacity empty state and positive-capacity states with a valid head and a length between zero and capacity.

For an arbitrary logical offset, index_in_bounds(start, capacity) and index_in_bounds(offset, capacity) imply that the sum can cross the buffer end at most once. circular_index_at_offset_correct proves that the branch calculation produces an in-bounds physical index equal to (start + offset) % capacity. Separate circular_successor_correct and circular_predecessor_correct lemmas prove the corresponding adjacent-index branches, including capacity-one buffers.

Small scalar wrappers instantiate those lemmas for tail lookup, element access, and push/pop transitions. Their contracts prove both the physical access bounds and preservation of the numeric Deque invariant after the head or length changes.

Capacity growth proves a separate arithmetic slice: after the runtime overflow guard, successful doubling produces a larger representable capacity, preserves the length, restores the numeric invariant with head = 0, and leaves a spare slot for the push that requested growth.

The proof scope is intentionally limited to scalar index arithmetic and invariant transitions. It does not model unchecked array intrinsics, allocation or copying, mutable Deque fields, or complete public methods; those remain ordinary runtime code covered by tests. The public API is unchanged.

[bobzhang]

Review sign-off (Claude)

Reviewed the diff with a full call-site safety audit, machine-checked the proof layer, and benchmarked the change. LGTM — sign-off.

Unchecked-access safety audit

I traced every converted site's precondition (capacity > 0, 0 <= head < capacity, 0 <= offset <= capacity) back to a public guard or loop bound:

• insert/push_front/push_back realloc first when full, so capacity > len holds before any wrap; insert's shift offsets stay <= len < cap, and its final write at offset index <= len < cap.
• remove, front/back, pop_front/pop_back, at/set/get all establish len > 0 (hence cap > 0) or full index bounds before touching the buffer; index_out_of_bounds aborts, so the fall-through in at/set is unreachable on bad input.
• blit_to's guard! plus the reserve_capacity branch give dst_offset + len <= dst cap and src_offset + len <= self.len <= cap; the self-blit reverse-copy logic is untouched.
• append reserves space up front, so self.len < cap throughout its loop, and the pre-existing capture of other's state keeps self-append correct.
• rev_in_place's cursors stay in [0, cap) inductively via wrap_index(·, 1, ·) / decrement_index.
• Crucially, none of the converted functions invoke user callbacks between establishing a precondition and the unchecked access — iter/each/retain-style callback paths keep their checked accesses, exactly as the PR claims.

The branch forms are equivalent to the modulo they replace under those preconditions (including the offset == capacity next-free-slot case), and the else-branch offset - contiguous indeed avoids materializing head + offset.

Proof layer — verified, not just documentation

The package doesn't opt into proof mode, but I enabled it locally (proof_enabled: true in options(...)) and ran moon prove deque with Why3 + Z3/CVC5/Alt-Ergo: 26 of 26 goals proved. So the wrap_index/decrement_index contracts, the proof_asserts, and every lemma in wrap_index.mbtp discharge automatically — there are no proof_axiomatized trusted bridges. Two notes for follow-ups:

• moon prove needs a Why3 config whose loadpath points at ~/.moon/lib/prelude_proof, otherwise it fails with Library file not found: moonbit_builtin_prelude — worth capturing when proof CI is set up.
• The lemmas document the per-call-site discharge argument but aren't yet referenced by contracts on the deque methods themselves (the methods carry no proof_require/proof_ensure). That's a reasonable first slice — the arithmetic invariant, not a full semantic model — and matches the stated opt-in scoping.

The updated invariant documentation (zero-capacity ⇒ head == 0, established by new_deque, realloc, and clear) matches the implementation.

Test

The model-based test is deterministic and well-formed: each 13-step cycle adds 6 and removes 6 elements, and the element count at every pop/remove step is provably ≥ 1, so model.remove/% model.length() never see an empty array. It exercises wrap drift, growth from capacities 0/1/3/5/15, mid-insert/remove, and reversal, with a full to_array equality check after every step.

Benchmarks (the PR ships none)

Native ARM64, moon bench --release, identical temporary bench file on this branch vs main:

Case	main	this PR	Speedup
push_back+pop_front cycle, len 64 (256 pairs)	1.48 µs	1.40 µs	1.06×
at scan, len 256, wrapped	144.3 ns	77.2 ns	1.87×
rev_in_place, len 255, wrapped	380.9 ns	132.9 ns	2.87×
insert+remove at midpoint, len 128	154.4 ns	69.0 ns	2.24×

The index-arithmetic-bound loops get 1.9–2.9×; the push/pop cycle improves modestly since those ops are dominated by other work. The motivation holds up.

Rebase & verification

The branch rebases onto current main with zero conflicts (I could not push it — the fork has maintainer edits disabled — but GitHub already reports the PR mergeable, and all verification below ran on the locally rebased tip): moon check clean, moon fmt + moon info zero drift (public API unchanged), moon test 7008/7008, deque+queue on native 285/285 and js 297/297 — the queue package now sitting on top of deque gets this for free.

🤖 Generated with Claude Code

[Copilot]

Pull request overview

Optimizes Deque’s circular-buffer index arithmetic by replacing %-based wrapping with branch-based helpers and leveraging unchecked buffer accesses where existing preconditions/invariants guarantee safety, aiming to reduce overhead in hot deque operations.

Changes:

• Introduces branch-based wrap_index / decrement_index helpers (plus proof predicates/lemmas) to avoid division and redundant checks.
• Switches multiple internal deque operations to use unchecked buffer get/set where loop bounds and invariants establish valid physical indices.
• Adds a model-based regression test that exercises mixed operations across wrap-around and growth scenarios.

Reviewed changes

Copilot reviewed 4 out of 4 changed files in this pull request and generated 1 comment.

File	Description
deque/wrap_index.mbtp	Adds proof predicates/lemmas documenting and supporting the wrap/decrement helpers and deque index invariants.
deque/types.mbt	Updates Deque documentation/invariants to describe wrapped indexing and the zero-capacity representation.
deque/deque.mbt	Implements branch-based wrapping helpers and applies unchecked buffer access in performance-sensitive paths.
deque/deque_test.mbt	Adds a model-based regression test to validate behavior across wrap and growth boundaries.

Suppressed comments (2)

deque/types.mbt:47

• The invariant refers to wrap(head + i, buf.length()), but there is no wrap helper and it also doesn’t match the signature of the new wrap_index(head, offset, capacity) helper used by the implementation. Align the doc with the actual wrapping helper (or the % form) so readers can directly relate the invariant to the code.

/// - Element at index `i` is at `buf[wrap(head + i, buf.length())]`

deque/types.mbt:34

• Same issue as above: wrap(...) is not an actual function in the codebase, so the example reads like a call to a missing API. Prefer wrap_index(head, offset, cap) (matches the implementation) or % in the doc example.

///   head = 1, len = 5, tail = wrap(1 + 5 - 1, 8) = 5

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[bobzhang]

Addressed in d97584e1 on the maintainer branch deque-optimize-3969 (this fork does not allow maintainer pushes, so the fix could not land on the PR branch directly): the layout examples and invariants now reference the real helper with its actual signature — tail = wrap_index(5, 5 - 1, 8) = 1, element i at buf[wrap_index(head, i, buf.length())], and the back element at buf[wrap_index(head, len - 1, buf.length())]. That branch also carries the rebase onto current main and the requested method-style accessors (buf.unsafe_get(i) / buf.unsafe_set(i, v)). @peter-jerry-ye you can git reset --hard origin/deque-optimize-3969 your branch to adopt all of it, or apply the patches posted above.

🤖 Generated with Claude Code

[bobzhang]

Maintainer style request (relayed by Claude)

@peter-jerry-ye — one styling request from review before merge: declare the unsafe buffer accessors as package-local methods on UninitializedArray instead of free functions, so the call sites read as method chains:

///|
/// The deque representation invariant guarantees these indices are in bounds.
/// Keep these private so callers cannot bypass bounds checks.
#inline
fn[T] UninitializedArray::unsafe_get(
  self : UninitializedArray[T],
  index : Int,
) -> T = "%fixedarray.unsafe_get"

///|
#inline
fn[T] UninitializedArray::unsafe_set(
  self : UninitializedArray[T],
  index : Int,
  value : T,
) -> Unit = "%fixedarray.unsafe_set"

so e.g. unsafe_buffer_set(dst.buf, dst_idx, unsafe_buffer_get(self.buf, src_idx)) becomes dst.buf.unsafe_set(dst_idx, self.buf.unsafe_get(src_idx)). Non-pub methods on a foreign type are package-local, so the public API and generated interfaces are unchanged.

I verified the converted branch locally (this fork has maintainer edits disabled, so I can't push it): moon check clean, moon fmt/moon info zero drift, full suite 7008/7008, deque+queue native 285/285, and the proof layer still proves 26/26 goals. Full ready-to-apply patch below (git am-able on top of the current branch):

Patch: style(deque): declare unsafe buffer accessors as local methods

---
 deque/deque.mbt | 55 ++++++++++++++++++++++++-------------------------
 1 file changed, 27 insertions(+), 28 deletions(-)

diff --git a/deque/deque.mbt b/deque/deque.mbt
index 016ed447..3cea95d2 100644
--- a/deque/deque.mbt
+++ b/deque/deque.mbt
@@ -19,12 +19,15 @@ fn[T] set_null(buffer : UninitializedArray[T], index : Int) = "%fixedarray.set_n
 /// The deque representation invariant guarantees these indices are in bounds.
 /// Keep these private so callers cannot bypass bounds checks.
 #inline
-fn[T] unsafe_buffer_get(buffer : UninitializedArray[T], index : Int) -> T = "%fixedarray.unsafe_get"
+fn[T] UninitializedArray::unsafe_get(
+  self : UninitializedArray[T],
+  index : Int,
+) -> T = "%fixedarray.unsafe_get"
 
 ///|
 #inline
-fn[T] unsafe_buffer_set(
-  buffer : UninitializedArray[T],
+fn[T] UninitializedArray::unsafe_set(
+  self : UninitializedArray[T],
   index : Int,
   value : T,
 ) -> Unit = "%fixedarray.unsafe_set"
@@ -345,13 +348,13 @@ pub fn[A] Deque::blit_to(
     for i in len>..0 {
       let dst_idx = wrap_index(dst.head, dst_offset + i, dst.buf.length())
       let src_idx = wrap_index(self.head, src_offset + i, self.buf.length())
-      unsafe_buffer_set(dst.buf, dst_idx, unsafe_buffer_get(self.buf, src_idx))
+      dst.buf.unsafe_set(dst_idx, self.buf.unsafe_get(src_idx))
     }
   } else {
     for i in 0..<len {
       let dst_idx = wrap_index(dst.head, dst_offset + i, dst.buf.length())
       let src_idx = wrap_index(self.head, src_offset + i, self.buf.length())
-      unsafe_buffer_set(dst.buf, dst_idx, unsafe_buffer_get(self.buf, src_idx))
+      dst.buf.unsafe_set(dst_idx, self.buf.unsafe_get(src_idx))
       if dst_offset + i >= dst_len {
         dst.len += 1
       }
@@ -418,11 +421,7 @@ pub fn[A] Deque::append(self : Deque[A], other : Deque[A]) -> Unit {
   for i in 0..<other_len {
     let read_idx = wrap_index(other_head, i, other_buf_len)
     let write_idx = wrap_index(self.head, self.len, cap)
-    unsafe_buffer_set(
-      self.buf,
-      write_idx,
-      unsafe_buffer_get(other_buf, read_idx),
-    )
+    self.buf.unsafe_set(write_idx, other_buf.unsafe_get(read_idx))
     self.len += 1
   }
 }
@@ -487,7 +486,7 @@ pub fn[A] Deque::insert(self : Deque[A], index : Int, value : A) -> Unit {
     for i in 0..<index {
       let to = wrap_index(new_head, i, cap)
       let from = wrap_index(self.head, i, cap)
-      unsafe_buffer_set(self.buf, to, unsafe_buffer_get(self.buf, from))
+      self.buf.unsafe_set(to, self.buf.unsafe_get(from))
     }
     self.head = new_head
   } else {
@@ -495,10 +494,10 @@ pub fn[A] Deque::insert(self : Deque[A], index : Int, value : A) -> Unit {
     for i = self.len; i > index; i = i - 1 {
       let from = wrap_index(self.head, i - 1, cap)
       let to = wrap_index(self.head, i, cap)
-      unsafe_buffer_set(self.buf, to, unsafe_buffer_get(self.buf, from))
+      self.buf.unsafe_set(to, self.buf.unsafe_get(from))
     }
   }
-  unsafe_buffer_set(self.buf, wrap_index(self.head, index, cap), value)
+  self.buf.unsafe_set(wrap_index(self.head, index, cap), value)
   self.len += 1
 }
 
@@ -563,7 +562,7 @@ pub fn[A] Deque::remove(self : Deque[A], index : Int) -> A {
     for i in index>..0 {
       let to = wrap_index(self.head, i + 1, cap)
       let from = wrap_index(self.head, i, cap)
-      unsafe_buffer_set(self.buf, to, unsafe_buffer_get(self.buf, from))
+      self.buf.unsafe_set(to, self.buf.unsafe_get(from))
     }
     set_null(self.buf, self.head)
     self.head = new_head
@@ -573,7 +572,7 @@ pub fn[A] Deque::remove(self : Deque[A], index : Int) -> A {
     for i in (index + 1)..<self.len {
       let to = wrap_index(self.head, i - 1, cap)
       let from = wrap_index(self.head, i, cap)
-      unsafe_buffer_set(self.buf, to, unsafe_buffer_get(self.buf, from))
+      self.buf.unsafe_set(to, self.buf.unsafe_get(from))
     }
     set_null(self.buf, tail_idx)
   }
@@ -657,7 +656,7 @@ pub fn[A] Deque::front(self : Deque[A]) -> A? {
   if self.len == 0 {
     None
   } else {
-    Some(unsafe_buffer_get(self.buf, self.head))
+    Some(self.buf.unsafe_get(self.head))
   }
 }
 
@@ -675,7 +674,7 @@ pub fn[A] Deque::back(self : Deque[A]) -> A? {
   if self.len == 0 {
     None
   } else {
-    Some(unsafe_buffer_get(self.buf, self.tail_index()))
+    Some(self.buf.unsafe_get(self.tail_index()))
   }
 }
 
@@ -698,7 +697,7 @@ pub fn[A] Deque::push_front(self : Deque[A], value : A) -> Unit {
   }
   let cap = self.buf.length()
   self.head = decrement_index(self.head, cap)
-  unsafe_buffer_set(self.buf, self.head, value)
+  self.buf.unsafe_set(self.head, value)
   self.len += 1
 }
 
@@ -721,7 +720,7 @@ pub fn[A] Deque::push_back(self : Deque[A], value : A) -> Unit {
   }
   let cap = self.buf.length()
   let write_idx = wrap_index(self.head, self.len, cap)
-  unsafe_buffer_set(self.buf, write_idx, value)
+  self.buf.unsafe_set(write_idx, value)
   self.len += 1
 }
 
@@ -832,7 +831,7 @@ pub fn[A] Deque::unsafe_pop_back(self : Deque[A]) -> Unit {
 /// ```
 pub fn[A] Deque::pop_front(self : Deque[A]) -> A? {
   guard self.len > 0 else { return None }
-  let value = unsafe_buffer_get(self.buf, self.head)
+  let value = self.buf.unsafe_get(self.head)
   set_null(self.buf, self.head)
   let cap = self.buf.length()
   self.head = wrap_index(self.head, 1, cap)
@@ -853,7 +852,7 @@ pub fn[A] Deque::pop_front(self : Deque[A]) -> A? {
 pub fn[A] Deque::pop_back(self : Deque[A]) -> A? {
   guard self.len > 0 else { return None }
   let tail_idx = self.tail_index()
-  let value = unsafe_buffer_get(self.buf, tail_idx)
+  let value = self.buf.unsafe_get(tail_idx)
   set_null(self.buf, tail_idx)
   self.len -= 1
   Some(value)
@@ -877,7 +876,7 @@ pub fn[A] Deque::at(self : Deque[A], index : Int) -> A {
     index_out_of_bounds(self.len, index)
   }
   let physical_index = wrap_index(self.head, index, self.buf.length())
-  unsafe_buffer_get(self.buf, physical_index)
+  self.buf.unsafe_get(physical_index)
 }
 
 ///|
@@ -899,7 +898,7 @@ pub fn[A] Deque::set(self : Deque[A], index : Int, value : A) -> Unit {
     index_out_of_bounds(self.len, index)
   }
   let physical_index = wrap_index(self.head, index, self.buf.length())
-  unsafe_buffer_set(self.buf, physical_index, value)
+  self.buf.unsafe_set(physical_index, value)
 }
 
 ///|
@@ -2368,7 +2367,7 @@ pub fn[A] Deque::binary_search_by(
 pub fn[A] Deque::get(self : Deque[A], index : Int) -> A? {
   if index >= 0 && index < self.len {
     let physical_index = wrap_index(self.head, index, self.buf.length())
-    Some(unsafe_buffer_get(self.buf, physical_index))
+    Some(self.buf.unsafe_get(physical_index))
   } else {
     None
   }
@@ -2490,9 +2489,9 @@ pub fn[A] Deque::rev_in_place(self : Deque[A]) -> Unit {
   guard self.len > 0 else { return }
   let cap = self.buf.length()
   for _ in 0..<(self.len / 2); left = self.head, right = self.tail_index() {
-    let temp = unsafe_buffer_get(self.buf, left)
-    unsafe_buffer_set(self.buf, left, unsafe_buffer_get(self.buf, right))
-    unsafe_buffer_set(self.buf, right, temp)
+    let temp = self.buf.unsafe_get(left)
+    self.buf.unsafe_set(left, self.buf.unsafe_get(right))
+    self.buf.unsafe_set(right, temp)
     let left = wrap_index(left, 1, cap)
     let right = decrement_index(right, cap)
     continue left, right
@@ -2534,7 +2533,7 @@ pub fn[A] Deque::rev(self : Deque[A]) -> Deque[A] {
   // Copy elements in reverse order
   for i in 0..<len {
     let src_idx = wrap_index(self.head, len - i - 1, self.buf.length())
-    unsafe_buffer_set(new_buf, i, unsafe_buffer_get(self.buf, src_idx))
+    new_buf.unsafe_set(i, self.buf.unsafe_get(src_idx))
   }
   // Create new deque with reversed elements
   { buf: new_buf, len, head: 0 }
-- 
2.51.0

🤖 Generated with Claude Code

[peter-jerry-ye]

The CI failed because the mbtp file is wrongly handled during test, during which it was not needed, creating duplicated symbols. moonbitlang/moon#2000 fixes this