# Theory IPv4

```(*  Title:      IPv4.thy
Authors:    Cornelius Diekmann, Julius Michaelis
*)
theory IPv4
NumberWang_IPv4
(* include "HOL-Library.Code_Target_Nat" if you need to work with actual numbers.*)
begin

text‹An IPv4 address is basically a 32 bit unsigned integer.›

‹a && 4294967295 = a› for a :: ipv4addr
proof -
have ‹take_bit 32 a = a›
by (rule take_bit_word_eq_self) simp
then show ?thesis
qed

text‹Conversion between natural numbers and IPv4 adresses›

lemma UNIV_ipv4addrset: "UNIV = {0 .. max_ipv4_addr}" (*not in the simp set, for a reason*)

text‹identity functions›

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
nat_of_ipv4addr ((a >> 16) AND 0xFF),
nat_of_ipv4addr ((a >> 8) AND 0xFF),

text‹Examples:›
lemma "ipv4addr_of_dotdecimal (192, 168, 0, 1) = 3232235521"
(*could be solved by eval, but needs "HOL-Library.Code_Target_Nat"*)
lemma "dotdecimal_of_ipv4addr 3232235521 = (192, 168, 0, 1)"

text‹a different notation for @{term ipv4addr_of_dotdecimal}›
proof -
{ fix x y
apply(induction x arbitrary: y)
} from this a b c
show ?thesis
apply(thin_tac _)+
by presburger
qed

"⟦ a < 256; b < 256; c < 256; d < 256 ⟧ ⟹
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 transfer
done
for a
apply transfer
done
from assms have b:
"nat_of_ipv4addr ((ipv4addr_of_nat (d + 256 * c + 65536 * b + 16777216 * a) >> 16) AND mask 8) = b"
apply transfer
using div65536
done
from assms have c:
"nat_of_ipv4addr ((ipv4addr_of_nat (d + 256 * c + 65536 * b + 16777216 * a) >> 8) AND mask 8) = c"
apply transfer
using div256
done
from ‹d < 256› have d: "nat_of_ipv4addr (ipv4addr_of_nat (d + 256 * c + 65536 * b + 16777216 * a) AND mask 8) = d"
apply transfer
done
from a b c d show ?thesis
done
qed

proof -
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
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 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)+ (*I'm so sorry for this ...*)
apply (subst blip_split)
apply simp
apply (simp flip: bit_equality)
done
thus ?thesis using word_bl.Rep_inverse[symmetric] by simp
qed

a < 256; b < 256; c < 256; d < 256; e < 256; f < 256; g < 256; h < 256 ⟧ ⟹
a = e ∧ b = f ∧ c = g ∧ d = h"

subsection‹IP Ranges: Examples›

(*Warning, not executable!*)

text‹192.168.0.0/24›

lemma "ipset_from_cidr (ipv4addr_of_dotdecimal (192,168,0,42)) 16 =

lemma "ip ∈ (ipset_from_cidr (ipv4addr_of_dotdecimal (0, 0, 0, 0)) 0)"

shows "ipset_from_cidr pre len = {(pre AND ((mask len) << (32 - len))) .. pre OR (mask (32 - len))}"

text‹making element check executable›
shows "addr ∈ (ipset_from_cidr pre len) ⟷

(*small numbers because we didn't load Code_Target_Nat. Should work by eval*)

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]
(*TODO: probably the following is a good idea?*)
(*
declare iffD1[OF wordinterval_eq_set_eq, cong]
*)

text‹This ‹LENGTH('a)› is 32 for IPv4 addresses.›
lemma ipv4cidr_to_interval_simps[code_unfold]: "ipcidr_to_interval ((pre::ipv4addr), len) = (