module Training.NativeObligation

family NativeReadiness : Type 0
constructor NativeEmitterAbsent
constructor NativeEmitterPresent
constructor NativeHardwareCorrect
constructor NativePerformanceQualified

end-family

family NativeObligation : Type 0
constructor NativeGradientAccumulatorClear
constructor NativeIncomingGradientClear
constructor NativeInputTransfer
constructor NativeEmbeddingGather1024
constructor NativeLayerNormForward1024
constructor NativeLayerNormForward64
constructor NativeLayerNormForward256
constructor NativeDenseHMMAForward
constructor NativeAttentionHMMAForward
constructor NativeRoutedHMMAForward
constructor NativeQKVRoPEForward
constructor NativeCausalSoftmaxForward256
constructor NativeHeadMajorTokenPermutation
constructor NativeTokenHashRoute
constructor NativeRoutingTelemetry
constructor NativeRoutedGather
constructor NativeGELUForward
constructor NativeInverseRouteGather
constructor NativeResidualAdd
constructor NativeNegativeClassRNG
constructor NativeClassRowGather256
constructor NativePositiveClassDot
constructor NativeImportanceCorrection
constructor NativeCandidateConcatenate
constructor NativeSampledCrossEntropy
constructor NativeLossSeed
constructor NativeCachedCrossEntropyBackward
constructor NativeCandidateSplit
constructor NativeAdjointCopy
constructor NativeDenseHMMAReverse
constructor NativeLayerNormBackward1024
constructor NativeLayerNormBackward64
constructor NativeLayerNormBackward256
constructor NativeLayerNormParameterGradient1024
constructor NativeLayerNormParameterGradient64
constructor NativeLayerNormParameterGradient256
constructor NativeQKVRoPEBackward
constructor NativeAttentionHMMAReverse
constructor NativeSoftmaxBackward256
constructor NativeTokenHeadPermutationBackward
constructor NativeRoutedGatherBackward
constructor NativeRoutedHMMAReverse
constructor NativeGELUBackward
constructor NativeInverseRouteBackward
constructor NativeResidualBackward
constructor NativePositiveClassDotBackward
constructor NativeClassRowScatter256
constructor NativeAdjointAccumulate
constructor NativeEmbeddingScatter1024
constructor NativeGradientAccumulate
constructor NativeReductionScratchClear
constructor NativeGradientSquareReduction
constructor NativeGradientPartialReduction
constructor NativeDeviceClipScale
constructor NativeDeviceGradientScale
constructor NativeAdamW
constructor NativeCrossEntropyRowsLaunch
constructor NativeCrossEntropyPartialLaunch
constructor NativeCrossEntropyFinalizeLaunch
constructor NativeEmbeddingScatter512

end-family

