Cedar.Spec.Ext.IPAddr

This file defines Cedar IpAddr values and functions.

source

@[reducible, inline]

abbrev Cedar.Spec.Ext.IPAddr.ADDR_SIZE (w : Nat) :

Nat

Equations

Cedar.Spec.Ext.IPAddr.ADDR_SIZE w = 2 ^ w

Instances For

source

@[reducible, inline]

abbrev Cedar.Spec.Ext.IPAddr.V4_WIDTH :

Nat

Equations

Cedar.Spec.Ext.IPAddr.V4_WIDTH = 5

Instances For

source

@[reducible, inline]

abbrev Cedar.Spec.Ext.IPAddr.V6_WIDTH :

Nat

Equations

Cedar.Spec.Ext.IPAddr.V6_WIDTH = 7

Instances For

source

@[reducible, inline]

abbrev Cedar.Spec.Ext.IPAddr.IPNetAddr (w : Nat) :

Type

Equations

Cedar.Spec.Ext.IPAddr.IPNetAddr w = BitVec (Cedar.Spec.Ext.IPAddr.ADDR_SIZE w)

Instances For

source

@[reducible, inline]

abbrev Cedar.Spec.Ext.IPAddr.IPv4Addr :

Type

IPv4 address: a 32 bit number partitioned into 4 groups. a0 is most signifcant and a3 is the least significant. In other words, the number represented is a0++a1++a2++a3. #

Equations

Cedar.Spec.Ext.IPAddr.IPv4Addr = Cedar.Spec.Ext.IPAddr.IPNetAddr Cedar.Spec.Ext.IPAddr.V4_WIDTH

Instances For

source

def Cedar.Spec.Ext.IPAddr.IPv4Addr.mk (a₀ a₁ a₂ a₃ : BitVec 8) :

IPv4Addr

Equations

Cedar.Spec.Ext.IPAddr.IPv4Addr.mk a₀ a₁ a₂ a₃ = a₀ ++ a₁ ++ a₂ ++ a₃

Instances For

source

@[reducible, inline]

abbrev Cedar.Spec.Ext.IPAddr.IPv6Addr :

Type

IPv6 address: a 128 bit number partitioned into 8 groups. a0 is most signifcant and a7 is the least significant. In other words, the number represented is a0++a1++a2++a3++a4++a5++a6++a7. #

Equations

Cedar.Spec.Ext.IPAddr.IPv6Addr = Cedar.Spec.Ext.IPAddr.IPNetAddr Cedar.Spec.Ext.IPAddr.V6_WIDTH

Instances For

source

def Cedar.Spec.Ext.IPAddr.IPv6Addr.mk (a₀ a₁ a₂ a₃ a₄ a₅ a₆ a₇ : BitVec 16) :

IPv6Addr

Equations

Cedar.Spec.Ext.IPAddr.IPv6Addr.mk a₀ a₁ a₂ a₃ a₄ a₅ a₆ a₇ = a₀ ++ a₁ ++ a₂ ++ a₃ ++ a₄ ++ a₅ ++ a₆ ++ a₇

Instances For

source

@[reducible, inline]

abbrev Cedar.Spec.Ext.IPAddr.IPNetPrefix (n : Nat) :

Type

Equations

Cedar.Spec.Ext.IPAddr.IPNetPrefix n = Option (BitVec n)

Instances For

source

@[reducible, inline]

abbrev Cedar.Spec.Ext.IPAddr.IPv4Prefix :

Type

Equations

Cedar.Spec.Ext.IPAddr.IPv4Prefix = Cedar.Spec.Ext.IPAddr.IPNetPrefix Cedar.Spec.Ext.IPAddr.V4_WIDTH

Instances For

source

@[reducible, inline]

abbrev Cedar.Spec.Ext.IPAddr.IPv6Prefix :

Type

Equations

Cedar.Spec.Ext.IPAddr.IPv6Prefix = Cedar.Spec.Ext.IPAddr.IPNetPrefix Cedar.Spec.Ext.IPAddr.V6_WIDTH

Instances For

source

def Cedar.Spec.Ext.IPAddr.IPNetPrefix.toNat {w : Nat} :

IPNetPrefix w → Nat

Equations

Cedar.Spec.Ext.IPAddr.IPNetPrefix.toNat none = Cedar.Spec.Ext.IPAddr.ADDR_SIZE w
Cedar.Spec.Ext.IPAddr.IPNetPrefix.toNat (some preSize) = preSize.toNat

