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.

structure Std.Net.MACAddr : Type

Representation of a MAC address.

• octets : Vector UInt8 6

  This structure represents the address: octets[0]:octets[1]:octets[2]:octets[3]:octets[4]:octets[5].

instance Std.Net.instInhabitedMACAddr : Inhabited MACAddr

Equations

• Std.Net.instInhabitedMACAddr = { default := Std.Net.instInhabitedMACAddr.default }

def Std.Net.instInhabitedMACAddr.default : MACAddr

Equations

• Std.Net.instInhabitedMACAddr.default = { octets := default }

def Std.Net.instDecidableEqMACAddr.decEq (x✝ x✝¹ : MACAddr) : Decidable (x✝ = x✝¹)

Equations

• Std.Net.instDecidableEqMACAddr.decEq { octets := a } { octets := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

instance Std.Net.instDecidableEqMACAddr : DecidableEq MACAddr

Equations

• Std.Net.instDecidableEqMACAddr = Std.Net.instDecidableEqMACAddr.decEq

structure Std.Net.IPv4Addr : Type

Representation of an IPv4 address.

• octets : Vector UInt8 4

  This structure represents the address: octets[0].octets[1].octets[2].octets[3].

def Std.Net.instInhabitedIPv4Addr.default : IPv4Addr

Equations

• Std.Net.instInhabitedIPv4Addr.default = { octets := default }

instance Std.Net.instInhabitedIPv4Addr : Inhabited IPv4Addr

Equations

• Std.Net.instInhabitedIPv4Addr = { default := Std.Net.instInhabitedIPv4Addr.default }

def Std.Net.instDecidableEqIPv4Addr.decEq (x✝ x✝¹ : IPv4Addr) : Decidable (x✝ = x✝¹)

Equations

• Std.Net.instDecidableEqIPv4Addr.decEq { octets := a } { octets := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

instance Std.Net.instDecidableEqIPv4Addr : DecidableEq IPv4Addr

Equations

• Std.Net.instDecidableEqIPv4Addr = Std.Net.instDecidableEqIPv4Addr.decEq

structure Std.Net.SocketAddressV4 : Type

A pair of an IPv4Addr and a port.

• addr : IPv4Addr
• port : UInt16

instance Std.Net.instInhabitedSocketAddressV4 : Inhabited SocketAddressV4

Equations

• Std.Net.instInhabitedSocketAddressV4 = { default := Std.Net.instInhabitedSocketAddressV4.default }

def Std.Net.instInhabitedSocketAddressV4.default : SocketAddressV4

Equations

• Std.Net.instInhabitedSocketAddressV4.default = { addr := default, port := default }

def Std.Net.instDecidableEqSocketAddressV4.decEq (x✝ x✝¹ : SocketAddressV4) : Decidable (x✝ = x✝¹)

Equations

• Std.Net.instDecidableEqSocketAddressV4.decEq { addr := a, port := a_1 } { addr := b, port := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

instance Std.Net.instDecidableEqSocketAddressV4 : DecidableEq SocketAddressV4

Equations

• Std.Net.instDecidableEqSocketAddressV4 = Std.Net.instDecidableEqSocketAddressV4.decEq

structure Std.Net.IPv6Addr : Type

Representation of an IPv6 address.

• segments : Vector UInt16 8

  This structure represents the address: segments[0]:segments[1]:....

instance Std.Net.instInhabitedIPv6Addr : Inhabited IPv6Addr

Equations

• Std.Net.instInhabitedIPv6Addr = { default := Std.Net.instInhabitedIPv6Addr.default }

def Std.Net.instInhabitedIPv6Addr.default : IPv6Addr

Equations

• Std.Net.instInhabitedIPv6Addr.default = { segments := default }

def Std.Net.instDecidableEqIPv6Addr.decEq (x✝ x✝¹ : IPv6Addr) : Decidable (x✝ = x✝¹)

Equations

• Std.Net.instDecidableEqIPv6Addr.decEq { segments := a } { segments := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

instance Std.Net.instDecidableEqIPv6Addr : DecidableEq IPv6Addr

Equations

• Std.Net.instDecidableEqIPv6Addr = Std.Net.instDecidableEqIPv6Addr.decEq

structure Std.Net.SocketAddressV6 : Type

A pair of an IPv6Addr and a port.

• addr : IPv6Addr
• port : UInt16

instance Std.Net.instInhabitedSocketAddressV6 : Inhabited SocketAddressV6

Equations

• Std.Net.instInhabitedSocketAddressV6 = { default := Std.Net.instInhabitedSocketAddressV6.default }

def Std.Net.instInhabitedSocketAddressV6.default : SocketAddressV6

Equations

• Std.Net.instInhabitedSocketAddressV6.default = { addr := default, port := default }

instance Std.Net.instDecidableEqSocketAddressV6 : DecidableEq SocketAddressV6

Equations

• Std.Net.instDecidableEqSocketAddressV6 = Std.Net.instDecidableEqSocketAddressV6.decEq

def Std.Net.instDecidableEqSocketAddressV6.decEq (x✝ x✝¹ : SocketAddressV6) : Decidable (x✝ = x✝¹)

Equations

• Std.Net.instDecidableEqSocketAddressV6.decEq { addr := a, port := a_1 } { addr := b, port := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

inductive Std.Net.IPAddr : Type

An IP address, either IPv4 or IPv6.

• v4 (addr : IPv4Addr) : IPAddr
• v6 (addr : IPv6Addr) : IPAddr

def Std.Net.instInhabitedIPAddr.default : IPAddr

Equations

• Std.Net.instInhabitedIPAddr.default = Std.Net.IPAddr.v4 default

instance Std.Net.instInhabitedIPAddr : Inhabited IPAddr

Equations

• Std.Net.instInhabitedIPAddr = { default := Std.Net.instInhabitedIPAddr.default }

instance Std.Net.instDecidableEqIPAddr : DecidableEq IPAddr

Equations

• Std.Net.instDecidableEqIPAddr = Std.Net.instDecidableEqIPAddr.decEq

def Std.Net.instDecidableEqIPAddr.decEq (x✝ x✝¹ : IPAddr) : Decidable (x✝ = x✝¹)

Equations

• Std.Net.instDecidableEqIPAddr.decEq (Std.Net.IPAddr.v4 a) (Std.Net.IPAddr.v4 b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Std.Net.instDecidableEqIPAddr.decEq (Std.Net.IPAddr.v4 addr) (Std.Net.IPAddr.v6 addr_1) = isFalse ⋯
• Std.Net.instDecidableEqIPAddr.decEq (Std.Net.IPAddr.v6 addr) (Std.Net.IPAddr.v4 addr_1) = isFalse ⋯
• Std.Net.instDecidableEqIPAddr.decEq (Std.Net.IPAddr.v6 a) (Std.Net.IPAddr.v6 b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

inductive Std.Net.SocketAddress : Type

Either a SocketAddressV4 or SocketAddressV6.

• v4 (addr : SocketAddressV4) : SocketAddress
• v6 (addr : SocketAddressV6) : SocketAddress

instance Std.Net.instInhabitedSocketAddress : Inhabited SocketAddress

Equations

• Std.Net.instInhabitedSocketAddress = { default := Std.Net.instInhabitedSocketAddress.default }

def Std.Net.instInhabitedSocketAddress.default : SocketAddress

Equations

• Std.Net.instInhabitedSocketAddress.default = Std.Net.SocketAddress.v4 default

def Std.Net.instDecidableEqSocketAddress.decEq (x✝ x✝¹ : SocketAddress) : Decidable (x✝ = x✝¹)

Equations

• Std.Net.instDecidableEqSocketAddress.decEq (Std.Net.SocketAddress.v4 a) (Std.Net.SocketAddress.v4 b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Std.Net.instDecidableEqSocketAddress.decEq (Std.Net.SocketAddress.v4 addr) (Std.Net.SocketAddress.v6 addr_1) = isFalse ⋯
• Std.Net.instDecidableEqSocketAddress.decEq (Std.Net.SocketAddress.v6 addr) (Std.Net.SocketAddress.v4 addr_1) = isFalse ⋯
• Std.Net.instDecidableEqSocketAddress.decEq (Std.Net.SocketAddress.v6 a) (Std.Net.SocketAddress.v6 b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

instance Std.Net.instDecidableEqSocketAddress : DecidableEq SocketAddress

Equations

• Std.Net.instDecidableEqSocketAddress = Std.Net.instDecidableEqSocketAddress.decEq

inductive Std.Net.AddressFamily : Type

The kinds of address families supported by Lean, currently only IP variants.

• ipv4 : AddressFamily
• ipv6 : AddressFamily

instance Std.Net.instInhabitedAddressFamily : Inhabited AddressFamily

Equations

• Std.Net.instInhabitedAddressFamily = { default := Std.Net.instInhabitedAddressFamily.default }

def Std.Net.instInhabitedAddressFamily.default : AddressFamily

Equations

• Std.Net.instInhabitedAddressFamily.default = Std.Net.AddressFamily.ipv4

instance Std.Net.instDecidableEqAddressFamily : DecidableEq AddressFamily

Equations

• Std.Net.instDecidableEqAddressFamily x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Std.Net.IPv4Addr.ofParts (a b c d : UInt8) : IPv4Addr

Build the IPv4 address a.b.c.d.

Equations

• Std.Net.IPv4Addr.ofParts a b c d = { octets := #v[a, b, c, d] }

@[extern lean_uv_pton_v4]

opaque Std.Net.IPv4Addr.ofString (s : String) : Option IPv4Addr

Try to parse s as an IPv4 address, returning none on failure.

@[extern lean_uv_ntop_v4]

opaque Std.Net.IPv4Addr.toString (addr : IPv4Addr) : String

Turn addr into a String in the usual IPv4 format.

instance Std.Net.IPv4Addr.instToString : ToString IPv4Addr

Equations

• Std.Net.IPv4Addr.instToString = { toString := Std.Net.IPv4Addr.toString }

instance Std.Net.IPv4Addr.instCoeIPAddr : Coe IPv4Addr IPAddr

Equations

• Std.Net.IPv4Addr.instCoeIPAddr = { coe := fun (addr : Std.Net.IPv4Addr) => Std.Net.IPAddr.v4 addr }

instance Std.Net.SocketAddressV4.instCoeSocketAddress : Coe SocketAddressV4 SocketAddress

Equations

• Std.Net.SocketAddressV4.instCoeSocketAddress = { coe := fun (addr : Std.Net.SocketAddressV4) => Std.Net.SocketAddress.v4 addr }

def Std.Net.IPv6Addr.ofParts (a b c d e f g h : UInt16) : IPv6Addr

Build the IPv6 address a:b:c:d:e:f:g:h.

Equations

• Std.Net.IPv6Addr.ofParts a b c d e f g h = { segments := #v[a, b, c, d, e, f, g, h] }

@[extern lean_uv_pton_v6]

opaque Std.Net.IPv6Addr.ofString (s : String) : Option IPv6Addr

Try to parse s as an IPv6 address according to RFC 2373, returning none on failure.

@[extern lean_uv_ntop_v6]

opaque Std.Net.IPv6Addr.toString (addr : IPv6Addr) : String

Turn addr into a String in the IPv6 format described in RFC 2373.

instance Std.Net.IPv6Addr.instToString : ToString IPv6Addr

Equations

• Std.Net.IPv6Addr.instToString = { toString := Std.Net.IPv6Addr.toString }

instance Std.Net.IPv6Addr.instCoeIPAddr : Coe IPv6Addr IPAddr

Equations

• Std.Net.IPv6Addr.instCoeIPAddr = { coe := fun (addr : Std.Net.IPv6Addr) => Std.Net.IPAddr.v6 addr }

instance Std.Net.SocketAddressV6.instCoeSocketAddress : Coe SocketAddressV6 SocketAddress

Equations

• Std.Net.SocketAddressV6.instCoeSocketAddress = { coe := fun (addr : Std.Net.SocketAddressV6) => Std.Net.SocketAddress.v6 addr }

def Std.Net.IPAddr.family : IPAddr → AddressFamily

Obtain the AddressFamily associated with an IPAddr.

Equations

• (Std.Net.IPAddr.v4 addr).family = Std.Net.AddressFamily.ipv4
• (Std.Net.IPAddr.v6 addr).family = Std.Net.AddressFamily.ipv6

def Std.Net.IPAddr.toString : IPAddr → String

Equations

• (Std.Net.IPAddr.v4 addr).toString = addr.toString
• (Std.Net.IPAddr.v6 addr).toString = addr.toString

instance Std.Net.IPAddr.instToString : ToString IPAddr

Equations

• Std.Net.IPAddr.instToString = { toString := Std.Net.IPAddr.toString }

def Std.Net.SocketAddress.family : SocketAddress → AddressFamily

Obtain the AddressFamily associated with a SocketAddress.

Equations

• (Std.Net.SocketAddress.v4 addr).family = Std.Net.AddressFamily.ipv4
• (Std.Net.SocketAddress.v6 addr).family = Std.Net.AddressFamily.ipv6

def Std.Net.SocketAddress.ipAddr : SocketAddress → IPAddr

Obtain the IPAddr contained in a SocketAddress.

Equations

• (Std.Net.SocketAddress.v4 addr).ipAddr = Std.Net.IPAddr.v4 addr.addr
• (Std.Net.SocketAddress.v6 addr).ipAddr = Std.Net.IPAddr.v6 addr.addr

def Std.Net.SocketAddress.port : SocketAddress → UInt16

Obtain the port contained in a SocketAddress.

Equations

• (Std.Net.SocketAddress.v4 addr).port = addr.port
• (Std.Net.SocketAddress.v6 addr).port = addr.port

structure Std.Net.InterfaceAddress : Type

Represents an interface address, including details such as the interface name, whether it is internal, the associated address, and the network mask.

• name : String

  The name of the network interface.

• physicalAddress : MACAddr
• isLoopback : Bool

  Indicates whether the interface is a loopback interface.

• address : IPAddr

  The IP address assigned to the interface.

• netMask : IPAddr

  The subnet mask associated with the interface.

def Std.Net.instInhabitedInterfaceAddress.default : InterfaceAddress

Equations

• Std.Net.instInhabitedInterfaceAddress.default = { name := default, physicalAddress := default, isLoopback := default, address := default, netMask := default }

instance Std.Net.instInhabitedInterfaceAddress : Inhabited InterfaceAddress

Equations

• Std.Net.instInhabitedInterfaceAddress = { default := Std.Net.instInhabitedInterfaceAddress.default }

instance Std.Net.instDecidableEqInterfaceAddress : DecidableEq InterfaceAddress

Equations

• Std.Net.instDecidableEqInterfaceAddress = Std.Net.instDecidableEqInterfaceAddress.decEq

def Std.Net.instDecidableEqInterfaceAddress.decEq (x✝ x✝¹ : InterfaceAddress) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

@[extern lean_uv_interface_addresses]

opaque Std.Net.interfaceAddresses : IO (Array InterfaceAddress)

Gets address information about the network interfaces on the system, including disabled ones and multiple addresses for each interface.