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.IPv4Addr : Type

Representation of an IPv4 address.

• octets : Vector UInt8 4

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

instance Std.Net.instInhabitedIPv4Addr : Inhabited IPv4Addr

Equations

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

instance Std.Net.instDecidableEqIPv4Addr : DecidableEq IPv4Addr

Equations

• Std.Net.instDecidableEqIPv4Addr = Std.Net.decEqIPv4Addr✝

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 := { addr := default, port := default } }

instance Std.Net.instDecidableEqSocketAddressV4 : DecidableEq SocketAddressV4

Equations

• Std.Net.instDecidableEqSocketAddressV4 = Std.Net.decEqSocketAddressV4✝

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 := { segments := default } }

instance Std.Net.instDecidableEqIPv6Addr : DecidableEq IPv6Addr

Equations

• Std.Net.instDecidableEqIPv6Addr = Std.Net.decEqIPv6Addr✝

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 := { addr := default, port := default } }

instance Std.Net.instDecidableEqSocketAddressV6 : DecidableEq SocketAddressV6

Equations

• Std.Net.instDecidableEqSocketAddressV6 = Std.Net.decEqSocketAddressV6✝

inductive Std.Net.IPAddr : Type

An IP address, either IPv4 or IPv6.

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

instance Std.Net.instInhabitedIPAddr : Inhabited IPAddr

Equations

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

instance Std.Net.instDecidableEqIPAddr : DecidableEq IPAddr

Equations

• Std.Net.instDecidableEqIPAddr = Std.Net.decEqIPAddr✝

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.SocketAddress.v4 default }

instance Std.Net.instDecidableEqSocketAddress : DecidableEq SocketAddress

Equations

• Std.Net.instDecidableEqSocketAddress = Std.Net.decEqSocketAddress✝

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.AddressFamily.ipv4 }

instance Std.Net.instDecidableEqAddressFamily : DecidableEq AddressFamily

Equations

• Std.Net.instDecidableEqAddressFamily x✝ y✝ = if h : x✝.toCtorIdx = y✝.toCtorIdx 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 := { toArray := #[a, b, c, d], size_toArray := ⋯ } }

@[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 := { toArray := #[a, b, c, d, e, f, g, h], size_toArray := ⋯ } }

@[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