`array_push` return values not captured in DNS/network address functions

[sagjoshi]

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)
  Getting error - service not available for socket type (error code: 4294964286)

Description

Three functions in src/runtime/uv/net_addr.cpp violate the array_push() API contract by not capturing its return value. While the bug is currently masked in typical usage, the code is incorrect and could fail in edge cases or with future runtime changes.

• lean_in_addr_to_ipv4_addr (line 85) - IPv4 DNS resolution
• lean_in6_addr_to_ipv6_addr (line 99) - IPv6 DNS resolution
• lean_phys_addr_to_mac_addr (line 111) - MAC address parsing

The bug doesn't manifest in typical usage because:

• Arrays are exclusively owned (no shared references)
• Initial capacity (4) is sufficient for all pushes
• Under these conditions, array_push() modifies in-place and returns the same pointer
  However, if the array were shared or needed reallocation, array_push() would return a NEW pointer to a modified copy, while the old pointer remains unchanged.

Context

The bug surfaced during implementing an HTTP client for AWS S3 operations in a Lean project. Attempts to connect to s3.amazonaws.com on port 443 consistently failed with "host is unreachable" errors, despite DNS resolution appearing to succeed. When test programs were created to examine the actual IP addresses being returned, where the system should have returned addresses like 52.217.116.224, the Lean implementation was producing 0.0.116.224. The first two octets were consistently zero. Tracing through the code in Std.Internal.UV.DNS and into the C++ runtime that return values from array_push() calls were being silently discarded, corrupting the IP address data.

What made this bug particularly insidious was understanding why it hadn't been caught earlier. The array_push() implementation happened to modify arrays in-place when they were exclusively owned with sufficient capacity, masking the incorrect code in typical usage scenarios. Only under specific memory patterns like those encountered during S3 DNS resolution, did the bug fully manifest.

Steps to Reproduce

There are no deterministic steps to reproduce.

Expected behavior:

Testing DNS resolution for S3...
✓ Resolved 16 addresses:

  IPv4: 52.217.116.224  ✓ All 4 octets correct!
  IPv4: 52.216.48.152
  IPv4: 16.15.176.114
  ...

Testing TCP connection...
Connecting to 52.217.116.224:443...
✓ Connected successfully!

Actual behavior: [Clear and concise description of what actually happens]

-- Attempting to connect to s3.amazonaws.com
let infos ← DNS.getAddrInfo "s3.amazonaws.com" "" 0
-- Success! Got 16 addresses back
let socket ← TCP.Socket.new
let connectPromise ← socket.connect sockAddr
-- Error: "host is unreachable" (error code: 4294967231)

let octets := ip.octets
IO.println s!"IP: {octets[0]}.{octets[1]}.{octets[2]}.{octets[3]}"

IP: 0.0.52.217
IP: 0.0.16.15
IP: 0.0.142.251

Versions

Lean 4.24.0
OS: macOS 15.7.1 (Sequoia)
Build: 24G231
Architecture: arm64 (Apple Silicon)

Additional Information

[Additional information, configuration or data that might be necessary to reproduce the issue]

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

[TwoFX]

This issue is already fixed on master, cf. #10854. Your (or your LLM's?) analysis of the problem is not correct, the code you're referring to is working correctly, because destructive updates are guaranteed in this situation. See the linked PR if you're interested in the real reason why this was broken.