module Runtime.NativeSocketPlan

import Runtime.NativeDescriptor
import Runtime.NativeSocketRoutine
import Runtime.NativeSocketEndpoint
import Runtime.SocketAddress
import Runtime.NativePhysicalProgram
import Runtime.NativeLaunchRecipeLoad
import Model.Word64
import Std.Natural

-- Target-local lowering of a bounded stream operation into the existing
-- native program. Admission/liveness owns the buffer extent. The caller must
-- assert the exact count before publishing destination visibility. Failures
-- can leave a partial prefix and require abandonment of this edge/session.
-- This declares the Linux x86-64 ABI. AArch64 HostLowering maps connected
-- stream IO to its native realization; endpoint establishment still requires
-- its own target support and is refused when that lowering is unavailable.
def nativeSocketOperation =
  (lambda unrestricted code : Bytes .
    (lambda unrestricted descriptor : (family NativePhysicalOperand) .
      (lambda unrestricted buffer : (family NativePhysicalOperand) .
        (lambda unrestricted extent : (family NativePhysicalOperand) .
          (lambda unrestricted timeoutMilliseconds : (family NativePhysicalOperand) .
            (lambda unrestricted attempts : (family NativePhysicalOperand) .
              (lambda unrestricted result : (family NativePhysicalResultBinding) .
                (constructor
                  NativePhysicalOperation
                  NativePhysicalMachineRoutine
                  code
                  (constructor
                    NativePhysicalArguments
                    NativePhysicalArgumentsValue
                    descriptor
                    buffer
                    extent
                    timeoutMilliseconds
                    attempts
                    (constructor
                      NativePhysicalOperand
                      NativePhysicalImmediate
                      (modelWord64FromNaturalTruncated 0)))
                  result))))))))

def nativeSocketRead =
  (nativeSocketOperation nativeSocketReadCode)

def nativeSocketWrite =
  (nativeSocketOperation nativeSocketWriteCode)

-- Endpoint operations speak the same Linux x86-64 ABI as stream IO. The
-- program owns every produced descriptor and must close it at session end.
-- Creation/accept use NONBLOCK|CLOEXEC atomically; connect/accept also check
-- NONBLOCK before entering a readiness race. Failure requires abandonment.
def nativeSocketConnect =
  (nativeSocketOperation nativeSocketConnectCode)

def nativeSocketAccept =
  (lambda unrestricted listener : (family NativePhysicalOperand) .
    (lambda unrestricted timeout : (family NativePhysicalOperand) .
      (lambda unrestricted attempts : (family NativePhysicalOperand) .
        (nativeSocketOperation
          nativeSocketAcceptCode
          listener
          (nativeLaunchRecipeImmediate 0)
          (nativeLaunchRecipeImmediate 1)
          timeout
          attempts))))

def nativeSocketDescriptorStatus =
  (lambda unrestricted descriptor : (family NativePhysicalOperand) .
    (nativeSocketOperation
      nativeSocketDescriptorStatusCode
      descriptor
      (nativeLaunchRecipeImmediate 0)
      (nativeLaunchRecipeImmediate 0)
      (nativeLaunchRecipeImmediate 0)
      (nativeLaunchRecipeImmediate 0)))

def nativeSocketSystemCall =
  (lambda unrestricted number : Nat .
    (lambda unrestricted arguments : (family NativePhysicalArguments) .
      (lambda unrestricted result : (family NativePhysicalResultBinding) .
        (constructor
          NativePhysicalOperation
          NativePhysicalSystemCall
          (nativeLaunchRecipeImmediate number)
          arguments
          b""
          result))))

def nativeSocketCreateIPv4 =
  (nativeSocketSystemCall
    41
    (nativeLaunchRecipeArguments
      (nativeLaunchRecipeImmediate linuxIPv4Family)
      (nativeLaunchRecipeImmediate (naturalAdd 1 nativeSocketEndpointFlags))
      (nativeLaunchRecipeImmediate 0)
      (nativeLaunchRecipeImmediate 0)))

-- Explicit latency policy for small request/acknowledgment frames. Linux TCP
-- may otherwise delay the separate digest write behind unacknowledged bytes.
-- The option is per socket, never a host-wide network setting. The caller
-- supplies a Linux int (0 or 1) at valueAddress and checks the syscall result.
-- Linux UAPI: IPPROTO_TCP=6, TCP_NODELAY=1, sizeof(int)=4 on this ABI.
-- https://man7.org/linux/man-pages/man7/tcp.7.html (TCP_NODELAY)
-- https://man7.org/linux/man-pages/man2/setsockopt.2.html
def nativeSocketNoDelay =
  (lambda unrestricted descriptor : (family NativePhysicalOperand) .
    (lambda unrestricted valueAddress : (family NativePhysicalOperand) .
      (nativeSocketSystemCall
        54
        (constructor
          NativePhysicalArguments
          NativePhysicalArgumentsValue
          descriptor
          (nativeLaunchRecipeImmediate 6)
          (nativeLaunchRecipeImmediate 1)
          valueAddress
          (nativeLaunchRecipeImmediate 4)
          (nativeLaunchRecipeImmediate 0)))))

