Function normalize_checked 

pub fn normalize_checked(
    ctx: &Context,
    term: &Term,
) -> Result<Term, (Term, Unreduced)>

Normalize a term, reporting honestly when the reduction did not finish.

Err((partial, why)) carries the term the reducer had reached, so a caller that wants best-effort behaviour can still have it — but it has to ask for it, which is the whole point.

Divergence is detected with Brent’s cycle-finding: one saved term (the “tortoise”), re-saved at powers of two, compared against each new term. It needs O(1) memory, finds a cycle of any period within about twice the cycle length, and — unlike a step budget — answers the δ-cycle case CORRECTLY rather than merely late.