Instances For

source

structure Cedar.Spec.Ext.IPAddr.CIDR (w : Nat) :

Type

addr : IPNetAddr w
pre : IPNetPrefix w

Instances For

source

def Cedar.Spec.Ext.IPAddr.CIDR.subnetWidth {w : Nat} (cidr : CIDR w) :

BitVec (ADDR_SIZE w)

Equations

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

Instances For

source

def Cedar.Spec.Ext.IPAddr.CIDR.range {w : Nat} (cidr : CIDR w) :

IPNetAddr w × IPNetAddr w

Equations

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

Instances For

source

def Cedar.Spec.Ext.IPAddr.CIDR.inRange {w : Nat} (cidr₁ cidr₂ : CIDR w) :

Bool

Equations

cidr₁.inRange cidr₂ = (decide (cidr₂.range.snd ≥ cidr₁.range.snd) && decide (cidr₁.range.fst ≥ cidr₂.range.fst))

Instances For

source

inductive Cedar.Spec.Ext.IPAddr.IPNet :

Type

V4 : CIDR V4_WIDTH → IPNet
V6 : CIDR V6_WIDTH → IPNet

Instances For

source

@[inline]

def Cedar.Spec.Ext.IPAddr.IPNet.isV4 :

IPNet → Bool

Equations

(Cedar.Spec.Ext.IPAddr.IPNet.V4 a).isV4 = true
x✝.isV4 = false

Instances For

source

@[inline]

def Cedar.Spec.Ext.IPAddr.IPNet.isV6 :

IPNet → Bool

Equations

(Cedar.Spec.Ext.IPAddr.IPNet.V6 a).isV6 = true
x✝.isV6 = false

Instances For

source

def Cedar.Spec.Ext.IPAddr.IPNet.inRange :

IPNet → IPNet → Bool

Equations

(Cedar.Spec.Ext.IPAddr.IPNet.V4 cidr₁).inRange (Cedar.Spec.Ext.IPAddr.IPNet.V4 cidr₂) = cidr₁.inRange cidr₂
(Cedar.Spec.Ext.IPAddr.IPNet.V6 cidr₁).inRange (Cedar.Spec.Ext.IPAddr.IPNet.V6 cidr₂) = cidr₁.inRange cidr₂
x✝¹.inRange x✝ = false

Instances For

source

def Cedar.Spec.Ext.IPAddr.LOOP_BACK_CIDR_V4 :

CIDR V4_WIDTH

Equations

Cedar.Spec.Ext.IPAddr.LOOP_BACK_CIDR_V4 = { addr := Cedar.Spec.Ext.IPAddr.LOOP_BACK_ADDRESS_V4✝, pre := 8 }

Instances For

source

def Cedar.Spec.Ext.IPAddr.LOOP_BACK_CIDR_V6 :

CIDR V6_WIDTH

Equations

Cedar.Spec.Ext.IPAddr.LOOP_BACK_CIDR_V6 = { addr := Cedar.Spec.Ext.IPAddr.LOOP_BACK_ADDRESS_V6✝, pre := 128 }

Instances For

source

def Cedar.Spec.Ext.IPAddr.MULTICAST_CIDR_V4 :

CIDR V4_WIDTH

Equations

Cedar.Spec.Ext.IPAddr.MULTICAST_CIDR_V4 = { addr := Cedar.Spec.Ext.IPAddr.MULTICAST_ADDRESS_V4✝, pre := 4 }

Instances For

source

def Cedar.Spec.Ext.IPAddr.MULTICAST_CIDR_V6 :

CIDR V6_WIDTH

Equations

Cedar.Spec.Ext.IPAddr.MULTICAST_CIDR_V6 = { addr := Cedar.Spec.Ext.IPAddr.MULTICAST_ADDRESS_V6✝, pre := 8 }

Instances For

source

def Cedar.Spec.Ext.IPAddr.IPNet.isLoopback :

IPNet → Bool

Equations

(Cedar.Spec.Ext.IPAddr.IPNet.V4 cidr).isLoopback = cidr.inRange Cedar.Spec.Ext.IPAddr.LOOP_BACK_CIDR_V4
(Cedar.Spec.Ext.IPAddr.IPNet.V6 cidr).isLoopback = cidr.inRange Cedar.Spec.Ext.IPAddr.LOOP_BACK_CIDR_V6

