Runtime.ArenaCertificate

A repeat of `count` iterations whose iteration k's events are `events k`, run from `state` without walking every iteration. Iterations 0 and 1 run; then iteration 2's events must be iteration 1's with every generation shifted by what iteration 1 advanced the last awaited generation (shift), and iteration 1 must leave the pending writes it found. Iteration k + 1 then starts from iteration k's state shifted by `shift`, with the same pending writes, and runs events shifted by `shift` (the steps are affine in k: their difference from k to k + 1 is fixed): every comparison the walk makes (a generation against the last, a range against the pending ones) is the same as iteration 1's, so it finds what iteration 1 found -- no hazard -- and ends shifted again. So the repeat ends `count - 2` shifts past iteration 1. A body whose next iteration is not so shifted is a hazard at its index.

304def arenaScheduleRepeat =
305  (lambda unrestricted count : Nat .
306    (lambda unrestricted events : (pi unrestricted iteration : Nat . (family ArenaEvents)) .
307      (lambda unrestricted state : (family ArenaScheduleState) .
308        (let unrestricted one = (arenaScheduleRun state (events 0)) in
309        (let unrestricted two = (arenaScheduleRun one (events 1)) in
310        (let unrestricted shift = (naturalSaturatingSubtract (arenaStateLastOf two) (arenaStateLastOf one)) in
311        (let unrestricted periodic =
312            (naturalAnd (arenaEventsShifted shift (events 1) (events 2))
313              (arenaRangesEqual (arenaStatePendingOf one) (arenaStatePendingOf two))) in
314        (let unrestricted rest = (naturalSaturatingSubtract count 2) in
315        (let unrestricted hazard = (arenaStateHazardOf two) in
316        (let unrestricted many =
317            (constructor ArenaScheduleState ArenaScheduleStateValue
318              (naturalAdd (arenaStateIndexOf two) (naturalMultiply rest (arenaEventsLength (events 1))))
319              (naturalAdd (arenaStateLastOf two) (naturalMultiply rest shift))
320              (arenaStatePendingOf two)
321              (naturalSelect hazard hazard (naturalSelect periodic 0 (arenaStateIndexOf two)))) in
322          (arenaSelectState (naturalIsZero count) state
323            (arenaSelectState (naturalEqual count 1) one
324              (arenaSelectState (naturalEqual count 2) two many)))))))))))))