module SM86.Scoreboard

import Accelerator.SM86.Control
import Accelerator.SM86.Instruction
import Accelerator.SM86.Operands
import Accelerator.SM86.Types
import Data.Bytes
import Std.List
import Std.Natural

-- The scoreboard pass: the machine-level check the functional model cannot
-- make.  SM86.MachineModel gives every instruction its result at once; the
-- silicon does not.  A variable-latency instruction (S2R, a global load,
-- shuffles, shared-memory and tensor-core forms) delivers its destination
-- later, and the only thing that orders a consumer after it is the control
-- word: the producer names a write barrier (SB0..SB5) and the consumer's
-- wait mask names that barrier.  A consumer without the wait reads whatever
-- the register held before -- on the RTX 3090 (2026-09-22) the first linear
-- step realization read zeros for W, x and t and wrote a record of zeros,
-- while the functional model had accepted it.
--
-- This pass walks the program in order as one straight-line issue stream
-- (predication does not change issue), keeping the registers whose value is
-- still in flight and the barrier each waits on.  An instruction first
-- retires every pending register whose barrier is in its wait mask, then any
-- register it reads or writes that is still pending is a hazard, then its
-- own variable-latency destinations become pending on its write barrier -- or
-- on a barrier no mask can name, when it declares none, so every later use
-- is a hazard.  The result is 0 for a clean program, else the ordinal (from
-- 1) of the first hazardous instruction.  Fixed-latency forms are ordered
-- by their stall counts, which this pass does not model.

family ScoreboardPending : Type 0
constructor ScoreboardPendingEnd
constructor ScoreboardPendingNext
field unrestricted scoreboardPendingRegister : Nat
field unrestricted scoreboardPendingBarrier : Nat
recursive unrestricted scoreboardPendingTail
end-family
-- Pending as seven byte masks, not a scanned list.  The old pending list
-- grew with every unretired variable-latency write -- barriers a step never
-- waits on, and barrier 8 (scoreboardNever) which no mask can name -- and
-- every instruction scanned the whole accumulation per register it touched:
-- quadratic in the program length (268 s for the wait-stripped 1,259
-- instruction mutant, 8.4 s clean).  One mask per barrier (1..6 and 8)
-- holds a 1 at each pending register, so membership is seven indexed reads,
-- issue is one indexed write per written register, and retire swaps in the
-- shared empty for every barrier the wait mask names: bounded work per
-- instruction, near-linear overall.
-- Equivalence (exact, on every program): the old list's multiplicity is
-- unobservable -- every query is membership by register and every removal
-- is a bulk delete by barrier, and the masks track exactly the set of live
-- (register, barrier) pairs through both.  RZ (255) is never inserted
-- (sm86RegisterRun names nothing from it) and stays guarded at lookup.
family ScoreboardMasks : Type 0
constructor ScoreboardMasksValue
field unrestricted scoreboardMasksBarrier1 : Bytes
field unrestricted scoreboardMasksBarrier2 : Bytes
field unrestricted scoreboardMasksBarrier3 : Bytes
field unrestricted scoreboardMasksBarrier4 : Bytes
field unrestricted scoreboardMasksBarrier5 : Bytes
field unrestricted scoreboardMasksBarrier6 : Bytes
field unrestricted scoreboardMasksNever : Bytes
end-family

-- The result of one instruction: the hazard flag and the pending set after issue.
family ScoreboardStep : Type 0
constructor ScoreboardStepValue
field unrestricted scoreboardStepHazard : Nat
field unrestricted scoreboardStepPending : (family ScoreboardMasks)
field unrestricted scoreboardStepReadPending : (family ScoreboardMasks)
end-family

def scoreboardNever : Nat = 8


-- What an instruction reads and writes is Accelerator.SM86.Operands'
-- one-elimination summary (sm86OpSummaryOfBody, shared with the register
-- demand: pairs for 64-bit operands, quads for the tensor core's A, C and
-- D -- until 2026-09-23 this pass listed those as pairs and could miss a
-- hazard on the upper half); the latency class rides in the same summary.


def sbControlOfBody = sm86BodyControlOf


