module Runtime.NativeSocketRoutine

import Compiler.MachineX86Native
import Compiler.MachineX86NativeAssembly
import Runtime.NativePhysicalNative
import Data.Bytes
import Model.Word64
import Std.Natural

-- Linux x86-64 connected SOCK_STREAM transport. The caller owns a valid
-- buffer of extent bytes and one endpoint for the duration of this call.
-- ABI: rdi=fd, rsi=buffer, rdx=extent, rcx=poll timeout milliseconds,
-- r8=maximum poll/IO attempts. Return extent or a negative Linux errno.
-- A partial failure NEVER authorizes consumption or retry from the beginning:
-- abandon this edge/session; the caller must discard partial destination data.
--
-- Each attempt consumes budget, including EINTR/EAGAIN and partial progress.
-- Poll is bounded, and MSG_DONTWAIT prevents readiness races from blocking.
-- This bounds syscall attempts/wait intervals, not scheduler delay or a global
-- monotonic deadline. MSG_NOSIGNAL makes a broken send a returned error.
-- Sources: Linux man-pages recv(2), send(2), poll(2) (man7.org, 2026-10-02);
-- Linux x86-64 syscall ABI asm/unistd_64.h. No libc/vendor runtime is called.
-- These are platform facts; a different host ABI needs its own realization.
--
-- Preserve all SysV callee-saved registers used by the enclosing native VM.
-- Stack offsets belong to this layout; each follows the preceding field.
def nativeSocketWordBytes =
  (bytes-length (dataBytesWord64LE (modelWord64FromNaturalTruncated 0)))

def nativeSocketSaveRBX : Nat =
  0

def nativeSocketSaveRBP : Nat =
  (naturalAdd nativeSocketSaveRBX nativeSocketWordBytes)

def nativeSocketSaveR12 : Nat =
  (naturalAdd nativeSocketSaveRBP nativeSocketWordBytes)

def nativeSocketSaveR13 : Nat =
  (naturalAdd nativeSocketSaveR12 nativeSocketWordBytes)

def nativeSocketSaveR14 : Nat =
  (naturalAdd nativeSocketSaveR13 nativeSocketWordBytes)

def nativeSocketSaveR15 : Nat =
  (naturalAdd nativeSocketSaveR14 nativeSocketWordBytes)

def nativeSocketPollSlot =
  (naturalAdd nativeSocketSaveR15 nativeSocketWordBytes)

def nativeSocketPollFdBytes : Nat =
  4

def nativeSocketPollEventsBytes : Nat =
  2

def nativeSocketPollReturnedBytes : Nat =
  2

def nativeSocketPollEventsSlot =
  (naturalAdd nativeSocketPollSlot nativeSocketPollFdBytes)

def nativeSocketStackBytes =
  (naturalAdd
    nativeSocketPollSlot
    (naturalAdd
      nativeSocketPollFdBytes
      (naturalAdd nativeSocketPollEventsBytes nativeSocketPollReturnedBytes)))

def nativeSocketImmediate =
  x86NativeImmediate32FromNatural

def nativeSocketDisplacement =
  x86NativeDisplacement32FromNatural

