---- the host ELF ----
`productIdentity` is the pairing's padded card name: the host payload's
identity in the envelope and the name the card must report.
`hostWriter` makes the host program an executable for the pairing's host:
Runtime.NativePhysicalNativeELF's direct writer for x86-64, Platform.
AArch64.HostLowering's for the DGX Spark.
791def bobNativeCaptureBoundary =
792 (lambda unrestricted phase : Nat .
793 (lambda unrestricted name : Bytes .
794 (lambda unrestricted after : (family NativeObservedSteps) .
795 (aosChoose
796 (family NativeObservedSteps)
797 (naturalAnd
798 (naturalEqual phase prTelemetryLearningValue)
799 (bytes-equal name b"Bob:loss-before-training"))
800 (nvidiaRequestCaptureMappedF32
801 bobNativeRowTag0
802 (bobStagingAt bobInitialLossAddress)
803 (phLoad prGPPut)
804 after)
805 (aosChoose
806 (family NativeObservedSteps)
807 (naturalAnd
808 (naturalEqual phase prTelemetryLearningValue)
809 (bytes-equal name b"Bob:loss-after-training"))
810 (nvidiaRequestCaptureMappedF32
811 bobNativeRowTag1
812 (bobStagingAt bobTrainingLossAddress)
813 (phLoad prGPPut)
814 after)
815 (nvidiaRequestCaptureBoundaryWithCheckpoint phase name after))))))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.