module Runtime.NativePhysicalTrainingRoutine

import Compiler.MachineX86Native
import Compiler.MachineX86NativeAssembly
import Model.Word64
import Runtime.NativePhysicalNative
import Runtime.NativeMemoryRoutine
import Std.Natural
import Model.Parameter

family NativePhysicalTrainingBitPatchDestinationWidth : Type 0
constructor NativePhysicalTrainingBitPatchDestination32
constructor NativePhysicalTrainingBitPatchDestination64
end-family

family NativePhysicalTrainingCheckedBitPatchParameterError : Type 0
constructor NativePhysicalTrainingCheckedBitPatchWidthZero
constructor NativePhysicalTrainingCheckedBitPatchSourceBounds
constructor NativePhysicalTrainingCheckedBitPatchDestinationBounds
constructor NativePhysicalTrainingCheckedBitPatchAddressBits
constructor NativePhysicalTrainingCheckedBitPatchAlignmentBits

end-family

family NativePhysicalTrainingCheckedBitPatchGeneration : Type 0
constructor NativePhysicalTrainingCheckedBitPatchParametersRejected
field unrestricted nativePhysicalTrainingCheckedBitPatchParameterError : (family NativePhysicalTrainingCheckedBitPatchParameterError)
constructor NativePhysicalTrainingCheckedBitPatchAssemblyGenerated
field unrestricted nativePhysicalTrainingCheckedBitPatchAssemblyResult : (family X86NativeAssemblyResult)

end-family

def nativePhysicalTrainingShiftLeftWord =
  (lambda unrestricted value : (family ModelWord64) .
    (lambda unrestricted count : Nat .
      (nat-eliminate
        (lambda unrestricted current : Nat . (family ModelWord64))
        value
        (lambda unrestricted predecessor : Nat .
          (lambda unrestricted induction : (family ModelWord64) .
            (app modelWord64ShiftLeftOne induction)))
        count)))

def nativePhysicalTrainingBitMask =
  (lambda unrestricted width : Nat .
    (app
      (app modelWord64Subtract
        (app
          (app nativePhysicalTrainingShiftLeftWord modelWord64One)
          width))
      modelWord64One))

def nativePhysicalTrainingImmediate64FromWord =
  (lambda unrestricted value : (family ModelWord64) .
    (eliminate ModelWord64
      (lambda unrestricted current : (family ModelWord64) .
        (family X86NativeImmediate64))
      value
      (branch ModelWord64Value b0 b1 b2 b3 b4 b5 b6 b7 .
        (constructor X86NativeImmediate64 X86NativeImmediate64Value
          b0 b1 b2 b3 b4 b5 b6 b7))))

def nativePhysicalTrainingImmediate8FromNatural =
  (lambda unrestricted value : Nat .
    (constructor X86NativeImmediate8 X86NativeImmediate8Value
      (nat-to-byte value)))

-- The Linux ioctl return value only proves transport success.  NVIDIA RM and
-- UVM replies carry a second 32-bit status inside the mutable payload.  This
-- routine performs both checks as one result-producing operation: nonzero
-- syscall returns pass through unchanged; successful syscalls return the
-- embedded status word at payload + statusOffset.
def nativePhysicalTrainingIoctlStatusFailureLabel =
  b"ioctl-syscall-fail"

def nativePhysicalTrainingIoctlStatusAssembly =
  (constructor X86NativeAssembly X86NativeAssemblyEmit
    (constructor X86NativeInstruction X86NativeAddRegister64
      (constructor X86NativeRegister64 X86NativeRDX)
      (constructor X86NativeRegister64 X86NativeR8))
    (constructor X86NativeAssembly X86NativeAssemblyEmit
      (constructor X86NativeInstruction X86NativeMoveImmediate32
        (constructor X86NativeRegister64 X86NativeRAX)
        (app nativePhysicalNativeI32Byte (byte 16)))
      (constructor X86NativeAssembly X86NativeAssemblyEmit
        (constructor X86NativeInstruction X86NativeSystemCall)
        (constructor X86NativeAssembly X86NativeAssemblyEmit
          (constructor X86NativeInstruction X86NativeTestRegister64
            (constructor X86NativeRegister64 X86NativeRAX)
            (constructor X86NativeRegister64 X86NativeRAX))
          (constructor X86NativeAssembly X86NativeAssemblyJumpCondition
            (constructor X86NativeCondition X86NativeConditionNotZero)
            nativePhysicalTrainingIoctlStatusFailureLabel
            (constructor X86NativeAssembly X86NativeAssemblyEmit
              (constructor X86NativeInstruction X86NativeLoadMemory32ZeroExtend64
                (constructor X86NativeRegister64 X86NativeRAX)
                (constructor X86NativeRegister64 X86NativeR8)
                nativePhysicalNativeD0)
              (constructor X86NativeAssembly X86NativeAssemblyEmit
                (constructor X86NativeInstruction X86NativeReturn)
                (constructor X86NativeAssembly X86NativeAssemblyLabel
                  nativePhysicalTrainingIoctlStatusFailureLabel
                  (constructor X86NativeAssembly X86NativeAssemblyEmit
                    (constructor X86NativeInstruction X86NativeReturn)
                    (constructor X86NativeAssembly X86NativeAssemblyEnd))))))))))