-- the write barrier as 1..6 (SB0..SB5), 0 for none
def scoreboardWriteBarrierOf =
  (lambda unrestricted control : (family SM86Control) .
    (eliminate SM86Control
      (lambda unrestricted current : (family SM86Control) . Nat)
      control
      (branch SM86ControlValue stall yield write read wait reuse .
        (eliminate SM86Barrier
          (lambda unrestricted current : (family SM86Barrier) . Nat)
          write
          (branch SM86Barrier0 . 1)
          (branch SM86Barrier1 . 2)
          (branch SM86Barrier2 . 3)
          (branch SM86Barrier3 . 4)
          (branch SM86Barrier4 . 5)
          (branch SM86Barrier5 . 6)
          (branch SM86Barrier6 . 7)
        (branch SM86BarrierNone . 0)))))

-- Read barriers retire late source reads. A write barrier retires the
-- destination but does not protect an LDG address on Ampere: this was
-- isolated on the RTX 3090 in c28712e8.
def scoreboardReadBarrierOf =
  (lambda unrestricted control : (family SM86Control) .
    (eliminate SM86Control
      (lambda unrestricted current : (family SM86Control) . Nat) control
      (branch SM86ControlValue stall yield write read wait reuse .
        (eliminate SM86Barrier
          (lambda unrestricted current : (family SM86Barrier) . Nat) read
          (branch SM86Barrier0 . 1) (branch SM86Barrier1 . 2)
          (branch SM86Barrier2 . 3) (branch SM86Barrier3 . 4)
          (branch SM86Barrier4 . 5) (branch SM86Barrier5 . 6)
          (branch SM86Barrier6 . 7) (branch SM86BarrierNone . 0)))))

def scoreboardWaitMaskOf =
  (lambda unrestricted control : (family SM86Control) .
    (eliminate SM86Control
      (lambda unrestricted current : (family SM86Control) . Nat)
      control
      (branch SM86ControlValue stall yield write read wait reuse . (byte-to-nat wait))))

-- bit (barrier - 1) of the mask, for barrier 1..6; never for 0 or 8
def scoreboardMaskNames =
  (lambda unrestricted mask : Nat .
    (lambda unrestricted barrier : Nat .
      (nat-eliminate
        (lambda unrestricted current : Nat . Nat)
        zero
        (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : Nat .
          (naturalAnd (naturalLess predecessor 7)
            (nat-modulo (nat-divide mask (naturalPowerOfTwo predecessor)) 2))))
        barrier)))

-- (an empty wait mask retires nothing: the pending masks are kept as they
-- are, not walked and rebuilt -- most instructions wait on no barrier)
def sbBytesEmpty : Bytes = (dataBytesRepeatByte (byte 0) 256)

def sbMasksEmpty : (family ScoreboardMasks) =
  (constructor ScoreboardMasks ScoreboardMasksValue
    sbBytesEmpty sbBytesEmpty sbBytesEmpty sbBytesEmpty sbBytesEmpty sbBytesEmpty sbBytesEmpty)

-- 1 when the register is pending on any barrier: seven indexed reads, one
-- machine operation each, no walk
def sbMasksLookup =
  (lambda unrestricted pending : (family ScoreboardMasks) .
    (lambda unrestricted register : Nat .
      (eliminate ScoreboardMasks
        (lambda unrestricted current : (family ScoreboardMasks) . Nat)
        pending
        (branch ScoreboardMasksValue b1 b2 b3 b4 b5 b6 bn .
          (nat-less-than zero
            (nat-add
              (nat-add
                (nat-add (bytes-index-nonzero b1 register) (bytes-index-nonzero b2 register))
                (nat-add (bytes-index-nonzero b3 register) (bytes-index-nonzero b4 register)))
              (nat-add
                (nat-add (bytes-index-nonzero b5 register) (bytes-index-nonzero b6 register))
                (bytes-index-nonzero bn register))))))))

