~/bend-docscommunity

proofs/containers/dlist_iterator/proof.bend checks

raw source on the hub · import bend-collections-laws-containers@1.0.0.0/proofs/containers/dlist_iterator/proof.bend as Proof

6 imports
import Base
import ../../../src/containers/dlist_iterator.bend as I
import ../../../src/containers/doubly_linked_list.bend as D
import ../../../src/containers/types/doubly_linked_list.bend as E
import ../../../src/containers/internal/dlist_storage.bend as R
import ../../../spec/containers/dlist_iterator.bend as S

Definitions

def finish_owns source · line 10 · raw

@s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<U32> -> @n:U32 -> @last:U32 -> @f:Bool -> @i:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.finish(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.IT{s, n, last, f, i}) == s : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<U32>}

Component laws over the actual cursor implementation. These are not a full sequence-refinement proof for all edits/traces or the underlying arena.

def next_exhausted source · line 13 · raw

@s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<U32> -> @+last:U32 -> @+f:Bool -> @+i:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.next(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.IT{s, 0, last, f, i}) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.IT{s, 0, last, f, i}, Fail{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.Exhausted{}}) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.Iterator<U32>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.Error, U32>)}

def set_requires_current source · line 18 · raw

@s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<U32> -> @+n:U32 -> @+f:Bool -> @+i:Nat -> @x:U32 -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.set(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.IT{s, n, 0, f, i}, x) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.IT{s, n, 0, f, i}, Fail{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.NoCurrent{}}) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.Iterator<U32>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.Error, Unit>)}

def remove_requires_current source · line 21 · raw

@s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<U32> -> @+n:U32 -> @+f:Bool -> @+i:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.remove(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.IT{s, n, 0, f, i}) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.IT{s, n, 0, f, i}, Fail{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.NoCurrent{}}) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.Iterator<U32>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.Error, Unit>)}

def has_next_state source · line 26 · raw

@s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<U32> -> @+n:U32 -> @+last:U32 -> @+f:Bool -> @+i:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.has_next(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.IT{s, n, last, f, i}) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.IT{s, n, last, f, i}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.present(n)) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.Iterator<U32>, Bool)}

def has_previous_state source · line 29 · raw

@s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<U32> -> @+n:U32 -> @+last:U32 -> @+f:Bool -> @+i:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.has_previous(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.IT{s, n, last, f, i}) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.IT{s, n, last, f, i}, Nat.is_lt(0n, i)) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.Iterator<U32>, Bool)}

def added_clears_current source · line 32 · raw

@s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<U32> -> @+n:U32 -> @last:U32 -> @+f:Bool -> @+i:Nat -> @h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.added(U32, n, last, f, i, (s, Done{h})) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.IT{s, n, 0, f, 1n+i}, Done{Unit{}}) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.Iterator<U32>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.Error, Unit>)}

def removed_forward source · line 35 · raw

@s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<U32> -> @n:U32 -> @last:U32 -> @+i:Nat -> @+after:U32 -> @x:U32 -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.removed(U32, n, last, True{}, i, after, (s, Done{x})) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.IT{s, after, 0, True{}, Nat.sub(i, 1n)}, Done{Unit{}}) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.Iterator<U32>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.Error, Unit>)}

def removed_backward source · line 38 · raw

@s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<U32> -> @n:U32 -> @last:U32 -> @+i:Nat -> @+after:U32 -> @x:U32 -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.removed(U32, n, last, False{}, i, after, (s, Done{x})) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.IT{s, after, 0, False{}, i}, Done{Unit{}}) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.Iterator<U32>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.Error, Unit>)}

def finish_owns_string source · line 41 · raw

@s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<String> -> @n:U32 -> @last:U32 -> @f:Bool -> @i:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.finish(String, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.IT{s, n, last, f, i}) == s : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<String>}

def next_exhausted_string source · line 44 · raw

@s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<String> -> @+last:U32 -> @+f:Bool -> @+i:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.next(String, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.IT{s, 0, last, f, i}) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.IT{s, 0, last, f, i}, Fail{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.Exhausted{}}) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.Iterator<String>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.Error, String>)}

def set_requires_current_string source · line 49 · raw

@s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<String> -> @+n:U32 -> @+f:Bool -> @+i:Nat -> @x:String -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.set(String, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.IT{s, n, 0, f, i}, x) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.IT{s, n, 0, f, i}, Fail{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.NoCurrent{}}) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.Iterator<String>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.Error, Unit>)}

def remove_requires_current_string source · line 52 · raw

@s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<String> -> @+n:U32 -> @+f:Bool -> @+i:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.remove(String, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.IT{s, n, 0, f, i}) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.IT{s, n, 0, f, i}, Fail{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.NoCurrent{}}) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.Iterator<String>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.Error, Unit>)}

