Struct Bisection 

pub struct Bisection {
    pub domain_size: u64,
    pub budget: Budget,
    pub lo: u64,
    pub hi: u64,
    pub threshold: u64,
}

Bounded monotone-boundary bisection carrier.

Fields

domain_size: u64

Size of the ordered domain.

budget: Budget

Budget that counts admitted probes.

lo: u64

Inclusive lower interval endpoint.

hi: u64

Inclusive upper interval endpoint.

threshold: u64

Monotone boundary retained inside the interval.

Implementations

impl Bisection

pub fn new( lo: u64, hi: u64, threshold: u64, domain_size: u64, max_probes: u64, ) -> Bisection

Init (TLA+ Init): a candidate interval straddling the threshold, no probes taken yet.

pub fn converged(&self) -> bool

Whether the interval has been narrowed to a point (TLA+ Converged guard).

pub fn probe(&mut self)

Probe the midpoint and narrow the interval – one atomic step (TLA+ ProbeLeft / ProbeRight). Maintains MonotonicityPreservation, at least halves the interval (the Halving property), and strictly decreases its width (the loop-termination measure).

pub fn bisect(&mut self)

Drive probes to convergence (the TLA+ EventualConvergence under fairness). The decreases hi - lo is the loop-termination witness: the loop halts, and on exit the interval is a point (hi - lo < 2) that still straddles the threshold.