structure Data.IP.IPv4 : Type

An IPv4 address stored as a 32-bit unsigned integer. $$\text{IPv4} = \{ \text{addr} : \text{UInt32} \}$$

• addr : UInt32

@[implicit_reducible]

instance Data.IP.instBEqIPv4 : BEq IPv4

Equations

• Data.IP.instBEqIPv4 = { beq := Data.IP.instBEqIPv4.beq }

def Data.IP.instBEqIPv4.beq : IPv4 → IPv4 → Bool

Equations

• Data.IP.instBEqIPv4.beq { addr := a } { addr := b } = (a == b)
• Data.IP.instBEqIPv4.beq x✝¹ x✝ = false

def Data.IP.instHashableIPv4.hash : IPv4 → UInt64

Equations

• Data.IP.instHashableIPv4.hash { addr := a } = mixHash 0 (hash a)

@[implicit_reducible]

instance Data.IP.instHashableIPv4 : Hashable IPv4

Equations

• Data.IP.instHashableIPv4 = { hash := Data.IP.instHashableIPv4.hash }

def Data.IP.instReprIPv4.repr : IPv4 → Nat → Std.Format

Equations

• Data.IP.instReprIPv4.repr x✝ prec✝ = Std.Format.bracket "{ " (Std.Format.nil ++ Std.Format.text "addr" ++ Std.Format.text " := " ++ (Std.Format.nest 8 (repr x✝.addr)).group) " }"

@[implicit_reducible]

instance Data.IP.instReprIPv4 : Repr IPv4

Equations

• Data.IP.instReprIPv4 = { reprPrec := Data.IP.instReprIPv4.repr }

def Data.IP.instInhabitedIPv4.default : IPv4

Equations

• Data.IP.instInhabitedIPv4.default = { addr := default }

@[implicit_reducible]

instance Data.IP.instInhabitedIPv4 : Inhabited IPv4

Equations

• Data.IP.instInhabitedIPv4 = { default := Data.IP.instInhabitedIPv4.default }

@[inline]

def Data.IP.IPv4.ofOctets (a b c d : UInt8) : IPv4

Create an IPv4 from four octets: a.b.c.d $$\text{ofOctets}(a, b, c, d) = (a \ll 24) \lor (b \ll 16) \lor (c \ll 8) \lor d$$

Equations

• Data.IP.IPv4.ofOctets a b c d = { addr := a.toUInt32 <<< 24 ||| b.toUInt32 <<< 16 ||| c.toUInt32 <<< 8 ||| d.toUInt32 }

def Data.IP.IPv4.toOctets (ip : IPv4) : UInt8 × UInt8 × UInt8 × UInt8

Extract the four octets.

Equations

• ip.toOctets = ((ip.addr >>> 24).toUInt8, (ip.addr >>> 16).toUInt8, (ip.addr >>> 8).toUInt8, ip.addr.toUInt8)

@[implicit_reducible]

instance Data.IP.IPv4.instToString : ToString IPv4

Equations

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

@[implicit_reducible]

instance Data.IP.IPv4.instOrd : Ord IPv4

Equations

• Data.IP.IPv4.instOrd = { compare := fun (a b : Data.IP.IPv4) => compare a.addr b.addr }

def Data.IP.IPv4.loopback : IPv4

The loopback address 127.0.0.1.

Equations

• Data.IP.IPv4.loopback = Data.IP.IPv4.ofOctets 127 0 0 1

def Data.IP.IPv4.any : IPv4

The any address 0.0.0.0.

Equations

• Data.IP.IPv4.any = { addr := 0 }

def Data.IP.IPv4.broadcast : IPv4

The broadcast address 255.255.255.255.

Equations

• Data.IP.IPv4.broadcast = { addr := 4294967295 }

structure Data.IP.IPv6 : Type

An IPv6 address stored as two 64-bit unsigned integers (high, low). $$\text{IPv6} = \{ \text{hi} : \text{UInt64},\; \text{lo} : \text{UInt64} \}$$

• hi : UInt64
• lo : UInt64

@[implicit_reducible]

instance Data.IP.instBEqIPv6 : BEq IPv6

Equations

• Data.IP.instBEqIPv6 = { beq := Data.IP.instBEqIPv6.beq }

def Data.IP.instBEqIPv6.beq : IPv6 → IPv6 → Bool

Equations

• Data.IP.instBEqIPv6.beq { hi := a, lo := a_1 } { hi := b, lo := b_1 } = (a == b && a_1 == b_1)
• Data.IP.instBEqIPv6.beq x✝¹ x✝ = false

def Data.IP.instHashableIPv6.hash : IPv6 → UInt64

Equations

• Data.IP.instHashableIPv6.hash { hi := a, lo := a_1 } = mixHash (mixHash 0 (hash a)) (hash a_1)

@[implicit_reducible]

instance Data.IP.instHashableIPv6 : Hashable IPv6

Equations

• Data.IP.instHashableIPv6 = { hash := Data.IP.instHashableIPv6.hash }

@[implicit_reducible]

instance Data.IP.instReprIPv6 : Repr IPv6

Equations

• Data.IP.instReprIPv6 = { reprPrec := Data.IP.instReprIPv6.repr }

def Data.IP.instReprIPv6.repr : IPv6 → Nat → Std.Format

Equations

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