def nativePhysicalTrainingGenerateIoctlStatusRoutine =
  (app x86NativeAssemble nativePhysicalTrainingIoctlStatusAssembly)

def nativePhysicalTrainingBitPatchAssemblyWithAccess =
  (lambda unrestricted load : (family X86NativeInstruction) .
    (lambda unrestricted store : (family X86NativeInstruction) .
      (lambda unrestricted sourceShift : (family X86NativeImmediate8) .
        (lambda unrestricted destinationShift : (family X86NativeImmediate8) .
          (lambda unrestricted sourceMask : (family X86NativeImmediate64) .
            (lambda unrestricted clearMask : (family X86NativeImmediate64) .
              (constructor X86NativeAssembly X86NativeAssemblyEmit
                load
                (constructor X86NativeAssembly X86NativeAssemblyEmit
                  (constructor X86NativeInstruction X86NativeMoveRegister64
                    (constructor X86NativeRegister64 X86NativeRSI)
                    (constructor X86NativeRegister64 X86NativeRCX))
                  (constructor X86NativeAssembly X86NativeAssemblyEmit
                    (constructor X86NativeInstruction X86NativeShiftRightImmediate64
                      (constructor X86NativeRegister64 X86NativeRCX)
                      sourceShift)
                    (constructor X86NativeAssembly X86NativeAssemblyEmit
                      (constructor X86NativeInstruction X86NativeMoveImmediate64
                        (constructor X86NativeRegister64 X86NativeRDX)
                        sourceMask)
                      (constructor X86NativeAssembly X86NativeAssemblyEmit
                        (constructor X86NativeInstruction X86NativeAndRegister64
                          (constructor X86NativeRegister64 X86NativeRDX)
                          (constructor X86NativeRegister64 X86NativeRCX))
                        (constructor X86NativeAssembly X86NativeAssemblyEmit
                          (constructor X86NativeInstruction X86NativeShiftLeftImmediate64
                            (constructor X86NativeRegister64 X86NativeRCX)
                            destinationShift)
                          (constructor X86NativeAssembly X86NativeAssemblyEmit
                            (constructor X86NativeInstruction X86NativeMoveImmediate64
                              (constructor X86NativeRegister64 X86NativeRDX)
                              clearMask)
                            (constructor X86NativeAssembly X86NativeAssemblyEmit
                              (constructor X86NativeInstruction X86NativeAndRegister64
                                (constructor X86NativeRegister64 X86NativeRDX)
                                (constructor X86NativeRegister64 X86NativeRAX))
                              (constructor X86NativeAssembly X86NativeAssemblyEmit
                                (constructor X86NativeInstruction X86NativeOrRegister64
                                  (constructor X86NativeRegister64 X86NativeRCX)
                                  (constructor X86NativeRegister64 X86NativeRAX))
                                (constructor X86NativeAssembly X86NativeAssemblyEmit
                                  store
                                  (constructor X86NativeAssembly X86NativeAssemblyEmit
                                    (constructor X86NativeInstruction X86NativeClear32
                                      (constructor X86NativeRegister64 X86NativeRAX))
                                    (constructor X86NativeAssembly X86NativeAssemblyEmit
                                      (constructor X86NativeInstruction X86NativeReturn)
                                      (constructor X86NativeAssembly
                                        X86NativeAssemblyEnd)))))))))))))))))))

