Theory CIDR_Split
theory CIDR_Split
imports IP_Address
Prefix_Match
Hs_Compat
begin
section‹CIDR Split Motivation (Example for IPv4)›
text‹When talking about ranges of IP addresses, we can make the ranges explicit by listing their elements.›
context
begin
private lemma "map (of_nat ∘ nat) [1 .. 4] = ([1, 2, 3, 4]:: 32 word list)" by eval
private definition ipv4addr_upto :: "32 word ⇒ 32 word ⇒ 32 word list" where
"ipv4addr_upto i j ≡ map (of_nat ∘ nat) [int (unat i) .. int (unat j)]"
private lemma ipv4addr_upto: "set (ipv4addr_upto i j) = {i .. j}"
proof -
have int_interval_eq_image: "{int m..int n} = int ` {m..n}" for m n
by (auto intro!: image_eqI [of _ int "nat k" for k])
have helpX:"⋀f (i::nat) (j::nat). (f ∘ nat) ` {int i..int j} = f ` {i .. j}"
by (auto simp add: image_comp int_interval_eq_image)
have hlp: ‹i ≤ word_of_nat (nat xa)› ‹word_of_nat (nat xa) ≤ j›
if ‹uint i ≤ xa› ‹xa ≤ uint j› for xa :: int
proof -
from uint_nonnegative [of i] ‹uint i ≤ xa›
have ‹0 ≤ xa› by (rule order_trans)
moreover from ‹xa ≤ uint j› uint_bounded [of j]
have ‹xa < 2 ^ 32› by simp
ultimately have xa: ‹take_bit 32 xa = xa›
by (simp add: take_bit_int_eq_self)
from xa ‹uint i ≤ xa› show ‹i ≤ word_of_nat (nat xa)›
by transfer simp
from xa ‹xa ≤ uint j› show ‹word_of_nat (nat xa) ≤ j›
by transfer simp
qed
show ?thesis
unfolding ipv4addr_upto_def
apply (rule set_eqI)
apply (auto simp add: hlp)
apply (metis (mono_tags) atLeastAtMost_iff image_iff unat_eq_nat_uint word_less_eq_iff_unsigned word_unat.Rep_inverse)
done
qed
text‹The function @{const ipv4addr_upto} gives back a list of all the ips in the list.
This list can be pretty huge! In the following, we will use CIDR notation (e.g. 192.168.0.0/24)
to describe the list more compactly.›
end
section‹CIDR Split›
context
begin
private lemma find_SomeD: "find f x = Some y ⟹ f y ∧ y ∈ set x"
by(induction x; simp split: if_splits)
private definition pfxes :: "'a::len0 itself ⇒ nat list" where
"pfxes _ = map nat [0..int(len_of TYPE ('a))]"
private lemma "pfxes TYPE(32) = map nat [0 .. 32]" by eval
private definition "largest_contained_prefix (a::('a :: len) word) r = (
let cs = (map (λs. PrefixMatch a s) (pfxes TYPE('a)));
cfs = find (λs. valid_prefix s ∧ wordinterval_subset (prefix_to_wordinterval s) r) cs in
cfs)
"
text‹Split off one prefix:›
private definition wordinterval_CIDR_split1
:: "'a::len wordinterval ⇒ 'a prefix_match option × 'a wordinterval" where
"wordinterval_CIDR_split1 r ≡ (
let ma = wordinterval_lowest_element r in
case ma of
None ⇒ (None, r) |
Some a ⇒ (case largest_contained_prefix a r of
None ⇒ (None, r) |
Some m ⇒ (Some m, wordinterval_setminus r (prefix_to_wordinterval m))))"
private lemma wordinterval_CIDR_split1_innard_helper: fixes a::"'a::len word"
shows "wordinterval_lowest_element r = Some a ⟹
largest_contained_prefix a r ≠ None"
proof -
assume a: "wordinterval_lowest_element r = Some a"
have b: "(a,len_of(TYPE('a))) ∈ set (map (Pair a) (pfxes TYPE('a)))"
unfolding pfxes_def set_map set_upto
using Set.image_iff atLeastAtMost_iff int_eq_iff order_refl by metis
have c: "valid_prefix (PrefixMatch a (len_of(TYPE('a))))" by(simp add: valid_prefix_def pfxm_mask_def)
have "wordinterval_to_set (prefix_to_wordinterval (PrefixMatch a (len_of(TYPE('a))))) = {a}"
unfolding prefix_to_wordinterval_def pfxm_mask_def by simp
moreover have "a ∈ wordinterval_to_set r"
using a wordinterval_lowest_element_set_eq wordinterval_lowest_none_empty
by (metis is_lowest_element_def option.distinct(1))
ultimately have d:
"wordinterval_to_set (prefix_to_wordinterval (PrefixMatch a (LENGTH('a)))) ⊆ wordinterval_to_set r"
by simp
show ?thesis
unfolding largest_contained_prefix_def Let_def
using b c d by(auto simp add: find_None_iff)
qed
private lemma r_split1_not_none: fixes r:: "'a::len wordinterval"
shows "¬ wordinterval_empty r ⟹ fst (wordinterval_CIDR_split1 r) ≠ None"
unfolding wordinterval_CIDR_split1_def Let_def
by(cases "wordinterval_lowest_element r")
(auto simp add: wordinterval_lowest_none_empty
dest: wordinterval_CIDR_split1_innard_helper)
private lemma largest_contained_prefix_subset:
"largest_contained_prefix a r = Some p ⟹ wordinterval_to_set (prefix_to_wordinterval p) ⊆ wordinterval_to_set r"
unfolding largest_contained_prefix_def Let_def
by(drule find_SomeD) simp
private lemma wordinterval_CIDR_split1_snd: "wordinterval_CIDR_split1 r = (Some s, u) ⟹ u = wordinterval_setminus r (prefix_to_wordinterval s)"
unfolding wordinterval_CIDR_split1_def Let_def by(clarsimp split: option.splits)
private lemma largest_contained_prefix_subset_s1D:
"wordinterval_CIDR_split1 r = (Some s, u) ⟹ wordinterval_to_set (prefix_to_wordinterval s) ⊆ wordinterval_to_set r"
by(intro largest_contained_prefix_subset[where a = "the (wordinterval_lowest_element r)"])
(simp add: wordinterval_CIDR_split1_def split: option.splits)
private theorem wordinterval_CIDR_split1_preserve: fixes r:: "'a::len wordinterval"
shows "wordinterval_CIDR_split1 r = (Some s, u) ⟹ wordinterval_eq (wordinterval_union (prefix_to_wordinterval s) u) r"
proof(unfold wordinterval_eq_set_eq)
assume as: "wordinterval_CIDR_split1 r = (Some s, u)"
have ud: "u = wordinterval_setminus r (prefix_to_wordinterval s)"
using as[THEN wordinterval_CIDR_split1_snd] .
with largest_contained_prefix_subset_s1D[OF as]
show "wordinterval_to_set (wordinterval_union (prefix_to_wordinterval s) u) = wordinterval_to_set r"
unfolding ud by auto
qed
private lemma wordinterval_CIDR_split1_some_r_ne:
"wordinterval_CIDR_split1 r = (Some s, u) ⟹ ¬ wordinterval_empty r"
proof(rule ccontr, goal_cases)
case 1
have "wordinterval_lowest_element r = None" unfolding wordinterval_lowest_none_empty using 1(2) unfolding not_not .
then have "wordinterval_CIDR_split1 r = (None, r)" unfolding wordinterval_CIDR_split1_def Let_def by simp
then show False using 1(1) by simp
qed
private lemma wordinterval_CIDR_split1_distinct: fixes r:: "'a::len wordinterval"
shows "wordinterval_CIDR_split1 r = (Some s, u) ⟹
wordinterval_empty (wordinterval_intersection (prefix_to_wordinterval s) u)"
proof(goal_cases)
case 1
have nn: "wordinterval_lowest_element r ≠ None"
using wordinterval_CIDR_split1_some_r_ne 1 wordinterval_lowest_none_empty by metis
from 1 have "u = wordinterval_setminus r (prefix_to_wordinterval s)"
by(elim wordinterval_CIDR_split1_snd)
then show ?thesis by simp
qed
private lemma wordinterval_CIDR_split1_distinct2: fixes r:: "'a::len wordinterval"
shows "wordinterval_CIDR_split1 r = (Some s, u) ⟹
wordinterval_empty (wordinterval_intersection (prefix_to_wordinterval s) u)"
by(rule wordinterval_CIDR_split1_distinct[where r = r]) simp
function wordinterval_CIDR_split_prefixmatch
:: "'a::len wordinterval ⇒ 'a prefix_match list" where
"wordinterval_CIDR_split_prefixmatch rs = (
if
¬ wordinterval_empty rs
then case wordinterval_CIDR_split1 rs
of (Some s, u) ⇒ s # wordinterval_CIDR_split_prefixmatch u
| _ ⇒ []
else
[]
)"
by pat_completeness simp
termination wordinterval_CIDR_split_prefixmatch
proof(relation "measure (card ∘ wordinterval_to_set)", rule wf_measure, unfold in_measure comp_def, goal_cases)
note vernichter = wordinterval_empty_set_eq wordinterval_intersection_set_eq wordinterval_union_set_eq wordinterval_eq_set_eq
case (1 rs x y x2)
note some = 1(2)[unfolded 1(3), symmetric]
from prefix_never_empty have "wordinterval_to_set (prefix_to_wordinterval x2) ≠ {}" unfolding vernichter .
thus ?case
unfolding wordinterval_CIDR_split1_preserve[OF some, unfolded vernichter, symmetric]
unfolding card_Un_disjoint[OF finite finite wordinterval_CIDR_split1_distinct[OF some, unfolded vernichter]]
by auto
qed
private lemma unfold_rsplit_case:
assumes su: "(Some s, u) = wordinterval_CIDR_split1 rs"
shows "(case wordinterval_CIDR_split1 rs of (None, u) ⇒ []
| (Some s, u) ⇒ s # wordinterval_CIDR_split_prefixmatch u) = s # wordinterval_CIDR_split_prefixmatch u"
using su by (metis option.simps(5) split_conv)
lemma "wordinterval_CIDR_split_prefixmatch
(RangeUnion (WordInterval (0x40000000) 0x5FEFBBCC) (WordInterval 0x5FEEBB1C 0x7FFFFFFF))
= [PrefixMatch (0x40000000::32 word) 2]" by eval
lemma "length (wordinterval_CIDR_split_prefixmatch (WordInterval 0 (0xFFFFFFFE::32 word))) = 32" by eval
declare wordinterval_CIDR_split_prefixmatch.simps[simp del]
theorem wordinterval_CIDR_split_prefixmatch:
"wordinterval_to_set r = (⋃x∈set (wordinterval_CIDR_split_prefixmatch r). prefix_to_wordset x)"
proof(induction r rule: wordinterval_CIDR_split_prefixmatch.induct)
case (1 rs)
show ?case proof(cases "wordinterval_empty rs")
case True
thus ?thesis by(simp add: wordinterval_CIDR_split_prefixmatch.simps)
next
case False
obtain x y where s1: "wordinterval_CIDR_split1 rs = (Some x, y)"
using r_split1_not_none[OF False] by(auto simp add: fst_def split: prod.splits)
have mIH: "wordinterval_to_set y = (⋃x∈set (wordinterval_CIDR_split_prefixmatch y). prefix_to_wordset x)"
using 1[OF False s1[symmetric] refl] .
have *: "wordinterval_to_set rs = prefix_to_wordset x ∪ (⋃x∈set (wordinterval_CIDR_split_prefixmatch y). prefix_to_wordset x)"
unfolding mIH[symmetric]
proof -
have ud: "y = wordinterval_setminus rs (prefix_to_wordinterval x)"
using wordinterval_CIDR_split1_snd[OF s1] .
have ss: "prefix_to_wordset x ⊆ wordinterval_to_set rs"
using largest_contained_prefix_subset_s1D[OF s1] by simp
show "wordinterval_to_set rs = prefix_to_wordset x ∪ wordinterval_to_set y"
unfolding ud using ss by simp blast
qed
show ?thesis
apply(subst wordinterval_CIDR_split_prefixmatch.simps)
apply(unfold if_P[OF False] s1 prod.simps option.simps *)
apply(simp)
done
qed
qed
lemma wordinterval_CIDR_split_prefixmatch_all_valid_Ball: fixes r:: "'a::len wordinterval"
shows "∀e∈set (wordinterval_CIDR_split_prefixmatch r). valid_prefix e ∧ pfxm_length e ≤ LENGTH('a)"
proof(induction r rule: wordinterval_CIDR_split_prefixmatch.induct)
case 1
case (1 rs)
show ?case proof(cases "wordinterval_empty rs")
case False
obtain x y where s1: "wordinterval_CIDR_split1 rs = (Some x, y)"
using r_split1_not_none[OF False] by(auto simp add: fst_def split: prod.splits)
hence i1: "valid_prefix x"
unfolding wordinterval_CIDR_split1_def Let_def largest_contained_prefix_def
by(auto dest: find_SomeD split: option.splits)
have i2: "pfxm_length x ≤ LENGTH('a)"
using s1 unfolding wordinterval_CIDR_split1_def Let_def largest_contained_prefix_def pfxes_def
by(force split: option.splits dest: find_SomeD simp: nat_le_iff)
have mIH: "∀a∈set (wordinterval_CIDR_split_prefixmatch y). valid_prefix a ∧ pfxm_length a ≤ LENGTH('a)"
using 1[OF False s1[symmetric] refl] .
with i1 i2 show ?thesis
apply(subst wordinterval_CIDR_split_prefixmatch.simps)
apply(unfold if_P[OF False] s1 prod.simps option.simps)
apply(simp)
done
qed (simp add: wordinterval_CIDR_split_prefixmatch.simps)
qed
private lemma wordinterval_CIDR_split_prefixmatch_all_valid_less_Ball_hlp:
"x ∈ set [s←map (PrefixMatch x2) (pfxes TYPE('a::len0)) . valid_prefix s ∧ wordinterval_to_set (prefix_to_wordinterval s) ⊆ wordinterval_to_set rs] ⟹ pfxm_length x ≤ LENGTH('a)"
by(clarsimp simp: pfxes_def) presburger
text‹Since @{const wordinterval_CIDR_split_prefixmatch} only returns valid prefixes, we can safely convert it to CIDR lists›
lemma "valid_prefix (PrefixMatch (0::16 word) 20)" by(simp add: valid_prefix_def)
lemma wordinterval_CIDR_split_disjunct: "a ∈ set (wordinterval_CIDR_split_prefixmatch i) ⟹
b ∈ set (wordinterval_CIDR_split_prefixmatch i) ⟹ a ≠ b ⟹
prefix_to_wordset a ∩ prefix_to_wordset b = {}"
proof(induction i rule: wordinterval_CIDR_split_prefixmatch.induct)
case (1 rs)
note IH = 1(1)
have prema: "a ∈ set (wordinterval_CIDR_split_prefixmatch rs)" (is "a ∈ ?os") using 1 by simp
have premb: "b ∈ ?os" using 1 by simp
show ?case proof(cases "wordinterval_empty rs")
case False
obtain x y where s1: "wordinterval_CIDR_split1 rs = (Some x, y)"
using r_split1_not_none[OF False] by(auto simp add: fst_def split: prod.splits)
have mi: "k ∈ set (wordinterval_CIDR_split_prefixmatch y)" (is "k ∈ ?rs")
if p: "k ≠ x" "k ∈ ?os" for k using p s1
by(subst (asm) wordinterval_CIDR_split_prefixmatch.simps) (simp only: if_P[OF False] split: prod.splits option.splits; simp)
have a: "k ∈ ?rs ⟹ prefix_to_wordset k ⊆ wordinterval_to_set y" for k
unfolding wordinterval_CIDR_split_prefixmatch by blast
have b: "prefix_to_wordset x ∩ wordinterval_to_set y = {}"
using wordinterval_CIDR_split1_snd[OF s1] by simp
show ?thesis
proof(cases "a = x"; cases "b = x")
assume as: "a = x" "b ≠ x"
with a[OF mi[OF as(2) premb]] b
show ?thesis by blast
next
assume as: "a ≠ x" "b = x"
with a[OF mi[OF as(1) prema]] b
show ?thesis by blast
next
assume as: "a ≠ x" "b ≠ x"
have i: "a ∈ ?rs" "b ∈ ?rs"
using as mi prema premb by blast+
show "prefix_to_wordset a ∩ prefix_to_wordset b = {}"
by(rule IH[OF False s1[symmetric] refl i]) (fact 1)
next
assume as: "a = x" "b = x"
with 1 have False by simp
thus ?thesis ..
qed
next
case True
hence "wordinterval_CIDR_split_prefixmatch rs = []" by(simp add: wordinterval_CIDR_split_prefixmatch.simps)
thus ?thesis using prema by simp
qed
qed
lemma wordinterval_CIDR_split_distinct: "distinct (wordinterval_CIDR_split_prefixmatch i)"
proof(induction i rule: wordinterval_CIDR_split_prefixmatch.induct)
case (1 rs)
show ?case proof(cases "wordinterval_empty rs")
case False
obtain x y where s1: "wordinterval_CIDR_split1 rs = (Some x, y)"
using r_split1_not_none[OF False] by(auto simp add: fst_def split: prod.splits)
have mIH: "distinct (wordinterval_CIDR_split_prefixmatch y)"
using 1[OF False s1[symmetric] refl] .
have "prefix_to_wordset x ∩ wordinterval_to_set y = {}"
using wordinterval_CIDR_split1_snd[OF s1] by simp
hence i1: "x ∉ set (wordinterval_CIDR_split_prefixmatch y)"
unfolding wordinterval_CIDR_split_prefixmatch using prefix_never_empty[of x, simplified] by blast
show ?thesis
using s1
by(subst wordinterval_CIDR_split_prefixmatch.simps)
(simp add: if_P[OF False] mIH i1 split: option.splits prod.splits)
qed (simp add: wordinterval_CIDR_split_prefixmatch.simps)
qed
lemma wordinterval_CIDR_split_existential:
"x ∈ wordinterval_to_set w ⟹ ∃s. s ∈ set (wordinterval_CIDR_split_prefixmatch w) ∧ x ∈ prefix_to_wordset s"
using wordinterval_CIDR_split_prefixmatch[symmetric] by fastforce
subsection‹Versions for @{const ipset_from_cidr}›
definition cidr_split :: "'i::len wordinterval ⇒ ('i word × nat) list" where
"cidr_split rs ≡ map prefix_match_to_CIDR (wordinterval_CIDR_split_prefixmatch rs)"
corollary cidr_split_prefix:
fixes r :: "'i::len wordinterval"
shows "(⋃x∈set (cidr_split r). uncurry ipset_from_cidr x) = wordinterval_to_set r"
unfolding wordinterval_CIDR_split_prefixmatch[symmetric] cidr_split_def
apply(simp add: prefix_match_to_CIDR_def2 wordinterval_CIDR_split_prefixmatch)
using prefix_to_wordset_ipset_from_cidr wordinterval_CIDR_split_prefixmatch_all_valid_Ball by blast
corollary cidr_split_prefix_single:
fixes start :: "'i::len word"
shows "(⋃x∈set (cidr_split (iprange_interval (start, end))). uncurry ipset_from_cidr x) = {start..end}"
unfolding wordinterval_to_set.simps[symmetric]
using cidr_split_prefix iprange_interval.simps by metis
private lemma interval_in_splitD: "xa ∈ foo ⟹ prefix_to_wordset xa ⊆ ⋃(prefix_to_wordset ` foo)" by auto
lemma cidrsplit_no_overlaps: "⟦
x ∈ set (wordinterval_CIDR_split_prefixmatch wi);
xa ∈ set (wordinterval_CIDR_split_prefixmatch wi);
pt && ~~ (pfxm_mask x) = pfxm_prefix x;
pt && ~~ (pfxm_mask xa) = pfxm_prefix xa
⟧
⟹ x = xa"
proof(rule ccontr, goal_cases)
case 1
hence "prefix_match_semantics x pt" "prefix_match_semantics xa pt" unfolding prefix_match_semantics_def by (simp_all add: word_bw_comms(1))
moreover have "valid_prefix x" "valid_prefix xa" using 1(1-2) wordinterval_CIDR_split_prefixmatch_all_valid_Ball by blast+
ultimately have "pt ∈ prefix_to_wordset x" "pt ∈ prefix_to_wordset xa"
using prefix_match_semantics_wordset by blast+
with wordinterval_CIDR_split_disjunct[OF 1(1,2) 1(5)] show False by blast
qed
end
end