def Data.IP.instInhabitedIPv6.default : IPv6

Equations

• Data.IP.instInhabitedIPv6.default = { hi := default, lo := default }

@[implicit_reducible]

instance Data.IP.instInhabitedIPv6 : Inhabited IPv6

Equations

• Data.IP.instInhabitedIPv6 = { default := Data.IP.instInhabitedIPv6.default }

def Data.IP.IPv6.loopback : IPv6

The loopback address ::1.

Equations

• Data.IP.IPv6.loopback = { hi := 0, lo := 1 }

def Data.IP.IPv6.any : IPv6

The any address ::.

Equations

• Data.IP.IPv6.any = { hi := 0, lo := 0 }

@[implicit_reducible]

instance Data.IP.IPv6.instOrd : Ord IPv6

Equations

• Data.IP.IPv6.instOrd = { compare := fun (a b : Data.IP.IPv6) => match compare a.hi b.hi with | Ordering.eq => compare a.lo b.lo | ord => ord }

@[implicit_reducible]

instance Data.IP.IPv6.instToString : ToString IPv6

Equations

• Data.IP.IPv6.instToString = { toString := fun (ip : Data.IP.IPv6) => toString ip.hi ++ toString ":" ++ toString ip.lo }

inductive Data.IP.IP : Type

A generic IP address (IPv4 or IPv6).

• v4 : IPv4 → IP
• v6 : IPv6 → IP

def Data.IP.instBEqIP.beq : IP → IP → Bool

Equations

• Data.IP.instBEqIP.beq (Data.IP.IP.v4 a) (Data.IP.IP.v4 b) = (a == b)
• Data.IP.instBEqIP.beq (Data.IP.IP.v6 a) (Data.IP.IP.v6 b) = (a == b)
• Data.IP.instBEqIP.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Data.IP.instBEqIP : BEq IP

Equations

• Data.IP.instBEqIP = { beq := Data.IP.instBEqIP.beq }

@[implicit_reducible]

instance Data.IP.instReprIP : Repr IP

Equations

• Data.IP.instReprIP = { reprPrec := Data.IP.instReprIP.repr }

def Data.IP.instReprIP.repr : IP → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Data.IP.IP.instToString : ToString IP

Equations

• Data.IP.IP.instToString = { toString := fun (x : Data.IP.IP) => match x with | Data.IP.IP.v4 a => toString a | Data.IP.IP.v6 a => toString a }

structure Data.IP.AddrRange4 : Type

An IPv4 CIDR range with bounded mask length. $$\text{AddrRange4} = \{ \text{base} : \text{IPv4},\; \text{mask} : \{n : \mathbb{N} \mid n \leq 32\} \}$$

• base : IPv4

  The network base address.

• maskLen : Nat

  The prefix length (0..32).

• valid : self.maskLen ≤ 32

  Proof that mask length is valid.

@[inline]

def Data.IP.AddrRange4.mask (r : AddrRange4) : UInt32

Compute the network mask from the prefix length. $$\text{mask}(n) = \text{0xFFFFFFFF} \ll (32 - n)$$

Equations

• r.mask = if (r.maskLen == 0) = true then 0 else 4294967295 <<< (32 - r.maskLen).toUInt32

@[inline]

def Data.IP.AddrRange4.isMatchedTo (ip : IPv4) (r : AddrRange4) : Bool

Check if an address falls within this CIDR range. $$\text{isMatchedTo}(ip, r) \iff (ip \land \text{mask}) = (\text{base} \land \text{mask})$$

Equations

• Data.IP.AddrRange4.isMatchedTo ip r = (ip.addr &&& r.mask == r.base.addr &&& r.mask)

@[implicit_reducible]

instance Data.IP.AddrRange4.instToString : ToString AddrRange4

Equations

• Data.IP.AddrRange4.instToString = { toString := fun (r : Data.IP.AddrRange4) => toString r.base ++ toString "/" ++ toString r.maskLen }

structure Data.IP.AddrRange6 : Type

An IPv6 CIDR range with bounded mask length. $$\text{AddrRange6} = \{ \text{base} : \text{IPv6},\; \text{mask} : \{n : \mathbb{N} \mid n \leq 128\} \}$$

• base : IPv6
• maskLen : Nat
• valid : self.maskLen ≤ 128

@[implicit_reducible]

instance Data.IP.AddrRange6.instToString : ToString AddrRange6

Equations

• Data.IP.AddrRange6.instToString = { toString := fun (r : Data.IP.AddrRange6) => toString r.base ++ toString "/" ++ toString r.maskLen }

inductive Data.IP.AddrRange : Type

A generic CIDR range.

• v4 : AddrRange4 → AddrRange
• v6 : AddrRange6 → AddrRange

@[implicit_reducible]

instance Data.IP.AddrRange.instToString : ToString AddrRange

Equations

• Data.IP.AddrRange.instToString = { toString := fun (x : Data.IP.AddrRange) => match x with | Data.IP.AddrRange.v4 r => toString r | Data.IP.AddrRange.v6 r => toString r }

def Data.IP.parseIPv4 (s : String) : Option IPv4

Parse an IPv4 address from dotted-decimal string. Returns none on invalid input.

Equations

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

def Data.IP.parseCIDR4 (s : String) : Option AddrRange4

Parse a CIDR range like "192.168.1.0/24".

Equations

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