def nativePhysicalTrainingBitPatchAssembly =
  (lambda unrestricted destinationWidth :
      (family NativePhysicalTrainingBitPatchDestinationWidth) .
    (lambda unrestricted sourceShift : Nat .
      (lambda unrestricted destinationShift : Nat .
        (lambda unrestricted width : Nat .
          (app
            (lambda unrestricted sourceMaskWord : (family ModelWord64) .
              (app
                (lambda unrestricted shiftedMaskWord : (family ModelWord64) .
                  (app
                    (lambda unrestricted clearMaskWord : (family ModelWord64) .
                      (eliminate NativePhysicalTrainingBitPatchDestinationWidth
                        (lambda unrestricted current :
                          (family NativePhysicalTrainingBitPatchDestinationWidth) .
                          (family X86NativeAssembly))
                        destinationWidth
                        (branch NativePhysicalTrainingBitPatchDestination32 .
                          (app
                            (app
                              (app
                                (app
                                  (app
                                    (app nativePhysicalTrainingBitPatchAssemblyWithAccess
                                      (constructor X86NativeInstruction
                                        X86NativeLoadMemory32ZeroExtend64
                                        (constructor X86NativeRegister64 X86NativeRAX)
                                        (constructor X86NativeRegister64 X86NativeRDI)
                                        nativePhysicalNativeD0))
                                    (constructor X86NativeInstruction
                                      X86NativeStoreMemory32
                                      (constructor X86NativeRegister64 X86NativeRDI)
                                      nativePhysicalNativeD0
                                      (constructor X86NativeRegister64 X86NativeRAX)))
                                  (app nativePhysicalTrainingImmediate8FromNatural
                                    sourceShift))
                                (app nativePhysicalTrainingImmediate8FromNatural
                                  destinationShift))
                              (app nativePhysicalTrainingImmediate64FromWord
                                sourceMaskWord))
                            (app nativePhysicalTrainingImmediate64FromWord
                              clearMaskWord)))
                        (branch NativePhysicalTrainingBitPatchDestination64 .
                          (app
                            (app
                              (app
                                (app
                                  (app
                                    (app nativePhysicalTrainingBitPatchAssemblyWithAccess
                                      (constructor X86NativeInstruction
                                        X86NativeLoadMemory64
                                        (constructor X86NativeRegister64 X86NativeRAX)
                                        (constructor X86NativeRegister64 X86NativeRDI)
                                        nativePhysicalNativeD0))
                                    (constructor X86NativeInstruction
                                      X86NativeStoreMemory64
                                      (constructor X86NativeRegister64 X86NativeRDI)
                                      nativePhysicalNativeD0
                                      (constructor X86NativeRegister64 X86NativeRAX)))
                                  (app nativePhysicalTrainingImmediate8FromNatural
                                    sourceShift))
                                (app nativePhysicalTrainingImmediate8FromNatural
                                  destinationShift))
                              (app nativePhysicalTrainingImmediate64FromWord
                                sourceMaskWord))
                            (app nativePhysicalTrainingImmediate64FromWord
                              clearMaskWord)))))
                    (app modelWord64Complement shiftedMaskWord)))
                (app
                  (app nativePhysicalTrainingShiftLeftWord sourceMaskWord)
                  destinationShift)))
            (app nativePhysicalTrainingBitMask width))))))

def nativePhysicalTrainingGenerateBitPatchRoutine =
  (lambda unrestricted destinationWidth :
      (family NativePhysicalTrainingBitPatchDestinationWidth) .
    (lambda unrestricted sourceShift : Nat .
      (lambda unrestricted destinationShift : Nat .
        (lambda unrestricted width : Nat .
          (app x86NativeAssemble
            (app
              (app
                (app
                  (app nativePhysicalTrainingBitPatchAssembly destinationWidth)
                  sourceShift)
                destinationShift)
              width))))))

def nativePhysicalTrainingPatch32Assembly =
  (constructor X86NativeAssembly X86NativeAssemblyEmit
    (constructor X86NativeInstruction X86NativeStoreMemory32
      (constructor X86NativeRegister64 X86NativeRDI)
      nativePhysicalNativeD0
      (constructor X86NativeRegister64 X86NativeRSI))
    (constructor X86NativeAssembly X86NativeAssemblyEmit
      (constructor X86NativeInstruction X86NativeClear32
        (constructor X86NativeRegister64 X86NativeRAX))
      (constructor X86NativeAssembly X86NativeAssemblyEmit
        (constructor X86NativeInstruction X86NativeReturn)
        (constructor X86NativeAssembly X86NativeAssemblyEnd))))

def nativePhysicalTrainingPatch64Assembly =
  (constructor X86NativeAssembly X86NativeAssemblyEmit
    (constructor X86NativeInstruction X86NativeStoreMemory64
      (constructor X86NativeRegister64 X86NativeRDI)
      nativePhysicalNativeD0
      (constructor X86NativeRegister64 X86NativeRSI))
    (constructor X86NativeAssembly X86NativeAssemblyEmit
      (constructor X86NativeInstruction X86NativeClear32
        (constructor X86NativeRegister64 X86NativeRAX))
      (constructor X86NativeAssembly X86NativeAssemblyEmit
        (constructor X86NativeInstruction X86NativeReturn)
        (constructor X86NativeAssembly X86NativeAssemblyEnd))))

def nativePhysicalTrainingPublish32Assembly =
  (constructor X86NativeAssembly X86NativeAssemblyEmit
    (constructor X86NativeInstruction X86NativeStoreMemory32
      (constructor X86NativeRegister64 X86NativeRDI)
      nativePhysicalNativeD0
      (constructor X86NativeRegister64 X86NativeRSI))
    (constructor X86NativeAssembly X86NativeAssemblyEmit
      (constructor X86NativeInstruction X86NativeStoreFence)
      (constructor X86NativeAssembly X86NativeAssemblyEmit
        (constructor X86NativeInstruction X86NativeStoreMemory32
          (constructor X86NativeRegister64 X86NativeRDX)
          nativePhysicalNativeD0
          (constructor X86NativeRegister64 X86NativeRCX))
        (constructor X86NativeAssembly X86NativeAssemblyEmit
          (constructor X86NativeInstruction X86NativeClear32
            (constructor X86NativeRegister64 X86NativeRAX))
          (constructor X86NativeAssembly X86NativeAssemblyEmit
            (constructor X86NativeInstruction X86NativeReturn)
            (constructor X86NativeAssembly X86NativeAssemblyEnd))))))

