module Runtime.NativeMemoryRoutine

import Compiler.MachineX86Native
import Compiler.MachineX86NativeAssembly
import Data.SHA256Digest
import Runtime.NativePhysicalNative

family NativeMemoryRoutineErrorCode : Type 0
constructor NativeMemoryRoutineDuplicateLabel
field unrestricted nativeMemoryRoutineDuplicateLabelName : Bytes
constructor NativeMemoryRoutineOffsetOverflow
constructor NativeMemoryRoutineMissingLabel
field unrestricted nativeMemoryRoutineMissingLabelName : Bytes
constructor NativeMemoryRoutineDisplacementOutOfRange
field unrestricted nativeMemoryRoutineDistantLabelName : Bytes

end-family

family NativeMemoryRoutineTelemetry : Type 0
constructor NativeMemoryRoutineTelemetryValue
field unrestricted nativeMemoryRoutineTelemetryInstructions : Nat
field unrestricted nativeMemoryRoutineTelemetryCodeBytes : Nat
field unrestricted nativeMemoryRoutineTelemetryFailures : Nat
field unrestricted nativeMemoryRoutineTelemetryFallbacks : Nat
field unrestricted nativeMemoryRoutineTelemetryCodeSHA256 : Bytes
field unrestricted nativeMemoryRoutineTelemetryLastError : Bytes

end-family

family NativeMemoryRoutine : Type 0
constructor NativeMemoryRoutineValue
field unrestricted nativeMemoryRoutineCode : Bytes
field unrestricted nativeMemoryRoutineCodeSHA256 : Bytes
field unrestricted nativeMemoryRoutineInstructionCount : Nat
field unrestricted nativeMemoryRoutineTelemetry : (family NativeMemoryRoutineTelemetry)

end-family

family NativeMemoryRoutineResult : Type 0
constructor NativeMemoryRoutineGenerated
field unrestricted nativeMemoryGeneratedRoutine : (family NativeMemoryRoutine)
field unrestricted nativeMemoryRoutineSuccessTelemetry : (family NativeMemoryRoutineTelemetry)
constructor NativeMemoryRoutineGenerationFailed
field unrestricted nativeMemoryRoutineGenerationError : (family NativeMemoryRoutineErrorCode)
field unrestricted nativeMemoryRoutineFailureTelemetry : (family NativeMemoryRoutineTelemetry)

end-family

def nativeMemoryRoutineErrorCodeBytes =
  (lambda unrestricted code : (family NativeMemoryRoutineErrorCode) .
    (eliminate
      NativeMemoryRoutineErrorCode
      (lambda unrestricted current : (family NativeMemoryRoutineErrorCode) . Bytes)
      code
      (branch
        NativeMemoryRoutineDuplicateLabel
        labelName
        .
        (bytes-append b"ALPHA-MEM-001-" labelName))
      (branch NativeMemoryRoutineOffsetOverflow . b"ALPHA-MEM-002")
      (branch
        NativeMemoryRoutineMissingLabel
        labelName
        .
        (bytes-append b"ALPHA-MEM-003-" labelName))
      (branch
        NativeMemoryRoutineDisplacementOutOfRange
        labelName
        .
        (bytes-append b"ALPHA-MEM-004-" labelName))))

def nativeMemoryRoutineLabelEntry : Bytes =
  b"mem-entry"

def nativeMemoryRoutineLabelLoop : Bytes =
  b"mem-loop"

def nativeMemoryRoutineLabelDone : Bytes =
  b"mem-done"

def nativeMemoryCopyInstructionCount : Nat =
  (byte-to-nat (byte 11))