def nativeSocketEntry =
  (lambda unrestricted tail : (family X86NativeAssembly) .
    (nativePhysicalNativeEmit
      (nativePhysicalNativeAddImmediate
        (constructor X86NativeRegister64 X86NativeRSP)
        (nativeSocketImmediate (naturalSaturatingSubtract 4294967296 nativeSocketStackBytes)))
      (nativePhysicalNativeEmit
        (nativePhysicalNativeStore64
          (constructor X86NativeRegister64 X86NativeRSP)
          (nativeSocketDisplacement nativeSocketSaveRBX)
          (constructor X86NativeRegister64 X86NativeRBX))
        (nativePhysicalNativeEmit
          (nativePhysicalNativeStore64
            (constructor X86NativeRegister64 X86NativeRSP)
            (nativeSocketDisplacement nativeSocketSaveRBP)
            (constructor X86NativeRegister64 X86NativeRBP))
          (nativePhysicalNativeEmit
            (nativePhysicalNativeStore64
              (constructor X86NativeRegister64 X86NativeRSP)
              (nativeSocketDisplacement nativeSocketSaveR12)
              (constructor X86NativeRegister64 X86NativeR12))
            (nativePhysicalNativeEmit
              (nativePhysicalNativeStore64
                (constructor X86NativeRegister64 X86NativeRSP)
                (nativeSocketDisplacement nativeSocketSaveR13)
                (constructor X86NativeRegister64 X86NativeR13))
              (nativePhysicalNativeEmit
                (nativePhysicalNativeStore64
                  (constructor X86NativeRegister64 X86NativeRSP)
                  (nativeSocketDisplacement nativeSocketSaveR14)
                  (constructor X86NativeRegister64 X86NativeR14))
                (nativePhysicalNativeEmit
                  (nativePhysicalNativeStore64
                    (constructor X86NativeRegister64 X86NativeRSP)
                    (nativeSocketDisplacement nativeSocketSaveR15)
                    (constructor X86NativeRegister64 X86NativeR15))
                  (nativePhysicalNativeEmit
                    (nativePhysicalNativeMove
                      (constructor X86NativeRegister64 X86NativeRDI)
                      (constructor X86NativeRegister64 X86NativeRBX))
                    (nativePhysicalNativeEmit
                      (nativePhysicalNativeMove
                        (constructor X86NativeRegister64 X86NativeRSI)
                        (constructor X86NativeRegister64 X86NativeR12))
                      (nativePhysicalNativeEmit
                        (nativePhysicalNativeMove
                          (constructor X86NativeRegister64 X86NativeRDX)
                          (constructor X86NativeRegister64 X86NativeR13))
                        (nativePhysicalNativeEmit
                          (nativePhysicalNativeMove
                            (constructor X86NativeRegister64 X86NativeRDX)
                            (constructor X86NativeRegister64 X86NativeRBP))
                          (nativePhysicalNativeEmit
                            (nativePhysicalNativeMove
                              (constructor X86NativeRegister64 X86NativeRCX)
                              (constructor X86NativeRegister64 X86NativeR14))
                            (nativePhysicalNativeEmit
                              (nativePhysicalNativeMove
                                (constructor X86NativeRegister64 X86NativeR8)
                                (constructor X86NativeRegister64 X86NativeR15))
                              (nativePhysicalNativeEmit
                                (nativePhysicalNativeCompareImmediate
                                  (constructor X86NativeRegister64 X86NativeRBX)
                                  (nativeSocketImmediate 2147483647))
                                (nativePhysicalNativeJumpCondition
                                  (constructor X86NativeCondition X86NativeConditionAbove)
                                  b"socket-invalid"
                                  (nativePhysicalNativeEmit
                                    (nativePhysicalNativeCompareImmediate
                                      (constructor X86NativeRegister64 X86NativeR14)
                                      (nativeSocketImmediate 2147483647))
                                    (nativePhysicalNativeJumpCondition
                                      (constructor X86NativeCondition X86NativeConditionAbove)
                                      b"socket-invalid"
                                      (nativePhysicalNativeEmit
                                        (nativePhysicalNativeTest
                                        (constructor X86NativeRegister64 X86NativeR13)
                                        (constructor X86NativeRegister64 X86NativeR13))
                                        (nativePhysicalNativeJumpCondition
                                        (constructor X86NativeCondition X86NativeConditionSign)
                                        b"socket-invalid"
                                        (nativePhysicalNativeEmit
                                        (nativePhysicalNativeMove
                                        (constructor X86NativeRegister64 X86NativeR12)
                                        (constructor X86NativeRegister64 X86NativeRAX))
                                        (nativePhysicalNativeEmit
                                        (nativePhysicalNativeAdd
                                        (constructor X86NativeRegister64 X86NativeR13)
                                        (constructor X86NativeRegister64 X86NativeRAX))
                                        (nativePhysicalNativeJumpCondition
                                        (constructor X86NativeCondition X86NativeConditionBelow)
                                        b"socket-invalid"
                                        tail)))))))))))))))))))))))