def nativePhysicalTrainingPublish64Assembly =
  (constructor X86NativeAssembly X86NativeAssemblyEmit
    (constructor X86NativeInstruction X86NativeStoreMemory64
      (constructor X86NativeRegister64 X86NativeRDI)
      nativePhysicalNativeD0
      (constructor X86NativeRegister64 X86NativeRSI))
    (constructor X86NativeAssembly X86NativeAssemblyEmit
      (constructor X86NativeInstruction X86NativeStoreFence)
      (constructor X86NativeAssembly X86NativeAssemblyEmit
        (constructor X86NativeInstruction X86NativeStoreMemory64
          (constructor X86NativeRegister64 X86NativeRDX)
          nativePhysicalNativeD0
          (constructor X86NativeRegister64 X86NativeRCX))
        (constructor X86NativeAssembly X86NativeAssemblyEmit
          (constructor X86NativeInstruction X86NativeClear32
            (constructor X86NativeRegister64 X86NativeRAX))
          (constructor X86NativeAssembly X86NativeAssemblyEmit
            (constructor X86NativeInstruction X86NativeReturn)
            (constructor X86NativeAssembly X86NativeAssemblyEnd))))))

def nativePhysicalTrainingPublish3264Assembly =
  (constructor X86NativeAssembly X86NativeAssemblyEmit
    (constructor X86NativeInstruction X86NativeStoreMemory32
      (constructor X86NativeRegister64 X86NativeRDI)
      nativePhysicalNativeD0
      (constructor X86NativeRegister64 X86NativeRSI))
    (constructor X86NativeAssembly X86NativeAssemblyEmit
      (constructor X86NativeInstruction X86NativeStoreFence)
      (constructor X86NativeAssembly X86NativeAssemblyEmit
        (constructor X86NativeInstruction X86NativeStoreMemory64
          (constructor X86NativeRegister64 X86NativeRDX)
          nativePhysicalNativeD0
          (constructor X86NativeRegister64 X86NativeRCX))
        (constructor X86NativeAssembly X86NativeAssemblyEmit
          (constructor X86NativeInstruction X86NativeClear32
            (constructor X86NativeRegister64 X86NativeRAX))
          (constructor X86NativeAssembly X86NativeAssemblyEmit
            (constructor X86NativeInstruction X86NativeReturn)
            (constructor X86NativeAssembly X86NativeAssemblyEnd))))))

def nativePhysicalTrainingPublish6432Assembly =
  (constructor X86NativeAssembly X86NativeAssemblyEmit
    (constructor X86NativeInstruction X86NativeStoreMemory64
      (constructor X86NativeRegister64 X86NativeRDI)
      nativePhysicalNativeD0
      (constructor X86NativeRegister64 X86NativeRSI))
    (constructor X86NativeAssembly X86NativeAssemblyEmit
      (constructor X86NativeInstruction X86NativeStoreFence)
      (constructor X86NativeAssembly X86NativeAssemblyEmit
        (constructor X86NativeInstruction X86NativeStoreMemory32
          (constructor X86NativeRegister64 X86NativeRDX)
          nativePhysicalNativeD0
          (constructor X86NativeRegister64 X86NativeRCX))
        (constructor X86NativeAssembly X86NativeAssemblyEmit
          (constructor X86NativeInstruction X86NativeClear32
            (constructor X86NativeRegister64 X86NativeRAX))
          (constructor X86NativeAssembly X86NativeAssemblyEmit
            (constructor X86NativeInstruction X86NativeReturn)
            (constructor X86NativeAssembly X86NativeAssemblyEnd))))))

def nativePhysicalTrainingGeneratePatch32Routine =
  (app x86NativeAssemble nativePhysicalTrainingPatch32Assembly)

def nativePhysicalTrainingGeneratePatch64Routine =
  (app x86NativeAssemble nativePhysicalTrainingPatch64Assembly)

def nativePhysicalTrainingGeneratePublish32Routine =
  (app x86NativeAssemble nativePhysicalTrainingPublish32Assembly)

def nativePhysicalTrainingGeneratePublish64Routine =
  (app x86NativeAssemble nativePhysicalTrainingPublish64Assembly)

def nativePhysicalTrainingGeneratePublish3264Routine =
  (app x86NativeAssemble nativePhysicalTrainingPublish3264Assembly)

def nativePhysicalTrainingGeneratePublish6432Routine =
  (app x86NativeAssemble nativePhysicalTrainingPublish6432Assembly)

def nativePhysicalTrainingGenerateCheckpointCopyRoutine =
  nativeMemoryGenerateCopyRoutine

def nativePhysicalTrainingFence32LoopLabel =
  b"fence-32-loop"

def nativePhysicalTrainingFence32SuccessLabel =
  b"fence-32-success"

def nativePhysicalTrainingFence32TimeoutLabel =
  b"fence-32-timeout"

def nativePhysicalTrainingFence64LoopLabel =
  b"fence-64-loop"

