The program as named blocks and named loop bodies, each prepending its
instructions to what follows, so a statement about the program is a
statement about its parts (Proof.LinearStepGeneratorForall): the
prologue, the loads, y, d, the loss, dW, W', Exit.
tid, the lane guard, the nine parameter words (4 addresses, eta)
184def lsPrologue =
185 (lambda unrestricted k : Nat . (lambda unrestricted m : Nat . (lambda unrestricted tail : (family SM86Program) .
186 (lsNext (constructor SM86InstructionBody SM86SpecialToRegister (lsR 0) (constructor SM86SpecialRegister SM86ThreadIdX) lsControlSetSB0)
187 (lsNext (constructor SM86InstructionBody SM86PredicateGreaterThanImmediate (constructor SM86Predicate SM86Predicate0) (lsR 0) sm86Unsigned32Zero lsControlWaitSB0)
188 (constructor SM86Program SM86ProgramNext (sm86PredicatedInstruction (constructor SM86Predicate SM86Predicate0) (constructor SM86InstructionBody SM86Exit lsControl))
189 (lsNext (lsConstant 2 352)
190 (lsNext (lsConstant 3 356)
191 (lsNext (lsConstant 4 360)
192 (lsNext (lsConstant 5 364)
193 (lsNext (lsConstant 6 368)
194 (lsNext (lsConstant 7 372)
195 (lsNext (lsConstant 8 376)
196 (lsNext (lsConstant 9 380)
197 (lsNext (lsConstant 10 400)
198 tail)))))))))))))))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.