every issue of the update trains on a context no earlier step read: the
cursor moves on by one context exactly once before each (it starts at
the checkpoint's position, the forward's context, which the first step
trains on and moves past), and the run issues the update once per step
550def coppeliusHostStepsFresh =
551 (lambda unrestricted steps : (family NvidiaPlanHostSteps) .
552 (app (app (app
553 (eliminate NvidiaPlanHostSteps
554 (lambda unrestricted current : (family NvidiaPlanHostSteps) .
555 (pi unrestricted moved : Nat . (pi unrestricted issued : Nat . (pi unrestricted ok : Nat . Nat))))
556 (nvidiaPlanHostStepsUnrolled steps)
557 (branch NvidiaPlanHostStepsEnd .
558 (lambda unrestricted moved : Nat . (lambda unrestricted issued : Nat . (lambda unrestricted ok : Nat .
559 (naturalAnd ok (naturalAnd (naturalIsZero moved) (naturalEqual issued coppeliusRunSteps)))))))
560 (branch NvidiaPlanHostStepSubmit gpPut stride tail induction . induction)
561 (branch NvidiaPlanHostStepRepeat count body tail bodyInduction tailInduction . tailInduction)
562 (branch NvidiaPlanHostStepRead file host extent offset stride tolerateEmpty tail induction . induction)
563 (branch NvidiaPlanHostStepReadCyclic host extent offset recordBytes count index indexStride tail induction . induction)
564 (branch NvidiaPlanHostStepWrite file host extent tail induction . induction)
565 (branch NvidiaPlanHostStepWriteAt file host extent offset tail induction . induction)
566 (branch NvidiaPlanHostStepWriteStat file tail induction . induction)
567 (branch NvidiaPlanHostStepWriteStatus file tail induction . induction)
568 (branch NvidiaPlanHostStepWriteTimestamps file tail induction . induction)
569 (branch NvidiaPlanHostStepRecordStat host statOffset extent tail induction . induction)
570 (branch NvidiaPlanHostStepStamp gpPut stride which tail induction . induction)
571 (branch NvidiaPlanHostStepFill host payload tail induction . induction)
572 (branch NvidiaPlanHostStepAssertWord identity host expected tail induction . induction)
573 (branch NvidiaPlanHostStepBindInputIdentity offset extent tail induction . induction)
574 (branch NvidiaPlanHostStepWriteInputIdentity tail induction . induction)
575 (branch NvidiaPlanHostStepBeginCheckpoint tail induction . induction)
576 (branch NvidiaPlanHostStepOperation tail induction . induction)
577 (branch NvidiaPlanHostStepSync file tail induction . induction)
578 (branch NvidiaPlanHostStepDataSync file tail induction . induction)
579 (branch NvidiaPlanHostStepClose file tail induction . induction)
580 (branch NvidiaPlanHostStepReissue gpPut stride piece pieceStride entry entryStride tail induction .
581 (lambda unrestricted moved : Nat . (lambda unrestricted issued : Nat . (lambda unrestricted ok : Nat .
582 (let unrestricted update = (naturalEqual piece coppeliusUpdatePiece) in
583 (induction (naturalSelect update 0 moved) (naturalAdd issued update)
584 (naturalAnd ok (naturalSelect update moved 1))))))))
585 (branch NvidiaPlanHostStepCommands commands tail induction . induction)
586 (branch NvidiaPlanHostStepCursorFromCheckpoint base scale tail induction . induction)
587 (branch NvidiaPlanHostStepReadAtCursor file host extent delta tail induction . induction)
588 (branch NvidiaPlanHostStepCursorAdvance bytes tail induction .
589 (lambda unrestricted moved : Nat . (lambda unrestricted issued : Nat . (lambda unrestricted ok : Nat .
590 (induction 1 issued (naturalAnd ok (naturalAnd (naturalIsZero moved) (naturalEqual bytes coppeliusContextStreamBytes))))))))
591 (branch NvidiaPlanHostStepCheckpointBegin tail induction . induction)
592 (branch NvidiaPlanHostStepCheckpointPublish updates invocations tail induction . induction))
593 0) 0) 1))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.