the results after the forward launches and after the training: the loss
block of that phase, the logit rows, the predictions
561def bobWriteResults =
562 (lambda unrestricted lossAddress : Nat .
563 (lambda unrestricted lossOffset : Nat .
564 (lambda unrestricted tail : (family NvidiaPlanHostSteps) .
565 (constructor
566 NvidiaPlanHostSteps
567 NvidiaPlanHostStepBoundary
568 prTelemetryLearningValue
569 (aosChoose
570 Bytes
571 (naturalEqual lossAddress bobInitialLossAddress)
572 b"Bob:loss-before-training"
573 b"Bob:loss-after-training")
574 (bobWriteAt
575 bobResult
576 lossAddress
577 bobLossBytes
578 lossOffset
579 (bobWriteAt
580 bobResult
581 bobLogitRowsAddress
582 bobLogitRowsBytes
583 bobResultLogitRowsOffset
584 (bobWriteAt bobPredictions bobPredictionsAddress bobPredictionsBytes 0 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.