Instances For

source

def Cedar.Spec.Ext.IPAddr.IPNet.isMulticast :

IPNet → Bool

Equations

(Cedar.Spec.Ext.IPAddr.IPNet.V4 cidr).isMulticast = cidr.inRange Cedar.Spec.Ext.IPAddr.MULTICAST_CIDR_V4
(Cedar.Spec.Ext.IPAddr.IPNet.V6 cidr).isMulticast = cidr.inRange Cedar.Spec.Ext.IPAddr.MULTICAST_CIDR_V6

Instances For

source

def Cedar.Spec.Ext.IPAddr.ip (str : String) :

Option IPNet

Equations

Cedar.Spec.Ext.IPAddr.ip str = Cedar.Spec.Ext.IPAddr.parse✝ str

Instances For

source

def Cedar.Spec.Ext.IPAddr.instReprCIDR.repr {w✝ : Nat} :

CIDR w✝ → Nat → Std.Format

Equations

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

Instances For

source

instance Cedar.Spec.Ext.IPAddr.instReprCIDR {w✝ : Nat} :

Repr (CIDR w✝)

Equations

Cedar.Spec.Ext.IPAddr.instReprCIDR = { reprPrec := Cedar.Spec.Ext.IPAddr.instReprCIDR.repr }

source

instance Cedar.Spec.Ext.IPAddr.instDecidableEqCIDR {w✝ : Nat} :

DecidableEq (CIDR w✝)

Equations

Cedar.Spec.Ext.IPAddr.instDecidableEqCIDR = Cedar.Spec.Ext.IPAddr.instDecidableEqCIDR.decEq

source

def Cedar.Spec.Ext.IPAddr.instDecidableEqCIDR.decEq {w✝ : Nat} (x✝ x✝¹ : CIDR w✝) :

Decidable (x✝ = x✝¹)

Equations

