feat: Std.Net.Addr (#6563)

This PR implements `Std.Net.Addr` which contains structures around IP
and socket addresses.

While we could implement our own parser instead of going through the
`addr_in`/`addr_in6` route we will need to implement these conversions
to make proper system calls anyway. Hence this is likely the approach
with the least amount of non trivial code overall. The only thing I am
uncertain about is whether `ofString` should return `Option` or
`Except`, unfortunately `libuv` doesn't hand out error messages on IP
parsing.

src/Std.lean

@@ -10,3 +10,4 @@ import Std.Sync
 import Std.Time
 import Std.Tactic
 import Std.Internal
+import Std.Net

src/Std/Net.lean

@@ -0,0 +1,7 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+prelude
+import Std.Net.Addr

src/Std/Net/Addr.lean

@@ -0,0 +1,197 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+prelude
+import Init.Data.Vector.Basic
+
+/-!
+This module contains Lean representations of IP and socket addresses:
+- `IPv4Addr`: Representing IPv4 addresses.
+- `SocketAddressV4`: Representing a pair of IPv4 address and port.
+- `IPv6Addr`: Representing IPv6 addresses.
+- `SocketAddressV6`: Representing a pair of IPv6 address and port.
+- `IPAddr`: Can either be an `IPv4Addr` or an `IPv6Addr`.
+- `SocketAddress`: Can either be a `SocketAddressV4` or `SocketAddressV6`.
+-/
+
+namespace Std
+namespace Net
+
+/--
+Representation of an IPv4 address.
+-/
+structure IPv4Addr where
+  /--
+  This structure represents the address: `octets[0].octets[1].octets[2].octets[3]`.
+  -/
+  octets : Vector UInt8 4
+  deriving Inhabited, DecidableEq
+
+/--
+A pair of an `IPv4Addr` and a port.
+-/
+structure SocketAddressV4 where
+  addr : IPv4Addr
+  port : UInt16
+  deriving Inhabited, DecidableEq
+
+/--
+Representation of an IPv6 address.
+-/
+structure IPv6Addr where
+  /--
+  This structure represents the address: `segments[0]:segments[1]:...`.
+  -/
+  segments : Vector UInt16 8
+  deriving Inhabited, DecidableEq
+
+/--
+A pair of an `IPv6Addr` and a port.
+-/
+structure SocketAddressV6 where
+  addr : IPv6Addr
+  port : UInt16
+  deriving Inhabited, DecidableEq
+
+/--
+An IP address, either IPv4 or IPv6.
+-/
+inductive IPAddr where
+  | v4 (addr : IPv4Addr)
+  | v6 (addr : IPv6Addr)
+  deriving Inhabited, DecidableEq
+
+/--
+Either a `SocketAddressV4` or `SocketAddressV6`.
+-/
+inductive SocketAddress where
+  | v4 (addr : SocketAddressV4)
+  | v6 (addr : SocketAddressV6)
+  deriving Inhabited, DecidableEq
+
+/--
+The kinds of address families supported by Lean, currently only IP variants.
+-/
+inductive AddressFamily where
+  | ipv4
+  | ipv6
+  deriving Inhabited, DecidableEq
+
+namespace IPv4Addr
+
+/--
+Build the IPv4 address `a.b.c.d`.
+-/
+def ofParts (a b c d : UInt8) : IPv4Addr :=
+  { octets := #v[a, b, c, d] }
+
+/--
+Try to parse `s` as an IPv4 address, returning `none` on failure.
+-/
+@[extern "lean_uv_pton_v4"]
+opaque ofString (s : @&String) : Option IPv4Addr
+
+/--
+Turn `addr` into a `String` in the usual IPv4 format.
+-/
+@[extern "lean_uv_ntop_v4"]
+opaque toString (addr : @&IPv4Addr) : String
+
+instance : ToString IPv4Addr where
+  toString := toString
+
+instance : Coe IPv4Addr IPAddr where
+  coe addr := .v4 addr
+
+end IPv4Addr
+
+namespace SocketAddressV4
+
+instance : Coe SocketAddressV4 SocketAddress where
+  coe addr := .v4 addr
+
+end SocketAddressV4
+
+namespace IPv6Addr
+
+/--
+Build the IPv6 address `a:b:c:d:e:f:g:h`.
+-/
+def ofParts (a b c d e f g h : UInt16) : IPv6Addr :=
+  { segments := #v[a, b, c, d, e, f, g, h] }
+
+/--
+Try to parse `s` as an IPv6 address according to
+[RFC 2373](https://datatracker.ietf.org/doc/html/rfc2373), returning `none` on failure.
+-/
+@[extern "lean_uv_pton_v6"]
+opaque ofString (s : @&String) : Option IPv6Addr
+
+/--
+Turn `addr` into a `String` in the IPv6 format described in
+[RFC 2373](https://datatracker.ietf.org/doc/html/rfc2373).
+-/
+@[extern "lean_uv_ntop_v6"]
+opaque toString (addr : @&IPv6Addr) : String
+
+instance : ToString IPv6Addr where
+  toString := toString
+
+instance : Coe IPv6Addr IPAddr where
+  coe addr := .v6 addr
+
+end IPv6Addr
+
+namespace SocketAddressV6
+
+instance : Coe SocketAddressV6 SocketAddress where
+  coe addr := .v6 addr
+
+end SocketAddressV6
+
+namespace IPAddr
+
+/--
+Obtain the `AddressFamily` associated with an `IPAddr`.
+-/
+def family : IPAddr → AddressFamily
+  | .v4 .. => .ipv4
+  | .v6 .. => .ipv6
+
+def toString : IPAddr → String
+  | .v4 addr => addr.toString
+  | .v6 addr => addr.toString
+
+instance : ToString IPAddr where
+  toString := toString
+
+end IPAddr
+
+namespace SocketAddress
+
+/--
+Obtain the `AddressFamily` associated with a `SocketAddress`.
+-/
+def family : SocketAddress → AddressFamily
+  | .v4 .. => .ipv4
+  | .v6 .. => .ipv6
+
+/--
+Obtain the `IPAddr` contained in a `SocketAddress`.
+-/
+def ipAddr : SocketAddress → IPAddr
+  | .v4 sa  => .v4 sa.addr
+  | .v6 sa  => .v6 sa.addr
+
+/--
+Obtain the port contained in a `SocketAddress`.
+-/
+def port : SocketAddress → UInt16
+  | .v4 sa | .v6 sa => sa.port
+
+end SocketAddress
+
+end Net
+end Std

src/runtime/CMakeLists.txt

@@ -2,7 +2,7 @@ set(RUNTIME_OBJS debug.cpp thread.cpp mpz.cpp utf8.cpp
 object.cpp apply.cpp exception.cpp interrupt.cpp memory.cpp
 stackinfo.cpp compact.cpp init_module.cpp load_dynlib.cpp io.cpp hash.cpp
 platform.cpp alloc.cpp allocprof.cpp sharecommon.cpp stack_overflow.cpp
-process.cpp object_ref.cpp mpn.cpp mutex.cpp libuv.cpp)
+process.cpp object_ref.cpp mpn.cpp mutex.cpp libuv.cpp uv/net_addr.cpp)
 add_library(leanrt_initial-exec STATIC ${RUNTIME_OBJS})
 set_target_properties(leanrt_initial-exec PROPERTIES
   ARCHIVE_OUTPUT_DIRECTORY ${CMAKE_CURRENT_BINARY_DIR})

src/runtime/uv/net_addr.cpp

@@ -0,0 +1,131 @@
+/*
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Henrik Böving
+*/
+
+#include "runtime/uv/net_addr.h"
+#include <cstring>
+
+namespace lean {
+
+#ifndef LEAN_EMSCRIPTEN
+
+void lean_ipv4_addr_to_in_addr(b_obj_arg ipv4_addr, in_addr* out) {
+    out->s_addr = 0;
+    for (int i = 0; i < 4; i++) {
+        uint32_t octet = (uint32_t)(uint8_t)lean_unbox(array_uget(ipv4_addr, i));
+        out->s_addr |= octet << (3 - i) * 8;
+    }
+    out->s_addr = htonl(out->s_addr);
+}
+
+void lean_ipv6_addr_to_in6_addr(b_obj_arg ipv6_addr, in6_addr* out) {
+    for (int i = 0; i < 8; i++) {
+        uint16_t segment = htons((uint16_t)lean_unbox(array_uget(ipv6_addr, i)));
+        out->s6_addr[2 * i] = (uint8_t)segment;
+        out->s6_addr[2 * i + 1] = (uint8_t)(segment >> 8);
+    }
+}
+
+lean_obj_res lean_in_addr_to_ipv4_addr(const in_addr* ipv4_addr) {
+    obj_res ret = alloc_array(0, 4);
+    uint32_t hostaddr = ntohl(ipv4_addr->s_addr);
+
+    for (int i = 0; i < 4; i++) {
+        uint8_t octet = (uint8_t)(hostaddr >> (3 - i) * 8);
+        array_push(ret, lean_box(octet));
+    }
+
+    lean_assert(array_size(ret) == 4);
+    return ret;
+}
+
+lean_obj_res lean_in6_addr_to_ipv6_addr(const in6_addr* ipv6_addr) {
+    obj_res ret = alloc_array(0, 8);
+
+    for (int i = 0; i < 16; i += 2) {
+        uint16_t part1 = (uint16_t)ipv6_addr->s6_addr[i];
+        uint16_t part2 = (uint16_t)ipv6_addr->s6_addr[i + 1];
+        uint16_t segment = ntohs((part2 << 8) | part1);
+        array_push(ret, lean_box(segment));
+    }
+
+    lean_assert(array_size(ret) == 8);
+    return ret;
+}
+
+/* Std.Net.IPV4Addr.ofString (s : @&String) : Option IPV4Addr */
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_pton_v4(b_obj_arg str_obj) {
+    const char* str = string_cstr(str_obj);
+    in_addr internal;
+    if (uv_inet_pton(AF_INET, str, &internal) == 0) {
+        return mk_option_some(lean_in_addr_to_ipv4_addr(&internal));
+    } else {
+        return mk_option_none();
+    }
+}
+
+/* Std.Net.IPV4Addr.toString (addr : @&IPV4Addr) : String */
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_ntop_v4(b_obj_arg ipv4_addr) {
+    in_addr internal;
+    lean_ipv4_addr_to_in_addr(ipv4_addr, &internal);
+    char dst[INET_ADDRSTRLEN];
+    int ret = uv_inet_ntop(AF_INET, &internal, dst, sizeof(dst));
+    lean_always_assert(ret == 0);
+    return lean_mk_string(dst);
+}
+
+/* Std.Net.IPV6Addr.ofString (s : @&String) : Option IPV6Addr */
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_pton_v6(b_obj_arg str_obj) {
+    const char* str = string_cstr(str_obj);
+    in6_addr internal;
+    if (uv_inet_pton(AF_INET6, str, &internal) == 0) {
+        return mk_option_some(lean_in6_addr_to_ipv6_addr(&internal));
+    } else {
+        return mk_option_none();
+    }
+}
+
+/* Std.Net.IPV6Addr.toString (addr : @&IPV6Addr) : String */
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_ntop_v6(b_obj_arg ipv6_addr) {
+    in6_addr internal;
+    lean_ipv6_addr_to_in6_addr(ipv6_addr, &internal);
+    char dst[INET6_ADDRSTRLEN];
+    int ret = uv_inet_ntop(AF_INET6, &internal, dst, sizeof(dst));
+    lean_always_assert(ret == 0);
+    return lean_mk_string(dst);
+}
+
+#else
+
+/* Std.Net.IPV4Addr.ofString (s : @&String) : Option IPV4Addr */
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_pton_v4(b_obj_arg str_obj) {
+    lean_always_assert(
+        false && ("Please build a version of Lean4 with libuv to invoke this.")
+    );
+}
+
+/* Std.Net.IPV4Addr.toString (addr : @&IPV4Addr) : String */
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_ntop_v4(b_obj_arg ipv4_addr) {
+    lean_always_assert(
+        false && ("Please build a version of Lean4 with libuv to invoke this.")
+    );
+}
+
+/* Std.Net.IPV6Addr.ofString (s : @&String) : Option IPV6Addr */
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_pton_v6(b_obj_arg str_obj) {
+    lean_always_assert(
+        false && ("Please build a version of Lean4 with libuv to invoke this.")
+    );
+}
+
+/* Std.Net.IPV6Addr.toString (addr : @&IPV6Addr) : String */
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_ntop_v6(b_obj_arg ipv6_addr) {
+    lean_always_assert(
+        false && ("Please build a version of Lean4 with libuv to invoke this.")
+    );
+}
+
+#endif
+}

src/runtime/uv/net_addr.h

@@ -0,0 +1,28 @@
+/*
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Henrik Böving
+*/
+#pragma once
+#include <lean/lean.h>
+#include "runtime/object.h"
+
+
+namespace lean {
+
+#ifndef LEAN_EMSCRIPTEN
+#include <uv.h>
+
+void lean_ipv4_addr_to_in_addr(b_obj_arg ipv4_addr, struct in_addr* out);
+void lean_ipv6_addr_to_in6_addr(b_obj_arg ipv6_addr, struct in6_addr* out);
+lean_obj_res lean_in_addr_to_ipv4_addr(const struct in_addr* ipv4_addr);
+lean_obj_res lean_in6_addr_to_ipv6_addr(const struct in6_addr* ipv6_addr);
+
+#endif
+
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_pton_v4(b_obj_arg str_obj);
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_ntop_v4(b_obj_arg ipv4_addr);
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_pton_v6(b_obj_arg str_obj);
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_ntop_v6(b_obj_arg ipv6_addr);
+
+}