def nativeSocketPoll =
  (lambda unrestricted events : Nat .
    (lambda unrestricted tail : (family X86NativeAssembly) .
      (nativePhysicalNativeLabel
        b"socket-loop"
        (nativePhysicalNativeEmit
          (nativePhysicalNativeTest
            (constructor X86NativeRegister64 X86NativeR13)
            (constructor X86NativeRegister64 X86NativeR13))
          (nativePhysicalNativeJumpCondition
            (constructor X86NativeCondition X86NativeConditionZero)
            b"socket-success"
            (nativePhysicalNativeEmit
              (nativePhysicalNativeTest
                (constructor X86NativeRegister64 X86NativeR15)
                (constructor X86NativeRegister64 X86NativeR15))
              (nativePhysicalNativeJumpCondition
                (constructor X86NativeCondition X86NativeConditionZero)
                b"socket-timeout"
                (nativePhysicalNativeEmit
                  (nativePhysicalNativeAddImmediate
                    (constructor X86NativeRegister64 X86NativeR15)
                    (nativeSocketImmediate (naturalSaturatingSubtract 4294967296 1)))
                  (nativePhysicalNativeEmit
                    (nativePhysicalNativeStore64
                      (constructor X86NativeRegister64 X86NativeRSP)
                      (nativeSocketDisplacement nativeSocketPollSlot)
                      (constructor X86NativeRegister64 X86NativeRBX))
                    (nativePhysicalNativeEmit
                      (nativePhysicalNativeMoveImmediate32
                        (constructor X86NativeRegister64 X86NativeRAX)
                        (nativeSocketImmediate events))
                      (nativePhysicalNativeEmit
                        (nativePhysicalNativeStore8
                          (constructor X86NativeRegister64 X86NativeRSP)
                          (nativeSocketDisplacement nativeSocketPollEventsSlot)
                          (constructor X86NativeRegister64 X86NativeRAX))
                        (nativePhysicalNativeEmit
                          (nativePhysicalNativeMove
                            (constructor X86NativeRegister64 X86NativeRSP)
                            (constructor X86NativeRegister64 X86NativeRDI))
                          (nativePhysicalNativeEmit
                            (nativePhysicalNativeAddImmediate
                              (constructor X86NativeRegister64 X86NativeRDI)
                              (nativeSocketImmediate nativeSocketPollSlot))
                            (nativePhysicalNativeEmit
                              (nativePhysicalNativeMoveImmediate32
                                (constructor X86NativeRegister64 X86NativeRSI)
                                (nativeSocketImmediate 1))
                              (nativePhysicalNativeEmit
                                (nativePhysicalNativeMove
                                  (constructor X86NativeRegister64 X86NativeR14)
                                  (constructor X86NativeRegister64 X86NativeRDX))
                                (nativePhysicalNativeEmit
                                  (nativePhysicalNativeMoveImmediate32
                                    (constructor X86NativeRegister64 X86NativeRAX)
                                    (nativeSocketImmediate 7))
                                  (nativePhysicalNativeEmit
                                    nativePhysicalNativeSystemCallInstruction
                                    (nativePhysicalNativeEmit
                                      (nativePhysicalNativeCompareImmediate
                                        (constructor X86NativeRegister64 X86NativeRAX)
                                        (nativeSocketImmediate
                                        (naturalSaturatingSubtract 4294967296 4)))
                                      (nativePhysicalNativeJumpCondition
                                        (constructor X86NativeCondition X86NativeConditionZero)
                                        b"socket-loop"
                                        (nativePhysicalNativeEmit
                                        (nativePhysicalNativeTest
                                        (constructor X86NativeRegister64 X86NativeRAX)
                                        (constructor X86NativeRegister64 X86NativeRAX))
                                        (nativePhysicalNativeJumpCondition
                                        (constructor X86NativeCondition X86NativeConditionSign)
                                        b"socket-return"
                                        (nativePhysicalNativeJumpCondition
                                        (constructor X86NativeCondition X86NativeConditionZero)
                                        b"socket-timeout"
                                        tail))))))))))))))))))))))