def nativeMemoryCopyAssembly : (family X86NativeAssembly) =
  (nativePhysicalNativeLabel
    nativeMemoryRoutineLabelEntry
    (nativePhysicalNativeEmit
      (nativePhysicalNativeTest
        (constructor X86NativeRegister64 X86NativeRDX)
        (constructor X86NativeRegister64 X86NativeRDX))
      (nativePhysicalNativeJumpCondition
        (constructor X86NativeCondition X86NativeConditionZero)
        nativeMemoryRoutineLabelDone
        (nativePhysicalNativeLabel
          nativeMemoryRoutineLabelLoop
          (nativePhysicalNativeEmit
            (nativePhysicalNativeLoad8
              (constructor X86NativeRegister64 X86NativeRAX)
              (constructor X86NativeRegister64 X86NativeRSI)
              nativePhysicalNativeD0)
            (nativePhysicalNativeEmit
              (nativePhysicalNativeStore8
                (constructor X86NativeRegister64 X86NativeRDI)
                nativePhysicalNativeD0
                (constructor X86NativeRegister64 X86NativeRAX))
              (nativePhysicalNativeEmit
                (nativePhysicalNativeAddImmediate
                  (constructor X86NativeRegister64 X86NativeRSI)
                  (nativePhysicalNativeI32Byte (byte 1)))
                (nativePhysicalNativeEmit
                  (nativePhysicalNativeAddImmediate
                    (constructor X86NativeRegister64 X86NativeRDI)
                    (nativePhysicalNativeI32Byte (byte 1)))
                  (nativePhysicalNativeEmit
                    (nativePhysicalNativeAddImmediate
                      (constructor X86NativeRegister64 X86NativeRDX)
                      nativePhysicalNativeI32NegativeOne)
                    (nativePhysicalNativeEmit
                      (nativePhysicalNativeTest
                        (constructor X86NativeRegister64 X86NativeRDX)
                        (constructor X86NativeRegister64 X86NativeRDX))
                      (nativePhysicalNativeJumpCondition
                        (constructor X86NativeCondition X86NativeConditionNotZero)
                        nativeMemoryRoutineLabelLoop
                        (nativePhysicalNativeLabel
                          nativeMemoryRoutineLabelDone
                          (nativePhysicalNativeEmit
                            (constructor
                              X86NativeInstruction
                              X86NativeClear32
                              (constructor X86NativeRegister64 X86NativeRAX))
                            (nativePhysicalNativeEmit
                              nativePhysicalNativeReturnInstruction
                              (constructor X86NativeAssembly X86NativeAssemblyEnd)))))))))))))))

def nativeMemoryRoutineTelemetrySuccess =
  (lambda unrestricted code : Bytes .
    (lambda unrestricted digest : Bytes .
      (constructor
        NativeMemoryRoutineTelemetry
        NativeMemoryRoutineTelemetryValue
        nativeMemoryCopyInstructionCount
        (bytes-length code)
        zero
        zero
        digest
        b"")))

def nativeMemoryRoutineTelemetryFailure =
  (lambda unrestricted error : (family NativeMemoryRoutineErrorCode) .
    (constructor
      NativeMemoryRoutineTelemetry
      NativeMemoryRoutineTelemetryValue
      nativeMemoryCopyInstructionCount
      zero
      (succ zero)
      zero
      b""
      (nativeMemoryRoutineErrorCodeBytes error)))

def nativeMemoryRoutineFail =
  (lambda unrestricted error : (family NativeMemoryRoutineErrorCode) .
    (constructor
      NativeMemoryRoutineResult
      NativeMemoryRoutineGenerationFailed
      error
      (nativeMemoryRoutineTelemetryFailure error)))

-- Generation remains pure and byte-identical, but is requested by the
-- actual lowering consumer rather than performed when this module is loaded.
def nativeMemoryGenerateCopyRoutine :
  (pi unrestricted request : Nat . (family NativeMemoryRoutineResult)) =
  (lambda unrestricted request : Nat .
    (eliminate
      X86NativeAssemblyResult
      (lambda unrestricted current : (family X86NativeAssemblyResult) .
        (family NativeMemoryRoutineResult))
      (x86NativeAssemble nativeMemoryCopyAssembly)
      (branch
        X86NativeAssemblyEncoded
        code
        .
        (app
          (lambda unrestricted digest : Bytes .
            (app
              (lambda unrestricted telemetry : (family NativeMemoryRoutineTelemetry) .
                (constructor
                  NativeMemoryRoutineResult
                  NativeMemoryRoutineGenerated
                  (constructor
                    NativeMemoryRoutine
                    NativeMemoryRoutineValue
                    code
                    digest
                    nativeMemoryCopyInstructionCount
                    telemetry)
                  telemetry))
              (nativeMemoryRoutineTelemetrySuccess code digest)))
          (sha256HexBytesOrEmpty (sha256Hex code))))
      (branch
        X86NativeAssemblyEncodeDuplicateLabel
        duplicateName
        .
        (nativeMemoryRoutineFail
          (constructor NativeMemoryRoutineErrorCode NativeMemoryRoutineDuplicateLabel duplicateName)))
      (branch
        X86NativeAssemblyEncodeOffsetOverflow
        .
        (nativeMemoryRoutineFail
          (constructor NativeMemoryRoutineErrorCode NativeMemoryRoutineOffsetOverflow)))
      (branch
        X86NativeAssemblyMissingLabel
        missingName
        .
        (nativeMemoryRoutineFail
          (constructor NativeMemoryRoutineErrorCode NativeMemoryRoutineMissingLabel missingName)))
      (branch
        X86NativeAssemblyDisplacementOutOfRange
        distantName
        .
        (nativeMemoryRoutineFail
          (constructor
            NativeMemoryRoutineErrorCode
            NativeMemoryRoutineDisplacementOutOfRange
            distantName)))))