def nativeSocketBindIPv4 =
  (lambda unrestricted descriptor : (family NativePhysicalOperand) .
    (lambda unrestricted address : (family NativePhysicalOperand) .
      (nativeSocketSystemCall
        49
        (nativeLaunchRecipeArguments
          descriptor
          address
          (nativeLaunchRecipeImmediate linuxIPv4SocketAddressBytes)
          (nativeLaunchRecipeImmediate 0)))))

def nativeSocketListen =
  (lambda unrestricted descriptor : (family NativePhysicalOperand) .
    (lambda unrestricted backlog : (family NativePhysicalOperand) .
      (nativeSocketSystemCall
        50
        (nativeLaunchRecipeArguments
          descriptor
          backlog
          (nativeLaunchRecipeImmediate 0)
          (nativeLaunchRecipeImmediate 0)))))

def nativeSocketLocalAddress =
  (lambda unrestricted descriptor : (family NativePhysicalOperand) .
    (lambda unrestricted address : (family NativePhysicalOperand) .
      (lambda unrestricted lengthAddress : (family NativePhysicalOperand) .
        (nativeSocketSystemCall
          51
          (nativeLaunchRecipeArguments
            descriptor
            address
            lengthAddress
            (nativeLaunchRecipeImmediate 0))))))

def nativeSocketClose =
  (lambda unrestricted descriptor : (family NativePhysicalOperand) .
    (nativeSocketSystemCall
      3
      (nativeLaunchRecipeArguments
        descriptor
        (nativeLaunchRecipeImmediate 0)
        (nativeLaunchRecipeImmediate 0)
        (nativeLaunchRecipeImmediate 0))))

def nativeSocketRequireDescriptor =
  nativeDescriptorRequire

def nativeSocketRequireZero =
  (lambda unrestricted operation : (family NativePhysicalOperation) .
    (lambda unrestricted scratchSlot : Nat .
      (lambda unrestricted error : Bytes .
        (lambda unrestricted tail : (family NativePhysicalCommands) .
          (nativeLaunchRecipeCommand
            operation
            error
            (nativeLaunchRecipeAssertEqual
              (nativeLaunchRecipeSlotValue scratchSlot)
              (nativeLaunchRecipeImmediate 0)
              error
              tail))))))

def nativeSocketOpenIPv4 =
  (lambda unrestricted descriptorSlot : Nat .
    (lambda unrestricted scratchSlot : Nat .
      (lambda unrestricted tail : (family NativePhysicalCommands) .
        (nativeLaunchRecipeCommand
          (nativeSocketCreateIPv4 (nativeLaunchRecipeStore descriptorSlot))
          b"socket-create"
          (nativeSocketRequireDescriptor
            (nativeLaunchRecipeSlotValue descriptorSlot)
            scratchSlot
            b"socket-create"
            tail)))))

def nativeSocketBindListener =
  (lambda unrestricted descriptor : (family NativePhysicalOperand) .
    (lambda unrestricted address : (family NativePhysicalOperand) .
      (lambda unrestricted backlog : (family NativePhysicalOperand) .
        (lambda unrestricted scratchSlot : Nat .
          (lambda unrestricted tail : (family NativePhysicalCommands) .
            (nativeSocketRequireZero
              (nativeSocketBindIPv4 descriptor address (nativeLaunchRecipeStore scratchSlot))
              scratchSlot
              b"socket-bind"
              (nativeSocketRequireZero
                (nativeSocketListen descriptor backlog (nativeLaunchRecipeStore scratchSlot))
                scratchSlot
                b"socket-listen"
                tail)))))))

def nativeSocketConnectChecked =
  (lambda unrestricted descriptor : (family NativePhysicalOperand) .
    (lambda unrestricted address : (family NativePhysicalOperand) .
      (lambda unrestricted timeout : (family NativePhysicalOperand) .
        (lambda unrestricted attempts : (family NativePhysicalOperand) .
          (lambda unrestricted scratchSlot : Nat .
            (nativeSocketRequireZero
              (nativeSocketConnect
                descriptor
                address
                (nativeLaunchRecipeImmediate linuxIPv4SocketAddressBytes)
                timeout
                attempts
                (nativeLaunchRecipeStore scratchSlot))
              scratchSlot
              b"socket-connect"))))))

def nativeSocketAcceptChecked =
  (lambda unrestricted listener : (family NativePhysicalOperand) .
    (lambda unrestricted timeout : (family NativePhysicalOperand) .
      (lambda unrestricted attempts : (family NativePhysicalOperand) .
        (lambda unrestricted descriptorSlot : Nat .
          (lambda unrestricted scratchSlot : Nat .
            (lambda unrestricted tail : (family NativePhysicalCommands) .
              (nativeLaunchRecipeCommand
                (nativeSocketAccept
                  listener
                  timeout
                  attempts
                  (nativeLaunchRecipeStore descriptorSlot))
                b"socket-accept"
                (nativeSocketRequireDescriptor
                  (nativeLaunchRecipeSlotValue descriptorSlot)
                  scratchSlot
                  b"socket-accept"
                  tail))))))))

def nativeSocketCloseChecked =
  (lambda unrestricted descriptor : (family NativePhysicalOperand) .
    (lambda unrestricted scratchSlot : Nat .
      (nativeSocketRequireZero
        (nativeSocketClose descriptor (nativeLaunchRecipeStore scratchSlot))
        scratchSlot
        b"socket-close")))