fix: capture the return value of array_push in net_addr.cpp

src/runtime/uv/net_addr.cpp

@@ -82,7 +82,7 @@ lean_obj_res lean_in_addr_to_ipv4_addr(const in_addr* ipv4_addr) {
 
     for (int i = 0; i < 4; i++) {
         uint8_t octet = (uint8_t)(hostaddr >> (3 - i) * 8);
-        array_push(ret, lean_box(octet));
+        ret = array_push(ret, lean_box(octet));
     }
 
     lean_assert(array_size(ret) == 4);
@@ -96,7 +96,7 @@ lean_obj_res lean_in6_addr_to_ipv6_addr(const in6_addr* ipv6_addr) {
         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));
+        ret = array_push(ret, lean_box(segment));
     }
 
     lean_assert(array_size(ret) == 8);
@@ -108,7 +108,7 @@ lean_obj_res lean_phys_addr_to_mac_addr(char phys_addr[6]) {
 
     for (int i = 0; i < 6; i++) {
         uint8_t byte = (uint8_t)phys_addr[i];
-        array_push(ret, lean_box(byte));
+        ret = array_push(ret, lean_box(byte));
     }
 
     lean_assert(array_size(ret) == 6);

tests/lean/run/async_dns.lean

@@ -25,6 +25,35 @@ def runDNS : Async Unit := do
   unless infos.size > 0 do
     (throw <| IO.userError <| "No DNS results for google.com" : IO _)
 
+  -- Regression test: validate that IP addresses have all octets populated
+  -- Bug fix: array_push return values were not captured in lean_in_addr_to_ipv4_addr
+  let ipv4 := infos.filterMap (fun | .v4 e => some e | _ => none)
+
+  if let some head := ipv4[0]? then
+    let parts : Vector UInt8 4 := head.octets
+
+    let isValid :=
+      -- Not in 0.0.0.0/8 (current network)
+      -- This check would fail with the bug since first octet was always 0
+      parts[0] != 0 &&
+      -- Not in 10.0.0.0/8 (private)
+      parts[0] != 10 &&
+      -- Not in 127.0.0.0/8 (loopback)
+      parts[0] != 127 &&
+      -- Not in 169.254.0.0/16 (link-local)
+      !(parts[0] == 169 && parts[1] == 254) &&
+      -- Not in 172.16.0.0/12 (private)
+      !(parts[0] == 172 && parts[1] >= 16 && parts[1] <= 31) &&
+      -- Not in 192.168.0.0/16 (private)
+      !(parts[0] == 192 && parts[1] == 168) &&
+      -- Not in 224.0.0.0/4 (multicast)
+      parts[0] < 224 &&
+      -- Not 255.255.255.255 (broadcast)
+      !(parts[0] == 255 && parts[1] == 255 && parts[2] == 255 && parts[3] == 255)
+
+    unless isValid do
+      throw <| IO.userError <| s!"Invalid IP address for google.com: {parts[0]}.{parts[1]}.{parts[2]}.{parts[3]}"
+
 def runDNSNoAscii : Async Unit := do
   let infos ← timeout (DNS.getAddrInfo "google.com▸" "http") 10000
 

tests/lean/run/async_dns_octets.lean

@@ -0,0 +1,99 @@
+import Std.Internal.Async
+import Std.Internal.UV
+import Std.Net.Addr
+
+open Std.Internal.IO Async
+open Std.Net
+
+/-!
+# DNS Resolution Octet Test
+
+This test specifically validates that all 4 octets of IPv4 addresses
+are correctly populated by DNS resolution.
+
+This is a regression test for a bug where `array_push` return values
+were not captured in `lean_in_addr_to_ipv4_addr`, causing only the
+last 2 octets to be populated (first 2 were always 0).
+-/
+
+def timeout [Inhabited α] (a : Async α) (time : Std.Time.Millisecond.Offset) : Async α := do
+  let result ← Async.race (a.map Except.ok) (sleep time |>.map Except.error)
+  match result with
+  | .ok res => pure res
+  | .error _ => throw (.userError "timeout")
+
+/--
+Test that DNS resolution returns valid IPv4 addresses with all 4 octets populated.
+We use 1.1.1.1 (Cloudflare DNS) as a test case since we know the expected result.
+-/
+def testDNSAllOctets : Async Unit := do
+  -- Resolve a known IP address to verify all octets are correct
+  let infos ← timeout (DNS.getAddrInfo "1.1.1.1" "") 1000
+
+  unless infos.size > 0 do
+    throw <| IO.userError "No DNS results for 1.1.1.1"
+
+  let ipv4 := infos.filterMap (fun | .v4 e => some e | _ => none)
+
+  unless ipv4.size > 0 do
+    throw <| IO.userError "No IPv4 results for 1.1.1.1"
+
+  let addr := ipv4[0]!
+  let octets := addr.octets
+
+  -- Verify all octets are correct for 1.1.1.1
+  unless octets[0] == 1 do
+    throw <| IO.userError s!"First octet incorrect: expected 1, got {octets[0]}"
+
+  unless octets[1] == 1 do
+    throw <| IO.userError s!"Second octet incorrect: expected 1, got {octets[1]}"
+
+  unless octets[2] == 1 do
+    throw <| IO.userError s!"Third octet incorrect: expected 1, got {octets[2]}"
+
+  unless octets[3] == 1 do
+    throw <| IO.userError s!"Fourth octet incorrect: expected 1, got {octets[3]}"
+
+  -- Also verify toString works correctly
+  let addrStr := addr.toString
+  unless addrStr == "1.1.1.1" do
+    throw <| IO.userError s!"Address string incorrect: expected '1.1.1.1', got '{addrStr}'"
+
+/--
+Test that DNS resolution for google.com returns valid public IP addresses
+with non-zero first octets (regression test for the array_push bug).
+-/
+def testDNSPublicIP : Async Unit := do
+  let infos ← timeout (DNS.getAddrInfo "google.com" "") 1000
+
+  unless infos.size > 0 do
+    throw <| IO.userError "No DNS results for google.com"
+
+  let ipv4 := infos.filterMap (fun | .v4 e => some e | _ => none)
+
+  unless ipv4.size > 0 do
+    throw <| IO.userError "No IPv4 results for google.com"
+
+  let addr := ipv4[0]!
+  let octets := addr.octets
+
+  -- The bug caused the first octet to always be 0
+  -- Google's IPs should never start with 0
+  unless octets[0] != 0 do
+    throw <| IO.userError s!"First octet is 0 - DNS resolution bug detected! Full address: {octets[0]}.{octets[1]}.{octets[2]}.{octets[3]}"
+
+  -- Verify it's a valid public IP (not private/reserved)
+  let isValid :=
+    octets[0] != 0 &&           -- Not in 0.0.0.0/8
+    octets[0] != 10 &&          -- Not in 10.0.0.0/8 (private)
+    octets[0] != 127 &&         -- Not in 127.0.0.0/8 (loopback)
+    !(octets[0] == 169 && octets[1] == 254) &&  -- Not in 169.254.0.0/16 (link-local)
+    !(octets[0] == 172 && octets[1] >= 16 && octets[1] <= 31) &&  -- Not in 172.16.0.0/12 (private)
+    !(octets[0] == 192 && octets[1] == 168) &&  -- Not in 192.168.0.0/16 (private)
+    octets[0] < 224  -- Not multicast or reserved
+
+  unless isValid do
+    throw <| IO.userError s!"Invalid public IP for google.com: {octets[0]}.{octets[1]}.{octets[2]}.{octets[3]}"
+
+#eval testDNSAllOctets.toIO >>= AsyncTask.block
+#eval testDNSPublicIP.toIO >>= AsyncTask.block