def nativeObligationReadiness =
  (lambda unrestricted obligation : (family NativeObligation) .
    (eliminate
      NativeObligation
      (lambda unrestricted current : (family NativeObligation) . (family NativeReadiness))
      obligation
      (branch
        NativeGradientAccumulatorClear
        .
        (constructor NativeReadiness NativePerformanceQualified))
      (branch NativeIncomingGradientClear . (constructor NativeReadiness NativeEmitterPresent))
      (branch NativeInputTransfer . (constructor NativeReadiness NativeEmitterPresent))
      (branch NativeEmbeddingGather1024 . (constructor NativeReadiness NativePerformanceQualified))
      (branch NativeLayerNormForward1024 . (constructor NativeReadiness NativePerformanceQualified))
      (branch NativeLayerNormForward64 . (constructor NativeReadiness NativeHardwareCorrect))
      (branch NativeLayerNormForward256 . (constructor NativeReadiness NativeHardwareCorrect))
      (branch NativeDenseHMMAForward . (constructor NativeReadiness NativePerformanceQualified))
      (branch NativeAttentionHMMAForward . (constructor NativeReadiness NativeEmitterPresent))
      (branch NativeRoutedHMMAForward . (constructor NativeReadiness NativeEmitterPresent))
      (branch NativeQKVRoPEForward . (constructor NativeReadiness NativeEmitterPresent))
      (branch
        NativeCausalSoftmaxForward256
        .
        (constructor NativeReadiness NativePerformanceQualified))
      (branch NativeHeadMajorTokenPermutation . (constructor NativeReadiness NativeHardwareCorrect))
      (branch NativeTokenHashRoute . (constructor NativeReadiness NativeEmitterPresent))
      (branch NativeRoutingTelemetry . (constructor NativeReadiness NativeEmitterPresent))
      (branch NativeRoutedGather . (constructor NativeReadiness NativeEmitterPresent))
      (branch NativeGELUForward . (constructor NativeReadiness NativeHardwareCorrect))
      (branch NativeInverseRouteGather . (constructor NativeReadiness NativeEmitterPresent))
      (branch NativeResidualAdd . (constructor NativeReadiness NativeHardwareCorrect))
      (branch NativeNegativeClassRNG . (constructor NativeReadiness NativeHardwareCorrect))
      (branch NativeClassRowGather256 . (constructor NativeReadiness NativeHardwareCorrect))
      (branch NativePositiveClassDot . (constructor NativeReadiness NativeHardwareCorrect))
      (branch NativeImportanceCorrection . (constructor NativeReadiness NativeHardwareCorrect))
      (branch NativeCandidateConcatenate . (constructor NativeReadiness NativeEmitterPresent))
      (branch NativeSampledCrossEntropy . (constructor NativeReadiness NativeEmitterPresent))
      (branch NativeLossSeed . (constructor NativeReadiness NativeEmitterPresent))
      (branch NativeCachedCrossEntropyBackward . (constructor NativeReadiness NativeEmitterPresent))
      (branch NativeCandidateSplit . (constructor NativeReadiness NativeEmitterPresent))
      (branch NativeAdjointCopy . (constructor NativeReadiness NativeHardwareCorrect))
      (branch NativeDenseHMMAReverse . (constructor NativeReadiness NativeEmitterPresent))
      (branch
        NativeLayerNormBackward1024
        .
        (constructor NativeReadiness NativePerformanceQualified))
      (branch NativeLayerNormBackward64 . (constructor NativeReadiness NativeHardwareCorrect))
      (branch NativeLayerNormBackward256 . (constructor NativeReadiness NativeHardwareCorrect))
      (branch
        NativeLayerNormParameterGradient1024
        .
        (constructor NativeReadiness NativePerformanceQualified))
      (branch
        NativeLayerNormParameterGradient64
        .
        (constructor NativeReadiness NativeHardwareCorrect))
      (branch
        NativeLayerNormParameterGradient256
        .
        (constructor NativeReadiness NativeHardwareCorrect))
      (branch NativeQKVRoPEBackward . (constructor NativeReadiness NativeEmitterPresent))
      (branch NativeAttentionHMMAReverse . (constructor NativeReadiness NativeHardwareCorrect))
      (branch NativeSoftmaxBackward256 . (constructor NativeReadiness NativePerformanceQualified))
      (branch
        NativeTokenHeadPermutationBackward
        .
        (constructor NativeReadiness NativeHardwareCorrect))
      (branch NativeRoutedGatherBackward . (constructor NativeReadiness NativeEmitterPresent))
      (branch NativeRoutedHMMAReverse . (constructor NativeReadiness NativeEmitterPresent))
      (branch NativeGELUBackward . (constructor NativeReadiness NativeHardwareCorrect))
      (branch NativeInverseRouteBackward . (constructor NativeReadiness NativeEmitterPresent))
      (branch NativeResidualBackward . (constructor NativeReadiness NativeHardwareCorrect))
      (branch NativePositiveClassDotBackward . (constructor NativeReadiness NativeHardwareCorrect))
      (branch NativeClassRowScatter256 . (constructor NativeReadiness NativeEmitterPresent))
      (branch NativeAdjointAccumulate . (constructor NativeReadiness NativeHardwareCorrect))
      (branch NativeEmbeddingScatter1024 . (constructor NativeReadiness NativeEmitterPresent))
      (branch NativeGradientAccumulate . (constructor NativeReadiness NativePerformanceQualified))
      (branch
        NativeReductionScratchClear
        .
        (constructor NativeReadiness NativePerformanceQualified))
      (branch
        NativeGradientSquareReduction
        .
        (constructor NativeReadiness NativePerformanceQualified))
      (branch
        NativeGradientPartialReduction
        .
        (constructor NativeReadiness NativePerformanceQualified))
      (branch NativeDeviceClipScale . (constructor NativeReadiness NativePerformanceQualified))
      (branch NativeDeviceGradientScale . (constructor NativeReadiness NativePerformanceQualified))
      (branch NativeAdamW . (constructor NativeReadiness NativePerformanceQualified))
      (branch NativeCrossEntropyRowsLaunch . (constructor NativeReadiness NativeEmitterPresent))
      (branch NativeCrossEntropyPartialLaunch . (constructor NativeReadiness NativeEmitterPresent))
      (branch NativeCrossEntropyFinalizeLaunch . (constructor NativeReadiness NativeEmitterPresent))
      (branch NativeEmbeddingScatter512 . (constructor NativeReadiness NativeEmitterPresent))))