-- RZ is never pending
def sbMasksAnyPending =
  (lambda unrestricted pending : (family ScoreboardMasks) .
    (lambda unrestricted registers : (family StdList Nat) .
      (eliminate StdList
        (lambda unrestricted current : (family StdList Nat) . Nat)
        registers
        (branch StdListEmpty . zero)
        (branch StdListCons register tail induction .
          (nat-eliminate (lambda unrestricted current : Nat . Nat)
            induction
            (lambda unrestricted flagPredecessor : Nat . (lambda unrestricted flagRest : Nat .
              (nat-eliminate (lambda unrestricted current : Nat . Nat)
                induction
                (lambda unrestricted flagPredecessor : Nat . (lambda unrestricted flagRest : Nat . (succ zero)))
                (sbMasksLookup pending register))))
            (nat-add (nat-less-than register 255) (nat-less-than 255 register)))))))

-- one register issued on one barrier: that barrier's mask gains the bit.
-- The case is a 0/1 elimination returning the mask unchanged or written,
-- so only the named mask is ever rebuilt.
def sbMasksIssueOne =
  (lambda unrestricted pending : (family ScoreboardMasks) .
    (lambda unrestricted register : Nat .
      (lambda unrestricted barrier : Nat .
        (eliminate ScoreboardMasks
          (lambda unrestricted current : (family ScoreboardMasks) . (family ScoreboardMasks))
          pending
          (branch ScoreboardMasksValue b1 b2 b3 b4 b5 b6 bn .
            (constructor ScoreboardMasks ScoreboardMasksValue
              (nat-eliminate (lambda unrestricted current : Nat . Bytes) b1 (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : Bytes . (bytes-set-index b1 register))) (naturalEqual barrier 1))
              (nat-eliminate (lambda unrestricted current : Nat . Bytes) b2 (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : Bytes . (bytes-set-index b2 register))) (naturalEqual barrier 2))
              (nat-eliminate (lambda unrestricted current : Nat . Bytes) b3 (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : Bytes . (bytes-set-index b3 register))) (naturalEqual barrier 3))
              (nat-eliminate (lambda unrestricted current : Nat . Bytes) b4 (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : Bytes . (bytes-set-index b4 register))) (naturalEqual barrier 4))
              (nat-eliminate (lambda unrestricted current : Nat . Bytes) b5 (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : Bytes . (bytes-set-index b5 register))) (naturalEqual barrier 5))
              (nat-eliminate (lambda unrestricted current : Nat . Bytes) b6 (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : Bytes . (bytes-set-index b6 register))) (naturalEqual barrier 6))
              (nat-eliminate (lambda unrestricted current : Nat . Bytes) bn (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : Bytes . (bytes-set-index bn register))) (naturalEqual barrier 8))))))))

def sbMasksIssue =
  (lambda unrestricted barrier : Nat .
    (lambda unrestricted registers : (family StdList Nat) .
      (lambda unrestricted pending : (family ScoreboardMasks) .
        (eliminate StdList
          (lambda unrestricted current : (family StdList Nat) . (family ScoreboardMasks))
          registers
          (branch StdListEmpty . pending)
          (branch StdListCons register tail induction .
            (sbMasksIssueOne induction register barrier))))))

-- retire every barrier the wait mask names by swapping in the shared empty;
-- barrier 8 is never named, so the never mask passes through
def sbMasksRetire =
  (lambda unrestricted mask : Nat .
    (lambda unrestricted pending : (family ScoreboardMasks) .
      (nat-eliminate
        (lambda unrestricted current : Nat . (family ScoreboardMasks))
        pending
        (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : (family ScoreboardMasks) .
          (eliminate ScoreboardMasks
            (lambda unrestricted current : (family ScoreboardMasks) . (family ScoreboardMasks))
            pending
            (branch ScoreboardMasksValue b1 b2 b3 b4 b5 b6 bn .
              (constructor ScoreboardMasks ScoreboardMasksValue
                (nat-eliminate (lambda unrestricted current : Nat . Bytes) b1 (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : Bytes . sbBytesEmpty)) (scoreboardMaskNames mask 1))
                (nat-eliminate (lambda unrestricted current : Nat . Bytes) b2 (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : Bytes . sbBytesEmpty)) (scoreboardMaskNames mask 2))
                (nat-eliminate (lambda unrestricted current : Nat . Bytes) b3 (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : Bytes . sbBytesEmpty)) (scoreboardMaskNames mask 3))
                (nat-eliminate (lambda unrestricted current : Nat . Bytes) b4 (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : Bytes . sbBytesEmpty)) (scoreboardMaskNames mask 4))
                (nat-eliminate (lambda unrestricted current : Nat . Bytes) b5 (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : Bytes . sbBytesEmpty)) (scoreboardMaskNames mask 5))
                (nat-eliminate (lambda unrestricted current : Nat . Bytes) b6 (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : Bytes . sbBytesEmpty)) (scoreboardMaskNames mask 6))
                bn)))))
        (naturalNonzero mask))))

