Theory IPv4
theory IPv4
imports IP_Address
NumberWang_IPv4
begin
section ‹IPv4 Adresses›
text‹An IPv4 address is basically a 32 bit unsigned integer.›
type_synonym ipv4addr = "32 word"
lemma ipv4addr_and_mask_eq_self [simp]:
‹a && 4294967295 = a› for a :: ipv4addr
proof -
have ‹take_bit 32 a = a›
by (rule take_bit_word_eq_self) simp
then show ?thesis
by (simp add: take_bit_eq_mask mask_numeral)
qed
text‹Conversion between natural numbers and IPv4 adresses›
definition nat_of_ipv4addr :: "ipv4addr ⇒ nat" where
"nat_of_ipv4addr a = unat a"
definition ipv4addr_of_nat :: "nat ⇒ ipv4addr" where
"ipv4addr_of_nat n = of_nat n"
text‹The maximum IPv4 addres›
definition max_ipv4_addr :: "ipv4addr" where
"max_ipv4_addr ≡ ipv4addr_of_nat ((2^32) - 1)"
lemma max_ipv4_addr_number: "max_ipv4_addr = 4294967295"
unfolding max_ipv4_addr_def ipv4addr_of_nat_def by(simp)
lemma "max_ipv4_addr = 0b11111111111111111111111111111111"
by(fact max_ipv4_addr_number)
lemma max_ipv4_addr_max_word: "max_ipv4_addr = - 1"
by(simp add: max_ipv4_addr_number)
lemma max_ipv4_addr_max[simp]: "∀a. a ≤ max_ipv4_addr"
by(simp add: max_ipv4_addr_max_word)
lemma UNIV_ipv4addrset: "UNIV = {0 .. max_ipv4_addr}"
by(simp add: max_ipv4_addr_max_word) fastforce
text‹identity functions›
lemma nat_of_ipv4addr_ipv4addr_of_nat_mod: "nat_of_ipv4addr (ipv4addr_of_nat n) = n mod 2^32"
by (simp add: ipv4addr_of_nat_def nat_of_ipv4addr_def unat_of_nat take_bit_eq_mod)
lemma nat_of_ipv4addr_ipv4addr_of_nat:
"⟦ n ≤ nat_of_ipv4addr max_ipv4_addr ⟧ ⟹ nat_of_ipv4addr (ipv4addr_of_nat n) = n"
by (simp add: nat_of_ipv4addr_ipv4addr_of_nat_mod max_ipv4_addr_def)
lemma ipv4addr_of_nat_nat_of_ipv4addr: "ipv4addr_of_nat (nat_of_ipv4addr addr) = addr"
by(simp add: ipv4addr_of_nat_def nat_of_ipv4addr_def)
subsection‹Representing IPv4 Adresses (Syntax)›
context
includes bit_operations_syntax
begin
fun ipv4addr_of_dotdecimal :: "nat × nat × nat × nat ⇒ ipv4addr" where
"ipv4addr_of_dotdecimal (a,b,c,d) = ipv4addr_of_nat (d + 256 * c + 65536 * b + 16777216 * a )"
fun dotdecimal_of_ipv4addr :: "ipv4addr ⇒ nat × nat × nat × nat" where
"dotdecimal_of_ipv4addr a = (nat_of_ipv4addr ((a >> 24) AND 0xFF),
nat_of_ipv4addr ((a >> 16) AND 0xFF),
nat_of_ipv4addr ((a >> 8) AND 0xFF),
nat_of_ipv4addr (a AND 0xff))"
declare ipv4addr_of_dotdecimal.simps[simp del]
declare dotdecimal_of_ipv4addr.simps[simp del]
text‹Examples:›
lemma "ipv4addr_of_dotdecimal (192, 168, 0, 1) = 3232235521"
by(simp add: ipv4addr_of_dotdecimal.simps ipv4addr_of_nat_def)
lemma "dotdecimal_of_ipv4addr 3232235521 = (192, 168, 0, 1)"
by(simp add: dotdecimal_of_ipv4addr.simps nat_of_ipv4addr_def)
text‹a different notation for @{term ipv4addr_of_dotdecimal}›
lemma ipv4addr_of_dotdecimal_bit:
"ipv4addr_of_dotdecimal (a,b,c,d) =
(ipv4addr_of_nat a << 24) + (ipv4addr_of_nat b << 16) +
(ipv4addr_of_nat c << 8) + ipv4addr_of_nat d"
proof -
have a: "(ipv4addr_of_nat a) << 24 = ipv4addr_of_nat (a * 16777216)"
by(simp add: ipv4addr_of_nat_def shiftl_t2n)
have b: "(ipv4addr_of_nat b) << 16 = ipv4addr_of_nat (b * 65536)"
by(simp add: ipv4addr_of_nat_def shiftl_t2n)
have c: "(ipv4addr_of_nat c) << 8 = ipv4addr_of_nat (c * 256)"
by(simp add: ipv4addr_of_nat_def shiftl_t2n)
have ipv4addr_of_nat_suc: "⋀x. ipv4addr_of_nat (Suc x) = word_succ (ipv4addr_of_nat (x))"
by(simp add: ipv4addr_of_nat_def, metis Abs_fnat_hom_Suc of_nat_Suc)
{ fix x y
have "ipv4addr_of_nat x + ipv4addr_of_nat y = ipv4addr_of_nat (x+y)"
apply(induction x arbitrary: y)
apply(simp add: ipv4addr_of_nat_def; fail)
by(simp add: ipv4addr_of_nat_suc word_succ_p1)
} from this a b c
show ?thesis
apply(simp add: ipv4addr_of_dotdecimal.simps)
apply(rule arg_cong[where f=ipv4addr_of_nat])
apply(thin_tac _)+
by presburger
qed
lemma size_ipv4addr: "size (x::ipv4addr) = 32" by(simp add:word_size)
lemma dotdecimal_of_ipv4addr_ipv4addr_of_dotdecimal:
"⟦ a < 256; b < 256; c < 256; d < 256 ⟧ ⟹
dotdecimal_of_ipv4addr (ipv4addr_of_dotdecimal (a,b,c,d)) = (a,b,c,d)"
proof -
assume "a < 256" and "b < 256" and "c < 256" and "d < 256"
note assms= ‹a < 256› ‹b < 256› ‹c < 256› ‹d < 256›
hence a: "nat_of_ipv4addr ((ipv4addr_of_nat (d + 256 * c + 65536 * b + 16777216 * a) >> 24) AND mask 8) = a"
apply (simp only: flip: take_bit_eq_mask)
apply (simp add: ipv4addr_of_nat_def nat_of_ipv4addr_def)
apply transfer
apply (simp add: drop_bit_take_bit nat_take_bit_eq flip: take_bit_eq_mask)
apply (simp add: drop_bit_eq_div take_bit_eq_mod)
done
have ipv4addr_of_nat_AND_mask8: "(ipv4addr_of_nat a) AND mask 8 = (ipv4addr_of_nat (a mod 256))"
for a
apply (simp only: flip: take_bit_eq_mask)
apply (simp add: ipv4addr_of_nat_def)
apply transfer
apply (simp flip: take_bit_eq_mask)
apply (simp add: take_bit_eq_mod of_nat_mod)
done
from assms have b:
"nat_of_ipv4addr ((ipv4addr_of_nat (d + 256 * c + 65536 * b + 16777216 * a) >> 16) AND mask 8) = b"
apply (simp only: flip: take_bit_eq_mask)
apply (simp add: ipv4addr_of_nat_def nat_of_ipv4addr_def)
apply transfer
apply (simp add: drop_bit_take_bit flip: take_bit_eq_mask)
using div65536
apply (simp add: drop_bit_eq_div take_bit_eq_mod)
done
from assms have c:
"nat_of_ipv4addr ((ipv4addr_of_nat (d + 256 * c + 65536 * b + 16777216 * a) >> 8) AND mask 8) = c"
apply (simp only: flip: take_bit_eq_mask)
apply (simp add: ipv4addr_of_nat_def nat_of_ipv4addr_def)
apply transfer
apply (simp add: drop_bit_take_bit flip: take_bit_eq_mask)
using div256
apply (simp add: drop_bit_eq_div take_bit_eq_mod)
done
from ‹d < 256› have d: "nat_of_ipv4addr (ipv4addr_of_nat (d + 256 * c + 65536 * b + 16777216 * a) AND mask 8) = d"
apply (simp only: flip: take_bit_eq_mask)
apply (simp add: ipv4addr_of_nat_AND_mask8 ipv4addr_of_nat_def nat_of_ipv4addr_def)
apply transfer
apply (simp flip: take_bit_eq_mask)
apply (simp add: take_bit_eq_mod nat_mod_distrib nat_add_distrib nat_mult_distrib mod256)
done
from a b c d show ?thesis
apply (simp add: ipv4addr_of_dotdecimal.simps dotdecimal_of_ipv4addr.simps mask_numeral)
done
qed
lemma ipv4addr_of_dotdecimal_dotdecimal_of_ipv4addr:
"(ipv4addr_of_dotdecimal (dotdecimal_of_ipv4addr ip)) = ip"
proof -
have ip_and_mask8_bl_drop24: "(ip::ipv4addr) AND mask 8 = of_bl (drop 24 (to_bl ip))"
by(simp add: of_drop_to_bl size_ipv4addr)
have List_rev_drop_geqn: "length x ≥ n ⟹ (take n (rev x)) = rev (drop (length x - n) x)"
for x :: "'a list" and n by(simp add: List.rev_drop)
have and_mask_bl_take: "length x ≥ n ⟹ ((of_bl x) AND mask n) = (of_bl (rev (take n (rev (x)))))"
for x n by(simp add: List_rev_drop_geqn of_bl_drop)
have ipv4addr_and_255: "x AND 255 = take_bit 8 x" for x :: ipv4addr
by (simp add: take_bit_eq_mask mask_numeral)
have bit_equality:
"((ip >> 24) AND 0xFF << 24) + ((ip >> 16) AND 0xFF << 16) + ((ip >> 8) AND 0xFF << 8) + (ip AND 0xFF) =
of_bl (take 8 (to_bl ip) @ take 8 (drop 8 (to_bl ip)) @ take 8 (drop 16 (to_bl ip)) @ drop 24 (to_bl ip))"
apply (simp add: ipv4addr_and_255 shiftl_def shiftr_def rev_drop rev_take drop_take)
apply (simp only: of_bl_append mult.commute [of ‹2 ^ n› for n] flip: push_bit_eq_mult)
apply (simp add: of_bl_drop_eq_take_bit take_drop of_bl_take_to_bl_eq_drop_bit take_bit_drop_bit take_bit_word_eq_self)
done
have blip_split: "⋀ blip. length blip = 32 ⟹
blip = (take 8 blip) @ (take 8 (drop 8 blip)) @ (take 8 (drop 16 blip)) @ (take 8 (drop 24 blip))"
by(rename_tac blip,case_tac blip,simp_all)+
have "ipv4addr_of_dotdecimal (dotdecimal_of_ipv4addr ip) = of_bl (to_bl ip)"
apply (subst blip_split)
apply simp
apply (simp add: ipv4addr_of_dotdecimal_bit dotdecimal_of_ipv4addr.simps)
apply (simp add: ipv4addr_of_nat_nat_of_ipv4addr)
apply (simp flip: bit_equality)
done
thus ?thesis using word_bl.Rep_inverse[symmetric] by simp
qed
lemma ipv4addr_of_dotdecimal_eqE:
"⟦ ipv4addr_of_dotdecimal (a,b,c,d) = ipv4addr_of_dotdecimal (e,f,g,h);
a < 256; b < 256; c < 256; d < 256; e < 256; f < 256; g < 256; h < 256 ⟧ ⟹
a = e ∧ b = f ∧ c = g ∧ d = h"
by (metis Pair_inject dotdecimal_of_ipv4addr_ipv4addr_of_dotdecimal)
subsection‹IP Ranges: Examples›
lemma "(UNIV :: ipv4addr set) = {0 .. max_ipv4_addr}" by(simp add: UNIV_ipv4addrset)
lemma "(42::ipv4addr) ∈ UNIV" by(simp)
lemma "ipset_from_netmask (ipv4addr_of_dotdecimal (192,168,0,42)) (ipv4addr_of_dotdecimal (255,255,0,0)) =
{ipv4addr_of_dotdecimal (192,168,0,0) .. ipv4addr_of_dotdecimal (192,168,255,255)}"
by(simp add: ipset_from_netmask_def ipv4addr_of_dotdecimal.simps ipv4addr_of_nat_def)
lemma "ipset_from_netmask (ipv4addr_of_dotdecimal (192,168,0,42)) (ipv4addr_of_dotdecimal (0,0,0,0)) = UNIV"
by(simp add: UNIV_ipv4addrset ipset_from_netmask_def ipv4addr_of_dotdecimal.simps
ipv4addr_of_nat_def max_ipv4_addr_max_word)
text‹192.168.0.0/24›
lemma fixes addr :: ipv4addr
shows "ipset_from_cidr addr pflength =
ipset_from_netmask addr ((mask pflength) << (32 - pflength))"
by(simp add: ipset_from_cidr_def)
lemma "ipset_from_cidr (ipv4addr_of_dotdecimal (192,168,0,42)) 16 =
{ipv4addr_of_dotdecimal (192,168,0,0) .. ipv4addr_of_dotdecimal (192,168,255,255)}"
by(simp add: ipset_from_cidr_alt mask_eq ipv4addr_of_dotdecimal.simps ipv4addr_of_nat_def)
lemma "ip ∈ (ipset_from_cidr (ipv4addr_of_dotdecimal (0, 0, 0, 0)) 0)"
by(simp add: ipset_from_cidr_0)
lemma ipv4set_from_cidr_32: fixes addr :: ipv4addr
shows "ipset_from_cidr addr 32 = {addr}"
by (simp add: ipset_from_cidr_alt mask_numeral)
lemma fixes pre :: ipv4addr
shows "ipset_from_cidr pre len = {(pre AND ((mask len) << (32 - len))) .. pre OR (mask (32 - len))}"
by (simp add: ipset_from_cidr_alt ipset_from_cidr_def)
text‹making element check executable›
lemma addr_in_ipv4set_from_netmask_code[code_unfold]:
fixes addr :: ipv4addr
shows "addr ∈ (ipset_from_netmask base netmask) ⟷
(base AND netmask) ≤ addr ∧ addr ≤ (base AND netmask) OR (NOT netmask)"
by (simp add: addr_in_ipset_from_netmask_code)
lemma addr_in_ipv4set_from_cidr_code[code_unfold]:
fixes addr :: ipv4addr
shows "addr ∈ (ipset_from_cidr pre len) ⟷
(pre AND ((mask len) << (32 - len))) ≤ addr ∧ addr ≤ pre OR (mask (32 - len))"
by(simp add: addr_in_ipset_from_cidr_code)
lemma "ipv4addr_of_dotdecimal (192,168,42,8) ∈ (ipset_from_cidr (ipv4addr_of_dotdecimal (192,168,0,0)) 16)"
by (simp add: ipv4addr_of_nat_def ipset_from_cidr_def ipv4addr_of_dotdecimal.simps
ipset_from_netmask_def mask_eq_exp_minus_1 word_le_def)
definition ipv4range_UNIV :: "32 wordinterval" where "ipv4range_UNIV ≡ wordinterval_UNIV"
lemma ipv4range_UNIV_set_eq: "wordinterval_to_set ipv4range_UNIV = UNIV"
by(simp only: ipv4range_UNIV_def wordinterval_UNIV_set_eq)
thm iffD1[OF wordinterval_eq_set_eq]
text‹This ‹LENGTH('a)› is 32 for IPv4 addresses.›
lemma ipv4cidr_to_interval_simps[code_unfold]: "ipcidr_to_interval ((pre::ipv4addr), len) = (
let netmask = (mask len) << (32 - len);
network_prefix = (pre AND netmask)
in (network_prefix, network_prefix OR (NOT netmask)))"
by(simp add: ipcidr_to_interval_def Let_def ipcidr_to_interval_start.simps ipcidr_to_interval_end.simps)
end
end