Linear iterator protocol (LiquidJava ``Iterator`` / hasNext-before-next).
Phases (``it_phase``):
0 — must call ``has_next`` before ``next``
1 — ``has_next`` returned true; ``next`` is legal
2 — exhausted (``has_next`` returned false); only ``discard`` remains
``it_remaining`` counts unread elements. Construct with ``from_array``.
def from_array (1 arr : (Array a)) : {it : (Iterator a) | it_phase it = 0 && it_remaining it = Array.size arr}
has_next
Probe whether more elements remain (phase 0 only).
If remaining > 0, recovers phase 1; otherwise phase 2.
def has_next (1 it : (Iterator a) | it_phase it = 0) : {
p : (IteratorProbe a) | probe_remaining p = it_remaining it
&&
(it_remaining it > 0 && probe_has_next p = true || it_remaining it = 0 && probe_has_next p = false)
}
has_next_flag
def has_next_flag (borrow p : (IteratorProbe a)) : {b : Bool | b = probe_has_next p}
ready_iterator
Recover iterator after a true probe → phase 1, same remaining.
def ready_iterator (1 p : (IteratorProbe a) | probe_has_next p = true) : {it : (Iterator a) | it_phase it = 1 && it_remaining it = probe_remaining p && it_remaining it > 0}
exhausted_iterator
Recover iterator after a false probe → phase 2, remaining 0.
def exhausted_iterator (1 p : (IteratorProbe a) | probe_has_next p = false) : {it : (Iterator a) | it_phase it = 2 && it_remaining it = 0 && probe_remaining p = 0}
next
Take the next element (phase 1 only); returns to phase 0 with remaining - 1.
def next (1 it : (Iterator a) | it_phase it = 1 && it_remaining it > 0) : {s : (IteratorStep a) | step_remaining s = it_remaining it - 1}
next_value
def next_value (_inst2843 : (Copy a))(borrow s : (IteratorStep a)) : a
next_iterator
def next_iterator (1 s : (IteratorStep a)) : {it : (Iterator a) | it_phase it = 0 && it_remaining it = step_remaining s}
discard
Drop an exhausted iterator (phase 2).
def discard (1 it : (Iterator a) | it_phase it = 2) : Unit
with_next
Move both the element and successor in one consumption.
def with_next (_inst2844 : (Copy a))(1 token : (IteratorStep a))(1 consume : (value : a) → (1 it : (Iterator a) | it_phase it = 0 && it_remaining it = step_remaining token) → b) : b
with_next_owned
Transfer linear elements instead of copying observations.
def with_next_owned (1 token : (IteratorStep a))(1 consume : (1 value : a) → (1 it : (Iterator a) | it_phase it = 0 && it_remaining it = step_remaining token) → b) : b
Uninterpreted
Functions declared as def f ... = uninterpreted: only their signature is known to the verifier; they have no body.