def sbRegistersNonempty =
  (lambda unrestricted registers : (family StdList Nat) .
    (eliminate StdList (lambda unrestricted current : (family StdList Nat) . Nat) registers
      (branch StdListEmpty . 0)
      (branch StdListCons register tail induction . 1)))

-- A read barrier is one outstanding token, even when successive stores
-- read different registers. Reusing SB5 on Coppelius's four AdamW stores
-- before waiting it left negative second moments in the first RTX 3090
-- checkpoint (2026-09-27); waiting before each reuse removed them.
def sbReadBarrierOccupied =
  (lambda unrestricted pending : (family ScoreboardMasks) .
    (lambda unrestricted barrier : Nat .
      (eliminate ScoreboardMasks
        (lambda unrestricted current : (family ScoreboardMasks) . Nat) pending
        (branch ScoreboardMasksValue b1 b2 b3 b4 b5 b6 bn .
          (naturalSelect (naturalEqual barrier 1) (naturalIsZero (bytes-equal b1 sbBytesEmpty))
            (naturalSelect (naturalEqual barrier 2) (naturalIsZero (bytes-equal b2 sbBytesEmpty))
              (naturalSelect (naturalEqual barrier 3) (naturalIsZero (bytes-equal b3 sbBytesEmpty))
                (naturalSelect (naturalEqual barrier 4) (naturalIsZero (bytes-equal b4 sbBytesEmpty))
                  (naturalSelect (naturalEqual barrier 5) (naturalIsZero (bytes-equal b5 sbBytesEmpty))
                    (naturalSelect (naturalEqual barrier 6) (naturalIsZero (bytes-equal b6 sbBytesEmpty)) 0))))))))))

def scoreboardStep =
  (lambda unrestricted pending : (family ScoreboardMasks) .
    (lambda unrestricted pendingReads : (family ScoreboardMasks) .
    (lambda unrestricted summary : (family SM86OpSummary) .
      (eliminate SM86OpSummary
        (lambda unrestricted current : (family SM86OpSummary) . (family ScoreboardStep))
        summary
        (branch SM86OpSummaryValue reads writes predicateWrites waitKeys setKeys stall latency variable minimum control .
          (let unrestricted retired = (sbMasksRetire (scoreboardWaitMaskOf control) pending)
          in (let unrestricted readsRetired = (sbMasksRetire (scoreboardWaitMaskOf control) pendingReads)
          in (let unrestricted hazard =
                (naturalOr
                  (naturalOr (sbMasksAnyPending retired reads) (sbMasksAnyPending retired writes))
                  (naturalOr (sbMasksAnyPending readsRetired writes)
                    (naturalAnd (sbRegistersNonempty reads)
                      (sbReadBarrierOccupied readsRetired (scoreboardReadBarrierOf control)))))
          in (let unrestricted declared = (scoreboardWriteBarrierOf control)
          in (let unrestricted declaredRead = (scoreboardReadBarrierOf control)
          in (let unrestricted barrier =
                (nat-eliminate
                  (lambda unrestricted current : Nat . Nat)
                  (nat-eliminate
                    (lambda unrestricted current : Nat . Nat)
                    zero
                    (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : Nat . scoreboardNever))
                    variable)
                  (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : Nat . declared))
                  declared)
          in
            (constructor ScoreboardStep ScoreboardStepValue
              hazard
              (nat-eliminate
                (lambda unrestricted current : Nat . (family ScoreboardMasks))
                retired
                (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : (family ScoreboardMasks) .
                  (sbMasksIssue barrier writes retired)))
                barrier)
              (nat-eliminate
                (lambda unrestricted current : Nat . (family ScoreboardMasks))
                readsRetired
                (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : (family ScoreboardMasks) .
                  (sbMasksIssue
                    (naturalSelect (naturalIsZero declaredRead) scoreboardNever declaredRead)
                    reads readsRetired)))
                (naturalAnd (naturalOr variable (naturalNonzero declaredRead))
                  (sbRegistersNonempty reads)))))))))))))))

