# Theory CIDR_Split

```(*  Title:      CIDR_Split.thy
Authors:    Julius Michaelis, Cornelius Diekmann
*)
theory CIDR_Split
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)]"
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›
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
apply (rule set_eqI)
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)

(*pfxes needs a dummy parameter. The first parameter is a dummy that we have the 'a::len0 type and
can refer to its length.*)
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)));
― ‹anything that is a subset should also be a valid prefix. but try proving that.›
cfs = find (λs. valid_prefix s ∧ wordinterval_subset (prefix_to_wordinterval s) r) cs in
cfs)
"
(* The joke is that it is always Some, given that a ∈ r. *)

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 (*400ms*)
have "wordinterval_to_set (prefix_to_wordinterval (PrefixMatch a (len_of(TYPE('a))))) = {a}"
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")
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)"])

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
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 *) (* WOOOOO simplifier bug (* try making this a simp add: *) *)
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)"
(* The induction is somewhat verbose, so it is less annoying to write the two down at once *)
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

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›
(* actually, just valid_prefix doesn't mean that the prefix length is sane. Fortunately, wordinterval_CIDR_split_prefixmatch_all_valid_Ball does entail that *)
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
(* this is actually a quite general statement, might make a lemma out of it *)
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" (* Nothing to do case *)
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" (* impossible case *)
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)"
(* wish this was a corollary *)
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

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
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
```