def nativeSocketIO =
  (lambda unrestricted flags : Nat .
    (lambda unrestricted syscallNumber : Nat .
      (lambda unrestricted tail : (family X86NativeAssembly) .
        (nativePhysicalNativeEmit
          (nativePhysicalNativeMove
            (constructor X86NativeRegister64 X86NativeRBX)
            (constructor X86NativeRegister64 X86NativeRDI))
          (nativePhysicalNativeEmit
            (nativePhysicalNativeMove
              (constructor X86NativeRegister64 X86NativeR12)
              (constructor X86NativeRegister64 X86NativeRSI))
            (nativePhysicalNativeEmit
              (nativePhysicalNativeMove
                (constructor X86NativeRegister64 X86NativeR13)
                (constructor X86NativeRegister64 X86NativeRDX))
              (nativePhysicalNativeEmit
                (nativePhysicalNativeMoveImmediate32
                  (constructor X86NativeRegister64 X86NativeR10)
                  (nativeSocketImmediate flags))
                (nativePhysicalNativeEmit
                  (constructor
                    X86NativeInstruction
                    X86NativeClear32
                    (constructor X86NativeRegister64 X86NativeR8))
                  (nativePhysicalNativeEmit
                    (constructor
                      X86NativeInstruction
                      X86NativeClear32
                      (constructor X86NativeRegister64 X86NativeR9))
                    (nativePhysicalNativeEmit
                      (nativePhysicalNativeMoveImmediate32
                        (constructor X86NativeRegister64 X86NativeRAX)
                        (nativeSocketImmediate syscallNumber))
                      (nativePhysicalNativeEmit
                        nativePhysicalNativeSystemCallInstruction
                        (nativePhysicalNativeEmit
                          (nativePhysicalNativeCompareImmediate
                            (constructor X86NativeRegister64 X86NativeRAX)
                            (nativeSocketImmediate (naturalSaturatingSubtract 4294967296 4)))
                          (nativePhysicalNativeJumpCondition
                            (constructor X86NativeCondition X86NativeConditionZero)
                            b"socket-loop"
                            (nativePhysicalNativeEmit
                              (nativePhysicalNativeCompareImmediate
                                (constructor X86NativeRegister64 X86NativeRAX)
                                (nativeSocketImmediate (naturalSaturatingSubtract 4294967296 11)))
                              (nativePhysicalNativeJumpCondition
                                (constructor X86NativeCondition X86NativeConditionZero)
                                b"socket-loop"
                                (nativePhysicalNativeEmit
                                  (nativePhysicalNativeTest
                                    (constructor X86NativeRegister64 X86NativeRAX)
                                    (constructor X86NativeRegister64 X86NativeRAX))
                                  (nativePhysicalNativeJumpCondition
                                    (constructor X86NativeCondition X86NativeConditionSign)
                                    b"socket-return"
                                    (nativePhysicalNativeJumpCondition
                                      (constructor X86NativeCondition X86NativeConditionZero)
                                      b"socket-eof"
                                      (nativePhysicalNativeEmit
                                        (nativePhysicalNativeCompare
                                        (constructor X86NativeRegister64 X86NativeR13)
                                        (constructor X86NativeRegister64 X86NativeRAX))
                                        (nativePhysicalNativeJumpCondition
                                        (constructor X86NativeCondition X86NativeConditionAbove)
                                        b"socket-invalid"
                                        (nativePhysicalNativeEmit
                                        (nativePhysicalNativeAdd
                                        (constructor X86NativeRegister64 X86NativeRAX)
                                        (constructor X86NativeRegister64 X86NativeR12))
                                        (nativePhysicalNativeEmit
                                        (nativePhysicalNativeSubtract
                                        (constructor X86NativeRegister64 X86NativeRAX)
                                        (constructor X86NativeRegister64 X86NativeR13))
                                        (nativePhysicalNativeJump b"socket-loop" tail)))))))))))))))))))))))