def nativePhysicalTrainingFence64SuccessLabel =
  b"fence-64-success"

def nativePhysicalTrainingFence64TimeoutLabel =
  b"fence-64-timeout"

def nativePhysicalTrainingFence32Assembly =
  (constructor X86NativeAssembly X86NativeAssemblyLabel
    nativePhysicalTrainingFence32LoopLabel
    (constructor X86NativeAssembly X86NativeAssemblyEmit
      (constructor X86NativeInstruction X86NativeLoadMemory32ZeroExtend64
        (constructor X86NativeRegister64 X86NativeRAX)
        (constructor X86NativeRegister64 X86NativeRDI)
        nativePhysicalNativeD0)
      (constructor X86NativeAssembly X86NativeAssemblyEmit
        (constructor X86NativeInstruction X86NativeStoreMemory32
          (constructor X86NativeRegister64 X86NativeRCX)
          nativePhysicalNativeD0
          (constructor X86NativeRegister64 X86NativeRAX))
        (constructor X86NativeAssembly X86NativeAssemblyEmit
          (constructor X86NativeInstruction X86NativeCompareRegister64
            (constructor X86NativeRegister64 X86NativeRSI)
            (constructor X86NativeRegister64 X86NativeRAX))
          (constructor X86NativeAssembly X86NativeAssemblyJumpCondition
            (constructor X86NativeCondition X86NativeConditionZero)
            nativePhysicalTrainingFence32SuccessLabel
            (constructor X86NativeAssembly X86NativeAssemblyEmit
              (constructor X86NativeInstruction X86NativeTestRegister64
                (constructor X86NativeRegister64 X86NativeRDX)
                (constructor X86NativeRegister64 X86NativeRDX))
              (constructor X86NativeAssembly X86NativeAssemblyJumpCondition
                (constructor X86NativeCondition X86NativeConditionZero)
                nativePhysicalTrainingFence32TimeoutLabel
                (constructor X86NativeAssembly X86NativeAssemblyEmit
                  (constructor X86NativeInstruction X86NativeAddImmediate64
                    (constructor X86NativeRegister64 X86NativeRDX)
                    nativePhysicalNativeI32NegativeOne)
                  (constructor X86NativeAssembly X86NativeAssemblyJump
                    nativePhysicalTrainingFence32LoopLabel
                    (constructor X86NativeAssembly X86NativeAssemblyLabel
                      nativePhysicalTrainingFence32SuccessLabel
                      (constructor X86NativeAssembly X86NativeAssemblyEmit
                        (constructor X86NativeInstruction X86NativeClear32
                          (constructor X86NativeRegister64 X86NativeRAX))
                        (constructor X86NativeAssembly X86NativeAssemblyEmit
                          (constructor X86NativeInstruction X86NativeReturn)
                          (constructor X86NativeAssembly X86NativeAssemblyLabel
                            nativePhysicalTrainingFence32TimeoutLabel
                            (constructor X86NativeAssembly X86NativeAssemblyEmit
                              (constructor X86NativeInstruction X86NativeMoveImmediate32
                                (constructor X86NativeRegister64 X86NativeRAX)
                                nativePhysicalNativeI32NegativeOne)
                              (constructor X86NativeAssembly X86NativeAssemblyEmit
                                (constructor X86NativeInstruction X86NativeReturn)
                                (constructor X86NativeAssembly
                                  X86NativeAssemblyEnd))))))))))))))))

def nativePhysicalTrainingFence64Assembly =
  (constructor X86NativeAssembly X86NativeAssemblyLabel
    nativePhysicalTrainingFence64LoopLabel
    (constructor X86NativeAssembly X86NativeAssemblyEmit
      (constructor X86NativeInstruction X86NativeLoadMemory64
        (constructor X86NativeRegister64 X86NativeRAX)
        (constructor X86NativeRegister64 X86NativeRDI)
        nativePhysicalNativeD0)
      (constructor X86NativeAssembly X86NativeAssemblyEmit
        (constructor X86NativeInstruction X86NativeStoreMemory64
          (constructor X86NativeRegister64 X86NativeRCX)
          nativePhysicalNativeD0
          (constructor X86NativeRegister64 X86NativeRAX))
        (constructor X86NativeAssembly X86NativeAssemblyEmit
          (constructor X86NativeInstruction X86NativeCompareRegister64
            (constructor X86NativeRegister64 X86NativeRSI)
            (constructor X86NativeRegister64 X86NativeRAX))
          (constructor X86NativeAssembly X86NativeAssemblyJumpCondition
            (constructor X86NativeCondition X86NativeConditionZero)
            nativePhysicalTrainingFence64SuccessLabel
            (constructor X86NativeAssembly X86NativeAssemblyEmit
              (constructor X86NativeInstruction X86NativeTestRegister64
                (constructor X86NativeRegister64 X86NativeRDX)
                (constructor X86NativeRegister64 X86NativeRDX))
              (constructor X86NativeAssembly X86NativeAssemblyJumpCondition
                (constructor X86NativeCondition X86NativeConditionZero)
                nativePhysicalTrainingFence64TimeoutLabel
                (constructor X86NativeAssembly X86NativeAssemblyEmit
                  (constructor X86NativeInstruction X86NativeAddImmediate64
                    (constructor X86NativeRegister64 X86NativeRDX)
                    nativePhysicalNativeI32NegativeOne)
                  (constructor X86NativeAssembly X86NativeAssemblyJump
                    nativePhysicalTrainingFence64LoopLabel
                    (constructor X86NativeAssembly X86NativeAssemblyLabel
                      nativePhysicalTrainingFence64SuccessLabel
                      (constructor X86NativeAssembly X86NativeAssemblyEmit
                        (constructor X86NativeInstruction X86NativeClear32
                          (constructor X86NativeRegister64 X86NativeRAX))
                        (constructor X86NativeAssembly X86NativeAssemblyEmit
                          (constructor X86NativeInstruction X86NativeReturn)
                          (constructor X86NativeAssembly X86NativeAssemblyLabel
                            nativePhysicalTrainingFence64TimeoutLabel
                            (constructor X86NativeAssembly X86NativeAssemblyEmit
                              (constructor X86NativeInstruction X86NativeMoveImmediate32
                                (constructor X86NativeRegister64 X86NativeRAX)
                                nativePhysicalNativeI32NegativeOne)
                              (constructor X86NativeAssembly X86NativeAssemblyEmit
                                (constructor X86NativeInstruction X86NativeReturn)
                                (constructor X86NativeAssembly
                                  X86NativeAssemblyEnd))))))))))))))))