def has_next_state_string source · line 57 · raw

@s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<String> -> @+n:U32 -> @+last:U32 -> @+f:Bool -> @+i:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.has_next(String, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.IT{s, n, last, f, i}) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.IT{s, n, last, f, i}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.present(n)) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.Iterator<String>, Bool)}

def has_previous_state_string source · line 60 · raw

@s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<String> -> @+n:U32 -> @+last:U32 -> @+f:Bool -> @+i:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.has_previous(String, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.IT{s, n, last, f, i}) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.IT{s, n, last, f, i}, Nat.is_lt(0n, i)) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.Iterator<String>, Bool)}

def added_clears_current_string source · line 63 · raw

@s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<String> -> @+n:U32 -> @last:U32 -> @+f:Bool -> @+i:Nat -> @h:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.added(String, n, last, f, i, (s, Done{h})) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.IT{s, n, 0, f, 1n+i}, Done{Unit{}}) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.Iterator<String>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.Error, Unit>)}

def removed_forward_string source · line 66 · raw

@s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<String> -> @n:U32 -> @last:U32 -> @+i:Nat -> @+after:U32 -> @x:String -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.removed(String, n, last, True{}, i, after, (s, Done{x})) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.IT{s, after, 0, True{}, Nat.sub(i, 1n)}, Done{Unit{}}) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.Iterator<String>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.Error, Unit>)}

def removed_backward_string source · line 69 · raw

@s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<String> -> @n:U32 -> @last:U32 -> @+i:Nat -> @+after:U32 -> @x:String -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.removed(String, n, last, False{}, i, after, (s, Done{x})) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.IT{s, after, 0, False{}, i}, Done{Unit{}}) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.Iterator<String>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.Error, Unit>)}

def end_gap_is_append source · line 75 · raw

@s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<U32> -> @x:U32 -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.cursor_insert_gap(U32, s, 0, x) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.insert_gap_result(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.push_back(U32, s, x)) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<U32>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle>)}

The end-gap insertion is exactly the public DLL append, including capacity growth, free-slot reuse, and generation bookkeeping. This is an algorithm bridge, not merely an equality with a model that invokes the iterator.

def end_gap_is_append_string source · line 80 · raw

@s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<String> -> @x:String -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.cursor_insert_gap(String, s, 0, x) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.insert_gap_result(String, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.push_back(String, s, x)) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<String>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Error, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/doubly_linked_list.Handle>)}

def move_forward_cursor source · line 85 · raw

@n:U32 -> @last:U32 -> @f:Bool -> @+i:Nat -> @+h:U32 -> @+after:U32 -> @+x:U32 -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.move_meta(U32, n, last, f, i, h, after, True{}, Done{x}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.M{after, h, True{}, 1n+i, Done{x}} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.Move<U32>}

def move_backward_cursor source · line 88 · raw

@n:U32 -> @last:U32 -> @f:Bool -> @+i:Nat -> @+h:U32 -> @+x:U32 -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.move_meta(U32, n, last, f, i, h, h, False{}, Done{x}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.M{h, h, False{}, Nat.sub(i, 1n), Done{x}} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.Move<U32>}

def failed_move_preserves_cursor source · line 91 · raw

@+n:U32 -> @+last:U32 -> @+f:Bool -> @+i:Nat -> @h:U32 -> @after:U32 -> @forward:Bool -> @+e:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.Error -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.move_meta(U32, n, last, f, i, h, after, forward, Fail{e}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.M{n, last, f, i, Fail{e}} : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.Move<U32>}

def has_element source · line 96 · raw

@s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<U32> -> @+n:U32 -> @+last:U32 -> @+f:Bool -> @+i:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.has_next(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.IT{s, n, last, f, i}) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.IT{s, n, last, f, i}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.present(n)) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.Iterator<U32>, Bool)}

def next_at_end source · line 99 · raw

@s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<U32> -> @+last:U32 -> @+f:Bool -> @+i:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.next(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.IT{s, 0, last, f, i}) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.IT{s, 0, last, f, i}, Fail{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.Exhausted{}}) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.Iterator<U32>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.Error, U32>)}

def replace_pre source · line 102 · raw

@s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<U32> -> @+n:U32 -> @+f:Bool -> @+i:Nat -> @x:U32 -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.set(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.IT{s, n, 0, f, i}, x) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.IT{s, n, 0, f, i}, Fail{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.NoCurrent{}}) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.Iterator<U32>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.Error, Unit>)}

def delete_pre source · line 105 · raw

@s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/doubly_linked_list.DList<U32> -> @+n:U32 -> @+f:Bool -> @+i:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.remove(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.IT{s, n, 0, f, i}) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.IT{s, n, 0, f, i}, Fail{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.NoCurrent{}}) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.Iterator<U32>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dlist_iterator.Error, Unit>)}