def nativeSocketReturn =
  (lambda unrestricted tail : (family X86NativeAssembly) .
    (nativePhysicalNativeLabel
      b"socket-invalid"
      (nativePhysicalNativeEmit
        (constructor
          X86NativeInstruction
          X86NativeClear32
          (constructor X86NativeRegister64 X86NativeRAX))
        (nativePhysicalNativeEmit
          (nativePhysicalNativeAddImmediate
            (constructor X86NativeRegister64 X86NativeRAX)
            (nativeSocketImmediate (naturalSaturatingSubtract 4294967296 22)))
          (nativePhysicalNativeJump
            b"socket-return"
            (nativePhysicalNativeLabel
              b"socket-timeout"
              (nativePhysicalNativeEmit
                (constructor
                  X86NativeInstruction
                  X86NativeClear32
                  (constructor X86NativeRegister64 X86NativeRAX))
                (nativePhysicalNativeEmit
                  (nativePhysicalNativeAddImmediate
                    (constructor X86NativeRegister64 X86NativeRAX)
                    (nativeSocketImmediate (naturalSaturatingSubtract 4294967296 110)))
                  (nativePhysicalNativeJump
                    b"socket-return"
                    (nativePhysicalNativeLabel
                      b"socket-eof"
                      (nativePhysicalNativeEmit
                        (constructor
                          X86NativeInstruction
                          X86NativeClear32
                          (constructor X86NativeRegister64 X86NativeRAX))
                        (nativePhysicalNativeEmit
                          (nativePhysicalNativeAddImmediate
                            (constructor X86NativeRegister64 X86NativeRAX)
                            (nativeSocketImmediate (naturalSaturatingSubtract 4294967296 61)))
                          (nativePhysicalNativeJump
                            b"socket-return"
                            (nativePhysicalNativeLabel
                              b"socket-success"
                              (nativePhysicalNativeEmit
                                (nativePhysicalNativeMove
                                  (constructor X86NativeRegister64 X86NativeRBP)
                                  (constructor X86NativeRegister64 X86NativeRAX))
                                (nativePhysicalNativeLabel
                                  b"socket-return"
                                  (nativePhysicalNativeEmit
                                    (nativePhysicalNativeLoad64
                                      (constructor X86NativeRegister64 X86NativeRBX)
                                      (constructor X86NativeRegister64 X86NativeRSP)
                                      (nativeSocketDisplacement nativeSocketSaveRBX))
                                    (nativePhysicalNativeEmit
                                      (nativePhysicalNativeLoad64
                                        (constructor X86NativeRegister64 X86NativeRBP)
                                        (constructor X86NativeRegister64 X86NativeRSP)
                                        (nativeSocketDisplacement nativeSocketSaveRBP))
                                      (nativePhysicalNativeEmit
                                        (nativePhysicalNativeLoad64
                                        (constructor X86NativeRegister64 X86NativeR12)
                                        (constructor X86NativeRegister64 X86NativeRSP)
                                        (nativeSocketDisplacement nativeSocketSaveR12))
                                        (nativePhysicalNativeEmit
                                        (nativePhysicalNativeLoad64
                                        (constructor X86NativeRegister64 X86NativeR13)
                                        (constructor X86NativeRegister64 X86NativeRSP)
                                        (nativeSocketDisplacement nativeSocketSaveR13))
                                        (nativePhysicalNativeEmit
                                        (nativePhysicalNativeLoad64
                                        (constructor X86NativeRegister64 X86NativeR14)
                                        (constructor X86NativeRegister64 X86NativeRSP)
                                        (nativeSocketDisplacement nativeSocketSaveR14))
                                        (nativePhysicalNativeEmit
                                        (nativePhysicalNativeLoad64
                                        (constructor X86NativeRegister64 X86NativeR15)
                                        (constructor X86NativeRegister64 X86NativeRSP)
                                        (nativeSocketDisplacement nativeSocketSaveR15))
                                        (nativePhysicalNativeEmit
                                        (nativePhysicalNativeAddImmediate
                                        (constructor X86NativeRegister64 X86NativeRSP)
                                        (nativeSocketImmediate nativeSocketStackBytes))
                                        (nativePhysicalNativeEmit
                                        nativePhysicalNativeReturnInstruction
                                        tail))))))))))))))))))))))))

-- ADD's signed imm32 produces the full negative 64-bit errno; MOV r32 would
-- zero-extend it and turn our synthetic failures into positive byte counts.
def nativeSocketReadAssembly =
  (nativeSocketEntry
    (nativeSocketPoll
      1
      (nativeSocketIO
        64
        45
        (nativeSocketReturn (constructor X86NativeAssembly X86NativeAssemblyEnd)))))

def nativeSocketWriteAssembly =
  (nativeSocketEntry
    (nativeSocketPoll
      4
      (nativeSocketIO
        (naturalAdd 64 16384)
        44
        (nativeSocketReturn (constructor X86NativeAssembly X86NativeAssemblyEnd)))))

def nativeSocketReadCode =
  (compiler-native-encode (family X86NativeAssembly) nativeSocketReadAssembly)

def nativeSocketWriteCode =
  (compiler-native-encode (family X86NativeAssembly) nativeSocketWriteAssembly)