#[cfg(any(verus, verus_keep_ghost))]
use vstd::prelude::*;
#[cfg(any(verus, verus_keep_ghost))]
verus! {
pub open spec fn spec_is_restricted_ipv4_octets(octets: [u8; 4]) -> bool {
let o0 = octets[0];
let o1 = octets[1];
let o2 = octets[2];
o0 == 0
|| o0 == 10
|| (o0 == 100 && (o1 & 0xC0) == 64)
|| o0 == 127
|| (o0 == 169 && o1 == 254)
|| (o0 == 172 && o1 >= 16 && o1 <= 31)
|| (o0 == 192 && o1 == 0 && o2 == 0)
|| (o0 == 192 && o1 == 0 && o2 == 2)
|| (o0 == 192 && o1 == 88 && o2 == 99)
|| (o0 == 192 && o1 == 168)
|| (o0 == 198 && (o1 == 18 || o1 == 19))
|| (o0 == 198 && o1 == 51 && o2 == 100)
|| (o0 == 203 && o1 == 0 && o2 == 113)
|| (o0 >= 224 && o0 <= 239)
|| (o0 >= 240)
}
pub open spec fn spec_is_restricted_ipv6_segments(segments: [u16; 8]) -> bool {
let s0 = segments[0];
let s1 = segments[1];
let s2 = segments[2];
let s3 = segments[3];
let s4 = segments[4];
let s5 = segments[5];
let s6 = segments[6];
let s7 = segments[7];
(s0 == 0 && s1 == 0 && s2 == 0 && s3 == 0 && s4 == 0 && s5 == 0 && s6 == 0 && s7 == 0)
|| (s0 == 0 && s1 == 0 && s2 == 0 && s3 == 0 && s4 == 0 && s5 == 0 && s6 == 0 && s7 == 1)
|| (s0 == 0 && s1 == 0 && s2 == 0 && s3 == 0 && s4 == 0 && s5 == 0xffff
&& spec_is_restricted_ipv4_octets([
((s6 >> 8) & 0xff) as u8,
(s6 & 0xff) as u8,
((s7 >> 8) & 0xff) as u8,
(s7 & 0xff) as u8,
]))
|| (s0 == 0 && s1 == 0 && s2 == 0 && s3 == 0 && s4 == 0xffff && s5 == 0)
|| (s0 == 0x0064 && s1 == 0xff9b && s2 == 0 && s3 == 0 && s4 == 0 && s5 == 0)
|| (s0 == 0x2001 && s1 == 0x0db8)
|| (s0 == 0x2001 && s1 == 0)
|| (s0 == 0x2002
&& spec_is_restricted_ipv4_octets([
((s1 >> 8) & 0xff) as u8,
(s1 & 0xff) as u8,
((s2 >> 8) & 0xff) as u8,
(s2 & 0xff) as u8,
]))
|| ((s0 & 0xfe00) == 0xfc00)
|| ((s0 & 0xffc0) == 0xfe80)
|| ((s0 & 0xffc0) == 0xfec0)
|| ((s0 & 0xff00) == 0xff00)
}
#[must_use]
#[inline]
pub const fn is_restricted_ipv4_octets(octets: [u8; 4]) -> (r: bool)
ensures r == spec_is_restricted_ipv4_octets(octets)
{
let o0 = octets[0];
let o1 = octets[1];
let o2 = octets[2];
o0 == 0
|| o0 == 10
|| (o0 == 100 && (o1 & 0xC0) == 64)
|| o0 == 127
|| (o0 == 169 && o1 == 254)
|| (o0 == 172 && o1 >= 16 && o1 <= 31)
|| (o0 == 192 && o1 == 0 && o2 == 0)
|| (o0 == 192 && o1 == 0 && o2 == 2)
|| (o0 == 192 && o1 == 88 && o2 == 99)
|| (o0 == 192 && o1 == 168)
|| (o0 == 198 && (o1 == 18 || o1 == 19))
|| (o0 == 198 && o1 == 51 && o2 == 100)
|| (o0 == 203 && o1 == 0 && o2 == 113)
|| (o0 >= 224 && o0 <= 239)
|| (o0 >= 240)
}
#[must_use]
#[inline]
#[allow(clippy::const_is_empty)]
pub const fn is_restricted_ipv6_segments(segments: [u16; 8]) -> (r: bool)
ensures r == spec_is_restricted_ipv6_segments(segments)
{
let seg = segments;
let s0 = seg[0];
let s1 = seg[1];
let s2 = seg[2];
let s3 = seg[3];
let s4 = seg[4];
let s5 = seg[5];
let s6 = seg[6];
let s7 = seg[7];
(s0 == 0
&& s1 == 0
&& s2 == 0
&& s3 == 0
&& s4 == 0
&& s5 == 0
&& s6 == 0
&& s7 == 0)
|| (s0 == 0
&& s1 == 0
&& s2 == 0
&& s3 == 0
&& s4 == 0
&& s5 == 0
&& s6 == 0
&& s7 == 1)
|| (s0 == 0
&& s1 == 0
&& s2 == 0
&& s3 == 0
&& s4 == 0
&& s5 == 0xffff
&& is_restricted_ipv4_octets([
((s6 >> 8) & 0xff) as u8,
(s6 & 0xff) as u8,
((s7 >> 8) & 0xff) as u8,
(s7 & 0xff) as u8,
]))
|| (s0 == 0
&& s1 == 0
&& s2 == 0
&& s3 == 0
&& s4 == 0xffff
&& s5 == 0)
|| (s0 == 0x0064
&& s1 == 0xff9b
&& s2 == 0
&& s3 == 0
&& s4 == 0
&& s5 == 0)
|| (s0 == 0x2001 && s1 == 0x0db8)
|| (s0 == 0x2001 && s1 == 0)
|| (s0 == 0x2002
&& is_restricted_ipv4_octets([
((s1 >> 8) & 0xff) as u8,
(s1 & 0xff) as u8,
((s2 >> 8) & 0xff) as u8,
(s2 & 0xff) as u8,
]))
|| ((s0 & 0xfe00) == 0xfc00)
|| ((s0 & 0xffc0) == 0xfe80)
|| ((s0 & 0xffc0) == 0xfec0)
|| ((s0 & 0xff00) == 0xff00)
}
}
#[cfg(not(any(verus, verus_keep_ghost)))]
mod plain {
#[must_use]
#[inline]
pub const fn is_restricted_ipv4_octets(octets: [u8; 4]) -> bool {
let o0 = octets[0];
let o1 = octets[1];
let o2 = octets[2];
o0 == 0
|| o0 == 10
|| (o0 == 100 && (o1 & 0xC0) == 64)
|| o0 == 127
|| (o0 == 169 && o1 == 254)
|| (o0 == 172 && o1 >= 16 && o1 <= 31)
|| (o0 == 192 && o1 == 0 && o2 == 0)
|| (o0 == 192 && o1 == 0 && o2 == 2)
|| (o0 == 192 && o1 == 88 && o2 == 99)
|| (o0 == 192 && o1 == 168)
|| (o0 == 198 && (o1 == 18 || o1 == 19))
|| (o0 == 198 && o1 == 51 && o2 == 100)
|| (o0 == 203 && o1 == 0 && o2 == 113)
|| (o0 >= 224 && o0 <= 239)
|| (o0 >= 240)
}
#[must_use]
#[inline]
pub const fn is_restricted_ipv6_segments(segments: [u16; 8]) -> bool {
let seg = segments;
let s0 = seg[0];
let s1 = seg[1];
let s2 = seg[2];
let s3 = seg[3];
let s4 = seg[4];
let s5 = seg[5];
let s6 = seg[6];
let s7 = seg[7];
(s0 == 0
&& s1 == 0
&& s2 == 0
&& s3 == 0
&& s4 == 0
&& s5 == 0
&& s6 == 0
&& s7 == 0)
|| (s0 == 0
&& s1 == 0
&& s2 == 0
&& s3 == 0
&& s4 == 0
&& s5 == 0
&& s6 == 0
&& s7 == 1)
|| (s0 == 0
&& s1 == 0
&& s2 == 0
&& s3 == 0
&& s4 == 0
&& s5 == 0xffff
&& is_restricted_ipv4_octets([
((s6 >> 8) & 0xff) as u8,
(s6 & 0xff) as u8,
((s7 >> 8) & 0xff) as u8,
(s7 & 0xff) as u8,
]))
|| (s0 == 0
&& s1 == 0
&& s2 == 0
&& s3 == 0
&& s4 == 0xffff
&& s5 == 0)
|| (s0 == 0x0064
&& s1 == 0xff9b
&& s2 == 0
&& s3 == 0
&& s4 == 0
&& s5 == 0)
|| (s0 == 0x2001 && s1 == 0x0db8)
|| (s0 == 0x2001 && s1 == 0)
|| (s0 == 0x2002
&& is_restricted_ipv4_octets([
((s1 >> 8) & 0xff) as u8,
(s1 & 0xff) as u8,
((s2 >> 8) & 0xff) as u8,
(s2 & 0xff) as u8,
]))
|| ((s0 & 0xfe00) == 0xfc00)
|| ((s0 & 0xffc0) == 0xfe80)
|| ((s0 & 0xffc0) == 0xfec0)
|| ((s0 & 0xff00) == 0xff00)
}
}
#[cfg(not(any(verus, verus_keep_ghost)))]
pub use plain::{is_restricted_ipv4_octets, is_restricted_ipv6_segments};
#[must_use]
#[inline]
pub fn is_restricted_ipv4(ip: &std::net::Ipv4Addr) -> bool {
is_restricted_ipv4_octets(ip.octets())
}
#[must_use]
#[inline]
pub fn is_restricted_ipv6(ip: &std::net::Ipv6Addr) -> bool {
is_restricted_ipv6_segments(ip.segments())
}
#[must_use]
#[inline]
pub fn is_restricted_ip(ip: std::net::IpAddr) -> bool {
match ip {
std::net::IpAddr::V4(v4) => is_restricted_ipv4(&v4),
std::net::IpAddr::V6(v6) => is_restricted_ipv6(&v6),
}
}
#[cfg(test)]
#[allow(clippy::unwrap_used, clippy::expect_used, clippy::panic, missing_docs)]
mod tests {
use super::*;
use std::net::{IpAddr, Ipv4Addr, Ipv6Addr};
#[test]
fn ipv4_octets_core_matches_std_adapter_exhaustively_sampled() {
let mut o0 = 0u16;
while o0 <= 255 {
for o1 in [
0u8, 1, 15, 16, 31, 63, 64, 100, 127, 128, 169, 191, 192, 254,
] {
let ip = Ipv4Addr::new(o0 as u8, o1, 7, 9);
assert_eq!(
is_restricted_ipv4(&ip),
is_restricted_ipv4_octets(ip.octets()),
"adapter/core divergence at {ip}"
);
}
o0 += 1;
}
}
#[test]
fn ipv6_segments_core_matches_std_adapter_on_boundary_classes() {
let cases: [Ipv6Addr; 12] = [
Ipv6Addr::UNSPECIFIED,
Ipv6Addr::LOCALHOST,
Ipv6Addr::new(0, 0, 0, 0, 0, 0xffff, 0x0a00, 0x0001),
Ipv6Addr::new(0, 0, 0, 0, 0, 0xffff, 0x0808, 0x0808),
Ipv6Addr::new(0, 0, 0, 0, 0xffff, 0, 0, 0),
Ipv6Addr::new(0x64, 0xff9b, 0, 0, 0, 0, 0, 1),
Ipv6Addr::new(0x2001, 0x0db8, 0, 0, 0, 0, 0, 1),
Ipv6Addr::new(0x2001, 0, 0xdead, 0xbeef, 0, 0, 0, 1),
Ipv6Addr::new(0x2002, 0x0a00, 0x0001, 0, 0, 0, 0, 1),
Ipv6Addr::new(0x2002, 0x0808, 0x0808, 0, 0, 0, 0, 1),
Ipv6Addr::new(0xfc00, 0, 0, 0, 0, 0, 0, 1),
Ipv6Addr::new(0xfe80, 0, 0, 0, 0, 0, 0, 1),
];
for ip in &cases {
assert_eq!(
is_restricted_ipv6(ip),
is_restricted_ipv6_segments(ip.segments()),
"adapter/core divergence at {ip}"
);
}
}
#[test]
fn ipv6_mapped_embedded_ipv4_matches_ipv4_core() {
for o0 in [0u8, 10, 127, 169, 172, 192, 8] {
for o1 in [0u8, 0, 254, 16, 168, 8] {
let mapped = Ipv4Addr::new(o0, o1, 3, 4).to_ipv6_mapped();
assert_eq!(
is_restricted_ipv6(&mapped),
is_restricted_ipv4_octets([o0, o1, 3, 4]),
"mapped/embedded divergence for {o0}.{o1}.3.4"
);
}
}
}
#[test]
fn dispatch_kernel_matches_component_kernels() {
assert!(is_restricted_ip(IpAddr::V4(Ipv4Addr::new(10, 0, 0, 1))));
assert!(is_restricted_ip(IpAddr::V6(Ipv6Addr::LOCALHOST)));
assert!(!is_restricted_ip(IpAddr::V4(Ipv4Addr::new(8, 8, 8, 8))));
assert!(!is_restricted_ip(IpAddr::V6(Ipv6Addr::new(
0x2606, 0x4700, 0, 0, 0, 0, 0, 0x1111
))));
}
}