def nativePhysicalTrainingGenerateFence32Routine =
  (app x86NativeAssemble nativePhysicalTrainingFence32Assembly)

def nativePhysicalTrainingGenerateFence64Routine =
  (app x86NativeAssemble nativePhysicalTrainingFence64Assembly)

def nativePhysicalTrainingRoutineHostFallbacks =
  zero

def nativePhysicalTrainingCheckedBitPatchCarryLabel =
  b"addr-carry"

def nativePhysicalTrainingCheckedBitPatchRangeLabel =
  b"addr-range"

def nativePhysicalTrainingCheckedBitPatchAlignmentLabel =
  b"addr-align"

def nativePhysicalTrainingCheckedBitPatchAssemblyAppend =
  (lambda unrestricted assembly : (family X86NativeAssembly) .
    (lambda unrestricted tail : (family X86NativeAssembly) .
      (eliminate
        X86NativeAssembly
        (lambda unrestricted current : (family X86NativeAssembly) . (family X86NativeAssembly))
        assembly
        (branch X86NativeAssemblyEnd . tail)
        (branch
          X86NativeAssemblyEmit
          instruction
          rest
          induction
          .
          (constructor X86NativeAssembly X86NativeAssemblyEmit instruction induction))
        (branch
          X86NativeAssemblyLabel
          name
          rest
          induction
          .
          (constructor X86NativeAssembly X86NativeAssemblyLabel name induction))
        (branch
          X86NativeAssemblyJump
          target
          rest
          induction
          .
          (constructor X86NativeAssembly X86NativeAssemblyJump target induction))
        (branch
          X86NativeAssemblyJumpCondition
          condition
          target
          rest
          induction
          .
          (constructor X86NativeAssembly X86NativeAssemblyJumpCondition condition target induction))
        (branch
          X86NativeAssemblyLoadEffectiveAddressRIPLabel
          destination
          target
          rest
          induction
          .
          (constructor
            X86NativeAssembly
            X86NativeAssemblyLoadEffectiveAddressRIPLabel
            destination
            target
            induction)))))

