pub fn trip_window(p: &SpatialProgram, trip: TripId) -> RangeInclusive<usize>Expand description
★ THE TRIP WINDOW — A FEW COUNTS PROVE EVERY COUNT. A loop run to a trip unrolls to a different graph at each
count, and a decode fold at a long context admits thousands of them. The certificate proves the counts
lo ..= min(hi, max(lo, s + 1)), where s bounds how far, in rounds of the trip’s loops, one engine can run ahead
of another it trades pages with — and that proves them all, by the shape the IR holds a trip loop to (a program
input for its count, no semaphore or multicast in its body, no trip loop in another, every buffer it touches
balanced per round — validate_trips and the per-round counting check):
• per-round balance means advancing EVERY engine of a coupled set by one round leaves every buffer’s occupancy
where it was;
• so a stall with every engine of a set strictly inside its rounds cannot be the run’s final state — the same
stall one round earlier is a smaller final state, and a marked graph has one;
• a stall with an engine still at the start of its rounds has every engine of its set within s rounds of
the start, and is the same stall at every count past s + 1: proved at s + 1, it is refused there;
• a stall with an engine past its rounds has every engine within s rounds of the end, and the same stall one
round shorter is a stall of the next count down — down to s + 1, which is proved.
s is the most any path of per-round page traffic lets one engine lead another: over each set of engines that
trade pages inside the trip’s loops, the sum of each such buffer’s depth, the pages it moves outside them, and one.