1515///|
1616fn [T ] set_null(buffer : UninitializedArray [T ], index : Int ) = " %fixedarray.set_null "
1717
18+ ///|
19+ /// The deque representation invariant guarantees these indices are in bounds.
20+ /// Keep these private so callers cannot bypass bounds checks.
21+ #inline
22+ fn [T ] unsafe_buffer_get(buffer : UninitializedArray [T ], index : Int ) -> T = " %fixedarray.unsafe_get "
23+
24+ ///|
25+ #inline
26+ fn [T ] unsafe_buffer_set(
27+ buffer : UninitializedArray [T ],
28+ index : Int ,
29+ value : T ,
30+ ) -> Unit = " %fixedarray.unsafe_set "
31+
1832///|
1933fn [A ] new_deque(capacity : Int ) -> Deque [A ] {
2034 { buf: UninitializedArray ::make(capacity), len: 0, head: 0 }
2135}
2236
37+ ///|
38+ /// Wraps an in-buffer offset without division. Comparing the offset with the
39+ /// contiguous space first also avoids overflowing `head + offset`.
40+ #inline
41+ fn wrap_index(
42+ head : Int ,
43+ offset : Int ,
44+ capacity : Int ,
45+ ) -> Int where {
46+ proof_require: wrap_index_pre(head, offset, capacity),
47+ proof_ensure: result => wrap_index_post(head, offset, capacity, result),
48+ proof_ensure: result => wrap_index_mod_equiv(head, offset, capacity, result),
49+ } {
50+ let contiguous = capacity - head
51+ if offset < contiguous {
52+ proof_assert (head + offset) % capacity == head + offset
53+ head + offset
54+ } else {
55+ proof_assert (head + offset) % capacity == offset - contiguous
56+ offset - contiguous
57+ }
58+ }
59+
60+ ///|
61+ /// Moves an in-buffer index back by one without division.
62+ #inline
63+ fn decrement_index(
64+ index : Int ,
65+ capacity : Int ,
66+ ) -> Int where {
67+ proof_require: decrement_index_pre(index, capacity),
68+ proof_ensure: result => decrement_index_post(index, capacity, result),
69+ proof_ensure: result => decrement_index_mod_equiv(index, capacity, result),
70+ } {
71+ if index == 0 {
72+ proof_assert (index + capacity - 1) % capacity == capacity - 1
73+ capacity - 1
74+ } else {
75+ proof_assert (index + capacity - 1) % capacity == index - 1
76+ index - 1
77+ }
78+ }
79+
2380///|
2481/// Computes the tail index (index of last element) on demand.
2582/// Only valid when len > 0.
2683fn [A ] Deque ::tail_index(self : Deque [A ]) -> Int {
27- (self.head + self.len - 1) % self.buf.length()
84+ wrap_index (self.head, self.len - 1, self.buf.length() )
2885}
2986
3087///|
@@ -286,15 +343,15 @@ pub fn[A] Deque::blit_to(
286343 }
287344 // Copy in reverse order
288345 for i in len>..0 {
289- let dst_idx = (dst.head + dst_offset + i) % dst.buf.length()
290- let src_idx = (self.head + src_offset + i) % self.buf.length()
291- dst.buf[ dst_idx] = self.buf[ src_idx]
346+ let dst_idx = wrap_index (dst.head, dst_offset + i, dst.buf.length() )
347+ let src_idx = wrap_index (self.head, src_offset + i, self.buf.length() )
348+ unsafe_buffer_set( dst.buf, dst_idx, unsafe_buffer_get( self.buf, src_idx))
292349 }
293350 } else {
294351 for i in 0..<len {
295- let dst_idx = (dst.head + dst_offset + i) % dst.buf.length()
296- let src_idx = (self.head + src_offset + i) % self.buf.length()
297- dst.buf[ dst_idx] = self.buf[ src_idx]
352+ let dst_idx = wrap_index (dst.head, dst_offset + i, dst.buf.length() )
353+ let src_idx = wrap_index (self.head, src_offset + i, self.buf.length() )
354+ unsafe_buffer_set( dst.buf, dst_idx, unsafe_buffer_get( self.buf, src_idx))
298355 if dst_offset + i >= dst_len {
299356 dst.len += 1
300357 }
@@ -359,9 +416,13 @@ pub fn[A] Deque::append(self : Deque[A], other : Deque[A]) -> Unit {
359416 let cap = self.buf.length()
360417 // Use captured state to read from other, avoiding aliasing issues
361418 for i in 0..<other_len {
362- let read_idx = (other_head + i) % other_buf_len
363- let write_idx = (self.head + self.len) % cap
364- self.buf[write_idx] = other_buf[read_idx]
419+ let read_idx = wrap_index(other_head, i, other_buf_len)
420+ let write_idx = wrap_index(self.head, self.len, cap)
421+ unsafe_buffer_set(
422+ self.buf,
423+ write_idx,
424+ unsafe_buffer_get(other_buf, read_idx),
425+ )
365426 self.len += 1
366427 }
367428}
@@ -422,22 +483,22 @@ pub fn[A] Deque::insert(self : Deque[A], index : Int, value : A) -> Unit {
422483 let cap = self.buf.length()
423484 if index < self.len / 2 {
424485 // Shift front elements left
425- let new_head = (self.head - 1 + cap) % cap
486+ let new_head = decrement_index (self.head, cap)
426487 for i in 0..<index {
427- let to = (new_head + i) % cap
428- let from = (self.head + i) % cap
429- self.buf[to] = self.buf[ from]
488+ let to = wrap_index (new_head, i, cap)
489+ let from = wrap_index (self.head, i, cap)
490+ unsafe_buffer_set( self.buf, to, unsafe_buffer_get( self.buf, from))
430491 }
431492 self.head = new_head
432493 } else {
433494 // Shift back elements right
434495 for i = self.len; i > index; i = i - 1 {
435- let from = (self.head + i - 1) % cap
436- let to = (self.head + i) % cap
437- self.buf[to] = self.buf[ from]
496+ let from = wrap_index (self.head, i - 1, cap)
497+ let to = wrap_index (self.head, i, cap)
498+ unsafe_buffer_set( self.buf, to, unsafe_buffer_get( self.buf, from))
438499 }
439500 }
440- self.buf[ (self.head + index) % cap] = value
501+ unsafe_buffer_set( self.buf, wrap_index (self.head, index, cap), value)
441502 self.len += 1
442503}
443504
@@ -498,21 +559,21 @@ pub fn[A] Deque::remove(self : Deque[A], index : Int) -> A {
498559 let cap = self.buf.length()
499560 if index < self.len / 2 {
500561 // Shift front elements right
501- let new_head = (self.head + 1) % cap
562+ let new_head = wrap_index (self.head, 1, cap)
502563 for i in index>..0 {
503- let to = (self.head + i + 1) % cap
504- let from = (self.head + i) % cap
505- self.buf[to] = self.buf[ from]
564+ let to = wrap_index (self.head, i + 1, cap)
565+ let from = wrap_index (self.head, i, cap)
566+ unsafe_buffer_set( self.buf, to, unsafe_buffer_get( self.buf, from))
506567 }
507568 set_null(self.buf, self.head)
508569 self.head = new_head
509570 } else {
510571 // Shift back elements left
511- let tail_idx = (self.head + self.len - 1) % cap
572+ let tail_idx = wrap_index (self.head, self.len - 1, cap)
512573 for i in (index + 1)..<self.len {
513- let to = (self.head + i - 1) % cap
514- let from = (self.head + i) % cap
515- self.buf[to] = self.buf[ from]
574+ let to = wrap_index (self.head, i - 1, cap)
575+ let from = wrap_index (self.head, i, cap)
576+ unsafe_buffer_set( self.buf, to, unsafe_buffer_get( self.buf, from))
516577 }
517578 set_null(self.buf, tail_idx)
518579 }
@@ -596,7 +657,7 @@ pub fn[A] Deque::front(self : Deque[A]) -> A? {
596657 if self.len == 0 {
597658 None
598659 } else {
599- Some (self.buf[ self.head] )
660+ Some (unsafe_buffer_get( self.buf, self.head) )
600661 }
601662}
602663
@@ -614,7 +675,7 @@ pub fn[A] Deque::back(self : Deque[A]) -> A? {
614675 if self.len == 0 {
615676 None
616677 } else {
617- Some (self.buf[ self.tail_index()] )
678+ Some (unsafe_buffer_get( self.buf, self.tail_index()) )
618679 }
619680}
620681
@@ -636,8 +697,8 @@ pub fn[A] Deque::push_front(self : Deque[A], value : A) -> Unit {
636697 self.realloc()
637698 }
638699 let cap = self.buf.length()
639- self.head = (self.head - 1 + cap) % cap
640- self.buf[ self.head] = value
700+ self.head = decrement_index (self.head, cap)
701+ unsafe_buffer_set( self.buf, self.head, value)
641702 self.len += 1
642703}
643704
@@ -659,8 +720,8 @@ pub fn[A] Deque::push_back(self : Deque[A], value : A) -> Unit {
659720 self.realloc()
660721 }
661722 let cap = self.buf.length()
662- let write_idx = (self.head + self.len) % cap
663- self.buf[ write_idx] = value
723+ let write_idx = wrap_index (self.head, self.len, cap)
724+ unsafe_buffer_set( self.buf, write_idx, value)
664725 self.len += 1
665726}
666727
@@ -682,7 +743,7 @@ pub fn[A] Deque::unsafe_pop_front(self : Deque[A]) -> Unit {
682743 guard self.len > 0 else { abort("The deque is empty!") }
683744 set_null(self.buf, self.head)
684745 let cap = self.buf.length()
685- self.head = (self.head + 1) % cap
746+ self.head = wrap_index (self.head, 1, cap)
686747 self.len -= 1
687748}
688749
@@ -771,10 +832,10 @@ pub fn[A] Deque::unsafe_pop_back(self : Deque[A]) -> Unit {
771832/// ```
772833pub fn[A ] Deque ::pop_front(self : Deque [A ]) -> A? {
773834 guard self.len > 0 else { return None }
774- let value = self.buf[ self.head]
835+ let value = unsafe_buffer_get( self.buf, self.head)
775836 set_null(self.buf, self.head)
776837 let cap = self.buf.length()
777- self.head = (self.head + 1) % cap
838+ self.head = wrap_index (self.head, 1, cap)
778839 self.len -= 1
779840 Some (value)
780841}
@@ -792,7 +853,7 @@ pub fn[A] Deque::pop_front(self : Deque[A]) -> A? {
792853pub fn[A ] Deque ::pop_back(self : Deque [A ]) -> A? {
793854 guard self.len > 0 else { return None }
794855 let tail_idx = self.tail_index()
795- let value = self.buf[ tail_idx]
856+ let value = unsafe_buffer_get( self.buf, tail_idx)
796857 set_null(self.buf, tail_idx)
797858 self.len -= 1
798859 Some (value)
@@ -815,11 +876,8 @@ pub fn[A] Deque::at(self : Deque[A], index : Int) -> A {
815876 if index < 0 || index >= self.len {
816877 index_out_of_bounds(self.len, index)
817878 }
818- if self.head + index < self.buf.length() {
819- self.buf[self.head + index]
820- } else {
821- self.buf[self.head + index - self.buf.length()]
822- }
879+ let physical_index = wrap_index(self.head, index, self.buf.length())
880+ unsafe_buffer_get(self.buf, physical_index)
823881}
824882
825883///|
@@ -840,11 +898,8 @@ pub fn[A] Deque::set(self : Deque[A], index : Int, value : A) -> Unit {
840898 if index < 0 || index >= self.len {
841899 index_out_of_bounds(self.len, index)
842900 }
843- if self.head + index < self.buf.length() {
844- self.buf[self.head + index] = value
845- } else {
846- self.buf[self.head + index - self.buf.length()] = value
847- }
901+ let physical_index = wrap_index(self.head, index, self.buf.length())
902+ unsafe_buffer_set(self.buf, physical_index, value)
848903}
849904
850905///|
@@ -2312,8 +2367,8 @@ pub fn[A] Deque::binary_search_by(
23122367/// Safe element access with bounds checking
23132368pub fn[A ] Deque ::get(self : Deque [A ], index : Int ) -> A? {
23142369 if index >= 0 && index < self.len {
2315- let physical_index = (self.head + index) % self.buf.length()
2316- Some (self.buf[ physical_index] )
2370+ let physical_index = wrap_index (self.head, index, self.buf.length() )
2371+ Some (unsafe_buffer_get( self.buf, physical_index) )
23172372 } else {
23182373 None
23192374 }
@@ -2435,10 +2490,12 @@ pub fn[A] Deque::rev_in_place(self : Deque[A]) -> Unit {
24352490 guard self.len > 0 else { return }
24362491 let cap = self.buf.length()
24372492 for _ in 0..<(self.len / 2); left = self.head, right = self.tail_index() {
2438- let temp = self.buf[left]
2439- self.buf[left] = self.buf[right]
2440- self.buf[right] = temp
2441- continue (left + 1) % cap, (right - 1 + cap) % cap
2493+ let temp = unsafe_buffer_get(self.buf, left)
2494+ unsafe_buffer_set(self.buf, left, unsafe_buffer_get(self.buf, right))
2495+ unsafe_buffer_set(self.buf, right, temp)
2496+ let left = wrap_index(left, 1, cap)
2497+ let right = decrement_index(right, cap)
2498+ continue left, right
24422499 }
24432500}
24442501
@@ -2476,8 +2533,8 @@ pub fn[A] Deque::rev(self : Deque[A]) -> Deque[A] {
24762533 let new_buf = UninitializedArray ::make(len)
24772534 // Copy elements in reverse order
24782535 for i in 0..<len {
2479- let src_idx = (self.head + len - i - 1) % self.buf.length()
2480- new_buf[i] = self.buf[ src_idx]
2536+ let src_idx = wrap_index (self.head, len - i - 1, self.buf.length() )
2537+ unsafe_buffer_set( new_buf, i, unsafe_buffer_get( self.buf, src_idx))
24812538 }
24822539 // Create new deque with reversed elements
24832540 { buf: new_buf, len, head: 0 }
0 commit comments