def scoreboardBodyOf =
  (lambda unrestricted instruction : (family SM86Instruction) .
    (eliminate SM86Instruction
      (lambda unrestricted current : (family SM86Instruction) . (family SM86InstructionBody))
      instruction
      (branch SM86InstructionValue guard body . body)))

-- 0 when clean, else the ordinal (from 1) of the first hazardous instruction.
def sm86Scoreboard =
  (lambda unrestricted program : (family SM86Program) .
    (app
      (app
        (app
        (eliminate SM86Program
          (lambda unrestricted current : (family SM86Program) .
            (pi unrestricted ordinal : Nat .
              (pi unrestricted pending : (family ScoreboardMasks) .
                (pi unrestricted pendingReads : (family ScoreboardMasks) . Nat))))
          program
          (branch SM86ProgramEnd .
            (lambda unrestricted ordinal : Nat .
              (lambda unrestricted pending : (family ScoreboardMasks) .
                (lambda unrestricted pendingReads : (family ScoreboardMasks) . zero))))
          (branch SM86ProgramNext instruction tail induction .
            (lambda unrestricted ordinal : Nat .
              (lambda unrestricted pending : (family ScoreboardMasks) .
              (lambda unrestricted pendingReads : (family ScoreboardMasks) .
              (eliminate ScoreboardStep
                (lambda unrestricted current : (family ScoreboardStep) . Nat)
                (scoreboardStep pending pendingReads (sm86OpSummaryOfBody (scoreboardBodyOf instruction)))
                (branch ScoreboardStepValue hazard next nextReads .
                  (nat-eliminate
                    (lambda unrestricted current : Nat . Nat)
                    (induction (succ ordinal) next nextReads)
                    (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : Nat . ordinal))
                    hazard))))))))
        1)
      sbMasksEmpty)
      sbMasksEmpty))

-- ---- fixed latency: the second machine-level pass ----
-- The barrier pass above orders variable-latency results.  This one orders
-- fixed-latency results by the stall counts: the program issues one
-- instruction, then waits its stall (at least one cycle) before the next;
-- a register or predicate a fixed-latency form writes may be read, or
-- written again, sm86FixedLatency cycles after that form issued
-- (Accelerator.SM86.Operands -- an ASSUMED table, held to silicon).  Barrier
-- waits only lengthen the time between issues, so counting the stalls alone
-- is the tighter bound.  A barrier an instruction sets is a key too, set
-- sm86BarrierSetCycles after issue and read by every wait on it.  An
-- instruction's own stall is at least its sm86MinimumStall (a BAR.SYNC's
-- 6).  0 for a clean program, else the ordinal (from 1) of the first
-- instruction that touches a result -- or waits on a barrier -- before it is
-- ready, or stalls less than its minimum.

-- 1 when some key is still in flight at cycle `now`.  The comparisons are
-- the primitive's own, each a 0/1 flag eliminated where it is made: the scan
-- stops at the first entry in flight (the rest is evaluated only when this
-- one is not), the value the helper form (naturalOr of naturalAnd of
-- naturalEqual and naturalLess over the whole list) gives
def flLate =
  (lambda unrestricted pending : (family ScoreboardPending) .
    (lambda unrestricted keys : (family StdList Nat) .
      (lambda unrestricted now : Nat .
        (eliminate StdList (lambda unrestricted current : (family StdList Nat) . Nat) keys
          (branch StdListEmpty . zero)
          (branch StdListCons key rest induction .
            (nat-eliminate (lambda unrestricted current : Nat . Nat) induction (lambda unrestricted flagPredecessor : Nat . (lambda unrestricted flagRest : Nat . (succ zero))) (eliminate ScoreboardPending (lambda unrestricted current : (family ScoreboardPending) . Nat) pending
              (branch ScoreboardPendingEnd . zero)
              (branch ScoreboardPendingNext bound ready tail inner .
                (nat-eliminate (lambda unrestricted current : Nat . Nat) inner (lambda unrestricted flagPredecessor : Nat . (lambda unrestricted flagRest : Nat . (nat-eliminate (lambda unrestricted current : Nat . Nat) inner (lambda unrestricted flagPredecessor : Nat . (lambda unrestricted flagRest : Nat . (succ zero))) (nat-less-than now ready)))) (nat-eliminate (lambda unrestricted current : Nat . Nat) (nat-eliminate (lambda unrestricted current : Nat . Nat) (succ zero) (lambda unrestricted flagPredecessor : Nat . (lambda unrestricted flagRest : Nat . zero)) (nat-less-than key bound)) (lambda unrestricted flagPredecessor : Nat . (lambda unrestricted flagRest : Nat . zero)) (nat-less-than bound key)))))))))))

