Runtime.SocketAddress

1module Runtime.SocketAddress
2
3import Data.Bytes
4import Std.Byte
5import Std.Foundation
6import Std.Natural
7
8family IPv4Address : Type 0
9constructor IPv4AddressOf
10field unrestricted ipv4First : Byte
11field unrestricted ipv4Second : Byte
12field unrestricted ipv4Third : Byte
13field unrestricted ipv4Fourth : Byte
14
15end-family
16
17family SocketAddressFailure : Type 0
18constructor SocketAddressPortOutOfRange
19
20end-family
21
22-- Linux sockaddr_in: native little-endian sa_family_t, network-endian port
23-- and address, then eight zero padding bytes. These are platform ABI facts,
24-- not a learning wire representation. Other platforms must realize their own
25-- address layout. Source: Linux UAPI linux/in.h and ip(7), 2026-10-02.
26def linuxIPv4Family : Nat =
27  2
28
29def linuxIPv4FamilyBytes : Bytes =
30  (bytes-cons (nat-to-byte linuxIPv4Family) (bytes 0))
31
32def linuxIPv4PortBytes : Nat =
33  2
34
35def linuxIPv4AddressBytes : Nat =
36  4
37
38def linuxIPv4Padding : Bytes =
39  (dataBytesRepeatByte (byte 0) 8)
40
41def linuxIPv4PortAt =
42  (bytes-length linuxIPv4FamilyBytes)
43
44def linuxIPv4AddressAt =
45  (naturalAdd linuxIPv4PortAt linuxIPv4PortBytes)
46
47def linuxIPv4PaddingAt =
48  (naturalAdd linuxIPv4AddressAt linuxIPv4AddressBytes)
49
50def linuxIPv4SocketAddressBytes =
51  (naturalAdd linuxIPv4PaddingAt (bytes-length linuxIPv4Padding))
52
53def ipv4Loopback =
54  (constructor IPv4Address IPv4AddressOf (byte 127) (byte 0) (byte 0) (byte 1))
55
56def ipv4Bytes =
57  (lambda unrestricted address : (family IPv4Address) .
58    (eliminate
59      IPv4Address
60      (lambda unrestricted current : (family IPv4Address) . Bytes)
61      address
62      (branch
63        IPv4AddressOf
64        a
65        b
66        c
67        d
68        .
69        (bytes-cons a (bytes-cons b (bytes-cons c (bytes-cons d b"")))))))
70
71def linuxIPv4SocketAddress =
72  (lambda unrestricted address : (family IPv4Address) .
73    (lambda unrestricted port : Nat .
74      (nat-eliminate
75        (lambda unrestricted ok : Nat . (family StdResult (family SocketAddressFailure) Bytes))
76        (constructor
77          StdResult
78          StdFailure
79          (family SocketAddressFailure)
80          Bytes
81          (constructor SocketAddressFailure SocketAddressPortOutOfRange))
82        (lambda unrestricted previous : Nat .
83          (lambda unrestricted ignored : (family StdResult (family SocketAddressFailure) Bytes) .
84            (constructor
85              StdResult
86              StdSuccess
87              (family SocketAddressFailure)
88              Bytes
89              (bytes-append
90                linuxIPv4FamilyBytes
91                (bytes-cons
92                  (nat-to-byte (naturalDivideUnchecked port 256))
93                  (bytes-cons
94                    (nat-to-byte (naturalModuloUnchecked port 256))
95                    (bytes-append (ipv4Bytes address) linuxIPv4Padding)))))))
96        (naturalLessOrEqual port 65535))))