def nativePhysicalTrainingCheckedBitPatchAssemblyGuard =
  (lambda unrestricted highMask : (family X86NativeImmediate64) .
    (lambda unrestricted alignmentMask : (family X86NativeImmediate64) .
      (lambda unrestricted body : (family X86NativeAssembly) .
        (constructor
          X86NativeAssembly
          X86NativeAssemblyEmit
          (constructor
            X86NativeInstruction
            X86NativeAddRegister64
            (constructor X86NativeRegister64 X86NativeRDX)
            (constructor X86NativeRegister64 X86NativeRSI))
          (constructor
            X86NativeAssembly
            X86NativeAssemblyJumpCondition
            (constructor X86NativeCondition X86NativeConditionBelow)
            nativePhysicalTrainingCheckedBitPatchCarryLabel
            (constructor
              X86NativeAssembly
              X86NativeAssemblyEmit
              (constructor
                X86NativeInstruction
                X86NativeMoveRegister64
                (constructor X86NativeRegister64 X86NativeRSI)
                (constructor X86NativeRegister64 X86NativeRCX))
              (constructor
                X86NativeAssembly
                X86NativeAssemblyEmit
                (constructor
                  X86NativeInstruction
                  X86NativeMoveImmediate64
                  (constructor X86NativeRegister64 X86NativeRDX)
                  highMask)
                (constructor
                  X86NativeAssembly
                  X86NativeAssemblyEmit
                  (constructor
                    X86NativeInstruction
                    X86NativeAndRegister64
                    (constructor X86NativeRegister64 X86NativeRDX)
                    (constructor X86NativeRegister64 X86NativeRCX))
                  (constructor
                    X86NativeAssembly
                    X86NativeAssemblyEmit
                    (constructor
                      X86NativeInstruction
                      X86NativeTestRegister64
                      (constructor X86NativeRegister64 X86NativeRCX)
                      (constructor X86NativeRegister64 X86NativeRCX))
                    (constructor
                      X86NativeAssembly
                      X86NativeAssemblyJumpCondition
                      (constructor X86NativeCondition X86NativeConditionNotZero)
                      nativePhysicalTrainingCheckedBitPatchRangeLabel
                      (constructor
                        X86NativeAssembly
                        X86NativeAssemblyEmit
                        (constructor
                          X86NativeInstruction
                          X86NativeMoveRegister64
                          (constructor X86NativeRegister64 X86NativeRSI)
                          (constructor X86NativeRegister64 X86NativeRCX))
                        (constructor
                          X86NativeAssembly
                          X86NativeAssemblyEmit
                          (constructor
                            X86NativeInstruction
                            X86NativeMoveImmediate64
                            (constructor X86NativeRegister64 X86NativeRDX)
                            alignmentMask)
                          (constructor
                            X86NativeAssembly
                            X86NativeAssemblyEmit
                            (constructor
                              X86NativeInstruction
                              X86NativeAndRegister64
                              (constructor X86NativeRegister64 X86NativeRDX)
                              (constructor X86NativeRegister64 X86NativeRCX))
                            (constructor
                              X86NativeAssembly
                              X86NativeAssemblyEmit
                              (constructor
                                X86NativeInstruction
                                X86NativeTestRegister64
                                (constructor X86NativeRegister64 X86NativeRCX)
                                (constructor X86NativeRegister64 X86NativeRCX))
                              (constructor
                                X86NativeAssembly
                                X86NativeAssemblyJumpCondition
                                (constructor X86NativeCondition X86NativeConditionNotZero)
                                nativePhysicalTrainingCheckedBitPatchAlignmentLabel
                                (app
                                  nativePhysicalTrainingCheckedBitPatchAssemblyAppend
                                  body
                                  (constructor
                                    X86NativeAssembly
                                    X86NativeAssemblyLabel
                                    nativePhysicalTrainingCheckedBitPatchCarryLabel
                                    (constructor
                                      X86NativeAssembly
                                      X86NativeAssemblyEmit
                                      (constructor
                                        X86NativeInstruction
                                        X86NativeMoveImmediate32
                                        (constructor X86NativeRegister64 X86NativeRAX)
                                        (app nativePhysicalNativeI32Byte (byte 1)))
                                      (constructor
                                        X86NativeAssembly
                                        X86NativeAssemblyEmit
                                        (constructor X86NativeInstruction X86NativeReturn)
                                        (constructor
                                        X86NativeAssembly
                                        X86NativeAssemblyLabel
                                        nativePhysicalTrainingCheckedBitPatchRangeLabel
                                        (constructor
                                        X86NativeAssembly
                                        X86NativeAssemblyEmit
                                        (constructor
                                        X86NativeInstruction
                                        X86NativeMoveImmediate32
                                        (constructor X86NativeRegister64 X86NativeRAX)
                                        (app nativePhysicalNativeI32Byte (byte 2)))
                                        (constructor
                                        X86NativeAssembly
                                        X86NativeAssemblyEmit
                                        (constructor X86NativeInstruction X86NativeReturn)
                                        (constructor
                                        X86NativeAssembly
                                        X86NativeAssemblyLabel
                                        nativePhysicalTrainingCheckedBitPatchAlignmentLabel
                                        (constructor
                                        X86NativeAssembly
                                        X86NativeAssemblyEmit
                                        (constructor
                                        X86NativeInstruction
                                        X86NativeMoveImmediate32
                                        (constructor X86NativeRegister64 X86NativeRAX)
                                        (app nativePhysicalNativeI32Byte (byte 3)))
                                        (constructor
                                        X86NativeAssembly
                                        X86NativeAssemblyEmit
                                        (constructor X86NativeInstruction X86NativeReturn)
                                        (constructor X86NativeAssembly X86NativeAssemblyEnd))))))))))))))))))))))))))

def nativePhysicalTrainingCheckedBitPatchRequire =
  (lambda unrestricted accepted : Nat .
    (lambda unrestricted error : (family NativePhysicalTrainingCheckedBitPatchParameterError) .
      (lambda unrestricted continuation : (pi unrestricted ignored : Nat . (family NativePhysicalTrainingCheckedBitPatchGeneration)) .
        (app
          (nat-eliminate
            (lambda unrestricted current : Nat .
              (pi unrestricted ignored : Nat .
                (family NativePhysicalTrainingCheckedBitPatchGeneration)))
            (lambda unrestricted ignored : Nat .
              (constructor
                NativePhysicalTrainingCheckedBitPatchGeneration
                NativePhysicalTrainingCheckedBitPatchParametersRejected
                error))
            (lambda unrestricted predecessor : Nat .
              (lambda unrestricted induction : (pi unrestricted ignored : Nat . (family NativePhysicalTrainingCheckedBitPatchGeneration)) .
                continuation))
            accepted)
          zero))))

