module Runtime.SocketAddress

import Data.Bytes
import Std.Byte
import Std.Foundation
import Std.Natural

family IPv4Address : Type 0
constructor IPv4AddressOf
field unrestricted ipv4First : Byte
field unrestricted ipv4Second : Byte
field unrestricted ipv4Third : Byte
field unrestricted ipv4Fourth : Byte

end-family

family SocketAddressFailure : Type 0
constructor SocketAddressPortOutOfRange

end-family

-- Linux sockaddr_in: native little-endian sa_family_t, network-endian port
-- and address, then eight zero padding bytes. These are platform ABI facts,
-- not a learning wire representation. Other platforms must realize their own
-- address layout. Source: Linux UAPI linux/in.h and ip(7), 2026-10-02.
def linuxIPv4Family : Nat =
  2

def linuxIPv4FamilyBytes : Bytes =
  (bytes-cons (nat-to-byte linuxIPv4Family) (bytes 0))

def linuxIPv4PortBytes : Nat =
  2

def linuxIPv4AddressBytes : Nat =
  4

def linuxIPv4Padding : Bytes =
  (dataBytesRepeatByte (byte 0) 8)

def linuxIPv4PortAt =
  (bytes-length linuxIPv4FamilyBytes)

def linuxIPv4AddressAt =
  (naturalAdd linuxIPv4PortAt linuxIPv4PortBytes)

def linuxIPv4PaddingAt =
  (naturalAdd linuxIPv4AddressAt linuxIPv4AddressBytes)

def linuxIPv4SocketAddressBytes =
  (naturalAdd linuxIPv4PaddingAt (bytes-length linuxIPv4Padding))

def ipv4Loopback =
  (constructor IPv4Address IPv4AddressOf (byte 127) (byte 0) (byte 0) (byte 1))

def ipv4Bytes =
  (lambda unrestricted address : (family IPv4Address) .
    (eliminate
      IPv4Address
      (lambda unrestricted current : (family IPv4Address) . Bytes)
      address
      (branch
        IPv4AddressOf
        a
        b
        c
        d
        .
        (bytes-cons a (bytes-cons b (bytes-cons c (bytes-cons d b"")))))))

def linuxIPv4SocketAddress =
  (lambda unrestricted address : (family IPv4Address) .
    (lambda unrestricted port : Nat .
      (nat-eliminate
        (lambda unrestricted ok : Nat . (family StdResult (family SocketAddressFailure) Bytes))
        (constructor
          StdResult
          StdFailure
          (family SocketAddressFailure)
          Bytes
          (constructor SocketAddressFailure SocketAddressPortOutOfRange))
        (lambda unrestricted previous : Nat .
          (lambda unrestricted ignored : (family StdResult (family SocketAddressFailure) Bytes) .
            (constructor
              StdResult
              StdSuccess
              (family SocketAddressFailure)
              Bytes
              (bytes-append
                linuxIPv4FamilyBytes
                (bytes-cons
                  (nat-to-byte (naturalDivideUnchecked port 256))
                  (bytes-cons
                    (nat-to-byte (naturalModuloUnchecked port 256))
                    (bytes-append (ipv4Bytes address) linuxIPv4Padding)))))))
        (naturalLessOrEqual port 65535))))