0 when clean, else the ordinal (from 1) of the first hazardous instruction.
316def sm86Scoreboard =
317 (lambda unrestricted program : (family SM86Program) .
318 (app
319 (app
320 (app
321 (eliminate SM86Program
322 (lambda unrestricted current : (family SM86Program) .
323 (pi unrestricted ordinal : Nat .
324 (pi unrestricted pending : (family ScoreboardMasks) .
325 (pi unrestricted pendingReads : (family ScoreboardMasks) . Nat))))
326 program
327 (branch SM86ProgramEnd .
328 (lambda unrestricted ordinal : Nat .
329 (lambda unrestricted pending : (family ScoreboardMasks) .
330 (lambda unrestricted pendingReads : (family ScoreboardMasks) . zero))))
331 (branch SM86ProgramNext instruction tail induction .
332 (lambda unrestricted ordinal : Nat .
333 (lambda unrestricted pending : (family ScoreboardMasks) .
334 (lambda unrestricted pendingReads : (family ScoreboardMasks) .
335 (eliminate ScoreboardStep
336 (lambda unrestricted current : (family ScoreboardStep) . Nat)
337 (scoreboardStep pending pendingReads (sm86OpSummaryOfBody (scoreboardBodyOf instruction)))
338 (branch ScoreboardStepValue hazard next nextReads .
339 (nat-eliminate
340 (lambda unrestricted current : Nat . Nat)
341 (induction (succ ordinal) next nextReads)
342 (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : Nat . ordinal))
343 hazard))))))))
344 1)
345 sbMasksEmpty)
346 sbMasksEmpty))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.