def nativePhysicalTrainingCheckedBitPatchFieldFits =
  (lambda unrestricted shift : Nat .
    (lambda unrestricted width : Nat .
      (lambda unrestricted limit : Nat .
        (app
          (nat-eliminate
            (lambda unrestricted current : Nat . (pi unrestricted ignored : Nat . Nat))
            (lambda unrestricted ignored : Nat .
              (app naturalIsZero (nat-less-than (app naturalSaturatingSubtract limit width) shift)))
            (lambda unrestricted predecessor : Nat .
              (lambda unrestricted induction : (pi unrestricted ignored : Nat . Nat) .
                (lambda unrestricted ignored : Nat . zero)))
            (nat-less-than limit width))
          zero))))

def nativePhysicalTrainingGenerateCheckedAddressBitPatchRoutine =
  (lambda unrestricted destinationWidth : (family NativePhysicalTrainingBitPatchDestinationWidth) .
    (lambda unrestricted sourceShift : Nat .
      (lambda unrestricted destinationShift : Nat .
        (lambda unrestricted width : Nat .
          (lambda unrestricted addressBits : Nat .
            (lambda unrestricted alignmentBits : Nat .
              (app
                (lambda unrestricted destinationBits : Nat .
                  (app
                    nativePhysicalTrainingCheckedBitPatchRequire
                    (app naturalNonzero width)
                    (constructor
                      NativePhysicalTrainingCheckedBitPatchParameterError
                      NativePhysicalTrainingCheckedBitPatchWidthZero)
                    (lambda unrestricted ignored : Nat .
                      (app
                        nativePhysicalTrainingCheckedBitPatchRequire
                        (app
                          nativePhysicalTrainingCheckedBitPatchFieldFits
                          sourceShift
                          width
                          (byte-to-nat (byte 64)))
                        (constructor
                          NativePhysicalTrainingCheckedBitPatchParameterError
                          NativePhysicalTrainingCheckedBitPatchSourceBounds)
                        (lambda unrestricted ignored : Nat .
                          (app
                            nativePhysicalTrainingCheckedBitPatchRequire
                            (app
                              nativePhysicalTrainingCheckedBitPatchFieldFits
                              destinationShift
                              width
                              destinationBits)
                            (constructor
                              NativePhysicalTrainingCheckedBitPatchParameterError
                              NativePhysicalTrainingCheckedBitPatchDestinationBounds)
                            (lambda unrestricted ignored : Nat .
                              (app
                                nativePhysicalTrainingCheckedBitPatchRequire
                                (app
                                  naturalAnd
                                  (app naturalNonzero addressBits)
                                  (app naturalLessOrEqual addressBits (byte-to-nat (byte 64))))
                                (constructor
                                  NativePhysicalTrainingCheckedBitPatchParameterError
                                  NativePhysicalTrainingCheckedBitPatchAddressBits)
                                (lambda unrestricted ignored : Nat .
                                  (app
                                    nativePhysicalTrainingCheckedBitPatchRequire
                                    (app
                                      naturalAnd
                                      (nat-less-than alignmentBits (byte-to-nat (byte 64)))
                                      (app naturalLessOrEqual alignmentBits addressBits))
                                    (constructor
                                      NativePhysicalTrainingCheckedBitPatchParameterError
                                      NativePhysicalTrainingCheckedBitPatchAlignmentBits)
                                    (lambda unrestricted ignored : Nat .
                                      (constructor
                                        NativePhysicalTrainingCheckedBitPatchGeneration
                                        NativePhysicalTrainingCheckedBitPatchAssemblyGenerated
                                        (app
                                        x86NativeAssemble
                                        (app
                                        nativePhysicalTrainingCheckedBitPatchAssemblyGuard
                                        (app
                                        nativePhysicalTrainingImmediate64FromWord
                                        (app
                                        modelWord64Complement
                                        (app nativePhysicalTrainingBitMask addressBits)))
                                        (app
                                        nativePhysicalTrainingImmediate64FromWord
                                        (app nativePhysicalTrainingBitMask alignmentBits))
                                        (app
                                        nativePhysicalTrainingBitPatchAssembly
                                        destinationWidth
                                        sourceShift
                                        destinationShift
                                        width)))))))))))))))
                (eliminate
                  NativePhysicalTrainingBitPatchDestinationWidth
                  (lambda unrestricted current : (family NativePhysicalTrainingBitPatchDestinationWidth) .
                    Nat)
                  destinationWidth
                  (branch NativePhysicalTrainingBitPatchDestination32 . (byte-to-nat (byte 32)))
                  (branch NativePhysicalTrainingBitPatchDestination64 . (byte-to-nat (byte 64)))))))))))