-- the entries still in flight at cycle `now`
def flPrune =
  (lambda unrestricted pending : (family ScoreboardPending) .
    (lambda unrestricted now : Nat .
      (eliminate ScoreboardPending (lambda unrestricted current : (family ScoreboardPending) . (family ScoreboardPending)) pending
        (branch ScoreboardPendingEnd . (constructor ScoreboardPending ScoreboardPendingEnd))
        (branch ScoreboardPendingNext bound ready tail induction .
          (nat-eliminate
            (lambda unrestricted current : Nat . (family ScoreboardPending))
            induction
            (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : (family ScoreboardPending) .
              (constructor ScoreboardPending ScoreboardPendingNext bound ready induction)))
            (naturalLess now ready))))))

-- the keys written, ready at `ready`
def flIssue =
  (lambda unrestricted keys : (family StdList Nat) .
    (lambda unrestricted ready : Nat .
      (lambda unrestricted pending : (family ScoreboardPending) .
        (eliminate StdList (lambda unrestricted current : (family StdList Nat) . (family ScoreboardPending)) keys
          (branch StdListEmpty . pending)
          (branch StdListCons key rest induction .
            (constructor ScoreboardPending ScoreboardPendingNext key ready induction))))))

def sm86FixedLatencyHazard =
  (lambda unrestricted program : (family SM86Program) .
    (app (app (app
      (eliminate SM86Program
        (lambda unrestricted current : (family SM86Program) .
          (pi unrestricted ordinal : Nat . (pi unrestricted now : Nat . (pi unrestricted pending : (family ScoreboardPending) . Nat))))
        program
        (branch SM86ProgramEnd .
          (lambda unrestricted ordinal : Nat . (lambda unrestricted now : Nat . (lambda unrestricted pending : (family ScoreboardPending) . zero))))
        (branch SM86ProgramNext instruction tail induction .
          (lambda unrestricted ordinal : Nat . (lambda unrestricted now : Nat . (lambda unrestricted pending : (family ScoreboardPending) .
            (eliminate SM86OpSummary
              (lambda unrestricted current : (family SM86OpSummary) . Nat)
              (sm86OpSummaryOfBody (sm86InstructionBodyOf instruction))
              (branch SM86OpSummaryValue readsBody writesBody predicateWrites waitKeys setKeys stall latency variable minimum control .
                (let unrestricted reads =
                  (stdListAppend Nat readsBody (stdListAppend Nat (sm86GuardKeys instruction) waitKeys))
                  in (let unrestricted writes = (stdListAppend Nat writesBody predicateWrites)
                  in (let unrestricted issued =
                        (flIssue setKeys (naturalAdd now sm86BarrierSetCycles) (flPrune pending now))
                    in (nat-eliminate
                         (lambda unrestricted current : Nat . Nat)
                         (induction (succ ordinal)
                           (naturalAdd now (naturalSelect (naturalNonzero stall) stall 1))
                           (nat-eliminate
                             (lambda unrestricted current : Nat . (family ScoreboardPending))
                             issued
                             (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : (family ScoreboardPending) .
                               (flIssue writes (naturalAdd now latency) issued)))
                             latency))
                         (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : Nat . ordinal))
                         (naturalOr (naturalLess (naturalSelect (naturalNonzero stall) stall 1) minimum)
                           (naturalOr (flLate pending reads now) (flLate pending writes now))))))))))))))
      1) 0) (constructor ScoreboardPending ScoreboardPendingEnd)))