Cedar.Spec.Ext.IPAddr.instDecidableEqCIDR.decEq { addr := a, pre := a_1 } { addr := b, pre := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

Instances For

source

def Cedar.Spec.Ext.IPAddr.instInhabitedCIDR.default {a✝ : Nat} :

CIDR a✝

Equations

Cedar.Spec.Ext.IPAddr.instInhabitedCIDR.default = { addr := default, pre := default }

Instances For

source

instance Cedar.Spec.Ext.IPAddr.instInhabitedCIDR {a✝ : Nat} :

Inhabited (CIDR a✝)

Equations

Cedar.Spec.Ext.IPAddr.instInhabitedCIDR = { default := Cedar.Spec.Ext.IPAddr.instInhabitedCIDR.default }

source

instance Cedar.Spec.Ext.IPAddr.instReprIPNet :

Repr IPNet

Equations

Cedar.Spec.Ext.IPAddr.instReprIPNet = { reprPrec := Cedar.Spec.Ext.IPAddr.instReprIPNet.repr }

source

def Cedar.Spec.Ext.IPAddr.instReprIPNet.repr :

IPNet → Nat → Std.Format

Equations

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

Instances For

source

def Cedar.Spec.Ext.IPAddr.instDecidableEqIPNet.decEq (x✝ x✝¹ : IPNet) :

Decidable (x✝ = x✝¹)

Equations

Cedar.Spec.Ext.IPAddr.instDecidableEqIPNet.decEq (Cedar.Spec.Ext.IPAddr.IPNet.V4 a) (Cedar.Spec.Ext.IPAddr.IPNet.V4 b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
Cedar.Spec.Ext.IPAddr.instDecidableEqIPNet.decEq (Cedar.Spec.Ext.IPAddr.IPNet.V4 a) (Cedar.Spec.Ext.IPAddr.IPNet.V6 a_1) = isFalse ⋯
Cedar.Spec.Ext.IPAddr.instDecidableEqIPNet.decEq (Cedar.Spec.Ext.IPAddr.IPNet.V6 a) (Cedar.Spec.Ext.IPAddr.IPNet.V4 a_1) = isFalse ⋯
Cedar.Spec.Ext.IPAddr.instDecidableEqIPNet.decEq (Cedar.Spec.Ext.IPAddr.IPNet.V6 a) (Cedar.Spec.Ext.IPAddr.IPNet.V6 b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

Instances For

source

instance Cedar.Spec.Ext.IPAddr.instDecidableEqIPNet :

DecidableEq IPNet

Equations

Cedar.Spec.Ext.IPAddr.instDecidableEqIPNet = Cedar.Spec.Ext.IPAddr.instDecidableEqIPNet.decEq

source

instance Cedar.Spec.Ext.IPAddr.instInhabitedIPNet :

Inhabited IPNet

Equations

Cedar.Spec.Ext.IPAddr.instInhabitedIPNet = { default := Cedar.Spec.Ext.IPAddr.instInhabitedIPNet.default }

source

def Cedar.Spec.Ext.IPAddr.instInhabitedIPNet.default :

IPNet

Equations

Cedar.Spec.Ext.IPAddr.instInhabitedIPNet.default = Cedar.Spec.Ext.IPAddr.IPNet.V4 default

Instances For

source

def Cedar.Spec.Ext.IPAddr.IPNetPrefix.lt {w : Nat} (p₁ p₂ : IPNetPrefix w) :

Bool

Equations

p₁.lt p₂ = decide (p₁.toNat < p₂.toNat)

Instances For

source

instance Cedar.Spec.Ext.IPAddr.instLTIPNetPrefix {w : Nat} :

LT (IPNetPrefix w)

Equations

Cedar.Spec.Ext.IPAddr.instLTIPNetPrefix = { lt := fun (d₁ d₂ : Cedar.Spec.Ext.IPAddr.IPNetPrefix w) => d₁.lt d₂ = true }

source

instance Cedar.Spec.Ext.IPAddr.IPNetPrefix.decLt {w : Nat} (d₁ d₂ : IPNetPrefix w) :

Decidable (d₁ < d₂)

Equations

d₁.decLt d₂ = if h : d₁.lt d₂ = true then isTrue h else isFalse h

source

def Cedar.Spec.Ext.IPAddr.CIDR.lt {w : Nat} (cidr₁ cidr₂ : CIDR w) :

Bool

Equations

cidr₁.lt cidr₂ = (decide (cidr₁.addr < cidr₂.addr) || decide (cidr₁.addr = cidr₂.addr) && decide (cidr₁.pre < cidr₂.pre))

Instances For

source

instance Cedar.Spec.Ext.IPAddr.instLTCIDR {w : Nat} :

LT (CIDR w)

Equations

Cedar.Spec.Ext.IPAddr.instLTCIDR = { lt := fun (d₁ d₂ : Cedar.Spec.Ext.IPAddr.CIDR w) => d₁.lt d₂ = true }

source

instance Cedar.Spec.Ext.IPAddr.CIDR.decLt {w : Nat} (d₁ d₂ : CIDR w) :

Decidable (d₁ < d₂)

Equations

d₁.decLt d₂ = if h : d₁.lt d₂ = true then isTrue h else isFalse h

source

def Cedar.Spec.Ext.IPAddr.IPNet.lt :

IPNet → IPNet → Bool

Equations

(Cedar.Spec.Ext.IPAddr.IPNet.V4 a).lt (Cedar.Spec.Ext.IPAddr.IPNet.V6 a_1) = true
(Cedar.Spec.Ext.IPAddr.IPNet.V6 a).lt (Cedar.Spec.Ext.IPAddr.IPNet.V4 a_1) = false
(Cedar.Spec.Ext.IPAddr.IPNet.V4 cidr₁).lt (Cedar.Spec.Ext.IPAddr.IPNet.V4 cidr₂) = decide (cidr₁ < cidr₂)
(Cedar.Spec.Ext.IPAddr.IPNet.V6 cidr₁).lt (Cedar.Spec.Ext.IPAddr.IPNet.V6 cidr₂) = decide (cidr₁ < cidr₂)

Instances For

source

instance Cedar.Spec.Ext.IPAddr.instLTIPNet :

LT IPNet

Equations

Cedar.Spec.Ext.IPAddr.instLTIPNet = { lt := fun (d₁ d₂ : Cedar.Spec.Ext.IPAddr.IPNet) => d₁.lt d₂ = true }

source

instance Cedar.Spec.Ext.IPAddr.IPNet.decLt (d₁ d₂ : IPNet) :

Decidable (d₁ < d₂)

Equations

d₁.decLt d₂ = if h : d₁.lt d₂ = true then isTrue h else isFalse h