Function pointer_publish_allowed 

pub fn pointer_publish_allowed(
    current: &PointerState,
    candidate_rank: u64,
) -> bool

THE monotonic pointer guard: may candidate_rank be published over the observed current pointer?

true for an open slot, a corrupt pointer, or a candidate at or above the existing cursor; false exactly when the existing pointer is parseable and STRICTLY newer — the refusal that makes a slow exporter’s stale publish a no-op instead of a regression.

Soundness of deciding on a read (before the conditional put): every writer uses this guard with a compare-and-swap, so the pointer’s rank is monotone non-decreasing — once “strictly newer” is observed, it can never become false, so refusal needs no CAS. Machine-checked as published cursor never regresses in tests/model.rs.