# Theory OpenFlow_Helpers

section‹Misc›
theory OpenFlow_Helpers
imports Main
begin

lemma hrule: "(S = UNIV) = (∀x. x ∈ S)"
by blast

subsection‹Single valuedness on lists›

lemma foldr_True_set: "foldr (λx. (∧) (f x)) l True = (∀x ∈ set l. f x)"
by (induction l) simp_all

fun single_valued_code where
"single_valued_code [] = True" |
"single_valued_code (e#es) = (foldr (λx. (∧) (fst x ≠ fst e ∨ snd x = snd e)) es True ∧ single_valued_code es)"
lemma single_valued_code_lam[code_unfold]:
"single_valued (set r) = single_valued_code r"
proof(induction r)
case Nil show ?case by simp
next
case (Cons e es)
show ?case
proof (rule iffI, goal_cases fwd bwd)
case bwd
have "single_valued (set es)" using Cons.IH conjunct2[OF bwd[unfolded single_valued_code.simps]] ..
moreover
have "∀x∈set es. fst x ≠ fst e ∨ snd x = snd e"
using conjunct1[OF bwd[unfolded single_valued_code.simps(2)], unfolded foldr_True_set] .
ultimately
show ?case unfolding single_valued_def by auto
next
case fwd
have "single_valued (set es)" using fwd unfolding single_valued_def by simp
with Cons.IH[symmetric] have "single_valued_code es" ..
moreover
have "∀x∈set es. fst x ≠ fst e ∨ snd x = snd e" using fwd unfolding single_valued_def by clarsimp
from conjI[OF this calculation, unfolded foldr_True_set[symmetric]]
show ?case unfolding single_valued_code.simps .
qed
qed

lemma set_Cons: "e ∈ set (a # as) ⟷ (e = a ∨ e ∈ set as)" by simp

subsection‹List fun›

lemma sorted_const: "sorted (map (λy. x) k)"
by(induction k) simp_all

lemma list_all_map: "list_all f (map g l) = list_all (f ∘ g) l"
unfolding comp_def by (simp add: list_all_length) (* by(induction l) simp_all *)

lemma distinct_2lcomprI: "distinct as ⟹ distinct bs ⟹
(⋀a b e i. f a b = f e i ⟹ a = e ∧ b = i) ⟹
distinct [f a b. a ← as, b ← bs]"
apply(induction as)
apply(simp;fail)
apply(clarsimp simp only: distinct.simps simp_thms list.map concat.simps map_append distinct_append)
apply(rule)
subgoal
apply(clarify;fail | subst distinct_map, rule)+
by (rule inj_onI) simp
subgoal by fastforce
done

lemma distinct_3lcomprI: "distinct as ⟹ distinct bs ⟹ distinct cs ⟹
(⋀a b c e i g. f a b c = f e i g ⟹ a = e ∧ b = i ∧ c = g) ⟹
distinct [f a b c. a ← as, b ← bs, c ← cs]"
apply(induction as)
apply(simp;fail)
apply(clarsimp simp only: distinct.simps simp_thms list.map concat.simps map_append distinct_append)
apply(rule)
apply(rule distinct_2lcomprI; simp_all; fail)
apply fastforce
done

lemma distinct_fst: "distinct (map fst a) ⟹ distinct a" by (metis distinct_zipI1 zip_map_fst_snd)
lemma distinct_snd: "distinct (map snd a) ⟹ distinct a" by (metis distinct_zipI2 zip_map_fst_snd)

lemma inter_empty_fst2: "(λ(p, m, a). (p, m))  S ∩ (λ(p, m, a). (p, m))  T = {} ⟹ S ∩ T = {}" by blast

subsection‹Cardinality and Existence of Distinct Members›

lemma card1_eI: "1 ≤ card S ⟹ ∃y S'. S = {y} ∪ S' ∧ y ∉ S'"
by (metis One_nat_def card.infinite card_le_Suc_iff insert_is_Un leD zero_less_Suc)
lemma card2_eI: "2 ≤ card S ⟹ ∃x y. x ≠ y ∧ x ∈ S ∧ y ∈ S"
proof goal_cases
case (1)
then have "1 ≤ card S" by simp
note card1_eI[OF this]
then obtain x S' where xs: "S = {x} ∪ S' ∧ x ∉ S'" by presburger
then have "1 ≤ card S'"
by (metis 1 Suc_1 card.infinite card_insert_if finite_Un insert_is_Un le0 not_less_eq_eq)
then obtain y where "y ∈ S'" by fastforce
then show ?case using xs by force
qed
lemma card3_eI: "3 ≤ card S ⟹ ∃x y z. x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ x ∈ S ∧ y ∈ S"
proof goal_cases
case 1
then have "2 ≤ card S" by simp
note card2_eI[OF this]
then obtain x y S' where xs: "S = {x,y} ∪ S' ∧ x ∉ S' ∧ y ∉ S' ∧ x ≠ y"
by (metis Set.set_insert Un_insert_left insert_eq_iff insert_is_Un)
then have "1 ≤ card S'"
using 1  by (metis One_nat_def Suc_leI Un_insert_left card_gt_0_iff insert_absorb numeral_3_eq_3 singleton_insert_inj_eq card.infinite card_insert_if finite_Un insert_is_Un le0 not_less_eq_eq) (* uuuh *)
then obtain z where "z ∈ S'" by fastforce
then show ?case using xs by force
qed

lemma card1_eE: "finite S ⟹ ∃y. y ∈ S ⟹ 1 ≤ card S" using card_0_eq by fastforce
lemma card2_eE: "finite S ⟹ ∃x y. x ≠ y ∧ x ∈ S ∧ y ∈ S ⟹ 2 ≤ card S"
using card1_eE card_Suc_eq card_insert_if by fastforce
lemma card3_eE: "finite S ⟹ ∃x y z. x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ x ∈ S ∧ y ∈ S ⟹ 3 ≤ card S"
using card2_eE card_Suc_eq card_insert_if oops

lemma f_Img_ex_set: "{f x|x. P x} = f  {x. P x}" by auto

lemma set_maps: "set (List.maps f a) = (⋃a∈set a. set (f a))"
unfolding List.maps_def set_concat set_map UN_simps(10) ..

end


# Theory Sort_Descending

theory Sort_Descending
imports Main
begin

section‹sorting descending›
context linorder
begin
fun sorted_descending :: "'a list ⇒ bool" where
"sorted_descending [] ⟷ True" |
"sorted_descending (a#as) ⟷ (∀x ∈ set as. a ≥ x) ∧ sorted_descending as"

definition sort_descending_key :: "('b ⇒ 'a) ⇒ 'b list ⇒ 'b list" where
"sort_descending_key f xs ≡ rev (sort_key f xs)"
end
lemma sorted_descending_Cons: "sorted_descending (x#xs) ⟷ sorted_descending xs ∧ (∀y∈set xs. y ≤ x)"
by(induction xs) auto

lemma sorted_descending_tail: "sorted_descending (xs@[x]) ⟷ sorted_descending xs ∧ (∀y∈set xs. x ≤ y)"
by(induction xs) auto

lemma sorted_descending_append: "sorted_descending (xs @ ys) =
(sorted_descending xs ∧ sorted_descending ys ∧ (∀x∈set xs. ∀y∈set ys. x ≥ y))"
by(induction xs) auto

lemma sorted_descending: "sorted_descending (rev xs) ⟷ sorted xs"
apply(induction xs)
apply(simp)
done
lemma sorted_descending_alt: "sorted_descending xs ⟷ sorted (rev xs)"
using sorted_descending[of "rev xs"] unfolding rev_rev_ident .

lemma sort_descending: "sorted_descending (sort_descending_key (λx. x) xs)"

lemma sort_descending_key_distinct: "distinct xs ⟹ distinct (sort_descending_key f xs)"

lemma sorted_descending_sort_descending_key: "sorted_descending (map f (sort_descending_key f xs))"
using sorted_descending by (metis rev_map sorted_sort_key)

lemma sorted_descending_split: "sorted_descending (map f l) ⟹
∃m n. l = m @ n ∧ (∀e ∈ set m. f (hd l) = f e) ∧ (∀e ∈ set n. f e < f (hd l))"
proof(induction l)
case Nil thus ?case by simp
next
case (Cons a as)
from Cons(2) have IHm: "sorted_descending (map f as)" by simp
note mIH = Cons(1)[OF this]
thus ?case (is ?kees)
proof(cases as)
case Nil
show ?kees unfolding Nil by force
next
case (Cons aa ass)
show ?kees
proof(cases "f a = f aa")
case True
from mIH obtain m n where mn: "as = m @ n" "(∀e∈set m. f a = f e)" "(∀e∈set n. f e < f a)"
using True local.Cons by auto
have "a # as = a # m @ n" using mn(1) by simp
moreover have "∀e∈set (a # m). f (hd (a # m)) = f e" unfolding list.sel(1) using True mn(2) using Cons by auto
ultimately show "∃m n. a # as = m @ n ∧ (∀e∈set m. f (hd (a # as)) = f e) ∧
(∀e∈set n. f e < f (hd (a # as)))" using mn(3) by (metis append.simps(2) list.sel(1))
next
case False
from Cons.prems have "∀y∈set (map f as). y < f a"
unfolding list.map(2)
unfolding sorted_descending_Cons
unfolding set_map
unfolding local.Cons
using False
by auto
then have "∀e∈set as. f e < f a" by simp
moreover have "a # as = [a] @ as ∧ (∀e∈set [a]. f (hd [a]) = f e)" by simp
ultimately show ?kees by (metis list.sel(1))
qed
qed
qed

lemma sort_descending_set_inv[simp]: "set (sort_descending_key k t) = set t"

end


# Theory List_Group

theory List_Group
imports Sort_Descending
begin

section‹List Group›

function (sequential) list_group_eq :: "'a list ⇒ 'a list list" where
"list_group_eq [] = []" |
"list_group_eq (x#xs) = [x # takeWhile ((=) x) xs] @ list_group_eq (dropWhile ((=) x) xs)"
by pat_completeness auto
termination list_group_eq
apply (relation "measure (λN. length N )")
done

value "list_group_eq [1::int,2,2,2,3,1,4,5,5,5]"

function (sequential) list_group_eq_key :: "('a ⇒ 'b) ⇒ 'a list ⇒ 'a list list" where
"list_group_eq_key _ [] = []" |
"list_group_eq_key f (x#xs) = [x # takeWhile (λy. f x = f y) xs] @ list_group_eq_key f (dropWhile (λy. f x = f y) xs)"
by pat_completeness auto
termination list_group_eq_key
apply (relation "measure (λ(f,N). length N )")
done

value "list_group_eq_key fst [(1::int, ''''), (2,''a''), (2,''b''), (2, ''c''), (3, ''c''), (1,''''), (4,'''')]"

lemma "list_group_eq_key id xs = list_group_eq xs"
apply(induction xs rule: list_group_eq.induct)

(*
lemma "sorted (map f (x#xs)) ⟹ list_group_eq_key f (x#xs) = [x # filter (λy. f x = f y) xs] @ list_group_eq_key f (filter (λy. f x ≠ f y) xs)"
apply(simp)
oops
lemma "sorted (x#xs) ⟹ distinct (list_group_eq_key f (x#xs)) ⟹ distinct (list_group_eq_key f xs)"
apply(induction xs)
apply(simp)
oops
*)

end


# Theory OpenFlow_Matches

theory OpenFlow_Matches
Simple_Firewall.Simple_Packet
(*"../Iptables_Semantics/Primitive_Matchers/Simple_Packet" (* I just want those TCP,UDP,… defs *)*)
"HOL-Library.List_Lexorder"
"HOL-Library.Char_ord" (* For a linorder on strings. See below. *)
begin

(* From OpenFlow 1.1, Table 3: *)
datatype of_match_field =
IngressPort string
| EtherSrc "48 word"
| EtherDst "48 word"
| EtherType "16 word"
| VlanId "16 word"
| VlanPriority "16 word"
(*	| MplsLabel
| MplsClass *)
| IPv4Src "32 prefix_match" (* could also be arbitrary bitmask - see page 80 of 1.5.1 *)
| IPv4Dst "32 prefix_match" (* ditto *)
| IPv4Proto "8 word"
(*	| IPv4ToS "16 word" *)
| L4Src "16 word" "16 word" (* openvswitch 1.6 supports bitmasks - does not seem to be in of 1.5.1, but I need it. *)
| L4Dst "16 word" "16 word"

(* I just do not want this proof in the documentation theory *)
schematic_goal of_match_field_typeset: "(field_match :: of_match_field) ∈ {
IngressPort (?s::string),
EtherSrc (?as::48 word), EtherDst (?ad::48 word),
EtherType (?t::16 word),
VlanId (?i::16 word), VlanPriority (?p::16 word),
IPv4Src (?pms::32 prefix_match),
IPv4Dst (?pmd::32 prefix_match),
IPv4Proto (?ipp :: 8 word),
L4Src (?ps :: 16 word) (?ms :: 16 word),
L4Dst (?pd :: 16 word) (?md :: 16 word)
}"
proof((cases field_match;clarsimp),goal_cases)
next case (IngressPort s)  thus "s = (case field_match of IngressPort s ⇒ s)"  unfolding IngressPort of_match_field.simps by rule
next case (EtherSrc s)     thus "s = (case field_match of EtherSrc s ⇒ s)"     unfolding EtherSrc of_match_field.simps by rule
next case (EtherDst s)     thus "s = (case field_match of EtherDst s ⇒ s)"     unfolding EtherDst of_match_field.simps by rule
next case (EtherType s)    thus "s = (case field_match of EtherType s ⇒ s)"    unfolding EtherType of_match_field.simps by rule
next case (VlanId s)       thus "s = (case field_match of VlanId s ⇒ s)"       unfolding VlanId of_match_field.simps by rule
next case (VlanPriority s) thus "s = (case field_match of VlanPriority s ⇒ s)" unfolding VlanPriority of_match_field.simps by rule
next case (IPv4Src s)      thus "s = (case field_match of IPv4Src s ⇒ s)"      unfolding IPv4Src of_match_field.simps by rule
next case (IPv4Dst s)      thus "s = (case field_match of IPv4Dst s ⇒ s)"      by simp
next case (IPv4Proto s)    thus "s = (case field_match of IPv4Proto s ⇒ s)"    by simp
next case (L4Src p l)      thus "p = (case field_match of L4Src p m ⇒ p) ∧ l = (case field_match of L4Src p m ⇒ m)" by simp
next case (L4Dst p l)      thus "p = (case field_match of L4Dst p m ⇒ p) ∧ l = (case field_match of L4Dst p m ⇒ m)" by simp
qed

(*

The semantics of an openflow match is by no means trivial. See Specification 7.2.3.6, v1.5.1
For example:
▪ An OXM TLV for oxm_type=OXM OF IPV4 SRC is allowed only if it is preceded by another en-
try with oxm_type=OXM_OF_ETH_TYPE, oxm_hasmask=0, and oxm_value=0x0800. That is, match-
ing on the IPv4 source address is allowed only if the Ethernet type is explicitly set to IPv4.
…
Even if OpenFlow 1.0 does not require this behavior, some switches may still silently drop matches without prerequsites.

*)

(* subtable of table in 7.2.3.8 of spec1.5 (also present in 1.3, and less cluttered) for the matches we implement *)
function prerequisites :: "of_match_field ⇒ of_match_field set ⇒ bool" where
"prerequisites (IngressPort _) _ = True" |
(* OF_ETH_DST None *)
"prerequisites (EtherDst _) _ = True" |
(* OF_ETH_SRC None *)
"prerequisites (EtherSrc _) _ = True" |
(* OF_ETH_TYPE None *)
"prerequisites (EtherType _) _ = True" |
(* OF_VLAN_VID None *)
"prerequisites (VlanId _) _ = True" |
(* OF_VLAN_PCP VLAN_VID!=NONE *)
"prerequisites (VlanPriority _) m = (∃id. let v = VlanId id in v ∈ m ∧ prerequisites v m)" |
(* OF_IPV4_PROTO ETH_TYPE=0x0800 or ETH_TYPE=0x86dd *)
"prerequisites (IPv4Proto _) m = (let v = EtherType 0x0800 in v ∈ m ∧ prerequisites v m)" (* IPv6 nah *) |
(* OF_IPV4_SRC ETH_TYPE=0x0800 *)
"prerequisites (IPv4Src _) m = (let v = EtherType 0x0800 in v ∈ m ∧ prerequisites v m)" |
(* OF_IPV4_DST ETH_TYPE=0x0800 *)
"prerequisites (IPv4Dst _) m = (let v = EtherType 0x0800 in v ∈ m ∧ prerequisites v m)" |
(* Now here goes a bit of fuzz: OF specifies differen OXM_OF_(TCP,UDP,L4_Protocol.SCTP,…)_(SRC,DST). I only have L4Src. So gotta make do with that. *)
"prerequisites (L4Src _ _) m = (∃proto ∈ {TCP,UDP,L4_Protocol.SCTP}. let v = IPv4Proto proto in v ∈ m ∧ prerequisites v m)" |
"prerequisites (L4Dst _ _) m = prerequisites (L4Src undefined undefined) m"
by pat_completeness auto
(* Ignoredd PACKET_TYPE=foo *)

fun match_sorter :: "of_match_field ⇒ nat" where
"match_sorter (IngressPort _) = 1" |
"match_sorter (VlanId _) = 2" |
"match_sorter (VlanPriority _) = 3" |
"match_sorter (EtherType _) = 4" |
"match_sorter (EtherSrc _) = 5" |
"match_sorter (EtherDst _) = 6" |
"match_sorter (IPv4Proto _) = 7" |
"match_sorter (IPv4Src _) = 8" |
"match_sorter (IPv4Dst _) = 9" |
"match_sorter (L4Src _ _) = 10" |
"match_sorter (L4Dst _ _) = 11"

termination prerequisites by(relation "measure (match_sorter ∘ fst)", simp_all)

definition less_eq_of_match_field1 :: "of_match_field ⇒ of_match_field ⇒ bool"
where "less_eq_of_match_field1 (a::of_match_field) (b::of_match_field) ⟷ (case (a, b) of
(IngressPort a, IngressPort b) ⇒ a ≤ b |
(VlanId a, VlanId b) ⇒ a ≤ b |
(EtherDst a, EtherDst b) ⇒ a ≤ b |
(EtherSrc a, EtherSrc b) ⇒ a ≤ b |
(EtherType a, EtherType b) ⇒ a ≤ b |
(VlanPriority a, VlanPriority b) ⇒ a ≤ b |
(IPv4Proto a, IPv4Proto b) ⇒ a ≤ b |
(IPv4Src a, IPv4Src b) ⇒ a ≤ b |
(IPv4Dst a, IPv4Dst b) ⇒ a ≤ b |
(L4Src a1 a2, L4Src b1 b2) ⇒ if a2 = b2 then a1 ≤ b1 else a2 ≤ b2 |
(L4Dst a1 a2, L4Dst b1 b2) ⇒ if a2 = b2 then a1 ≤ b1 else a2 ≤ b2 |
(a, b) ⇒ match_sorter a < match_sorter b)"

(* feel free to move this to OpenFlowSerialize if it gets in the way. *)
instantiation of_match_field :: linorder
begin

definition
"less_eq_of_match_field (a::of_match_field) (b::of_match_field) ⟷ less_eq_of_match_field1 a b"

definition
"less_of_match_field (a::of_match_field) (b::of_match_field) ⟷ a ≠ b ∧ less_eq_of_match_field1 a b"

instance
by standard (auto simp add: less_eq_of_match_field_def less_of_match_field_def less_eq_of_match_field1_def split: prod.splits of_match_field.splits if_splits)

end

fun match_no_prereq :: "of_match_field ⇒ (32, 'a) simple_packet_ext_scheme ⇒ bool" where
"match_no_prereq (IngressPort i) p = (p_iiface p = i)" |
"match_no_prereq (EtherDst i) p = (p_l2src p = i)" |
"match_no_prereq (EtherSrc i) p = (p_l2dst p = i)" |
"match_no_prereq (EtherType i) p = (p_l2type p = i)" |
"match_no_prereq (VlanId i) p = (p_vlanid p = i)" | (* hack, otherwise it would be iso/osi *)
"match_no_prereq (VlanPriority i) p = (p_vlanprio p = i)" |
"match_no_prereq (IPv4Proto i) p = (p_proto p = i)" |
"match_no_prereq (IPv4Src i) p = (prefix_match_semantics i (p_src p))" |
"match_no_prereq (IPv4Dst i) p = (prefix_match_semantics i (p_dst p))" |
"match_no_prereq (L4Src i m) p = (p_sport p && m = i)" |
"match_no_prereq (L4Dst i m) p = (p_dport p && m = i)"

definition match_prereq :: "of_match_field ⇒ of_match_field set ⇒ (32,'a) simple_packet_ext_scheme ⇒ bool option" where
"match_prereq i s p = (if prerequisites i s then Some (match_no_prereq i p) else None)"

definition "set_seq s ≡ if (∀x ∈ s. x ≠ None) then Some (the  s) else None"
definition "all_true s ≡ ∀x ∈ s. x"
term map_option
definition OF_match_fields :: "of_match_field set ⇒ (32,'a) simple_packet_ext_scheme ⇒ bool option" where "OF_match_fields m p = map_option all_true (set_seq ((λf. match_prereq f m p)  m))"
definition OF_match_fields_unsafe :: "of_match_field set ⇒ (32,'a) simple_packet_ext_scheme ⇒ bool" where "OF_match_fields_unsafe m p = (∀f ∈ m. match_no_prereq f p)"
definition "OF_match_fields_safe m ≡ the ∘ OF_match_fields m"

definition "all_prerequisites m ≡ ∀f ∈ m. prerequisites f m"

lemma (* as stated in paper *)
"all_prerequisites p ⟹
L4Src x y ∈ p ⟹
IPv4Proto  {TCP, UDP, L4_Protocol.SCTP} ∩ p ≠ {}"
unfolding all_prerequisites_def by auto

lemma of_safe_unsafe_match_eq: "all_prerequisites m ⟹ OF_match_fields m p = Some (OF_match_fields_unsafe m p)"
unfolding OF_match_fields_def OF_match_fields_unsafe_def comp_def set_seq_def match_prereq_def all_prerequisites_def
proof goal_cases
case 1
have 2: "(λf. if prerequisites f m then Some (match_no_prereq f p) else None)  m = (λf. Some (match_no_prereq f p))  m"
using 1 by fastforce
have 3: "∀x∈(λf. Some (match_no_prereq f p))  m. x ≠ None" by blast
show ?case
unfolding 2 unfolding eqTrueI[OF 3] unfolding if_True unfolding image_comp comp_def unfolding option.sel by(simp add: all_true_def)
qed

lemma of_match_fields_safe_eq: assumes "all_prerequisites m" shows "OF_match_fields_safe m = OF_match_fields_unsafe m"
unfolding OF_match_fields_safe_def[abs_def] fun_eq_iff comp_def unfolding of_safe_unsafe_match_eq[OF assms] unfolding option.sel by clarify

lemma OF_match_fields_alt: "OF_match_fields m p =
(if ∃f ∈ m. ¬prerequisites f m then None else
if ∀f ∈ m. match_no_prereq f p then Some True else Some False)"
unfolding OF_match_fields_def all_true_def[abs_def] set_seq_def match_prereq_def

lemma of_match_fields_safe_eq2: assumes "all_prerequisites m" shows "OF_match_fields_safe m p ⟷ OF_match_fields m p = Some True"
unfolding OF_match_fields_safe_def[abs_def] fun_eq_iff comp_def unfolding of_safe_unsafe_match_eq[OF assms] unfolding option.sel by simp

end


# Theory OpenFlow_Action

theory OpenFlow_Action
imports
OpenFlow_Matches
begin

(* Beware the differences between Actions and Instructions. OF1.0 doesn't support the former and they're thus not modelled here. *)

(* OF1.0 says actions are a list and executed in-order, OF1.5 has two things: an action set with fixed order in 5.6 and an action list.
So… list. *)

(* Just those which we need(ed). *)
datatype of_action = Forward (oiface_sel: string) | ModifyField_l2dst "48 word"
(* Note that the 1.0 is not entirely clear that there's no drop action. 1.5 clarifies that this is represented by and empty instruction/action set. *)

(* So each flow entry has a list of these. Semantics… The actions are executed in order, but the order of the side-effects is not defined. *)
fun of_action_semantics where
"of_action_semantics p [] = {}" |
"of_action_semantics p (a#as) = (case a of
Forward i ⇒ insert (i,p) (of_action_semantics p as) |
ModifyField_l2dst a ⇒ of_action_semantics (p⦇p_l2dst := a⦈) as)"

value "of_action_semantics p []" (* Drop *)
value "of_action_semantics p [ModifyField_l2dst 66, Forward ''oif'']" (* set mac and send *)

end


# Theory Semantics_OpenFlow

theory Semantics_OpenFlow
imports List_Group Sort_Descending
OpenFlow_Helpers
begin

datatype 'a flowtable_behavior = Action 'a | NoAction | Undefined

definition "option_to_ftb b ≡ case b of Some a ⇒ Action a | None ⇒ NoAction"
definition "ftb_to_option b ≡ case b of Action a ⇒ Some a | NoAction ⇒ None"

(*section‹OpenFlow›*)

(*"OpenFlow packets are received on an ingress port [...]. The packet ingress port is a property of the packet
throughout the OpenFlow pipeline and represents the OpenFlow port on which the packet was received
into the OpenFlow switch."
*)

(* "Packet forwarded to non-existent ports are just dropped"*)

(*we do not support egress tables (those are optional in the standard).
we only support flow table 0 (ingress table).
Essentially, this means, we only support one flow table and no pipelining.
This corresponds to OpenFlow 1.0.0
*)

(*priority × Match Fields × instructions
not modeled: counters, timeouts, cookie ("Not used when processing packets"), flags,
instructions (only an output list of egress ports will be modeled)
*)

datatype ('m, 'a) flow_entry_match = OFEntry (ofe_prio: "16 word") (ofe_fields: "'m set") (ofe_action: 'a)

(* why is there curry *)
find_consts "(('a × 'b) ⇒ 'c) ⇒ 'a ⇒ 'b ⇒ 'c"
(* but no "uncurry" *)
find_consts "('a ⇒ 'b ⇒ 'c) ⇒ ('a × 'b) ⇒ 'c"
(* Anyway, we want this to easily construct OFEntrys from tuples *)
definition "split3 f p ≡ case p of (a,b,c) ⇒ f a b c"
find_consts "('a ⇒ 'b ⇒ 'c ⇒ 'd) ⇒ ('a × 'b × 'c) ⇒ 'd"

(*
"If there are multiple matching flow entries with the same highest priority, the selected flow entry is explicitly undefined."
OFP 1.0.0 also stated that non-wildcarded matches implicitly have the highest priority (which is gone in 1.5).
*)
(*Defined None ⟷ No match
Defined (Some a) ⟷ Match and instruction is a
Undefined ⟷ Undefined*)

type_synonym ('m, 'a) flowtable = "(('m, 'a) flow_entry_match) list"
type_synonym ('m, 'p) field_matcher = "('m set ⇒ 'p ⇒ bool)"

definition OF_same_priority_match2 :: "('m, 'p) field_matcher ⇒ ('m, 'a) flowtable ⇒ 'p ⇒ 'a flowtable_behavior" where
"OF_same_priority_match2 γ flow_entries packet ≡ let s =
{ofe_action f|f. f ∈ set flow_entries ∧ γ (ofe_fields f) packet ∧
(∀fo ∈ set flow_entries. ofe_prio fo > ofe_prio f ⟶ ¬γ (ofe_fields fo) packet)} in
case card s of 0       ⇒ NoAction
| (Suc 0) ⇒ Action (the_elem s)
| _       ⇒ Undefined"

(* are there any overlaping rules? *)
definition "check_no_overlap γ ft = (∀a ∈ set ft. ∀b ∈ set ft. ∀p ∈ UNIV. (ofe_prio a = ofe_prio b ∧ γ (ofe_fields a) p ∧ a ≠ b) ⟶ ¬γ (ofe_fields b) p)"
definition "check_no_overlap2 γ ft = (∀a ∈ set ft. ∀b ∈ set ft. (a ≠ b ∧ ofe_prio a = ofe_prio b) ⟶ ¬(∃p ∈ UNIV. γ (ofe_fields a) p ∧ γ (ofe_fields b) p))"
lemma check_no_overlap_alt: "check_no_overlap γ ft = check_no_overlap2 γ ft"
unfolding check_no_overlap2_def check_no_overlap_def
by blast

(* If there are no overlapping rules, our match should check out. *)
lemma no_overlap_not_unefined: "check_no_overlap γ ft ⟹ OF_same_priority_match2 γ ft p ≠ Undefined"
proof
assume goal1: "check_no_overlap γ ft" "OF_same_priority_match2 γ ft p = Undefined"
let ?as = "{f. f ∈ set ft ∧ γ (ofe_fields f) p ∧ (∀fo ∈ set ft. ofe_prio f < ofe_prio fo ⟶ ¬ γ (ofe_fields fo) p)}"
have fin: "finite ?as" by simp
note goal1(2)[unfolded OF_same_priority_match2_def]
then have "2 ≤ card (ofe_action  ?as)" unfolding f_Img_ex_set
unfolding Let_def
by(cases "card (ofe_action  ?as)", simp) (rename_tac nat1, case_tac nat1, simp add: image_Collect, presburger)
then have "2 ≤ card ?as" using card_image_le[OF fin, of ofe_action] by linarith
then obtain a b where ab: "a ≠ b" "a ∈ ?as" "b ∈ ?as" using card2_eI by blast
then have ab2: "a ∈ set ft" "γ (ofe_fields a) p" "(∀fo∈set ft. ofe_prio a < ofe_prio fo ⟶ ¬ γ (ofe_fields fo) p)"
"b ∈ set ft" "γ (ofe_fields b) p" "(∀fo∈set ft. ofe_prio b < ofe_prio fo ⟶ ¬ γ (ofe_fields fo) p)" by simp_all
then have "ofe_prio a = ofe_prio b"
by fastforce
note goal1(1)[unfolded check_no_overlap_def] ab2(1) ab2(4) this ab2(2) ab(1) ab2(5)
then show False by blast
qed

fun OF_match_linear :: "('m, 'p) field_matcher ⇒ ('m, 'a) flowtable ⇒ 'p ⇒ 'a flowtable_behavior" where
"OF_match_linear _ [] _ = NoAction" |
"OF_match_linear γ (a#as) p = (if γ (ofe_fields a) p then Action (ofe_action a) else OF_match_linear γ as p)"

lemma OF_match_linear_ne_Undefined: "OF_match_linear γ ft p ≠ Undefined"
by(induction ft) auto

lemma OF_match_linear_append: "OF_match_linear γ (a @ b) p = (case OF_match_linear γ a p of NoAction ⇒ OF_match_linear γ b p | x ⇒ x)"
by(induction a) simp_all
lemma OF_match_linear_match_allsameaction: "⟦gr ∈ set oms; γ gr p = True⟧
⟹ OF_match_linear γ (map (λx. split3 OFEntry (pri, x, act)) oms) p = Action act"
by(induction oms) (auto simp add: split3_def)
lemma OF_lm_noa_none_iff: "OF_match_linear γ ft p = NoAction ⟷ (∀e∈set ft. ¬ γ (ofe_fields e) p)"
by(induction ft) (simp_all split: if_splits)

lemma set_eq_rule: "(⋀x. x ∈ a ⟹ x ∈ b) ⟹ (⋀x. x ∈ b ⟹ x ∈ a) ⟹ a = b" by(rule antisym[OF subsetI subsetI])

lemma unmatching_insert_agnostic: "¬ γ (ofe_fields a) p ⟹ OF_same_priority_match2 γ (a # ft) p = OF_same_priority_match2 γ ft p"
proof -
let ?as = "{f. f ∈ set ft ∧ γ (ofe_fields f) p ∧ (∀fo ∈ set ft. ofe_prio f < ofe_prio fo ⟶ ¬ γ (ofe_fields fo) p)}"
let ?aas = "{f |f. f ∈ set (a # ft) ∧ γ (ofe_fields f) p ∧ (∀fo∈set (a # ft). ofe_prio f < ofe_prio fo ⟶ ¬ γ (ofe_fields fo) p)}"
assume nm: "¬ γ (ofe_fields a) p"
have aa: "?aas = ?as"
proof(rule set_eq_rule)
fix x
assume "x ∈ {f |f. f ∈ set (a # ft) ∧ γ (ofe_fields f) p ∧ (∀fo∈set (a # ft). ofe_prio f < ofe_prio fo ⟶ ¬ γ (ofe_fields fo) p)}"
hence as: "x ∈ set (a # ft) ∧ γ (ofe_fields x) p ∧ (∀fo∈set (a # ft). ofe_prio x < ofe_prio fo ⟶ ¬ γ (ofe_fields fo) p)" by simp
with nm have "x ∈ set ft" by fastforce
moreover from as have "(∀fo∈set ft. ofe_prio x < ofe_prio fo ⟶ ¬ γ (ofe_fields fo) p)" by simp
ultimately show "x ∈ {f ∈ set ft. γ (ofe_fields f) p ∧ (∀fo∈set ft. ofe_prio f < ofe_prio fo ⟶ ¬ γ (ofe_fields fo) p)}" using as by force
next
fix x
assume "x ∈ {f ∈ set ft. γ (ofe_fields f) p ∧ (∀fo∈set ft. ofe_prio f < ofe_prio fo ⟶ ¬ γ (ofe_fields fo) p)}"
hence as: "x ∈ set ft" "γ (ofe_fields x) p" "(∀fo∈set ft. ofe_prio x < ofe_prio fo ⟶ ¬ γ (ofe_fields fo) p)" by simp_all
from as(1) have "x ∈ set (a # ft)" by simp
moreover from as(3) have "(∀fo∈set (a # ft). ofe_prio x < ofe_prio fo ⟶ ¬ γ (ofe_fields fo) p)" using nm by simp
ultimately show "x ∈ {f |f. f ∈ set (a # ft) ∧ γ (ofe_fields f) p ∧ (∀fo∈set (a # ft). ofe_prio f < ofe_prio fo ⟶ ¬ γ (ofe_fields fo) p)}" using as(2) by blast
qed
note uf = arg_cong[OF aa, of "() ofe_action", unfolded image_Collect]
show ?thesis unfolding OF_same_priority_match2_def using uf by presburger
qed

lemma OF_match_eq: "sorted_descending (map ofe_prio ft) ⟹ check_no_overlap γ ft ⟹
OF_same_priority_match2 γ ft p = OF_match_linear γ ft p"
proof(induction "ft")
case (Cons a ft)
have 1: "sorted_descending (map ofe_prio ft)" using Cons(2) by simp
have 2: "check_no_overlap γ ft" using Cons(3) unfolding check_no_overlap_def using set_subset_Cons by fast
note mIH = Cons(1)[OF 1 2]
show ?case (is ?kees)
proof(cases "γ (ofe_fields a) p")
case False thus ?kees
by(simp only: OF_match_linear.simps if_False mIH[symmetric] unmatching_insert_agnostic[of γ, OF False])
next
note sorted_descending_split[OF Cons(2)]
then obtain m n where mn: "a # ft = m @ n" "∀e∈set m. ofe_prio a = ofe_prio e" "∀e∈set n. ofe_prio e < ofe_prio a"
unfolding list.sel by blast
hence aem: "a ∈ set m"
by (metis UnE less_imp_neq list.set_intros(1) set_append)
have mover: "check_no_overlap γ m" using Cons(3) unfolding check_no_overlap_def
by (metis Un_iff mn(1) set_append)
let ?fc = "(λs.
{f. f ∈ set s ∧ γ (ofe_fields f) p ∧
(∀fo∈set (a # ft). ofe_prio f < ofe_prio fo ⟶ ¬ γ (ofe_fields fo) p)})"
case True
have "?fc (m @ n) = ?fc m ∪ ?fc n" by auto
moreover have "?fc n = {}"
proof(rule set_eq_rule, rule ccontr, goal_cases)
case (1 x)
hence g1: "x ∈ set n" "γ (ofe_fields x) p"
"(∀fo∈set m. ofe_prio x < ofe_prio fo ⟶ ¬ γ (ofe_fields fo) p)"
"(∀fo∈set n. ofe_prio x < ofe_prio fo ⟶ ¬ γ (ofe_fields fo) p)"
unfolding mn(1) by(simp_all)
from g1(1) mn(3) have le: "ofe_prio x < ofe_prio a" by simp
note le g1(3) aem True
then show False by blast
qed simp
ultimately have cc: "?fc (m @ n) = ?fc m" by blast
have cm: "?fc m = {a}" (* using Cons(3) *)
proof -
have "∀f ∈ set m. (∀fo∈set (a # ft). ofe_prio f < ofe_prio fo ⟶ ¬ γ (ofe_fields fo) p)"
by (metis UnE less_asym mn set_append)
hence 1: "?fc m = {f ∈ set m. γ (ofe_fields f) p}" by blast
show "{f ∈ set m. γ (ofe_fields f) p ∧ (∀fo∈set (a # ft). ofe_prio f < ofe_prio fo ⟶ ¬ γ (ofe_fields fo) p)} = {a} " unfolding 1
proof(rule set_eq_rule, goal_cases fwd bwd)
case (bwd x)
have "a ∈ {f ∈ set m. γ (ofe_fields f) p}" using True aem by simp
thus ?case using bwd by simp
next
case (fwd x) show ?case proof(rule ccontr)
assume "x ∉ {a}" hence ne: "x ≠ a" by simp
from fwd have 1: "x ∈ set m" "γ (ofe_fields x) p" by simp_all
have 2: "ofe_prio x = ofe_prio a" using 1(1) mn(2) by simp
show False using 1 ne mover aem True 2 unfolding check_no_overlap_def by blast
qed
qed
qed
show ?kees
unfolding mn(1)
unfolding OF_same_priority_match2_def
unfolding f_Img_ex_set
unfolding cc[unfolded mn(1)]
unfolding cm[unfolded mn(1)]
unfolding Let_def
by(simp only: mn(1)[symmetric] OF_match_linear.simps True if_True, simp)
qed

lemma overlap_sort_invar[simp]: "check_no_overlap γ (sort_descending_key k ft) = check_no_overlap γ ft"
unfolding check_no_overlap_def
unfolding sort_descending_set_inv
..

lemma OF_match_eq2:
assumes "check_no_overlap γ ft"
shows "OF_same_priority_match2 γ ft p = OF_match_linear γ (sort_descending_key ofe_prio ft) p"
proof -
have "sorted_descending (map ofe_prio (sort_descending_key ofe_prio ft))" by (simp add: sorted_descending_sort_descending_key)
note ceq = OF_match_eq[OF this, unfolded overlap_sort_invar, OF ‹check_no_overlap γ ft›, symmetric]
show ?thesis
unfolding ceq
unfolding OF_same_priority_match2_def
unfolding sort_descending_set_inv
..
qed

(* Just me, thinking about some alternate ways of writing this down. *)
lemma prio_match_matcher_alt: "{f. f ∈ set flow_entries ∧ γ (ofe_fields f) packet ∧
(∀fo ∈ set flow_entries. ofe_prio fo > ofe_prio f ⟶ ¬γ (ofe_fields fo) packet)}
= (
let matching = {f. f ∈ set flow_entries ∧ γ (ofe_fields f) packet}
in {f. f ∈ matching ∧ (∀fo ∈ matching. ofe_prio fo ≤ ofe_prio f)}
)"
lemma prio_match_matcher_alt2: "(
let matching = {f. f ∈ set flow_entries ∧ γ (ofe_fields f) packet}
in {f. f ∈ matching ∧ (∀fo ∈ matching. ofe_prio fo ≤ ofe_prio f)}
) = set (
let matching = filter (λf. γ (ofe_fields f) packet) flow_entries
in filter (λf. ∀fo ∈ set matching. ofe_prio fo ≤ ofe_prio f) matching
)"

definition OF_priority_match where
"OF_priority_match γ flow_entries packet ≡
let m  = filter (λf. γ (ofe_fields f) packet) flow_entries;
m' = filter (λf. ∀fo ∈ set m. ofe_prio fo ≤ ofe_prio f) m in
case m' of []  ⇒ NoAction
| [s] ⇒ Action (ofe_action s)
|  _  ⇒ Undefined"

definition OF_priority_match_ana where
"OF_priority_match_ana γ flow_entries packet ≡
let m  = filter (λf. γ (ofe_fields f) packet) flow_entries;
m' = filter (λf. ∀fo ∈ set m. ofe_prio fo ≤ ofe_prio f) m in
case m' of []  ⇒ NoAction
| [s] ⇒ Action s
|  _  ⇒ Undefined"

lemma filter_singleton: "[x←s. f x] = [y] ⟹ f y ∧ y ∈ set s" by (metis filter_eq_Cons_iff in_set_conv_decomp)

lemma OF_spm3_get_fe: "OF_priority_match γ ft p = Action a ⟹ ∃fe. ofe_action fe = a ∧ fe ∈ set ft ∧ OF_priority_match_ana γ ft p = Action fe"
unfolding OF_priority_match_def OF_priority_match_ana_def
by(clarsimp split: flowtable_behavior.splits list.splits) (drule filter_singleton; simp)

fun no_overlaps where
"no_overlaps _ [] = True" |
"no_overlaps γ (a#as) = (no_overlaps γ as ∧ (
∀b ∈ set as. ofe_prio a = ofe_prio b ⟶ ¬(∃p ∈ UNIV. γ (ofe_fields a) p ∧ γ (ofe_fields b) p)))"

lemma no_overlap_ConsI: "check_no_overlap2 γ (x#xs) ⟹ check_no_overlap2 γ xs"
unfolding check_no_overlap2_def by simp

lemma no_overlapsI: "check_no_overlap γ t ⟹ distinct t ⟹ no_overlaps γ t"
unfolding check_no_overlap_alt
proof(induction t)
case (Cons a t)
from no_overlap_ConsI[OF Cons(2)] Cons(3,1)
have "no_overlaps γ t" by simp
thus ?case using Cons(2,3) unfolding check_no_overlap2_def by auto

lemma check_no_overlapI: "no_overlaps γ t ⟹ check_no_overlap γ t"
unfolding check_no_overlap_alt
proof(induction t)
case (Cons a t)
from Cons(1)[OF conjunct1[OF Cons(2)[unfolded no_overlaps.simps]]]
show ?case
using conjunct2[OF Cons(2)[unfolded no_overlaps.simps]]
unfolding check_no_overlap2_def
by auto

lemma "(⋀e p. e ∈ set t ⟹ ¬γ (ofe_fields e) p) ⟹ no_overlaps γ t"
by(induction t) simp_all
lemma no_overlaps_append: "no_overlaps γ (x @ y) ⟹ no_overlaps γ y"
by(induction x) simp_all
lemma no_overlaps_ne1: "no_overlaps γ (x @ a # y @ b # z) ⟹ ((∃p. γ (ofe_fields a) p) ∨ (∃p. γ (ofe_fields b) p)) ⟹ a ≠ b"
proof (rule notI, goal_cases contr)
case contr
from contr(1) no_overlaps_append have "no_overlaps γ (a # y @ b # z)" by blast
note this[unfolded no_overlaps.simps]
with contr(3) have "¬ (∃p∈UNIV. γ (ofe_fields a) p ∧ γ (ofe_fields b) p)" by simp
with contr(2) show False unfolding contr(3) by simp
qed

lemma no_overlaps_defeq: "no_overlaps γ fe ⟹ OF_same_priority_match2 γ fe p = OF_priority_match γ fe p"
unfolding OF_same_priority_match2_def OF_priority_match_def
unfolding f_Img_ex_set
unfolding prio_match_matcher_alt
unfolding prio_match_matcher_alt2
proof (goal_cases uf)
case uf
let ?m' = "let m = [f←fe . γ (ofe_fields f) p] in [f←m . ∀fo∈set m. ofe_prio fo ≤ ofe_prio f]"
let ?s = "ofe_action  set ?m'"
from uf show ?case
proof(cases ?m')
case Nil
moreover then have "card ?s = 0" by force
ultimately show ?thesis by(simp add: Let_def)
next
case (Cons a as)
have "as = []"
proof(rule ccontr)
assume "as ≠ []"
then obtain b bs where bbs: "as = b # bs" by (meson neq_Nil_conv)
note no = Cons[unfolded Let_def filter_filter]
have f1: "a ∈ set ?m'" "b ∈ set ?m'" unfolding bbs local.Cons by simp_all
hence "ofe_prio a = ofe_prio b" by (simp add: antisym)
moreover have ms: "γ (ofe_fields a) p" "γ (ofe_fields b) p" using no[symmetric] unfolding bbs by(blast dest: Cons_eq_filterD)+
moreover have abis: "a ∈ set fe" "b ∈ set fe" using f1 by auto
moreover have "a ≠ b" proof(cases "∃x y z. fe = x @ a # y @ b # z")
case True
then obtain x y z where xyz: "fe = x @ a # y @ b # z" by blast
from no_overlaps_ne1 ms(1) uf[unfolded xyz]
show ?thesis by blast
next
case False
then obtain x y z where xyz: "fe = x @ b # y @ a # z"
using no unfolding bbs
by (metis (no_types, lifting) Cons_eq_filterD)
from no_overlaps_ne1 ms(1) uf[unfolded xyz]
show ?thesis by blast
qed
ultimately show False using check_no_overlapI[OF uf, unfolded check_no_overlap_def] by blast
qed
then have oe: "a # as = [a]" by simp
show ?thesis using Cons[unfolded oe] by force
qed
qed
(* the above lemma used to be this, but it's slightly weaker than I wanted. *)
lemma "distinct fe ⟹ check_no_overlap γ fe ⟹ OF_same_priority_match2 γ fe p = OF_priority_match γ fe p"
by(rule no_overlaps_defeq) (drule (2) no_overlapsI)

theorem OF_eq:
assumes no: "no_overlaps γ f"
and so: "sorted_descending (map ofe_prio f)"
shows "OF_match_linear γ f p = OF_priority_match γ f p"
unfolding no_overlaps_defeq[symmetric,OF no] OF_match_eq[OF so check_no_overlapI[OF no]]
..

corollary OF_eq_sort:
assumes no: "no_overlaps γ f"
shows "OF_priority_match γ f p = OF_match_linear γ (sort_descending_key ofe_prio f) p"
using OF_match_eq2 check_no_overlapI no no_overlaps_defeq by fastforce

lemma OF_lm_noa_none: "OF_match_linear γ ft p = NoAction ⟹ ∀e∈set ft. ¬ γ (ofe_fields e) p"
by(induction ft) (simp_all split: if_splits)

(* this should be provable without the overlaps assumption, but that's quite a bit harder. *)
lemma OF_spm3_noa_none:
assumes no: "no_overlaps γ ft"
shows "OF_priority_match γ ft p = NoAction ⟹ ∀e ∈ set ft. ¬γ (ofe_fields e) p"
unfolding OF_eq_sort[OF no] by(drule OF_lm_noa_none) simp

(* repetition of the lemma for definition 2 for definition 3 *)
lemma no_overlaps_not_unefined: "no_overlaps γ ft ⟹ OF_priority_match γ ft p ≠ Undefined"
using check_no_overlapI no_overlap_not_unefined no_overlaps_defeq by fastforce

end


# Theory OpenFlow_Serialize

theory OpenFlow_Serialize
imports OpenFlow_Matches
OpenFlow_Action
Semantics_OpenFlow
Simple_Firewall.Primitives_toString
begin

definition "serialization_test_entry ≡ OFEntry 7 {EtherDst 0x1, IPv4Dst (PrefixMatch 0xA000201 32), IngressPort ''s1-lan'', L4Dst 0x50 0, L4Src 0x400 0x3FF, IPv4Proto 6, EtherType 0x800} [ModifyField_l2dst 0xA641F185E862, Forward ''s1-wan'']"

value "(map ((<<) (1::48 word) ∘ (*) 8) ∘ rev) [0..<6]"

definition "serialize_mac (m::48 word) ≡ (intersperse (CHR '':'') ∘ map (hex_string_of_word 1 ∘ (λh. (m >> h * 8) && 0xff)) ∘ rev) [0..<6]"

definition "serialize_action pids a ≡ (case a of
Forward oif ⇒ ''output:'' @ pids oif |
ModifyField_l2dst na ⇒ ''mod_dl_dst:'' @ serialize_mac na)"

definition "serialize_actions pids a ≡ if length a = 0 then ''drop'' else (intersperse (CHR '','') ∘ map (serialize_action pids)) a"

lemma "serialize_actions (λoif. ''42'') (ofe_action serialization_test_entry) =
''mod_dl_dst:a6:41:f1:85:e8:62,output:42''" by eval
lemma "serialize_actions anything [] = ''drop''"

definition "prefix_to_string pfx ≡ ipv4_cidr_toString (pfxm_prefix pfx, pfxm_length pfx)"

primrec serialize_of_match where
"serialize_of_match pids (IngressPort p) = ''in_port='' @ pids p" |
"serialize_of_match _ (VlanId i) = ''dl_vlan='' @ dec_string_of_word0 i" |
"serialize_of_match _ (VlanPriority _) = undefined" | (* uh, äh… We don't use that anyway… *)
"serialize_of_match _ (EtherType i) = ''dl_type=0x'' @ hex_string_of_word0 i" |
"serialize_of_match _ (EtherSrc m) = ''dl_src='' @ serialize_mac m" |
"serialize_of_match _ (EtherDst m) = ''dl_dst='' @ serialize_mac m" |
"serialize_of_match _ (IPv4Proto i) = ''nw_proto='' @ dec_string_of_word0 i" |
"serialize_of_match _ (IPv4Src p) = ''nw_src='' @ prefix_to_string p" |
"serialize_of_match _ (IPv4Dst p) = ''nw_dst='' @ prefix_to_string p" |
"serialize_of_match _ (L4Src i m) = ''tp_src='' @ dec_string_of_word0 i @ (if m = max_word then [] else ''/0x'' @ hex_string_of_word 3 m)" |
"serialize_of_match _ (L4Dst i m) = ''tp_dst='' @ dec_string_of_word0 i @ (if m = max_word then [] else ''/0x'' @ hex_string_of_word 3 m)"

definition serialize_of_matches :: "(string ⇒ string) ⇒ of_match_field set ⇒ string"
where
"serialize_of_matches pids ≡ (@) ''hard_timeout=0,idle_timeout=0,'' ∘ intersperse (CHR '','') ∘ map (serialize_of_match pids) ∘ sorted_list_of_set"

lemma "serialize_of_matches pids of_matches=
(List.append ''hard_timeout=0,idle_timeout=0,'')
(intersperse (CHR '','') (map (serialize_of_match pids) (sorted_list_of_set of_matches)))"

export_code serialize_of_matches checking SML (*needs "HOL-Library.Code_Char"*)

lemma "serialize_of_matches (λoif. ''42'') (ofe_fields serialization_test_entry) =
''hard_timeout=0,idle_timeout=0,in_port=42,dl_type=0x800,dl_dst=00:00:00:00:00:01,nw_proto=6,nw_dst=10.0.2.1/32,tp_src=1024/0x03ff,tp_dst=80/0x0000''"
by eval

definition "serialize_of_entry pids e ≡ (case e of (OFEntry p f a) ⇒ ''priority='' @ dec_string_of_word0 p @ '','' @ serialize_of_matches pids f @ '','' @ ''action='' @ serialize_actions pids a)"

lemma "serialize_of_entry (the ∘ map_of [(''s1-lan'',''42''),(''s1-wan'',''1337'')]) serialization_test_entry =
''priority=7,hard_timeout=0,idle_timeout=0,in_port=42,dl_type=0x800,dl_dst=00:00:00:00:00:01,nw_proto=6,nw_dst=10.0.2.1/32,tp_src=1024/0x03ff,tp_dst=80/0x0000,action=mod_dl_dst:a6:41:f1:85:e8:62,output:1337''"
by eval

end


# Theory Featherweight_OpenFlow_Comparison

theory Featherweight_OpenFlow_Comparison
imports Semantics_OpenFlow
begin

(* compare to https://github.com/frenetic-lang/featherweight-openflow/blob/master/coq/OpenFlow/OpenFlowSemantics.v#L260 *)
inductive guha_table_semantics :: "('m, 'p) field_matcher ⇒ ('m, 'a) flowtable ⇒ 'p ⇒ 'a option ⇒ bool" where
guha_matched: "γ (ofe_fields fe) p = True ⟹
∀fe' ∈ set (ft1 @ ft2). ofe_prio fe' > ofe_prio fe ⟶ γ (ofe_fields fe') p = False ⟹
guha_table_semantics γ (ft1 @ fe # ft2) p (Some (ofe_action fe))" |
guha_unmatched: "∀fe ∈ set ft. γ (ofe_fields fe) p = False ⟹
guha_table_semantics γ ft p None"

(*
so... there's the possibility for a flow table with two matching entries.
I'm not so sure it is a good idea to model undefined behavior by nondeterministic but very defined behavior..
*)
lemma guha_table_semantics_ex2res:
assumes ta: "CARD('a) ≥ 2" (* if there's only one action, the whole thing is moot. *)
assumes ms: "∃ff. γ ff p" (* if our matcher rejects the packet for any match condition, it is borked. *)
shows "∃ft (a1 :: 'a) (a2 :: 'a). a1 ≠ a2 ∧ guha_table_semantics γ ft p (Some a1) ∧ guha_table_semantics γ ft p (Some a2)"
proof -
from ms	obtain ff  where m: "γ ff p" ..
from ta obtain a1 a2 :: 'a where as: "a1 ≠ a2" using card2_eI by blast
let ?fe1 = "OFEntry 0 ff a1"
let ?fe2 = "OFEntry 0 ff a2"
let ?ft = "[?fe1, ?fe2]"
have "guha_table_semantics γ ?ft p (Some a1)" "guha_table_semantics γ ?ft p (Some a2)"
by(rule guha_table_semantics.intros(1)[of γ ?fe1 p "[]" "[?fe2]", unfolded append_Nil flow_entry_match.sel] |
rule guha_table_semantics.intros(1)[of γ ?fe2 p "[?fe1]" "[]", unfolded append_Nil2 flow_entry_match.sel append.simps] |
thus ?thesis using as by(intro exI conjI)
qed

lemma guha_umstaendlich: (* or maybe it's Coq where the original formulation is more beneficial *)
assumes ae: "a = ofe_action fe"
assumes ele: "fe ∈ set ft"
assumes rest: "γ (ofe_fields fe) p"
"∀fe' ∈ set ft. ofe_prio fe' > ofe_prio fe ⟶ ¬γ (ofe_fields fe') p"
shows "guha_table_semantics γ ft p (Some a)"
proof -
from ele obtain ft1 ft2 where ftspl: "ft = ft1 @ fe # ft2" using split_list by fastforce
show ?thesis unfolding ae ftspl
apply(rule guha_table_semantics.intros(1))
using rest(1) apply(simp)
using rest(2)[unfolded ftspl] apply simp
done
qed

lemma guha_matched_rule_inversion:
assumes "guha_table_semantics γ ft p (Some a)"
shows "∃fe ∈ set ft. a = ofe_action fe ∧ γ (ofe_fields fe) p ∧ (∀fe' ∈ set ft. ofe_prio fe' > ofe_prio fe ⟶ ¬γ (ofe_fields fe') p)"
proof -
{
fix d
assume "guha_table_semantics γ ft p d"
hence "Some a = d ⟹ (∃fe ∈ set ft. a = ofe_action fe ∧ γ (ofe_fields fe) p ∧ (∀fe' ∈ set ft. ofe_prio fe' > ofe_prio fe ⟶ ¬γ (ofe_fields fe') p))"
by(induction rule: guha_table_semantics.induct) simp_all (* strange to show this by induction, but I don't see an exhaust or cases I could use. *)
}
from this[OF assms refl]
show ?thesis .
qed

lemma guha_equal_Action:
assumes no: "no_overlaps γ ft"
assumes spm: "OF_priority_match γ ft p = Action a"
shows "guha_table_semantics γ ft p (Some a)"
proof -
note spm[THEN OF_spm3_get_fe] then obtain fe where a: "ofe_action fe = a" and fein: "fe ∈ set ft" and feana: "OF_priority_match_ana γ ft p = Action fe" by blast
show ?thesis
apply(rule guha_umstaendlich)
apply(rule a[symmetric])
apply(rule fein)
using feana unfolding OF_priority_match_ana_def
apply(auto dest!: filter_singleton split: list.splits)
done
qed

lemma guha_equal_NoAction:
assumes no: "no_overlaps γ ft"
assumes spm: "OF_priority_match γ ft p = NoAction"
shows "guha_table_semantics γ ft p None"
using spm unfolding OF_priority_match_def
by(auto simp add: filter_empty_conv OF_spm3_noa_none[OF no spm] intro: guha_table_semantics.intros(2) split: list.splits)

lemma guha_equal_hlp:
assumes no: "no_overlaps γ ft"
shows "guha_table_semantics γ ft p (ftb_to_option (OF_priority_match γ ft p))"
unfolding ftb_to_option_def
apply(cases "(OF_priority_match γ ft p)")
apply(subgoal_tac False, simp)
done

lemma guha_deterministic1: "guha_table_semantics γ ft p (Some x1) ⟹ ¬ guha_table_semantics γ ft p None"

lemma guha_deterministic2: "⟦no_overlaps γ ft; guha_table_semantics γ ft p (Some x1); guha_table_semantics γ ft p (Some a)⟧ ⟹ x1 = a"
proof(rule ccontr, goal_cases)
case 1
note 1(2-3)[THEN guha_matched_rule_inversion] then obtain fe1 fe2 where fes:
"fe1∈set ft" "x1 = ofe_action fe1" "γ (ofe_fields fe1) p" "(∀fe'∈set ft. ofe_prio fe1 < ofe_prio fe' ⟶ ¬ γ (ofe_fields fe') p)"
"fe2∈set ft" "a  = ofe_action fe2" "γ (ofe_fields fe2) p" "(∀fe'∈set ft. ofe_prio fe2 < ofe_prio fe' ⟶ ¬ γ (ofe_fields fe') p)"
by blast
from ‹x1 ≠ a› have fene: "fe1 ≠ fe2" using fes(2,6) by blast
have pe: "ofe_prio fe1 = ofe_prio fe2" using fes(1,3-4,5,7-8) less_linear by blast
note ‹no_overlaps γ ft›[THEN check_no_overlapI, unfolded check_no_overlap_def]
note this[unfolded Ball_def, THEN spec, THEN mp, OF fes(1), THEN spec, THEN mp, OF fes(5),THEN spec, THEN mp, OF UNIV_I, of p] pe fene fes(3,7)
thus False by blast
qed

lemma guha_equal:
assumes no: "no_overlaps γ ft"
shows "OF_priority_match γ ft p = option_to_ftb d ⟷ guha_table_semantics γ ft p d"
using guha_equal_hlp[OF no, of p] unfolding ftb_to_option_def option_to_ftb_def
apply(cases "OF_priority_match γ ft p"; cases d)
apply(simp_all)
using guha_deterministic1 apply fast
using guha_deterministic2[OF no] apply blast
using guha_deterministic1 apply fast
using no_overlaps_not_unefined[OF no] apply fastforce
using no_overlaps_not_unefined[OF no] apply fastforce
done

lemma guha_nondeterministicD:
assumes "¬check_no_overlap γ ft"
shows "∃fe1 fe2 p. fe1 ∈ set ft ∧ fe2 ∈ set ft
∧ guha_table_semantics γ ft p (Some (ofe_action fe1))
∧ guha_table_semantics γ ft p (Some (ofe_action fe2))"
using assms
apply(unfold check_no_overlap_def)
apply(clarsimp)
apply(rename_tac fe1 fe2 p)
apply(rule_tac x = fe1 in exI)
apply(simp)
apply(rule_tac x = fe2 in exI)
apply(simp)
apply(rule_tac x = p in exI)
apply(rule conjI)
apply(subst guha_table_semantics.simps)
apply(rule disjI1)
apply(clarsimp)
apply(rule_tac x = fe1 in exI)
apply(drule split_list)
apply(clarify)
apply(rename_tac ft1 ft2)
apply(rule_tac x = ft1 in exI)
apply(rule_tac x = ft2 in exI)
apply(simp)
oops (* shadowed overlaps yay! *)

text‹The above lemma does indeed not hold, the reason for this are (possibly partially) shadowed overlaps.
This is exemplified below: If there are at least three different possible actions (necessary assumption)
and a match expression that matches all packets (convenience assumption), it is possible to construct a flow
table that is admonished by @{const check_no_overlap} but still will never run into undefined behavior.
›
(* This is not the terribly most important lemma. Feel free to delete it if the proof gives you trouble. *)
lemma
assumes "CARD('action) ≥ 3"
assumes "∀p. γ x p" (* with a sane γ, x = {} *)
shows "∃ft::('a, 'action) flow_entry_match list. ¬check_no_overlap γ ft ∧
¬(∃fe1 fe2 p. fe1 ∈ set ft ∧ fe2 ∈ set ft ∧ fe1 ≠ fe2 ∧ ofe_prio fe1 = ofe_prio fe2
∧ guha_table_semantics γ ft p (Some (ofe_action fe1))
∧ guha_table_semantics γ ft p (Some (ofe_action fe2)))"
proof -
obtain adef aa ab :: 'action where anb[simp]: "aa ≠ ab" "adef ≠ aa" "adef ≠ ab" using assms(1) card3_eI by blast
let ?cex = "[OFEntry 1 x adef, OFEntry 0 x aa, OFEntry 0 x ab]"
have ol: "¬check_no_overlap γ ?cex"
unfolding check_no_overlap_def ball_simps
apply(rule bexI[where x = "OFEntry 0 x aa", rotated], (simp;fail))
apply(rule bexI[where x = "OFEntry 0 x ab", rotated], (simp;fail))
done
have df: "guha_table_semantics γ ?cex p oc ⟹ oc = Some adef" for p oc
unfolding guha_table_semantics.simps
apply(elim disjE; clarsimp simp: assms)
subgoal for fe ft1 ft2
apply(cases "ft1 = []")
apply(fastforce)
apply(cases "ft2 = []")
apply(fastforce)
apply(subgoal_tac "ft1 = [OFEntry 1 x adef] ∧ fe = OFEntry 0 x aa ∧ ft2 = [OFEntry 0 x ab]")
apply(simp;fail)
apply(rename_tac ya ys yz)
apply(case_tac ys; clarsimp simp add: List.neq_Nil_conv)
done done
show ?thesis
apply(intro exI[where x = ?cex], intro conjI, fact ol)
apply(clarify)
apply(unfold set_simps)
apply(elim insertE; clarsimp)
apply((drule df)+; unfold option.inject; (elim anb[symmetric, THEN notE] | (simp;fail))?)+
done
qed

end


# Theory LinuxRouter_OpenFlow_Translation

theory LinuxRouter_OpenFlow_Translation
Automatic_Refinement.Misc (*TODO@Peter: rename and make available at better place :)*)
Simple_Firewall.Generic_SimpleFw
Semantics_OpenFlow
OpenFlow_Matches
OpenFlow_Action
Routing.Linux_Router
begin
hide_const Misc.uncurry
hide_fact Misc.uncurry_def

(* For reference:
iiface :: "iface" --"in-interface"
oiface :: "iface" --"out-interface"
dst :: "(ipv4addr × nat) " --"destination"
proto :: "protocol"
sports :: "(16 word × 16 word)" --"source-port first:last"
dports :: "(16 word × 16 word)" --"destination-port first:last"

p_iiface :: string
p_oiface :: string
p_proto :: primitive_protocol
p_sport :: "16 word"
p_dport :: "16 word"
p_tcp_flags :: "tcp_flag set"
*)

definition "route2match r =
⦇iiface = ifaceAny, oiface = ifaceAny,
src = (0,0), dst=(pfxm_prefix (routing_match r),pfxm_length (routing_match r)),
proto=ProtoAny, sports=(0,max_word), ports=(0,max_word)⦈"

definition toprefixmatch where
"toprefixmatch m ≡ (let pm = PrefixMatch (fst m) (snd m) in if pm = PrefixMatch 0 0 then None else Some pm)"
lemma prefix_match_semantics_simple_match:
assumes some: "toprefixmatch m = Some pm"
assumes vld: "valid_prefix pm"
shows "prefix_match_semantics pm = simple_match_ip m"
using some
by(cases m)
(clarsimp
split: if_splits)

definition simple_match_to_of_match_single ::
"(32, 'a) simple_match_scheme
⇒ char list option ⇒ protocol ⇒ (16 word × 16 word) option ⇒ (16 word × 16 word) option ⇒ of_match_field set"
where
"simple_match_to_of_match_single m iif prot sport dport ≡
uncurry L4Src  option2set sport ∪ uncurry L4Dst  option2set dport
∪ IPv4Proto  (case prot of ProtoAny ⇒ {} | Proto p ⇒ {p}) ― ‹protocol is an 8 word option anyway...›
∪ IngressPort  option2set iif
∪ IPv4Src  option2set (toprefixmatch (src m)) ∪ IPv4Dst  option2set (toprefixmatch (dst m))
∪ {EtherType 0x0800}"
(* okay, we need to make sure that no packets are output on the interface they were input on. So for rules that don't have an input interface, we'd need to do a product over all interfaces, if we stay naive.
The more smart way would be to insert a rule with the same match condition that additionally matches the input interface and drops. However, I'm afraid this is going to be very tricky to verify… *)
definition simple_match_to_of_match :: "32 simple_match ⇒ string list ⇒ of_match_field set list" where
"simple_match_to_of_match m ifs ≡ (let
npm = (λp. fst p = 0 ∧ snd p = max_word);
sb = (λp. (if npm p then [None] else if fst p ≤ snd p
then map (Some ∘ (λpfx. (pfxm_prefix pfx, NOT (pfxm_mask pfx)))) (wordinterval_CIDR_split_prefixmatch (WordInterval (fst p) (snd p))) else []))
in [simple_match_to_of_match_single m iif (proto m) sport dport.
iif ← (if iiface m = ifaceAny then [None] else [Some i. i ← ifs, match_iface (iiface m) i]),
sport ← sb (sports m),
dport ← sb (dports m)]
)"
(* I wonder… should I check whether list_all (match_iface (iiface m)) ifs instead of iiface m = ifaceAny? It would be pretty stupid if that wasn't the same, but you know… *)

lemma smtoms_eq_hlp: "simple_match_to_of_match_single r a b c d = simple_match_to_of_match_single r f g h i ⟷ (a = f ∧ b = g ∧ c = h ∧ d = i)"
(* In case this proof breaks: there are two alternate proofs in the repo. They are of similar quality, though. Good luck. *)
proof(rule iffI,goal_cases)
case 1
thus ?case proof(intro conjI)
have *: "⋀P z x. ⟦∀x :: of_match_field. P x; z = Some x⟧ ⟹ P (IngressPort x)" by simp
show "a = f" using 1 by(cases a; cases f)
(simp add: option2set_None simple_match_to_of_match_single_def toprefixmatch_def option2set_def;
subst(asm) set_eq_iff; drule (1) *; simp split: option.splits uncurry_splits protocol.splits)+
next
have *: "⋀P z x. ⟦∀x :: of_match_field. P x; z = Proto x⟧ ⟹ P (IPv4Proto x)" by simp
show "b = g" using 1 by(cases b; cases g)
(simp add: option2set_None simple_match_to_of_match_single_def toprefixmatch_def option2set_def;
subst(asm) set_eq_iff; drule (1) *; simp split: option.splits uncurry_splits protocol.splits)+
next
have *: "⋀P z x. ⟦∀x :: of_match_field. P x; z = Some x⟧ ⟹ P (uncurry L4Src x)" by simp
show "c = h" using 1 by(cases c; cases h)
(simp add: option2set_None simple_match_to_of_match_single_def toprefixmatch_def option2set_def;
subst(asm) set_eq_iff; drule (1) *; simp split: option.splits uncurry_splits protocol.splits)+
next
have *: "⋀P z x. ⟦∀x :: of_match_field. P x; z = Some x⟧ ⟹ P (uncurry L4Dst x)" by simp
show "d = i" using 1 by(cases d; cases i)
(simp add: option2set_None simple_match_to_of_match_single_def toprefixmatch_def option2set_def;
subst(asm) set_eq_iff; drule (1) *; simp split: option.splits uncurry_splits protocol.splits)+
qed
qed simp

lemma simple_match_to_of_match_generates_prereqs: "simple_match_valid m ⟹ r ∈ set (simple_match_to_of_match m ifs) ⟹ all_prerequisites r"
unfolding simple_match_to_of_match_def Let_def
proof(clarsimp, goal_cases)
case (1 xiface xsrcp xdstp)
note o = this
show ?case unfolding simple_match_to_of_match_single_def all_prerequisites_def
unfolding ball_Un
proof((intro conjI; ((simp;fail)| - )), goal_cases)
case 1
have e: "(fst (sports m) = 0 ∧ snd (sports m) = max_word) ∨ proto m = Proto TCP ∨ proto m = Proto UDP ∨ proto m = Proto L4_Protocol.SCTP"
using o(1)
unfolding simple_match_valid_alt Let_def
by(clarsimp split: if_splits)
show ?case
using o(3) e
by(elim disjE; simp add: option2set_def split: if_splits prod.splits uncurry_splits)
next
case 2
have e: "(fst (dports m) = 0 ∧ snd (dports m) = max_word) ∨ proto m = Proto TCP ∨ proto m = Proto UDP ∨ proto m = Proto L4_Protocol.SCTP"
using o(1)
unfolding simple_match_valid_alt Let_def
by(clarsimp split: if_splits)
show ?case
using o(4) e
by(elim disjE; simp add: option2set_def split: if_splits prod.splits uncurry_splits)
qed
qed

lemma and_assoc: "a ∧ b ∧ c ⟷ (a ∧ b) ∧ c" by simp

lemmas custom_simpset = Let_def set_concat set_map map_map comp_def concat_map_maps set_maps UN_iff fun_app_def Set.image_iff

abbreviation "simple_fw_prefix_to_wordinterval ≡ prefix_to_wordinterval ∘ uncurry PrefixMatch"

lemma simple_match_port_alt: "simple_match_port m p ⟷ p ∈ wordinterval_to_set (uncurry WordInterval m)" by(simp split: uncurry_splits)

lemma simple_match_src_alt: "simple_match_valid r ⟹
simple_match_ip (src r) p ⟷ prefix_match_semantics (PrefixMatch (fst (src r)) (snd (src r))) p"
lemma simple_match_dst_alt: "simple_match_valid r ⟹
simple_match_ip (dst r) p ⟷ prefix_match_semantics (PrefixMatch (fst (dst r)) (snd (dst r))) p"

lemma "x ∈ set (wordinterval_CIDR_split_prefixmatch w) ⟹ valid_prefix x"
using wordinterval_CIDR_split_prefixmatch_all_valid_Ball[THEN bspec, THEN conjunct1] .

lemma simple_match_to_of_matchI:
assumes mv: "simple_match_valid r"
assumes mm: "simple_matches r p"
assumes ii: "p_iiface p ∈ set ifs"
assumes ippkt: "p_l2type p = 0x800"
shows eq: "∃gr ∈ set (simple_match_to_of_match r ifs). OF_match_fields gr p = Some True"
proof -
let ?npm = "λp. fst p = 0 ∧ snd p = max_word"
let ?sb = "λp r. (if ?npm p then None else Some r)"
obtain si where si: "case si of Some ssi ⇒ p_sport p ∈ prefix_to_wordset ssi | None ⇒ True"
"case si of None ⇒ True | Some ssi ⇒ ssi ∈ set (
wordinterval_CIDR_split_prefixmatch (uncurry WordInterval (sports r)))"
"si = None ⟷ ?npm (sports r)"
proof(cases "?npm (sports r)", goal_cases)
case 1 (* True *)
hence "(case None of None ⇒ True | Some ssi ⇒ p_sport p ∈ prefix_to_wordset ssi) ∧
(case None of None ⇒ True
| Some ssi ⇒ ssi ∈ set (wordinterval_CIDR_split_prefixmatch (uncurry WordInterval (sports r))))" by simp
with 1 show ?thesis by blast
next
case 2 (* False *)
from mm have "p_sport p ∈ wordinterval_to_set (uncurry WordInterval (sports r))"
by(simp only: simple_matches.simps simple_match_port_alt)
then obtain ssi where ssi:
"ssi ∈ set (wordinterval_CIDR_split_prefixmatch (uncurry WordInterval (sports r)))"
"p_sport p ∈ prefix_to_wordset ssi"
using wordinterval_CIDR_split_existential by fast
hence "(case Some ssi of None ⇒ True | Some ssi ⇒ p_sport p ∈ prefix_to_wordset ssi) ∧
(case Some ssi of None ⇒ True
| Some ssi ⇒ ssi ∈ set (wordinterval_CIDR_split_prefixmatch (uncurry WordInterval (sports r))))" by simp
with 2 show ?thesis by blast
qed
obtain di where di: "case di of Some ddi ⇒ p_dport p ∈ prefix_to_wordset ddi | None ⇒ True"
"case di of None ⇒ True | Some ddi ⇒ ddi ∈ set (
wordinterval_CIDR_split_prefixmatch (uncurry WordInterval (dports r)))"
"di = None ⟷ ?npm (dports r)"
proof(cases "?npm (dports r)", goal_cases)
case 1
hence "(case None of None ⇒ True | Some ssi ⇒ p_dport p ∈ prefix_to_wordset ssi) ∧
(case None of None ⇒ True
| Some ssi ⇒ ssi ∈ set (wordinterval_CIDR_split_prefixmatch (uncurry WordInterval (dports r))))" by simp
with 1 show ?thesis by blast
next
case 2
from mm have "p_dport p ∈ wordinterval_to_set (uncurry WordInterval (dports r))"
by(simp only: simple_matches.simps simple_match_port_alt)
then obtain ddi where ddi:
"ddi ∈ set (wordinterval_CIDR_split_prefixmatch (uncurry WordInterval (dports r)))"
"p_dport p ∈ prefix_to_wordset ddi"
using wordinterval_CIDR_split_existential by fast
hence "(case Some ddi of None ⇒ True | Some ssi ⇒ p_dport p ∈ prefix_to_wordset ssi) ∧
(case Some ddi of None ⇒ True
| Some ssi ⇒ ssi ∈ set (wordinterval_CIDR_split_prefixmatch (uncurry WordInterval (dports r))))" by simp
with 2 show ?thesis by blast
qed
show ?thesis
proof
let ?mf = "map_option (apsnd (wordNOT ∘ mask ∘ (-) 16) ∘ prefix_match_dtor)"
let ?gr = "simple_match_to_of_match_single r
(if iiface r = ifaceAny then None else Some (p_iiface p))
(if proto r = ProtoAny then ProtoAny else Proto (p_proto p))
(?mf si) (?mf di)"
note mfu = simple_match_port.simps[of "fst (sports r)" "snd (sports r)", unfolded surjective_pairing[of "sports r",symmetric]]
simple_match_port.simps[of "fst (dports r)" "snd (dports r)", unfolded surjective_pairing[of "dports r",symmetric]]
note u = mm[unfolded simple_matches.simps mfu ord_class.atLeastAtMost_iff simple_packet_unext_def simple_packet.simps]
note of_safe_unsafe_match_eq[OF simple_match_to_of_match_generates_prereqs]
from u have ple: "fst (sports r) ≤ snd (sports r)" "fst (dports r) ≤ snd (dports r)" by force+
show eg: "?gr ∈ set (simple_match_to_of_match r ifs)"
unfolding simple_match_to_of_match_def
unfolding custom_simpset
unfolding smtoms_eq_hlp
proof(intro bexI, (intro conjI; ((rule refl)?)), goal_cases)
case 2 thus ?case using ple(2) di
split: option.splits prod.splits uncurry_splits)
apply(erule bexI[rotated])
apply(simp split: prefix_match.splits)
done
next
case 3 thus ?case using ple(1) si
split: option.splits prod.splits uncurry_splits)
apply(erule bexI[rotated])
apply(simp split: prefix_match.splits)
done
next
case 4 thus ?case
using u ii by(clarsimp simp: set_maps split: if_splits)
next
case 1 thus ?case using ii u by simp_all (metis match_proto.elims(2))
qed
have dpm: "di = Some (PrefixMatch x1 x2) ⟹ p_dport p && ~~ (mask (16 - x2)) = x1" for x1 x2
proof -
have *: "di = Some (PrefixMatch x1 x2) ⟹ prefix_match_semantics (the di) (p_dport p) ⟹ p_dport p && ~~ (mask (16 - x2)) = x1"
have **: "pfx ∈ set (wordinterval_CIDR_split_prefixmatch ra) ⟹ prefix_match_semantics pfx a = (a ∈ prefix_to_wordset pfx)" for pfx ra and a :: "16 word"
by (fact prefix_match_semantics_wordset[OF wordinterval_CIDR_split_prefixmatch_all_valid_Ball[THEN bspec, THEN conjunct1]])
have "⟦di = Some (PrefixMatch x1 x2); p_dport p ∈ prefix_to_wordset (PrefixMatch x1 x2); PrefixMatch x1 x2 ∈ set (wordinterval_CIDR_split_prefixmatch (uncurry WordInterval (dports r)))⟧
⟹ p_dport p && ~~ (mask (16 - x2)) = x1"
using di(1,2)
using * ** by auto
thus "di = Some (PrefixMatch x1 x2) ⟹ p_dport p && ~~ (mask (16 - x2)) = x1"  using di(1,2) by auto
qed
have spm: "si = Some (PrefixMatch x1 x2) ⟹ p_sport p && ~~ (mask (16 - x2)) = x1" for x1 x2
using si
proof -
have *: "si = Some (PrefixMatch x1 x2) ⟹ prefix_match_semantics (the si) (p_sport p) ⟹ p_sport p && ~~ (mask (16 - x2)) = x1"
have **: "pfx ∈ set (wordinterval_CIDR_split_prefixmatch ra) ⟹ prefix_match_semantics pfx a = (a ∈ prefix_to_wordset pfx)" for pfx ra and a :: "16 word"
by (fact prefix_match_semantics_wordset[OF wordinterval_CIDR_split_prefixmatch_all_valid_Ball[THEN bspec, THEN conjunct1]])
have "⟦si = Some (PrefixMatch x1 x2); p_sport p ∈ prefix_to_wordset (PrefixMatch x1 x2); PrefixMatch x1 x2 ∈ set (wordinterval_CIDR_split_prefixmatch (uncurry WordInterval (sports r)))⟧
⟹ p_sport p && ~~ (mask (16 - x2)) = x1"
using si(1,2)
using * ** by auto
thus "si = Some (PrefixMatch x1 x2) ⟹ p_sport p && ~~ (mask (16 - x2)) = x1"  using si(1,2) by auto
qed
show "OF_match_fields ?gr p = Some True"
unfolding of_safe_unsafe_match_eq[OF simple_match_to_of_match_generates_prereqs[OF mv eg]]
by(cases si; cases di)
(simp_all
option2set_def u ippkt prefix_match_dtor_def toprefixmatch_def dpm
simple_match_dst_alt[OF mv, symmetric] simple_match_src_alt[OF mv, symmetric]
split: prefix_match.splits)
qed
qed

lemma prefix_match_00[simp,intro!]: "prefix_match_semantics (PrefixMatch 0 0) p"

lemma simple_match_to_of_matchD:
assumes eg: "gr ∈ set (simple_match_to_of_match r ifs)"
assumes mo: "OF_match_fields gr p = Some True"
assumes me: "match_iface (oiface r) (p_oiface p)"
assumes mv: "simple_match_valid r"
shows "simple_matches r p"
proof -
from mv have validpfx:
"valid_prefix (uncurry PrefixMatch (src r))" "valid_prefix (uncurry PrefixMatch (dst r))"
"⋀pm. toprefixmatch (src r) = Some pm ⟹ valid_prefix pm"
"⋀pm. toprefixmatch (dst r) = Some pm ⟹ valid_prefix pm"
unfolding simple_match_valid_def valid_prefix_fw_def toprefixmatch_def
by(simp_all split: uncurry_splits if_splits)
from mo have mo: "OF_match_fields_unsafe gr p"
unfolding of_safe_unsafe_match_eq[OF simple_match_to_of_match_generates_prereqs[OF mv eg]]
by simp
note this[unfolded OF_match_fields_unsafe_def]
note eg[unfolded simple_match_to_of_match_def simple_match_to_of_match_single_def  custom_simpset option2set_def]
then guess x ..	moreover from this(2) guess xa ..	moreover from this(2) guess xb ..
note xx = calculation(1,3) this

{ fix a b xc xa
fix pp :: "16 word"
have "⟦pp && ~~ (pfxm_mask xc) = pfxm_prefix xc⟧
⟹ prefix_match_semantics xc (pp)" for xc
moreover have "pp ∈ wordinterval_to_set (WordInterval a b) ⟹ a ≤ pp ∧ pp ≤ b" by simp
moreover have "xc ∈ set (wordinterval_CIDR_split_prefixmatch (WordInterval a b)) ⟹ pp ∈ prefix_to_wordset xc  ⟹ pp ∈ wordinterval_to_set (WordInterval a b)"
by(subst wordinterval_CIDR_split_prefixmatch) blast
moreover have "⟦xc ∈ set (wordinterval_CIDR_split_prefixmatch (WordInterval a b)); xa = Some (pfxm_prefix xc, ~~ (pfxm_mask xc)); prefix_match_semantics xc (pp)⟧ ⟹ pp ∈ prefix_to_wordset xc"
apply(subst(asm)(1) prefix_match_semantics_wordset)
apply(erule wordinterval_CIDR_split_prefixmatch_all_valid_Ball[THEN bspec, THEN conjunct1];fail)
apply assumption
done
ultimately have "⟦xc ∈ set (wordinterval_CIDR_split_prefixmatch (WordInterval a b)); xa = Some (pfxm_prefix xc, ~~ (pfxm_mask xc));
pp && ~~ (pfxm_mask xc) = pfxm_prefix xc⟧
⟹ a ≤ pp ∧ pp ≤ b"
by metis
} note l4port_logic = this

show ?thesis unfolding simple_matches.simps
proof(unfold and_assoc, (rule)+)
show "match_iface (iiface r) (p_iiface p)"
apply(cases "iiface r = ifaceAny")
using xx(1) mo unfolding xx(4) OF_match_fields_unsafe_def
apply(simp only: if_False set_maps UN_iff)
apply(clarify)
apply(rename_tac a; subgoal_tac "match_iface (iiface r) a")
apply(rule ccontr,simp;fail)
done
next
show "match_iface (oiface r) (p_oiface p)" using me .
next
show "simple_match_ip (src r) (p_src p)"
using mo unfolding xx(4) OF_match_fields_unsafe_def toprefixmatch_def
by(clarsimp
simp add: simple_packet_unext_def option2set_def validpfx simple_match_src_alt[OF mv] toprefixmatch_def
split: if_splits)
next
show "simple_match_ip (dst r) (p_dst p)"
using mo unfolding xx(4) OF_match_fields_unsafe_def toprefixmatch_def
by(clarsimp
simp add: simple_packet_unext_def option2set_def validpfx simple_match_dst_alt[OF mv] toprefixmatch_def
split: if_splits)
next
show "match_proto (proto r) (p_proto p)"
using mo unfolding xx(4) OF_match_fields_unsafe_def
using xx(1) by(clarsimp
simp add: singleton_iff simple_packet_unext_def option2set_def prefix_match_semantics_simple_match ball_Un
split: if_splits protocol.splits)
next
show "simple_match_port (sports r) (p_sport p)"
using mo xx(2) unfolding xx(4) OF_match_fields_unsafe_def
by(cases "sports r") (clarsimp simp add: l4port_logic simple_packet_unext_def option2set_def prefix_match_semantics_simple_match split: if_splits)
next
show "simple_match_port (dports r) (p_dport p)"
using mo xx(3) unfolding xx(4) OF_match_fields_unsafe_def
by(cases "dports r") (clarsimp simp add: l4port_logic simple_packet_unext_def option2set_def prefix_match_semantics_simple_match split: if_splits)
qed
qed

primrec annotate_rlen where
"annotate_rlen [] = []" |
"annotate_rlen (a#as) = (length as, a) # annotate_rlen as"
lemma "annotate_rlen ''asdf'' = [(3, CHR ''a''), (2, CHR ''s''), (1, CHR ''d''), (0, CHR ''f'')]" by simp

lemma fst_annotate_rlen_le: "(k, a) ∈ set (annotate_rlen l) ⟹ k < length l"
by(induction l arbitrary: k; simp; force)

lemma distinct_fst_annotate_rlen: "distinct (map fst (annotate_rlen l))"
using fst_annotate_rlen_le by(induction l) (simp, fastforce)
lemma distinct_annotate_rlen: "distinct (annotate_rlen l)"
using distinct_fst_annotate_rlen unfolding distinct_map by blast
lemma in_annotate_rlen: "(a,x) ∈ set (annotate_rlen l) ⟹ x ∈ set l"
by(induction l) (simp_all, blast)
lemma map_snd_annotate_rlen: "map snd (annotate_rlen l) = l"
by(induction l) simp_all
lemma "sorted_descending (map fst (annotate_rlen l))"
by(induction l; clarsimp) (force dest: fst_annotate_rlen_le)
lemma "annotate_rlen l = zip (rev [0..<length l]) l"
by(induction l; simp) (* It would probably have been better to just use the zip, but oh well… *)

primrec annotate_rlen_code where
"annotate_rlen_code [] = (0,[])" |
"annotate_rlen_code (a#as) = (case annotate_rlen_code as of (r,aas) ⇒ (Suc r, (r, a) # aas))"
lemma annotate_rlen_len: "fst (annotate_rlen_code r) = length r"
by(induction r) (clarsimp split: prod.splits)+
lemma annotate_rlen_code[code]: "annotate_rlen s = snd (annotate_rlen_code s)"
proof(induction s)
case (Cons s ss) thus ?case using annotate_rlen_len[of ss] by(clarsimp split: prod.split)
qed simp

lemma suc2plus_inj_on: "inj_on (of_nat :: nat ⇒ ('l :: len) word) {0..unat (max_word :: 'l word)}"
proof(rule inj_onI)
let ?mmw = "(max_word :: 'l word)"
let ?mstp = "(of_nat :: nat ⇒ 'l word)"
fix x y :: nat
assume "x ∈ {0..unat ?mmw}" "y ∈ {0..unat ?mmw}"
hence se: "x ≤ unat ?mmw" "y ≤ unat ?mmw" by simp_all
assume eq: "?mstp x = ?mstp y"
note f = le_unat_uoi[OF se(1)] le_unat_uoi[OF se(2)]
show "x = y" using eq le_unat_uoi se by metis
qed

lemma distinct_of_nat_list: (* TODO: Move to CaesarWordLemmaBucket *)
"distinct l ⟹ ∀e ∈ set l. e ≤ unat (max_word :: ('l::len) word) ⟹ distinct (map (of_nat :: nat ⇒ 'l word) l)"
proof(induction l)
let ?mmw = "(max_word :: 'l word)"
let ?mstp = "(of_nat :: nat ⇒ 'l word)"
case (Cons a as)
have "distinct as" "∀e∈set as. e ≤ unat ?mmw" using Cons.prems by simp_all
note mIH = Cons.IH[OF this]
moreover have "?mstp a ∉ ?mstp  set as"
proof
have representable_set: "set as ⊆ {0..unat ?mmw}" using ‹∀e∈set (a # as). e ≤ unat max_word› by fastforce
have a_reprbl: "a ∈ {0..unat ?mmw}" using ‹∀e∈set (a # as). e ≤ unat max_word› by simp
assume "?mstp a ∈ ?mstp  set as"
with inj_on_image_mem_iff[OF suc2plus_inj_on a_reprbl representable_set]
have "a ∈ set as" by simp
with ‹distinct (a # as)› show False by simp
qed
ultimately show ?case by simp
qed simp

lemma annotate_first_le_hlp:
"length l < unat (max_word :: ('l :: len) word) ⟹ ∀e∈set (map fst (annotate_rlen l)). e ≤ unat (max_word :: 'l word)"
by(clarsimp) (meson fst_annotate_rlen_le less_trans nat_less_le)
lemmas distinct_of_prio_hlp = distinct_of_nat_list[OF distinct_fst_annotate_rlen annotate_first_le_hlp]
(* don't need these right now, but maybe later? *)

lemma fst_annotate_rlen: "map fst (annotate_rlen l) = rev [0..<length l]"
by(induction l) (simp_all)

lemma sorted_word_upt:
defines[simp]: "won ≡ (of_nat :: nat ⇒ ('l :: len) word)"
assumes "length l ≤ unat (max_word :: 'l word)"
shows "sorted_descending (map won (rev [0..<Suc (length l)]))"
using assms
by(induction l rule: rev_induct;clarsimp)
(metis (mono_tags, hide_lams) le_SucI le_unat_uoi of_nat_Suc order_refl word_le_nat_alt)
(* This proof is kind of ugly. In case it breaks unfixably, go back to rev a9c4927 and get word_upto.
The lemmas on word_upto can be used to shows this trivially. *)

lemma sorted_annotated:
assumes "length l ≤ unat (max_word :: ('l :: len) word)"
shows "sorted_descending (map fst (map (apfst (of_nat :: nat ⇒ 'l word)) (annotate_rlen l)))"
proof -
let ?won = "(of_nat :: nat ⇒ 'l word)"
have "sorted_descending (map ?won (rev [0..<Suc (length l)]))"
using sorted_word_upt[OF assms] .
hence "sorted_descending (map ?won (map fst (annotate_rlen l)))" by(simp add: fst_annotate_rlen)
thus "sorted_descending (map fst (map (apfst ?won) (annotate_rlen l)))" by simp
qed

text‹l3 device to l2 forwarding›
definition "lr_of_tran_s3 ifs ard = (
[(p, b, case a of simple_action.Accept ⇒ [Forward c] | simple_action.Drop ⇒ []).
(p,r,(c,a)) ← ard, b ← simple_match_to_of_match r ifs])"

definition "oif_ne_iif_p1 ifs ≡ [(simple_match_any⦇oiface := Iface oif, iiface := Iface iif⦈, simple_action.Accept). oif ← ifs, iif ← ifs, oif ≠ iif]"
definition "oif_ne_iif_p2 ifs = [(simple_match_any⦇oiface := Iface i, iiface := Iface i⦈, simple_action.Drop). i ← ifs]"
definition "oif_ne_iif ifs = oif_ne_iif_p2 ifs @ oif_ne_iif_p1 ifs" (* order irrelephant *)
(*value "oif_ne_iif [''a'', ''b'']"*)
(* I first tried something like "oif_ne_iif ifs ≡ [(simple_match_any⦇oiface := Iface oi, iiface := Iface ii⦈, if oi = ii then simple_action.Drop else simple_action.Accept). oi ← ifs, ii ← ifs]",
but making the statement I wanted with that was really tricky. Much easier to have the second element constant and do it separately. *)
definition "lr_of_tran_s4 ard ifs ≡ generalized_fw_join ard (oif_ne_iif ifs)"

definition "lr_of_tran_s1 rt = [(route2match r, output_iface (routing_action r)). r ← rt]"

definition "lr_of_tran_fbs rt fw ifs ≡ let
gfw = map simple_rule_dtor fw; ― ‹generalized simple fw, hopefully for FORWARD›
frt = lr_of_tran_s1 rt; ― ‹rt as fw›
prd = generalized_fw_join frt gfw
in prd
"

definition "pack_OF_entries ifs ard ≡ (map (split3 OFEntry) (lr_of_tran_s3 ifs ard))"
definition "no_oif_match ≡ list_all (λm. oiface (match_sel m) = ifaceAny)"

definition "lr_of_tran rt fw ifs ≡
if ¬ (no_oif_match fw ∧ has_default_policy fw ∧ simple_fw_valid fw	∧ valid_prefixes rt ∧ has_default_route rt ∧ distinct ifs)
then Inl ''Error in creating OpenFlow table: prerequisites not satisifed''
else (
let	nrd = lr_of_tran_fbs rt fw ifs;
ard = map (apfst of_nat) (annotate_rlen nrd) ― ‹give them a priority›
in
if length nrd < unat (max_word :: 16 word)
then Inr (pack_OF_entries ifs ard)
else Inl ''Error in creating OpenFlow table: priority number space exhausted'')
"

definition "is_iface_name i ≡ i ≠ [] ∧ ¬Iface.iface_name_is_wildcard i"
definition "is_iface_list ifs ≡ distinct ifs ∧ list_all is_iface_name ifs"

lemma max_16_word_max[simp]: "(a :: 16 word) ≤ 0xffff"
proof -
have "0xFFFF = (- 1 :: 16 word)" by simp
then show ?thesis by (simp only:) simp
qed

lemma replicate_FT_hlp: "x ≤ 16 ∧ y ≤ 16 ⟹ replicate (16 - x) False @ replicate x True = replicate (16 - y) False @ replicate y True ⟹ x = y"
proof -
let ?ns = "{0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16}"
assume "x ≤ 16 ∧ y ≤ 16"
hence "x ∈ ?ns" "y ∈ ?ns" by(simp; presburger)+
moreover assume "replicate (16 - x) False @ replicate x True = replicate (16 - y) False @ replicate y True"
ultimately show "x = y" by simp (elim disjE; simp_all add: numeral_eq_Suc) (* that's only 289 subgoals after the elim *)
qed

proof(intro inj_onI, goal_cases)
case (1 x y)
from 1(3)
have oe: "of_bl (replicate (16 - x) False @ replicate x True) = (of_bl (replicate (16 - y) False @ replicate y True) :: 16 word)"
have "⋀z. z ≤ 16 ⟹ length (replicate (16 - z) False @ replicate z True) = 16" by auto
with 1(1,2)
have ps: "replicate (16 - x) False @ replicate x True ∈ {bl. length bl = LENGTH(16)}" " replicate (16 - y) False @ replicate y True ∈ {bl. length bl = LENGTH(16)}" by simp_all
from inj_onD[OF word_bl.Abs_inj_on, OF oe ps]
show ?case using 1(1,2) by(fastforce intro: replicate_FT_hlp)
qed

lemma distinct_simple_match_to_of_match_portlist_hlp:
fixes ps :: "(16 word × 16 word)"
shows "distinct ifs ⟹
distinct
(if fst ps = 0 ∧ snd ps = max_word then [None]
else if fst ps ≤ snd ps
then map (Some ∘ (λpfx. (pfxm_prefix pfx, ~~ (pfxm_mask pfx))))
(wordinterval_CIDR_split_prefixmatch (WordInterval (fst ps) (snd ps)))
else [])"
proof -
assume di: "distinct ifs"
{ define wis where "wis = set (wordinterval_CIDR_split_prefixmatch (WordInterval (fst ps) (snd ps)))"
fix x y :: "16 prefix_match"
obtain xm xn ym yn where xyd[simp]: "x = PrefixMatch xm xn" "y = PrefixMatch ym yn" by(cases x; cases y)
assume iw: "x ∈ wis" "y ∈ wis" and et: "(pfxm_prefix x, ~~ (pfxm_mask x)) = (pfxm_prefix y, ~~ (pfxm_mask y))"
hence le16: "xn ≤ 16" "yn ≤ 16" unfolding wis_def using wordinterval_CIDR_split_prefixmatch_all_valid_Ball[unfolded Ball_def, THEN spec, THEN mp] by force+
with et have "16 - xn = 16 - yn" unfolding pfxm_mask_def by(auto intro: mask_inj_hlp1[THEN inj_onD])
hence "x = y" using et le16 using diff_diff_cancel by simp
} note * = this
show ?thesis
apply(clarsimp simp add: smtoms_eq_hlp distinct_map wordinterval_CIDR_split_distinct)
apply(subst comp_inj_on_iff[symmetric]; intro inj_onI)
using * by simp_all
qed

lemma distinct_simple_match_to_of_match: "distinct ifs ⟹ distinct (simple_match_to_of_match m ifs)"
apply(unfold simple_match_to_of_match_def Let_def)
apply(rule distinct_3lcomprI)
subgoal by(induction ifs; clarsimp)
subgoal by(fact distinct_simple_match_to_of_match_portlist_hlp)
subgoal by(fact distinct_simple_match_to_of_match_portlist_hlp)
done

lemma inj_inj_on: "inj F ⟹ inj_on F A" using subset_inj_on by auto (* TODO: include Word_Lib *)

lemma no_overlaps_lroft_hlp2: "distinct (map fst amr) ⟹ (⋀r. distinct (fm r)) ⟹
distinct (concat (map (λ(p, r, c, a). map (λb. (p, b, fs a c)) (fm r)) amr))"
by(induction amr; force intro: injI inj_onI simp add: distinct_map split: prod.splits)

lemma distinct_lroft_s3: "⟦distinct (map fst amr); distinct ifs⟧ ⟹ distinct (lr_of_tran_s3 ifs amr)"
unfolding lr_of_tran_s3_def

lemma no_overlaps_lroft_hlp3: "distinct (map fst amr) ⟹
(aa, ab, ac) ∈ set (lr_of_tran_s3 ifs amr) ⟹ (ba, bb, bc) ∈ set (lr_of_tran_s3 ifs amr) ⟹
ac ≠ bc ⟹ aa ≠ ba"
apply(unfold lr_of_tran_s3_def)
apply(clarsimp)
apply(clarsimp split: simple_action.splits)
apply(metis map_of_eq_Some_iff old.prod.inject option.inject)
apply(metis map_of_eq_Some_iff old.prod.inject option.inject simple_action.distinct(2))+
done

lemma no_overlaps_lroft_s3_hlp_hlp: (* I hlps *)
"⟦distinct (map fst amr); OF_match_fields_unsafe ab p; ab ≠ ad ∨ ba ≠ bb; OF_match_fields_unsafe ad p;
(ac, ab, ba) ∈ set (lr_of_tran_s3 ifs amr); (ac, ad, bb) ∈ set (lr_of_tran_s3 ifs amr)⟧
⟹ False"
proof(elim disjE, goal_cases)
case 1
have 4: "⟦distinct (map fst amr);  (ac, ab, x1, x2) ∈ set amr; (ac, bb, x4, x5) ∈ set amr; ab ≠ bb⟧
⟹ False" for ab x1 x2 bb x4 x5
by (meson distinct_map_fstD old.prod.inject)
have conjunctSomeProtoAnyD: "Some ProtoAny = simple_proto_conjunct a (Proto b) ⟹ False" for a b
using conjunctProtoD by force
have 5:
"⟦OF_match_fields_unsafe am p; OF_match_fields_unsafe bm p; am ≠ bm;
am ∈ set (simple_match_to_of_match ab ifs); bm ∈ set (simple_match_to_of_match bb ifs); ¬ ab ≠ bb⟧
⟹ False" for ab bb am bm
by(clarify | unfold
simple_match_to_of_match_def smtoms_eq_hlp Let_def set_concat set_map de_Morgan_conj not_False_eq_True)+
(auto dest: conjunctSomeProtoAnyD cidrsplit_no_overlaps
simp add: OF_match_fields_unsafe_def simple_match_to_of_match_single_def option2set_def comp_def
split: if_splits
cong: smtoms_eq_hlp) (*1min*)
from 1 show ?case
using 4 5 by(clarsimp simp add: lr_of_tran_s3_def) blast
qed(metis no_overlaps_lroft_hlp3)

lemma no_overlaps_lroft_s3_hlp: "distinct (map fst amr) ⟹ distinct ifs ⟹
no_overlaps OF_match_fields_unsafe (map (split3 OFEntry) (lr_of_tran_s3 ifs amr))"
apply(rule no_overlapsI[rotated])
apply(subst distinct_map, rule conjI)
subgoal by(erule (1) distinct_lroft_s3)
subgoal
apply(rule inj_inj_on)
apply(rule injI)
apply(rename_tac x y, case_tac x, case_tac y)
done
subgoal
apply(unfold check_no_overlap_def)
apply(clarify)
apply(unfold set_map)
apply(clarify)
apply(unfold split3_def prod.simps flow_entry_match.simps flow_entry_match.sel de_Morgan_conj)
apply(clarsimp simp only:)
apply(erule (1) no_overlaps_lroft_s3_hlp_hlp)
apply simp
apply assumption
apply assumption
apply simp
done
done

lemma lr_of_tran_no_overlaps: assumes "distinct ifs" shows "Inr t = (lr_of_tran rt fw ifs) ⟹ no_overlaps OF_match_fields_unsafe t"
apply(unfold lr_of_tran_def Let_def pack_OF_entries_def)
apply(simp split: if_splits)
apply(thin_tac "t = _")
apply(drule distinct_of_prio_hlp)
apply(rule no_overlaps_lroft_s3_hlp[rotated])
done

lemma sorted_lr_of_tran_s3_hlp: "∀x∈set f. fst x ≤ a ⟹ b ∈ set (lr_of_tran_s3 s f) ⟹ fst b ≤ a"

lemma lr_of_tran_s3_Cons: "lr_of_tran_s3 ifs (a#ard) = (
[(p, b, case a of simple_action.Accept ⇒ [Forward c] | simple_action.Drop ⇒ []).
(p,r,(c,a)) ← [a], b ← simple_match_to_of_match r ifs]) @ lr_of_tran_s3 ifs ard"
by(clarsimp simp: lr_of_tran_s3_def)

lemma sorted_lr_of_tran_s3: "sorted_descending (map fst f) ⟹ sorted_descending (map fst (lr_of_tran_s3 s f))"
apply(induction f)
apply(clarsimp simp: lr_of_tran_s3_Cons map_concat comp_def)
apply(unfold sorted_descending_append)
apply(simp add: sorted_descending_alt rev_map sorted_lr_of_tran_s3_hlp sorted_const)
done

lemma sorted_lr_of_tran_hlp: "(ofe_prio ∘ split3 OFEntry) = fst" by(simp add: fun_eq_iff comp_def split3_def)

lemma lr_of_tran_sorted_descending: "Inr r = lr_of_tran rt fw ifs ⟹ sorted_descending (map ofe_prio r)"
apply(unfold lr_of_tran_def Let_def)
apply(simp split: if_splits)
apply(thin_tac "r = _")
apply(unfold sorted_lr_of_tran_hlp pack_OF_entries_def split3_def[abs_def] fun_app_def map_map comp_def prod.case_distrib)
apply(rule sorted_lr_of_tran_s3)
apply(drule sorted_annotated[OF less_or_eq_imp_le, OF disjI1])
done

lemma lr_of_tran_s1_split: "lr_of_tran_s1 (a # rt) = (route2match a, output_iface (routing_action a)) # lr_of_tran_s1 rt"
by(unfold lr_of_tran_s1_def list.map, rule)

lemma route2match_correct: "valid_prefix (routing_match a) ⟹ prefix_match_semantics (routing_match a) (p_dst p) ⟷ simple_matches (route2match a) (p)"

lemma s1_correct: "valid_prefixes rt ⟹ has_default_route (rt::('i::len) prefix_routing) ⟹
∃rm ra. generalized_sfw (lr_of_tran_s1 rt) p = Some (rm,ra) ∧ ra = output_iface (routing_table_semantics rt (p_dst p))"
apply(induction rt)
apply(simp;fail)
apply(drule valid_prefixes_split)
apply(clarsimp)
apply(erule disjE)
subgoal for a rt
apply(case_tac a)
apply(rename_tac routing_m metric routing_action)
apply(case_tac routing_m)
lr_of_tran_s1_def route2match_def simple_matches.simps match_ifaceAny match_iface_refl ipset_from_cidr_0
max_word_mask[where 'a = 'i, symmetric, simplified])
done
subgoal
apply(rule conjI)
lr_of_tran_s1_split generalized_sfw_simps)
done
done

definition "to_OF_action a ≡ (case a of (p,d) ⇒ (case d of simple_action.Accept ⇒ [Forward p] | simple_action.Drop ⇒ []))"
definition "from_OF_action a = (case a of [] ⇒ ('''',simple_action.Drop) | [Forward p] ⇒ (p, simple_action.Accept))"

lemma OF_match_linear_not_noD: "OF_match_linear γ oms p ≠ NoAction ⟹ ∃ome. ome ∈ set oms ∧ γ (ofe_fields ome) p"
apply(induction oms)
apply(simp)
apply(simp split: if_splits)
apply blast+
done

lemma s3_noaction_hlp: "⟦simple_match_valid ac; ¬simple_matches ac p; match_iface (oiface ac) (p_oiface p)⟧ ⟹
OF_match_linear OF_match_fields_safe (map (λx. split3 OFEntry (x1, x, case ba of simple_action.Accept ⇒ [Forward ad] | simple_action.Drop ⇒ [])) (simple_match_to_of_match ac ifs)) p = NoAction"
apply(rule ccontr)
apply(drule OF_match_linear_not_noD)
apply(clarsimp)
apply(rename_tac x)
apply(subgoal_tac "all_prerequisites x")
apply(drule simple_match_to_of_matchD)
apply(subst(asm) of_match_fields_safe_eq2)
apply(simp;fail)+
using simple_match_to_of_match_generates_prereqs by blast

lemma aux:
‹v = Some x ⟹ the v = x›
by simp

lemma s3_correct:
assumes vsfwm: "list_all simple_match_valid (map (fst ∘ snd) ard)"
assumes ippkt: "p_l2type p = 0x800"
assumes iiifs: "p_iiface p ∈ set ifs"
assumes oiifs: "list_all (λm. oiface (fst (snd m)) = ifaceAny) ard"
shows "OF_match_linear OF_match_fields_safe (pack_OF_entries ifs ard) p = Action ao ⟷ (∃r af. generalized_sfw (map snd ard) p = (Some (r,af)) ∧ (if snd af = simple_action.Drop then ao = [] else ao = [Forward (fst af)]))"
unfolding pack_OF_entries_def lr_of_tran_s3_def fun_app_def
using vsfwm oiifs
apply(induction ard)
apply simp
apply(clarsimp simp add: generalized_sfw_simps split: prod.splits)
apply(intro conjI) (* make two subgoals from one *)
subgoal for ard x1 ac ad ba
apply(clarsimp simp add: OF_match_linear_append split: prod.splits)
apply(drule simple_match_to_of_matchI[rotated])
apply(rule iiifs)
apply(rule ippkt)
apply blast
apply(drule
OF_match_linear_match_allsameaction[where
γ=OF_match_fields_safe and pri = x1 and
oms = "simple_match_to_of_match ac ifs" and
act = "case ba of simple_action.Accept ⇒ [Forward ad] | simple_action.Drop ⇒ []"])
apply(unfold OF_match_fields_safe_def comp_def)
apply(erule aux)
apply(clarsimp)
apply(intro iffI)
subgoal
apply(rule exI[where x = ac])
apply(rule exI[where x = ba])
apply(clarsimp simp: split3_def split: simple_action.splits flowtable_behavior.splits if_splits)
done
subgoal
apply(clarsimp)
apply(rename_tac b)
apply(case_tac b)
apply(simp_all)
done
done
subgoal for ard x1 ac ad ba
apply(clarify)
apply(subgoal_tac "OF_match_linear OF_match_fields_safe (map (λx. split3 OFEntry (x1, x, case ba of simple_action.Accept ⇒ [Forward ad] | simple_action.Drop ⇒ [])) (simple_match_to_of_match ac ifs)) p = NoAction")
apply(simp;fail)
apply(erule (1) s3_noaction_hlp)
done
done

context
notes valid_prefix_00[simp, intro!]
begin
lemma lr_of_tran_s1_valid: "valid_prefixes rt ⟹ gsfw_valid (lr_of_tran_s1 rt)"
unfolding lr_of_tran_s1_def route2match_def gsfw_valid_def list_all_iff
apply(clarsimp simp: simple_match_valid_def valid_prefix_fw_def)
apply(intro conjI)
apply force
done
end

lemma simple_match_valid_fbs_rlen: "⟦valid_prefixes rt; simple_fw_valid fw; (a, aa, ab, b) ∈ set (annotate_rlen (lr_of_tran_fbs rt fw ifs))⟧ ⟹ simple_match_valid aa"
proof(goal_cases)
case 1
note 1[unfolded lr_of_tran_fbs_def Let_def]
have "gsfw_valid (map simple_rule_dtor fw)" using gsfw_validI 1 by blast
moreover have "gsfw_valid (lr_of_tran_s1 rt)" using 1 lr_of_tran_s1_valid by blast
ultimately have "gsfw_valid (generalized_fw_join (lr_of_tran_s1 rt) (map simple_rule_dtor fw))" using gsfw_join_valid by blast
moreover have "(aa, ab, b) ∈ set (lr_of_tran_fbs rt fw ifs)" using 1 using in_annotate_rlen by fast
ultimately show ?thesis unfolding lr_of_tran_fbs_def Let_def gsfw_valid_def list_all_iff by fastforce
qed

lemma simple_match_valid_fbs: "⟦valid_prefixes rt; simple_fw_valid fw⟧ ⟹ list_all simple_match_valid (map fst (lr_of_tran_fbs rt fw ifs))"
proof(goal_cases)
case 1
note 1[unfolded lr_of_tran_fbs_def Let_def]
have "gsfw_valid (map simple_rule_dtor fw)" using gsfw_validI 1 by blast
moreover have "gsfw_valid (lr_of_tran_s1 rt)" using 1 lr_of_tran_s1_valid by blast
ultimately have "gsfw_valid (generalized_fw_join (lr_of_tran_s1 rt) (map simple_rule_dtor fw))" using gsfw_join_valid by blast
thus ?thesis unfolding lr_of_tran_fbs_def Let_def gsfw_valid_def list_all_iff by fastforce
qed

lemma lr_of_tran_prereqs: "valid_prefixes rt ⟹ simple_fw_valid fw ⟹ lr_of_tran rt fw ifs = Inr oft ⟹
list_all (all_prerequisites ∘ ofe_fields) oft"
unfolding lr_of_tran_def pack_OF_entries_def lr_of_tran_s3_def Let_def
apply(simp add: map_concat comp_def prod.case_distrib split3_def split: if_splits)
apply(clarsimp)
apply(drule simple_match_valid_fbs_rlen[rotated])
apply(rule simple_match_to_of_match_generates_prereqs; assumption)
done

(* TODO: move. where? *)
lemma OF_unsafe_safe_match3_eq: "
list_all (all_prerequisites ∘ ofe_fields) oft ⟹
OF_priority_match OF_match_fields_unsafe oft = OF_priority_match OF_match_fields_safe oft"
unfolding OF_priority_match_def[abs_def]
proof(goal_cases)
case 1
from 1 have "⋀packet. [f←oft . OF_match_fields_unsafe (ofe_fields f) packet] = [f←oft . OF_match_fields_safe (ofe_fields f) packet]"
using of_match_fields_safe_eq by(metis (mono_tags, lifting) filter_cong)
thus ?case by metis
qed

lemma OF_unsafe_safe_match_linear_eq: "
list_all (all_prerequisites ∘ ofe_fields) oft ⟹
OF_match_linear OF_match_fields_unsafe oft = OF_match_linear OF_match_fields_safe oft"
unfolding fun_eq_iff
by(induction oft) (clarsimp simp add: list_all_iff of_match_fields_safe_eq)+

lemma simple_action_ne[simp]:
"b ≠ simple_action.Accept ⟷ b = simple_action.Drop"
"b ≠ simple_action.Drop ⟷ b = simple_action.Accept"
using simple_action.exhaust by blast+

lemma map_snd_apfst: "map snd (map (apfst x) l) = map snd l"
unfolding map_map comp_def snd_apfst ..

lemma match_ifaceAny_eq: "oiface m = ifaceAny ⟹ simple_matches m p = simple_matches m (p⦇p_oiface := any⦈)"
by(cases m) (simp add: simple_matches.simps match_ifaceAny)
lemma no_oif_matchD: "no_oif_match fw ⟹ simple_fw fw p = simple_fw fw (p⦇p_oiface := any⦈)"
by(induction fw)
(auto simp add: no_oif_match_def simple_fw_alt dest: match_ifaceAny_eq)

lemma lr_of_tran_fbs_acceptD:
assumes s1: "valid_prefixes rt" "has_default_route rt"
assumes s2: "no_oif_match fw"
shows "generalized_sfw (lr_of_tran_fbs rt fw ifs) p = Some (r, oif, simple_action.Accept) ⟹
simple_linux_router_nol12 rt fw p = Some (p⦇p_oiface := oif⦈)"
proof(goal_cases)
case 1
note 1[unfolded lr_of_tran_fbs_def Let_def, THEN generalized_fw_joinD]
then guess r1 .. then guess r2 .. note r12 = this
note s1_correct[OF s1, of p]
then guess rm .. then guess ra .. note rmra = this
from r12 rmra have oifra: "oif = ra" by simp
from r12 have sfw: "simple_fw fw p = Decision FinalAllow" using simple_fw_iff_generalized_fw_accept by blast
note ifupdateirrel = no_oif_matchD[OF s2, where any = " output_iface (routing_table_semantics rt (p_dst p))" and p = p, symmetric]
show ?case unfolding simple_linux_router_nol12_def by(simp add: Let_def ifupdateirrel sfw oifra rmra split: Option.bind_splits option.splits)
qed

lemma lr_of_tran_fbs_acceptI:
assumes s1: "valid_prefixes rt" "has_default_route rt"
assumes s2: "no_oif_match fw" "has_default_policy fw"
shows "simple_linux_router_nol12 rt fw p = Some (p⦇p_oiface := oif⦈) ⟹
∃r. generalized_sfw (lr_of_tran_fbs rt fw ifs) p = Some (r, oif, simple_action.Accept)"
proof(goal_cases)
from s2 have nud: "⋀p. simple_fw fw p ≠ Undecided" by (metis has_default_policy state.distinct(1))
note ifupdateirrel = no_oif_matchD[OF s2(1), symmetric]
case 1
from 1 have "simple_fw fw p = Decision FinalAllow" by(simp add: simple_linux_router_nol12_def Let_def nud ifupdateirrel split: Option.bind_splits state.splits final_decision.splits)
then obtain r where r: "generalized_sfw (map simple_rule_dtor fw) p = Some (r, simple_action.Accept)" using simple_fw_iff_generalized_fw_accept by blast
have oif_def: "oif = output_iface (routing_table_semantics rt (p_dst p))" using 1 by(cases p) (simp add: simple_linux_router_nol12_def Let_def nud ifupdateirrel split: Option.bind_splits state.splits final_decision.splits)
note s1_correct[OF s1, of p] then guess rm .. then guess ra .. note rmra = this
show ?case unfolding lr_of_tran_fbs_def Let_def
apply(rule exI)
apply(rule generalized_fw_joinI)
unfolding oif_def using rmra apply simp
apply(rule r)
done
qed

lemma lr_of_tran_fbs_dropD:
assumes s1: "valid_prefixes rt" "has_default_route rt"
assumes s2: "no_oif_match fw"
shows "generalized_sfw (lr_of_tran_fbs rt fw ifs) p = Some (r, oif, simple_action.Drop) ⟹
simple_linux_router_nol12 rt fw p = None"
proof(goal_cases)
note ifupdateirrel = no_oif_matchD[OF s2(1), symmetric]
case 1
from 1[unfolded lr_of_tran_fbs_def Let_def, THEN generalized_fw_joinD]
obtain rr fr where "generalized_sfw (lr_of_tran_s1 rt) p = Some (rr, oif) ∧
generalized_sfw (map simple_rule_dtor fw) p = Some (fr, simple_action.Drop) ∧ Some r = simple_match_and rr fr" by presburger
hence fd: "⋀u. simple_fw fw (p⦇p_oiface := u⦈) = Decision FinalDeny" unfolding ifupdateirrel
using simple_fw_iff_generalized_fw_drop by blast
show ?thesis
by(clarsimp simp: simple_linux_router_nol12_def Let_def fd split: Option.bind_splits)
qed

lemma lr_of_tran_fbs_dropI:
assumes s1: "valid_prefixes rt" "has_default_route rt"
assumes s2: "no_oif_match fw" "has_default_policy fw"
shows "simple_linux_router_nol12 rt fw p = None ⟹
∃r oif. generalized_sfw (lr_of_tran_fbs rt fw ifs) p = Some (r, oif, simple_action.Drop)"
proof(goal_cases)
from s2 have nud: "⋀p. simple_fw fw p ≠ Undecided" by (metis has_default_policy state.distinct(1))
note ifupdateirrel = no_oif_matchD[OF s2(1), symmetric]
case 1
from 1 have "simple_fw fw p = Decision FinalDeny" by(simp add: simple_linux_router_nol12_def Let_def nud ifupdateirrel split: Option.bind_splits state.splits final_decision.splits)
then obtain r where r: "generalized_sfw (map simple_rule_dtor fw) p = Some (r, simple_action.Drop)" using simple_fw_iff_generalized_fw_drop by blast
note s1_correct[OF s1, of p] then guess rm .. then guess ra .. note rmra = this
show ?case unfolding lr_of_tran_fbs_def Let_def
apply(rule exI)
apply(rule exI[where x = ra])
apply(rule generalized_fw_joinI)
using rmra apply simp
apply(rule r)
done
qed

lemma no_oif_match_fbs:
"no_oif_match fw ⟹ list_all (λm. oiface (fst (snd m)) = ifaceAny) (map (apfst of_nat) (annotate_rlen (lr_of_tran_fbs rt fw ifs)))"
proof(goal_cases)
case 1
have c: "⋀mr ar mf af f a. ⟦(mr, ar) ∈ set (lr_of_tran_s1 rt); (mf, af) ∈ simple_rule_dtor  set fw; simple_match_and mr mf = Some a⟧ ⟹ oiface a = ifaceAny"
proof(goal_cases)
case (1 mr ar mf af f a)
have "oiface mr = ifaceAny" using 1(1) unfolding lr_of_tran_s1_def route2match_def by(clarsimp simp add: Set.image_iff)
moreover have "oiface mf = ifaceAny" using 1(2) ‹no_oif_match fw› unfolding no_oif_match_def simple_rule_dtor_def[abs_def]
by(clarsimp simp: list_all_iff split: simple_rule.splits) fastforce
ultimately show ?case using 1(3) by(cases a; cases mr; cases mf) (simp add: iface_conjunct_ifaceAny split: option.splits)
qed
have la: "list_all (λm. oiface (fst m) = ifaceAny) (lr_of_tran_fbs rt fw ifs)"
unfolding lr_of_tran_fbs_def Let_def list_all_iff
apply(clarify)
apply(subst(asm) generalized_sfw_join_set)
apply(clarsimp)
using c by blast
thus ?case
proof(goal_cases)
case 1
have *: "(λm. oiface (fst (snd m)) = ifaceAny) = (λm. oiface (fst m) = ifaceAny) ∘ snd" unfolding comp_def ..
show ?case unfolding * list_all_map[symmetric] map_snd_apfst map_snd_annotate_rlen using la .
qed
qed

lemma lr_of_tran_correct:
fixes p :: "(32, 'a) simple_packet_ext_scheme"
assumes nerr: "lr_of_tran rt fw ifs = Inr oft"
and ippkt: "p_l2type p = 0x800"
and ifvld: "p_iiface p ∈ set ifs"
shows "OF_priority_match OF_match_fields_safe oft p = Action [Forward oif] ⟷ simple_linux_router_nol12 rt fw p = (Some (p⦇p_oiface := oif⦈))"
"OF_priority_match OF_match_fields_safe oft p = Action [] ⟷ simple_linux_router_nol12 rt fw p = None"
(* fun stuff: *)
"OF_priority_match OF_match_fields_safe oft p ≠ NoAction" "OF_priority_match OF_match_fields_safe oft p ≠ Undefined"
"OF_priority_match OF_match_fields_safe oft p = Action ls ⟶ length ls ≤ 1"
"∃ls. length ls ≤ 1 ∧ OF_priority_match OF_match_fields_safe oft p = Action ls"
proof -
have s1: "valid_prefixes rt" "has_default_route rt"
and s2: "has_default_policy fw" "simple_fw_valid fw" "no_oif_match fw"
and difs: "distinct ifs"
using nerr unfolding lr_of_tran_def by(simp_all split: if_splits)
have "no_oif_match fw" using nerr unfolding lr_of_tran_def by(simp split: if_splits)
note s2 = s2 this
have unsafe_safe_eq:
"OF_priority_match OF_match_fields_unsafe oft = OF_priority_match OF_match_fields_safe oft"
"OF_match_linear OF_match_fields_unsafe oft = OF_match_linear OF_match_fields_safe oft"
apply(subst OF_unsafe_safe_match3_eq; (rule lr_of_tran_prereqs s1 s2 nerr refl)+)
apply(subst OF_unsafe_safe_match_linear_eq; (rule lr_of_tran_prereqs s1 s2 nerr refl)+)
done
have lin: "OF_priority_match OF_match_fields_safe oft = OF_match_linear OF_match_fields_safe oft"
using OF_eq[OF lr_of_tran_no_overlaps lr_of_tran_sorted_descending, OF difs nerr[symmetric] nerr[symmetric]] unfolding fun_eq_iff unsafe_safe_eq by metis
let ?ard = "map (apfst of_nat) (annotate_rlen (lr_of_tran_fbs rt fw ifs))"
have oft_def: "oft = pack_OF_entries ifs ?ard" using nerr unfolding lr_of_tran_def Let_def by(simp split: if_splits)
have vld: "list_all simple_match_valid (map (fst ∘ snd) ?ard)"
unfolding fun_app_def map_map[symmetric] snd_apfst map_snd_apfst map_snd_annotate_rlen using simple_match_valid_fbs[OF s1(1) s2(2)] .
have *: "list_all (λm. oiface (fst (snd m)) = ifaceAny) ?ard" using no_oif_match_fbs[OF s2(3)] .
have not_undec: "⋀p. simple_fw fw p ≠ Undecided" by (metis has_default_policy s2(1) state.simps(3))
have w1_1: "⋀oif. OF_match_linear OF_match_fields_safe oft p = Action [Forward oif] ⟹ simple_linux_router_nol12 rt fw p = Some (p⦇p_oiface := oif⦈)
∧ oif = output_iface (routing_table_semantics rt (p_dst p))"
proof(intro conjI, goal_cases)
case (1 oif)
note s3_correct[OF vld ippkt ifvld(1) *, THEN iffD1, unfolded oft_def[symmetric], OF 1]
hence "∃r. generalized_sfw (map snd (map (apfst of_nat) (annotate_rlen (lr_of_tran_fbs rt fw ifs)))) p = Some (r, (oif, simple_action.Accept))"
by(clarsimp split: if_splits)
then obtain r where "generalized_sfw (lr_of_tran_fbs rt fw ifs) p = Some (r, (oif, simple_action.Accept))"
unfolding map_map comp_def snd_apfst map_snd_annotate_rlen by blast
thus ?case using lr_of_tran_fbs_acceptD[OF s1 s2(3)] by metis
thus "oif = output_iface (routing_table_semantics rt (p_dst p))"
by(cases p) (clarsimp simp: simple_linux_router_nol12_def Let_def not_undec split: Option.bind_splits state.splits final_decision.splits)
qed
have w1_2: "⋀oif. simple_linux_router_nol12 rt fw p = Some (p⦇p_oiface := oif⦈) ⟹ OF_match_linear OF_match_fields_safe oft p = Action [Forward oif]"
proof(goal_cases)
case (1 oif)
note lr_of_tran_fbs_acceptI[OF s1 s2(3) s2(1) this, of ifs] then guess r .. note r = this
hence "generalized_sfw (map snd (map (apfst of_nat) (annotate_rlen (lr_of_tran_fbs rt fw ifs)))) p = Some (r, (oif, simple_action.Accept))"
unfolding map_snd_apfst map_snd_annotate_rlen .
moreover note s3_correct[OF vld ippkt ifvld(1) *, THEN iffD2, unfolded oft_def[symmetric], of "[Forward oif]"]
ultimately show ?case by simp
qed
show w1: "⋀oif. (OF_priority_match OF_match_fields_safe oft p = Action [Forward oif]) = (simple_linux_router_nol12 rt fw p = Some (p⦇p_oiface := oif⦈))"
unfolding lin using w1_1 w1_2 by blast
show w2: "(OF_priority_match OF_match_fields_safe oft p = Action []) = (simple_linux_router_nol12 rt fw p = None)"
unfolding lin
proof(rule iffI, goal_cases)
case 1
note s3_correct[OF vld ippkt ifvld(1) *, THEN iffD1, unfolded oft_def[symmetric], OF 1]
then obtain r oif where roif: "generalized_sfw (lr_of_tran_fbs rt fw ifs) p = Some (r, oif, simple_action.Drop)"
unfolding map_snd_apfst map_snd_annotate_rlen by(clarsimp split: if_splits)
note lr_of_tran_fbs_dropD[OF s1 s2(3) this]
thus ?case .
next
case 2
note lr_of_tran_fbs_dropI[OF s1 s2(3) s2(1) this, of ifs] then
obtain r oif where "generalized_sfw (lr_of_tran_fbs rt fw ifs) p = Some (r, oif, simple_action.Drop)" by blast
hence "generalized_sfw (map snd (map (apfst of_nat) (annotate_rlen (lr_of_tran_fbs rt fw ifs)))) p = Some (r, oif, simple_action.Drop)"
unfolding map_snd_apfst map_snd_annotate_rlen .
moreover note s3_correct[OF vld ippkt ifvld(1) *, THEN iffD2, unfolded oft_def[symmetric], of "[]"]
ultimately show ?case by force
qed
have lr_determ: "⋀a. simple_linux_router_nol12 rt fw p = Some a ⟹ a = p⦇p_oiface := output_iface (routing_table_semantics rt (p_dst p))⦈"
by(clarsimp simp: simple_linux_router_nol12_def Let_def not_undec split: Option.bind_splits state.splits final_decision.splits)
show notno: "OF_priority_match OF_match_fields_safe oft p ≠ NoAction"
apply(cases "simple_linux_router_nol12 rt fw p")
using w2 apply(simp)
using w1[of "output_iface (routing_table_semantics rt (p_dst p))"] apply(simp)
apply(drule lr_determ)
apply(simp)
done
show notub: "OF_priority_match OF_match_fields_safe oft p ≠ Undefined" unfolding lin using OF_match_linear_ne_Undefined .
show notmult: "⋀ls. OF_priority_match OF_match_fields_safe oft p = Action ls ⟶ length ls ≤ 1"
apply(cases "simple_linux_router_nol12 rt fw p")
using w2 apply(simp)
using w1[of "output_iface (routing_table_semantics rt (p_dst p))"] apply(simp)
apply(drule lr_determ)
apply(clarsimp)
done
show "∃ls. length ls ≤ 1 ∧ OF_priority_match OF_match_fields_safe oft p = Action ls"
apply(cases "OF_priority_match OF_match_fields_safe oft p")
using notmult apply blast
using notno   apply blast
using notub   apply blast
done
qed

end


# Theory OF_conv_test

theory OF_conv_test
imports
Iptables_Semantics.Parser
Simple_Firewall.SimpleFw_toString
Routing.IpRoute_Parser
"../../LinuxRouter_OpenFlow_Translation"
"../../OpenFlow_Serialize"
begin

(*section‹Example: Simple Test for Translation to OpenFlow›*)

parse_iptables_save SQRL_fw="iptables-save"

term SQRL_fw
thm SQRL_fw_def
thm SQRL_fw_FORWARD_default_policy_def

value[code] "map (λ(c,rs). (c, map (quote_rewrite ∘ common_primitive_rule_toString) rs)) SQRL_fw"
definition "unfolded = unfold_ruleset_FORWARD SQRL_fw_FORWARD_default_policy (map_of_string_ipv4 SQRL_fw)"
lemma "map (quote_rewrite ∘ common_primitive_rule_toString) unfolded =
[''-p icmp -j ACCEPT'',
''-i s1-lan -p tcp -m tcp --spts [1024:65535] -m tcp --dpts [80] -j ACCEPT'',
''-i s1-wan -p tcp -m tcp --spts [80] -m tcp --dpts [1024:65535] -j ACCEPT'',
'' -j DROP'']" by eval

lemma "length unfolded = 4" by eval

value[code] "map (quote_rewrite ∘ common_primitive_rule_toString) (upper_closure unfolded)"
lemma "length (upper_closure unfolded) = 4" by eval

value[code] "upper_closure (packet_assume_new unfolded)"

lemma "length (lower_closure unfolded) = 4" by eval

lemma "check_simple_fw_preconditions (upper_closure unfolded) = True" by eval
lemma "∀m ∈ get_matchset (upper_closure (packet_assume_new unfolded)). normalized_nnf_match m" by eval
lemma "∀m ∈ get_matchset (optimize_matches abstract_for_simple_firewall (upper_closure (packet_assume_new unfolded))). normalized_nnf_match m" by eval
lemma "check_simple_fw_preconditions (upper_closure (optimize_matches abstract_for_simple_firewall (upper_closure (packet_assume_new unfolded))))" by eval
lemma "length (to_simple_firewall (upper_closure (packet_assume_new unfolded))) = 4" by eval

lemma "(lower_closure (optimize_matches abstract_for_simple_firewall (lower_closure (packet_assume_new unfolded)))) = lower_closure unfolded"
"lower_closure unfolded = upper_closure unfolded"
"(upper_closure (optimize_matches abstract_for_simple_firewall (upper_closure (packet_assume_new unfolded)))) = upper_closure unfolded" by eval+

value[code] "(getParts (to_simple_firewall (lower_closure (optimize_matches abstract_for_simple_firewall (lower_closure (packet_assume_new unfolded))))))"

definition "SQRL_fw_simple ≡ remdups_rev (to_simple_firewall (upper_closure (optimize_matches abstract_for_simple_firewall (upper_closure (packet_assume_new unfolded)))))"
value[code] "SQRL_fw_simple"
lemma "simple_fw_valid SQRL_fw_simple" by eval

(*section‹Example: SQRL RTBL›*)

parse_ip_route SQRL_rtbl_main = "ip-route"
value SQRL_rtbl_main
lemma "SQRL_rtbl_main = [⦇routing_match = PrefixMatch 0xA000100 24, metric = 0, routing_action = ⦇output_iface = ''s1-lan'', next_hop = None⦈⦈,
⦇routing_match = PrefixMatch 0xA000200 24, metric = 0, routing_action = ⦇output_iface = ''s1-wan'', next_hop = None⦈⦈,
⦇routing_match = PrefixMatch 0 0, metric = 0, routing_action = ⦇output_iface = ''s1-wan'', next_hop = Some 0xA000201⦈⦈]" by eval
lemma "SQRL_rtbl_main = [
rr_ctor (10,0,1,0) 24 ''s1-lan'' None 0,
rr_ctor (10,0,2,0) 24 ''s1-wan'' None 0,
rr_ctor (0,0,0,0) 0 ''s1-wan'' (Some (10,0,2,1)) 0
]"
by eval

definition "SQRL_rtbl_main_sorted ≡ rev (sort_key (λr. pfxm_length (routing_match r)) SQRL_rtbl_main)"
value SQRL_rtbl_main_sorted
definition "SQRL_ifs ≡ [
⦇iface_name = ''s1-lan'', iface_mac = 0x10001⦈,
⦇iface_name = ''s1-wan'', iface_mac = 0x10002⦈
]"
value SQRL_ifs

definition "SQRL_macs ≡ [
]"

definition "SQRL_ports ≡ [
(''s1-lan'', ''1''),
(''s1-wan'', ''2'')
]"

(* preconditions (get checked by lr_of_tran, too) *)
lemma "let fw = SQRL_fw_simple in no_oif_match fw ∧ has_default_policy fw ∧ simple_fw_valid fw" by eval
lemma "let rt = SQRL_rtbl_main_sorted in valid_prefixes rt ∧ has_default_route rt" by eval
lemma "let ifs = (map iface_name SQRL_ifs) in distinct ifs" by eval

definition "ofi ≡
case (lr_of_tran SQRL_rtbl_main_sorted SQRL_fw_simple (map iface_name SQRL_ifs))
of (Inr openflow_rules) ⇒ map (serialize_of_entry (the ∘ map_of SQRL_ports)) openflow_rules"
lemma "ofi =
[''priority=11,hard_timeout=0,idle_timeout=0,dl_type=0x800,nw_proto=1,nw_dst=10.0.2.0/24,action=output:2'',
''priority=10,hard_timeout=0,idle_timeout=0,in_port=1,dl_type=0x800,nw_proto=6,nw_dst=10.0.2.0/24,tp_src=1024/0xfc00,tp_dst=80,action=output:2'',
''priority=10,hard_timeout=0,idle_timeout=0,in_port=1,dl_type=0x800,nw_proto=6,nw_dst=10.0.2.0/24,tp_src=2048/0xf800,tp_dst=80,action=output:2'',
''priority=10,hard_timeout=0,idle_timeout=0,in_port=1,dl_type=0x800,nw_proto=6,nw_dst=10.0.2.0/24,tp_src=4096/0xf000,tp_dst=80,action=output:2'',
''priority=10,hard_timeout=0,idle_timeout=0,in_port=1,dl_type=0x800,nw_proto=6,nw_dst=10.0.2.0/24,tp_src=8192/0xe000,tp_dst=80,action=output:2'',
''priority=10,hard_timeout=0,idle_timeout=0,in_port=1,dl_type=0x800,nw_proto=6,nw_dst=10.0.2.0/24,tp_src=16384/0xc000,tp_dst=80,action=output:2'',
''priority=10,hard_timeout=0,idle_timeout=0,in_port=1,dl_type=0x800,nw_proto=6,nw_dst=10.0.2.0/24,tp_src=32768/0x8000,tp_dst=80,action=output:2'',
''priority=9,hard_timeout=0,idle_timeout=0,in_port=2,dl_type=0x800,nw_proto=6,nw_dst=10.0.2.0/24,tp_src=80,tp_dst=1024/0xfc00,action=output:2'',
''priority=9,hard_timeout=0,idle_timeout=0,in_port=2,dl_type=0x800,nw_proto=6,nw_dst=10.0.2.0/24,tp_src=80,tp_dst=2048/0xf800,action=output:2'',
''priority=9,hard_timeout=0,idle_timeout=0,in_port=2,dl_type=0x800,nw_proto=6,nw_dst=10.0.2.0/24,tp_src=80,tp_dst=4096/0xf000,action=output:2'',
''priority=9,hard_timeout=0,idle_timeout=0,in_port=2,dl_type=0x800,nw_proto=6,nw_dst=10.0.2.0/24,tp_src=80,tp_dst=8192/0xe000,action=output:2'',
''priority=9,hard_timeout=0,idle_timeout=0,in_port=2,dl_type=0x800,nw_proto=6,nw_dst=10.0.2.0/24,tp_src=80,tp_dst=16384/0xc000,action=output:2'',
''priority=9,hard_timeout=0,idle_timeout=0,in_port=2,dl_type=0x800,nw_proto=6,nw_dst=10.0.2.0/24,tp_src=80,tp_dst=32768/0x8000,action=output:2'',
''priority=8,hard_timeout=0,idle_timeout=0,dl_type=0x800,nw_dst=10.0.2.0/24,action=drop'',
''priority=7,hard_timeout=0,idle_timeout=0,dl_type=0x800,nw_proto=1,nw_dst=10.0.1.0/24,action=output:1'',
''priority=6,hard_timeout=0,idle_timeout=0,in_port=1,dl_type=0x800,nw_proto=6,nw_dst=10.0.1.0/24,tp_src=1024/0xfc00,tp_dst=80,action=output:1'',
''priority=6,hard_timeout=0,idle_timeout=0,in_port=1,dl_type=0x800,nw_proto=6,nw_dst=10.0.1.0/24,tp_src=2048/0xf800,tp_dst=80,action=output:1'',
''priority=6,hard_timeout=0,idle_timeout=0,in_port=1,dl_type=0x800,nw_proto=6,nw_dst=10.0.1.0/24,tp_src=4096/0xf000,tp_dst=80,action=output:1'',
''priority=6,hard_timeout=0,idle_timeout=0,in_port=1,dl_type=0x800,nw_proto=6,nw_dst=10.0.1.0/24,tp_src=8192/0xe000,tp_dst=80,action=output:1'',
''priority=6,hard_timeout=0,idle_timeout=0,in_port=1,dl_type=0x800,nw_proto=6,nw_dst=10.0.1.0/24,tp_src=16384/0xc000,tp_dst=80,action=output:1'',
''priority=6,hard_timeout=0,idle_timeout=0,in_port=1,dl_type=0x800,nw_proto=6,nw_dst=10.0.1.0/24,tp_src=32768/0x8000,tp_dst=80,action=output:1'',
''priority=5,hard_timeout=0,idle_timeout=0,in_port=2,dl_type=0x800,nw_proto=6,nw_dst=10.0.1.0/24,tp_src=80,tp_dst=1024/0xfc00,action=output:1'',
''priority=5,hard_timeout=0,idle_timeout=0,in_port=2,dl_type=0x800,nw_proto=6,nw_dst=10.0.1.0/24,tp_src=80,tp_dst=2048/0xf800,action=output:1'',
''priority=5,hard_timeout=0,idle_timeout=0,in_port=2,dl_type=0x800,nw_proto=6,nw_dst=10.0.1.0/24,tp_src=80,tp_dst=4096/0xf000,action=output:1'',
''priority=5,hard_timeout=0,idle_timeout=0,in_port=2,dl_type=0x800,nw_proto=6,nw_dst=10.0.1.0/24,tp_src=80,tp_dst=8192/0xe000,action=output:1'',
''priority=5,hard_timeout=0,idle_timeout=0,in_port=2,dl_type=0x800,nw_proto=6,nw_dst=10.0.1.0/24,tp_src=80,tp_dst=16384/0xc000,action=output:1'',
''priority=5,hard_timeout=0,idle_timeout=0,in_port=2,dl_type=0x800,nw_proto=6,nw_dst=10.0.1.0/24,tp_src=80,tp_dst=32768/0x8000,action=output:1'',
''priority=4,hard_timeout=0,idle_timeout=0,dl_type=0x800,nw_dst=10.0.1.0/24,action=drop'',
''priority=3,hard_timeout=0,idle_timeout=0,dl_type=0x800,nw_proto=1,action=output:2'',
''priority=2,hard_timeout=0,idle_timeout=0,in_port=1,dl_type=0x800,nw_proto=6,tp_src=1024/0xfc00,tp_dst=80,action=output:2'',
''priority=2,hard_timeout=0,idle_timeout=0,in_port=1,dl_type=0x800,nw_proto=6,tp_src=2048/0xf800,tp_dst=80,action=output:2'',
''priority=2,hard_timeout=0,idle_timeout=0,in_port=1,dl_type=0x800,nw_proto=6,tp_src=4096/0xf000,tp_dst=80,action=output:2'',
''priority=2,hard_timeout=0,idle_timeout=0,in_port=1,dl_type=0x800,nw_proto=6,tp_src=8192/0xe000,tp_dst=80,action=output:2'',
''priority=2,hard_timeout=0,idle_timeout=0,in_port=1,dl_type=0x800,nw_proto=6,tp_src=16384/0xc000,tp_dst=80,action=output:2'',
''priority=2,hard_timeout=0,idle_timeout=0,in_port=1,dl_type=0x800,nw_proto=6,tp_src=32768/0x8000,tp_dst=80,action=output:2'',
''priority=1,hard_timeout=0,idle_timeout=0,in_port=2,dl_type=0x800,nw_proto=6,tp_src=80,tp_dst=1024/0xfc00,action=output:2'',
''priority=1,hard_timeout=0,idle_timeout=0,in_port=2,dl_type=0x800,nw_proto=6,tp_src=80,tp_dst=2048/0xf800,action=output:2'',
''priority=1,hard_timeout=0,idle_timeout=0,in_port=2,dl_type=0x800,nw_proto=6,tp_src=80,tp_dst=4096/0xf000,action=output:2'',
''priority=1,hard_timeout=0,idle_timeout=0,in_port=2,dl_type=0x800,nw_proto=6,tp_src=80,tp_dst=8192/0xe000,action=output:2'',
''priority=1,hard_timeout=0,idle_timeout=0,in_port=2,dl_type=0x800,nw_proto=6,tp_src=80,tp_dst=16384/0xc000,action=output:2'',
''priority=1,hard_timeout=0,idle_timeout=0,in_port=2,dl_type=0x800,nw_proto=6,tp_src=80,tp_dst=32768/0x8000,action=output:2'',
''priority=0,hard_timeout=0,idle_timeout=0,dl_type=0x800,action=drop'']" by eval

value[code] "ofi"

(*ML‹
val evterm = the (Code_Evaluation.dynamic_value @{context} @{term "intersperse (Char Nibble0 NibbleA) ofi"});
val opstr = Syntax.string_of_term (Config.put show_markup false @{context}) evterm;
File.write (Path.explode (File.platform_path(Resources.master_directory @{theory}) ^ "/pretty_str.txt")) opstr;
›*)

end


# Theory RFC2544

theory RFC2544
imports
Iptables_Semantics.Parser
Routing.IpRoute_Parser
"../../LinuxRouter_OpenFlow_Translation"
"../../OpenFlow_Serialize"
begin

(*section‹Example: Simple Test for Translation to OpenFlow›*)

parse_iptables_save SQRL_fw="iptables-save"

term SQRL_fw
thm SQRL_fw_def
thm SQRL_fw_FORWARD_default_policy_def

value[code] "map (λ(c,rs). (c, map (quote_rewrite ∘ common_primitive_rule_toString) rs)) SQRL_fw"
definition "unfolded = unfold_ruleset_FORWARD SQRL_fw_FORWARD_default_policy (map_of_string_ipv4 SQRL_fw)"

lemma "length unfolded = 26" by eval

value[code] "unfolded"
value[code] "(upper_closure unfolded)"
value[code] "map (quote_rewrite ∘ common_primitive_rule_toString) (upper_closure unfolded)"
lemma "length (upper_closure unfolded) = 26" by eval

value[code] "upper_closure (packet_assume_new unfolded)"

lemma "length (lower_closure unfolded) = 26" by eval

lemma "check_simple_fw_preconditions (upper_closure unfolded)" by eval
lemma "∀m ∈ get_matchset (upper_closure (packet_assume_new unfolded)). normalized_nnf_match m" by eval
lemma "∀m ∈ get_matchset (optimize_matches abstract_for_simple_firewall (upper_closure (packet_assume_new unfolded))). normalized_nnf_match m" by eval
lemma "check_simple_fw_preconditions (upper_closure (optimize_matches abstract_for_simple_firewall (upper_closure (packet_assume_new unfolded))))" by eval
lemma "length (to_simple_firewall (upper_closure (packet_assume_new unfolded))) = 26" by eval

lemma "(lower_closure (optimize_matches abstract_for_simple_firewall (lower_closure (packet_assume_new unfolded)))) = lower_closure unfolded"
"lower_closure unfolded = upper_closure unfolded"
"(upper_closure (optimize_matches abstract_for_simple_firewall (upper_closure (packet_assume_new unfolded)))) = upper_closure unfolded" by eval+

value[code] "(getParts (to_simple_firewall (lower_closure (optimize_matches abstract_for_simple_firewall (lower_closure (packet_assume_new unfolded))))))"

definition "SQRL_fw_simple ≡ remdups_rev (to_simple_firewall (upper_closure (optimize_matches abstract_for_simple_firewall (upper_closure (packet_assume_new unfolded)))))"
value[code] "SQRL_fw_simple"
lemma "simple_fw_valid SQRL_fw_simple" by eval

parse_ip_route SQRL_rtbl_main = "ip-route"
value SQRL_rtbl_main
lemma "SQRL_rtbl_main = [⦇routing_match = PrefixMatch 0xC6120100 24, metric = 0, routing_action = ⦇output_iface = ''ip1'', next_hop = None⦈⦈,
⦇routing_match = PrefixMatch 0xC6130100 24, metric = 0, routing_action = ⦇output_iface = ''op1'', next_hop = None⦈⦈,
⦇routing_match = PrefixMatch 0 0, metric = 0, routing_action = ⦇output_iface = ''op1'', next_hop = Some 0xC6130102⦈⦈]" by eval
lemma "SQRL_rtbl_main = [
rr_ctor (198,18,1,0) 24 ''ip1'' None 0,
rr_ctor (198,19,1,0) 24 ''op1'' None 0,
rr_ctor (0,0,0,0) 0 ''op1'' (Some (198,19,1,2)) 0
]"
by eval

definition "SQRL_ports ≡ [
(''ip1'', ''1''),
(''op1'', ''2'')
]"

definition "ofi ≡
case (lr_of_tran SQRL_rtbl_main SQRL_fw_simple (map fst SQRL_ports))
of (Inr openflow_rules) ⇒ map (serialize_of_entry (the ∘ map_of SQRL_ports)) openflow_rules"
lemma "ofi =
[''priority=27,hard_timeout=0,idle_timeout=0,dl_type=0x800,nw_dst=198.18.1.0/24,action=drop'',
''priority=26,hard_timeout=0,idle_timeout=0,dl_type=0x800,nw_dst=198.19.1.0/24,action=drop'',
''priority=25,hard_timeout=0,idle_timeout=0,dl_type=0x800,nw_src=192.18.1.1/32,nw_dst=192.18.101.1/32,action=drop'',
''priority=24,hard_timeout=0,idle_timeout=0,dl_type=0x800,nw_src=192.18.2.2/32,nw_dst=192.18.102.2/32,action=drop'',
''priority=23,hard_timeout=0,idle_timeout=0,dl_type=0x800,nw_src=192.18.3.3/32,nw_dst=192.18.103.3/32,action=drop'',
''priority=22,hard_timeout=0,idle_timeout=0,dl_type=0x800,nw_src=192.18.4.4/32,nw_dst=192.18.104.4/32,action=drop'',
''priority=21,hard_timeout=0,idle_timeout=0,dl_type=0x800,nw_src=192.18.5.5/32,nw_dst=192.18.105.5/32,action=drop'',
''priority=20,hard_timeout=0,idle_timeout=0,dl_type=0x800,nw_src=192.18.6.6/32,nw_dst=192.18.106.6/32,action=drop'',
''priority=19,hard_timeout=0,idle_timeout=0,dl_type=0x800,nw_src=192.18.7.7/32,nw_dst=192.18.107.7/32,action=drop'',
''priority=18,hard_timeout=0,idle_timeout=0,dl_type=0x800,nw_src=192.18.8.8/32,nw_dst=192.18.108.8/32,action=drop'',
''priority=17,hard_timeout=0,idle_timeout=0,dl_type=0x800,nw_src=192.18.9.9/32,nw_dst=192.18.109.9/32,action=drop'',
''priority=16,hard_timeout=0,idle_timeout=0,dl_type=0x800,nw_src=192.18.10.10/32,nw_dst=192.18.110.10/32,action=drop'',
''priority=15,hard_timeout=0,idle_timeout=0,dl_type=0x800,nw_src=192.18.11.11/32,nw_dst=192.18.111.11/32,action=drop'',
''priority=14,hard_timeout=0,idle_timeout=0,dl_type=0x800,nw_src=192.18.12.12/32,nw_dst=192.18.112.12/32,action=drop'',
''priority=13,hard_timeout=0,idle_timeout=0,dl_type=0x800,nw_src=192.19.1.2/32,nw_dst=192.19.65.1/32,action=output:2'',
''priority=12,hard_timeout=0,idle_timeout=0,dl_type=0x800,nw_src=192.18.13.13/32,nw_dst=192.18.113.13/32,action=drop'',
''priority=11,hard_timeout=0,idle_timeout=0,dl_type=0x800,nw_src=192.18.14.14/32,nw_dst=192.18.114.14/32,action=drop'',
''priority=10,hard_timeout=0,idle_timeout=0,dl_type=0x800,nw_src=192.18.15.15/32,nw_dst=192.18.115.15/32,action=drop'',
''priority=9,hard_timeout=0,idle_timeout=0,dl_type=0x800,nw_src=192.18.16.16/32,nw_dst=192.18.116.16/32,action=drop'',
''priority=8,hard_timeout=0,idle_timeout=0,dl_type=0x800,nw_src=192.18.17.17/32,nw_dst=192.18.117.17/32,action=drop'',
''priority=7,hard_timeout=0,idle_timeout=0,dl_type=0x800,nw_src=192.18.18.18/32,nw_dst=192.18.118.18/32,action=drop'',
''priority=6,hard_timeout=0,idle_timeout=0,dl_type=0x800,nw_src=192.18.19.19/32,nw_dst=192.18.119.19/32,action=drop'',
''priority=5,hard_timeout=0,idle_timeout=0,dl_type=0x800,nw_src=192.18.20.20/32,nw_dst=192.18.120.20/32,action=drop'',
''priority=4,hard_timeout=0,idle_timeout=0,dl_type=0x800,nw_src=192.18.21.21/32,nw_dst=192.18.121.21/32,action=drop'',
''priority=3,hard_timeout=0,idle_timeout=0,dl_type=0x800,nw_src=192.18.22.22/32,nw_dst=192.18.122.22/32,action=drop'',
''priority=2,hard_timeout=0,idle_timeout=0,dl_type=0x800,nw_src=192.18.23.23/32,nw_dst=192.18.123.23/32,action=drop'',
''priority=1,hard_timeout=0,idle_timeout=0,dl_type=0x800,nw_src=192.18.24.24/32,nw_dst=192.18.124.24/32,action=drop'',
''priority=0,hard_timeout=0,idle_timeout=0,dl_type=0x800,action=drop'']" by eval
value[code] "length ofi"

(* TODO: Well, that's something… I'd really like to have a proper file with newlines though… *)
(*ML‹
val evterm = the (Code_Evaluation.dynamic_value @{context} @{term "intersperse (Char Nibble0 NibbleA) ofi"});
val opstr = Syntax.string_of_term (Config.put show_markup false @{context}) evterm;
File.write (Path.explode (File.platform_path(Resources.master_directory @{theory}) ^ "/pretty_str.txt")) opstr;
›*)

end


# Theory OpenFlow_Documentation

text_raw‹
\twocolumn
\columnsep 2pc          %    Space between columns
\textwidth 42pc         % Width of text line.
\part{Documentation}
\label{part2}
›
section‹Configuration Translation›
text_raw‹\label{sec:conv}›
text‹
All the results we present in this section are formalized and verified in Isabelle/HOL~\cite{nipkow2002isabelle}.
This means that their formal correctness can be trusted a level close to absolute certainty.
The definitions and lemmas stated here are merely a repetition of lemmas stated in other theory files.
This means that they have been directly set to this document from Isabelle and no typos or hidden assumptions are possible.
Additionally, it allows us to omit various helper lemmas that do not help the understanding.
However, it causes some notation inaccuracy, as type and function definitions are stated as lemmas or schematic goals.
›
theory OpenFlow_Documentation
(*<*)
imports
LinuxRouter_OpenFlow_Translation
Featherweight_OpenFlow_Comparison
"HOL-Library.LaTeXsugar"
begin
(*>*)

subsection‹Linux Firewall Model›
text_raw‹\label{sec:lfw}›
text‹We want to write a program that translates the configuration of a linux firewall to that of an OpenFlow switch.
We furthermore want to verify that translation.
For this purpose, we need a clear definition of the behavior of the two device types -- we need their models and semantics.
In case of a linux firewall, this is problematic because a linux firewall is a highly complex device that is ultimately capable of general purpose computation.
Creating a comprehensive semantics that encompasses all possible configuration types of a linux firewall is thus
highly non-trivial and not useful for the purpose of analysis.
We decided to approach the problem from the other side: we created a model that includes only the most basic features. (This implies neglecting IPv6.)
Fortunately, many of the highly complex features are rarely essential and even our basic model is still of some use.
›

text‹We first divided the firewall into subsystems.
Given a routing table @{term rt}, the firewall rules @{term fw},
the routing decision for a packet @{term p} can be obtained by @{term "routing_table_semantics rt (p_dst p)"},
the firewall decision by @{term "simple_fw fw p"}.
We draft the first description of our linux router model:
\begin{enumerate}
\item The destination MAC address of an arriving packet is checked: Does it match the MAC address of the ingress port?
If it does, we continue, otherwise, the packet is discarded.
\item The routing decision @{term "rd ≡ routing_table_semantics rt p"} is obtained.
\item The packet's output interface is updated based on @{term rd}\footnote{Note that we assume a packet model with input and output interfaces. The origin of this is explained in Section~\ref{sec:lfwfw}}.
\item The firewall is queried for a decision: @{term "simple_fw fw p"}. If the decision is to @{const[names_short] simple_action.Drop}, the packet is discarded.
\item The next hop is computed: If @{term rd} provides a next hop, that is used.
Otherwise, the destination address of the packet is used.
\item The MAC address of the next hop is looked up; the packet is updated with it and sent.
\end{enumerate}
We decided that this description is best formalized as an abortable program in the option monad:›
lemma "simple_linux_router rt fw mlf ifl p ≡ do {
_ ← iface_packet_check ifl p;
let rd ― ‹(routing decision)› = routing_table_semantics rt (p_dst p);
let p = p⦇p_oiface := output_iface rd⦈;
let fd ― ‹(firewall decision)› = simple_fw fw p;
_ ← (case fd of Decision FinalAllow ⇒ Some () | Decision FinalDeny ⇒ None);
let nh = (case next_hop rd of None ⇒ p_dst p | Some a ⇒ a);
ma ← mlf nh;
Some (p⦇p_l2dst := ma⦈)
}"
unfolding fromMaybe_def[symmetric] by(fact simple_linux_router_def)
text‹where @{term "mlf :: ipv4addr ⇒ 48 word"} is a function that looks up the MAC address for an IP address.›

text‹There are already a few important aspects that have not been modelled, but they are not core essential for the functionality of a firewall.
Namely, there is no local traffic from/to the firewall.
This is problematic since this model can not generate ARP replies --- thus, an equivalent OpenFlow device will not do so, either.
Furthermore, this model is problematic because it requires access to a function that looks up a MAC address,
something that may not be known at the time of time running a translation to an OpenFlow configuration.
›
text‹It is possible to circumvent these problems by inserting static ARP table entries in the directly connected devices
and looking up their MAC addresses \emph{a priori}.
A test-wise implementation of the translation based on this model showed acceptable results.
However, we deemed the \emph{a priori} lookup of the MAC addresses to be rather inelegant and built a second model.›
definition "simple_linux_router_altered rt fw ifl p ≡ do {
let rd = routing_table_semantics rt (p_dst p);
let p = p⦇p_oiface := output_iface rd⦈;
_ ← if p_oiface p = p_iiface p then None else Some ();
let fd = simple_fw fw p;
_ ← (case fd of Decision FinalAllow ⇒ Some () | Decision FinalDeny ⇒ None);
Some p
}"
(* TODO: Would a router actually forward a packet on the same interface? *)
text‹In this model, all access to the MAC layer has been eliminated.
This is done by the approximation that the firewall will be asked to route a packet
(i.e. be addressed on the MAC layer) iff the destination IP address of the packet causes it to be routed out on a different interface.
Because this model does not insert destination MAC addresses, the destination MAC address has to be already correct when the packet is sent.
This can only be achieved by changing the subnet of all connected device, moving them into one common subnet\footnote{There are cases where this is not possible --- A limitation of our system.}.
›
text‹
While a test-wise implementation based on this model also showed acceptable results, the model is still problematic.
The check @{term "p_oiface p = p_iiface p"} and the firewall require access to the output interface.
The details of why this cannot be provided are be elaborated in Section~\ref{sec:convi}.
The intuitive explanation is that an OpenFlow match can not have a field for the output interface.
We thus simplified the model even further:
›
lemma "simple_linux_router_nol12 rt fw p ≡ do {
let rd = routing_table_semantics rt (p_dst p);
let p = p⦇p_oiface := output_iface rd⦈;
let fd = simple_fw fw p;
_ ← (case fd of Decision FinalAllow ⇒ Some () | Decision FinalDeny ⇒ None);
Some p
}" by(fact simple_linux_router_nol12_def)
text‹We continue with this definition as a basis for our translation.
Even this strongly altered version and the original linux firewall still behave the same in a substantial amount of cases:›
theorem
"⟦iface_packet_check ifl pii ≠ None;
mlf (case next_hop (routing_table_semantics rt (p_dst pii)) of None ⇒ p_dst pii | Some a ⇒ a) ≠ None⟧ ⟹
∃x. map_option (λp. p⦇p_l2dst := x⦈) (simple_linux_router_nol12 rt fw pii) = simple_linux_router rt fw mlf ifl pii"
by(fact rtr_nomac_eq[unfolded fromMaybe_def])
text‹The conditions are to be read as The check whether a received packet has the correct destination MAC never returns @{const False}'' and
The next hop MAC address for all packets can be looked up''.
Obviously, these conditions do not hold for all packets.
We will show an example where this makes a difference in Section~\ref{sec:mnex}.›

subsubsection‹Routing Table›
text_raw‹\label{sec:lfwr}›
text‹
The routing system in linux features multiple tables and a system that can use the iptables firewall and an additional match language to select a routing table.
Based on our directive, we only focused on the single most used \texttt{main} routing table.›
text‹
We define a routing table entry to be a record (named tuple) of a prefix match, a metric and the routing action, which in turn is a record of an output interface and an optional next-hop address.›
schematic_goal "(?rtbl_entry :: ('a::len) routing_rule) = ⦇ routing_match = PrefixMatch pfx len, metric = met, routing_action = ⦇ output_iface = oif_string, next_hop = (h :: 'a word option) ⦈ ⦈" ..
text‹A routing table is then a list of these entries:›
lemma "(rtbl :: ('a :: len) prefix_routing) = (rtbl :: 'a routing_rule list)" by rule
text‹Not all members of the type @{type prefix_routing} are sane routing tables. There are three different validity criteria that we require so that our definitions are adequate.
\begin{itemize}
\item The prefixes have to be 0 in bits exceeding their length.
\item There has to be a default rule, i.e. one with prefix length 0. With the condition above, that implies that all its prefix bits are zero and it thus matches any address.
\item The entries have to be sorted by prefix length and metric.
\end{itemize}
The first two are set into code in the following way:
›
lemma "valid_prefix (PrefixMatch pfx len) ≡ pfx && (2 ^ (32 - len) - 1) = (0 :: 32 word)"
lemma "has_default_route rt ⟷ (∃r ∈ set rt. pfxm_length (routing_match r) = 0)"
by(fact has_default_route_alt)
text‹The third is not needed in any of the further proofs, so we omit it.›

text‹The semantics of a routing table is to simply traverse the list until a matching entry is found.›
schematic_goal "routing_table_semantics (rt_entry # rt) dst_addr = (if prefix_match_semantics (routing_match rt_entry) dst_addr then routing_action rt_entry else routing_table_semantics rt dst_addr)" by(fact routing_table_semantics.simps)
text‹If no matching entry is found, the behavior is undefined.›

subsubsection‹iptables Firewall›
text_raw‹\label{sec:lfwfw}›
text‹The firewall subsystem in a linux router is not any less complex than any of the of the other systems.
Fortunately, this complexity has been dealt with in~\cite{diekmann2016verified,Iptables_Semantics-AFP} already and we can directly use the result.›
text‹In short, one of the results is that a complex \emph{iptables} configuration can be simplified to be represented by a single list of matches that only support the following match conditions:
\begin{itemize}
\item (String) prefix matches on the input and output interfaces.
\item A @{type prefix_match} on the source and destination IP address.
\item An exact match on the layer 4 protocol.
\item Interval matches on the source or destination port, e.g. @{term "p⇩d ∈ {(1::16 word)..1023}"}
\end{itemize}
The model/type of the packet is adjusted to fit that: it is a record of the fields matched on.
This also means that input and output interface are coded to the packet.
Given that this information is usually stored alongside the packet content, this can be deemed a reasonable model.
In case the output interface is not needed (e.g., when evaluating an OpenFlow table), it can simply be left blank.

Obviously, a simplification into the above match type cannot always produce an equivalent firewall, and the set of accepted packets has to be over- or underapproximated.
The reader interested in the details of this is strongly referred to~\cite{diekmann2016verified}; we are simply going to continue with the result: @{const simple_fw}.
›
text‹One property of the simplification is worth noting here: The simplified firewall does not know state and the simplification approximates stateful matches by stateless ones.
Thus, the overapproximation of a stateful firewall ruleset that begins with accepting packets of established connections usually begins with a rule that accepts all packets.
Dealing with this by writing a meaningful simplification of stateful firewalls is future work.
›

subsection‹OpenFlow Switch Model›
text‹In this section, we present our model of an OpenFlow switch.
The requirements for this model are derived from the fact that it models devices that are the target of a configuration translation.
This has two implications:
\begin{itemize}
\item All configurations that are representable in our model should produce the correct behavior wrt. their semantics.
The problem is that correct here means that the behavior is the same that any real device would produce.
Since we cannot possibly account for all device types, we instead focus on those that conform to the OpenFlow specifications.
To account for the multiple different versions of the specification (e.g.~\cite{specification10,specification15}), we tried making our model a subset of
both the oldest stable version 1.0~\cite{specification10} and the newest available specification version 1.5.1~\cite{specification15}.
\item Conversely, our model does not need to represent all possible behavior of an OpenFlow switch, just the behavior that can be invoked by the result of our translation.
This is especially useful regarding for controller interaction, but also for MPLS or VLANs, which we did not model in Section \ref{sec:lfw}.
\end{itemize}›

text‹More concretely, we set the following rough outline for our model.
\begin{itemize}
\item A switch consists of a single flow table.
\item A flow table entry consists of a priority, a match condition and an action list.
\item The only possible action (we require) is to forward the packet on a port.
\item We do not model controller interaction.
\end{itemize}
Additionally, we decided that we wanted to be able to ensure the validity of the flow table in all qualities,
i.e. we want to model the conditions no overlapping flow entries appear', all match conditions have their necessary preconditions'.
The details of this are explained in the following sections.
›

subsubsection‹Matching Flow Table entries›
text_raw‹\label{sec:of_match}›
text‹Table 3 of Section 3.1 of \cite{specification10} gives a list of required packet fields that can be used to match packets.
This directly translates into the type for a match expression on a single field:›

schematic_goal "(field_match :: of_match_field) ∈ {
IngressPort (?s::string),
EtherSrc (?as::48 word), EtherDst (?ad::48 word),
EtherType (?t::16 word),
VlanId (?i::16 word), VlanPriority (?p::16 word),
IPv4Src (?pms::32 prefix_match),
IPv4Dst (?pmd::32 prefix_match),
IPv4Proto (?ipp :: 8 word),
L4Src (?ps :: 16 word) (?ms :: 16 word),
L4Dst (?pd :: 16 word) (?md :: 16 word)
}" by(fact of_match_field_typeset)
text‹
Two things are worth additional mention: L3 and L4 addressess''.
The @{term IPv4Src} and @{term IPv4Dst} matches are specified as can be subnet masked'' in~\cite{specification10},
whereras~\cite{specification15} states clearly that arbitrary bitmasks can be used. We took the conservative approach here.
Our alteration of @{term L4Src} and @{term L4Dst} is more grave. While~\cite{specification10} does not state anything about layer 4 ports and masks,
\cite{specification15} specifically forbids using masks on them.
Nevertheless, OpenVSwitch \cite{openvswitch} and some other implementations support them.
We will explain in detail why we must include bitmasks on layer 4 ports to obtain a meaningful translation in Section~\ref{sec:convi}.›

text‹One @{type of_match_field} is not enough to classify a packet.
To match packets, we thus use entire sets of match fields.
As Guha \emph{et al.}~\cite{guha2013machine} noted\footnote{See also: \cite[§2.3]{michaelis2016middlebox}}, executing a set of given @{type of_match_field}s on a packet requires careful consideration.
For example, it is not meaningful to use @{term IPv4Dst} if the given packet is not actually an IP packet, i.e.
@{term IPv4Dst} has the prerequisite of @{term "EtherType 0x0800"} being among the match fields.
Guha \emph{et al.} decided to use the fact that the preconditions can be arranged on a directed acyclic graph (or rather: an acyclic forest).
They evaluated match conditions in a manner following that graph:
first, all field matches without preconditions are evaluated.
Upon evaluating a field match (e.g., @{term "EtherType 0x0800"}), the matches that had their precondition fulfilled by it
(e.g., @{term IPv4Src} and @{term IPv4Src} in this example) are evalutated.
This mirrors the faulty behavior of some implementations (see \cite{guha2013machine}).
Adopting that behavior into our model would mean that any packet matches against the field match set @{term "{IPv4Dst (PrefixMatch 134744072 32)}"}
instead of just those destined for 8.8.8.8 or causing an error. We found this to be unsatisfactory.›

text‹To solve this problem, we made three definitions.
The first, @{term match_no_prereq} matches an @{type of_match_field} against a packet without considering prerequisites.
The second, @{term prerequisites}, checks for a given @{type of_match_field} whether its prerequisites are in a set of given match fields.
Especially:
›
lemma
"prerequisites (VlanPriority pri) m = (∃id. let v = VlanId id in v ∈ m ∧ prerequisites v m)"
"prerequisites (IPv4Proto pr) m = (let v = EtherType 0x0800 in v ∈ m ∧ prerequisites v m)"
"prerequisites (IPv4Src a) m = (let v = EtherType 0x0800 in v ∈ m ∧ prerequisites v m)"
"prerequisites (IPv4Dst a) m = (let v = EtherType 0x0800 in v ∈ m ∧ prerequisites v m)"
"prerequisites (L4Src p msk) m = (∃proto ∈ {TCP,UDP,L4_Protocol.SCTP}. let v = IPv4Proto proto in v ∈ m ∧ prerequisites v m)"
"prerequisites (L4Dst p msk) m = prerequisites (L4Src undefined undefined) m"
by(fact prerequisites.simps)+
text‹Then, to actually match a set of @{type of_match_field} against a packet, we use the option type:›
lemma "OF_match_fields m p =
(if ∃f ∈ m. ¬prerequisites f m then None else
if ∀f ∈ m. match_no_prereq f p then Some True else Some False)"
by(fact OF_match_fields_alt)

subsubsection‹Evaluating a Flow Table›
text‹In the previous section, we explained how we match the set of match fields belonging to a single flow entry against a packet.
This section explains how the correct flow entry from a table can be selected.
To prevent to much entanglement with the previous section, we assume an arbitrary match function @{term "γ :: 'match_field set ⇒ 'packet ⇒ bool"}.
This function @{term "γ"} takes the match condition @{term m} from a flow entry @{term "OFEntry (priority::16 word) (m::'match_field set) action"}
and decides whether a packet matches those.›

text‹The flow table is simply a list of flow table entries @{type flow_entry_match}.
Deciding the right flow entry to use for a given packet is explained in the OpenFlow specification \cite{specification10}, Section 3.4:
\begin{quote}
Packets are matched against flow entries based on prioritization.
An entry that specifies an exact match (i.e., has no wildcards) is always the highest priority\footnote{This behavior has been deprecated.}.
All wildcard entries have a priority associated with them.
Higher priority entries must match before lower priority ones.
If multiple entries have the same priority, the switch is free to choose any ordering.
\end{quote}
We use the term overlapping'' for  the flow entries that can cause a packet to match multiple flow entries with the same priority.
Guha \emph{et al.}~\cite{guha2013machine} have dealt with overlapping.
However, the semantics for a flow table they presented \cite[Figure 5]{guha2013machine}
is slightly different from what they actually used in their theory files.
We have tried to reproduce the original inductive definition (while keeping our abstraction @{term γ}),
in Isabelle/HOL\footnote{The original is written in Coq~\cite{barras1997coq} and we can not use it directly.}:›
lemma "γ (ofe_fields fe) p = True ⟹
∀fe' ∈ set (ft1 @ ft2). ofe_prio fe' > ofe_prio fe ⟶ γ (ofe_fields fe') p = False ⟹
guha_table_semantics γ (ft1 @ fe # ft2) p (Some (ofe_action fe))"
"∀fe ∈ set ft. γ (ofe_fields fe) p = False ⟹
guha_table_semantics γ ft p None" by(fact guha_matched guha_unmatched)+
text‹Guha \emph{et al.} have deliberately made their semantics non-deterministic, to match the fact that the switch may choose any ordering''.
This can lead to undesired results:›
lemma "CARD('action) ≥ 2 ⟹ ∃ff. γ ff p ⟹ ∃ft (a1 :: 'action) (a2 :: 'action). a1 ≠ a2 ∧ guha_table_semantics γ ft p (Some a1) ∧ guha_table_semantics γ ft p (Some a2)"
by(fact guha_table_semantics_ex2res)
text‹This means that, given at least two distinct actions exist and our matcher @{term γ} is not false for all possible match conditions,
we can say that a flow table and two actions exist such that both actions are executed. This can be misleading, as the switch might choose an
ordering on some flow table and never execute some of the (overlapped) actions.›

text‹Instead, we decided to follow Section 5.3 of the specification \cite{specification15}, which states:
\begin{quote}
If there are multiple matching flow entries, the selected flow entry is explicitly undefined.
\end{quote}
This still leaves some room for interpretation, but it clearly states that overlapping flow entries are undefined behavior,
and undefined behavior should not be invoked.
Thus, we came up with a semantics that clearly indicates when undefined behavior has been invoked:›
lemma
"OF_priority_match γ flow_entries packet = (
let m  = filter (λf. γ (ofe_fields f) packet) flow_entries;
m' = filter (λf. ∀fo ∈ set m. ofe_prio fo ≤ ofe_prio f) m in
case m' of []  ⇒ NoAction
| [s] ⇒ Action (ofe_action s)
|  _  ⇒ Undefined)"
unfolding OF_priority_match_def ..
text‹The definition works the following way\footnote{Note that the order of the flow table entries is irrelevant.
We could have made this definition on sets but chose not to for consistency.}:
\begin{enumerate}
\item The flow table is filtered for those entries that match, the result is called $m$.
\item $m$ is filtered again, leaving only those entries for which no entries with lower priority could be found, i.e. the matching flow table entries with minimal priority. The result is called $m'$.
\item A case distinction on $m'$ is made. If only one matching entry was found, its action is returned for execution.
If $m$ is empty, the flow table semantics returns @{term NoAction} to indicate that the flow table does not decide an action for the packet.
If,  not zero or one entry is found, but more, the special value @{term Undefined} for indicating undefined behavior is returned.
\end{enumerate}
The use of @{term Undefined} immediately raises the question in which condition it cannot occur.
We give the following definition:›
lemma "check_no_overlap γ ft = (∀a ∈ set ft. ∀b ∈ set ft. (a ≠ b ∧ ofe_prio a = ofe_prio b) ⟶ ¬(∃p. γ (ofe_fields a) p ∧ γ (ofe_fields b) p))" unfolding check_no_overlap_alt check_no_overlap2_def by force
text‹Together with distinctness of the flow table, this provides the abscence of @{term Undefined}\footnote{It is slightly stronger than necessary, overlapping rules might be shadowed and thus never influence the behavior.}:›
lemma "⟦check_no_overlap γ ft; distinct ft⟧ ⟹
OF_priority_match γ ft p ≠ Undefined" by (simp add: no_overlapsI no_overlaps_not_unefined)

text‹Given the absence of overlapping or duplicate flow entries, we can show two interesting equivalences.
the first is the equality to the semantics defined by Guha \emph{et al.}:›
lemma "⟦check_no_overlap γ ft; distinct ft⟧ ⟹
OF_priority_match γ ft p = option_to_ftb d ⟷ guha_table_semantics γ ft p d"
text‹where @{term option_to_ftb} maps between the return type of @{term OF_priority_match} and an option type as one would expect.›

text‹The second equality for @{term OF_priority_match} is one that helps reasoning about flow tables.
We define a simple recursive traversal for flow tables:›
lemma
"OF_match_linear γ [] p = NoAction"
"OF_match_linear γ (a#as) p = (if γ (ofe_fields a) p then Action (ofe_action a) else OF_match_linear γ as p)"
by(fact OF_match_linear.simps)+
text‹For this definition to be equivalent, we need the flow table to be sorted:›
lemma"
⟦no_overlaps γ f ;sorted_descending (map ofe_prio f)⟧ ⟹
OF_match_linear γ f p = OF_priority_match γ f p"
by(fact  OF_eq)

text‹As the last step, we implemented a serialization function for flow entries; it has to remain unverified.
The serialization function deals with one little inaccuracy: We have modelled the @{term IngressPort} match to use the interface name, but OpenFlow requires numerical interface IDs instead.
We deemed that pulling this translation step into the main translation would only make the correctness lemma of the translation more complicated while not increasing the confidence in the correctness significantly.
We thus made replacing interface names by their ID part of the serialization.
›

text‹Having collected all important definitions and models, we can move on to the conversion.›
(*text‹\todo{Maybe I should make a sweet little subsection that merges this all into a single model definition.}›*)

subsection‹Translation Implementation›
text_raw‹\label{sec:convi}›
text‹This section explains how the functions that are executed sequentially in a linux firewall can be compressed into a single OpenFlow table.
Creating this flow table in a single step would be immensely complicated.
We thus divided the task into several steps using the following key insights:
\begin{itemize}
\item All steps that are executed in the linux router can be formulated as a firewall, more specifically, a generalization of @{term simple_fw} that allows arbitrary actions instead of just accept and drop.
\item A function that computes the conjunction of two @{term simple_fw} matches is already present.
Extending this to a function that computes the join of two firewalls is relatively simple. This is explained in Section \ref{sec:fwconj}
\end{itemize}
›
subsubsection‹Chaining Firewalls›
text_raw‹\label{sec:fwconj}›
text‹This section explains how to compute the join of two firewalls.›
text‹The basis of this is a generalization of @{const simple_fw}.
Instead of only allowing @{const simple_action.Accept} or @{const simple_action.Drop} as actions, it allows arbitrary actions. The type of the function that evaluates this generalized simple firewall is
@{term "generalized_sfw :: ('i::len simple_match × 'a) list ⇒ ('i, 'b) simple_packet_scheme ⇒ ('i simple_match × 'a) option"}.
The definition is straightforward:›
lemma
"generalized_sfw [] p = None"
"generalized_sfw (a # as) p = (if (case a of (m,_) ⇒ simple_matches m p) then Some a else generalized_sfw as p)"
by(fact generalized_sfw_simps)+
text‹Based on that, we asked: if @{term fw⇩1} makes the decision @{term a} (where @{term a} is the second element of the result tuple from @{const generalized_sfw}) and @{term fw⇩2} makes the decision @{term b}, how can we compute the firewall that
makes the decision @{term "(a,b)"}\footnote{Note that tuples are right-associative in Isabelle/HOL, i.e., @{term "(a::'a,(b,c)::('b×'c))"} is a pair of @{term a} and the pair @{term "(b,c)"}}.
One possible answer is given by the following definition:
›
lemma "generalized_fw_join l1 l2 ≡ [(u,a,b). (m1,a) ← l1, (m2,b) ← l2, u ← (case simple_match_and m1 m2 of None ⇒ [] | Some s ⇒ [s])]"
by(fact generalized_fw_join_def[unfolded option2list_def])+
text‹This definition validates the following lemma:›
lemma "generalized_sfw (generalized_fw_join fw⇩1 fw⇩2) p = Some (u, d⇩1,d⇩2) ⟷ (∃r⇩1 r⇩2. generalized_sfw fw⇩1 p = Some (r⇩1,d⇩1) ∧ generalized_sfw fw⇩2 p = Some (r⇩2,d⇩2) ∧ Some u = simple_match_and r⇩1 r⇩2)"
by (auto dest: generalized_fw_joinD sym simp add: generalized_fw_joinI)
text‹Thus, @{const generalized_fw_join} has a number of applications.
For example, it could be used to compute a firewall ruleset that represents two firewalls that are executed in sequence.
›
definition "simple_action_conj a b ≡ (if a = simple_action.Accept ∧ b = simple_action.Accept then simple_action.Accept else simple_action.Drop)"
definition "simple_rule_conj ≡ (uncurry SimpleRule ∘ apsnd (uncurry simple_action_conj))"
theorem "simple_fw rs⇩1 p = Decision FinalAllow ∧ simple_fw rs⇩2 p = Decision FinalAllow ⟷
simple_fw (map simple_rule_conj (generalized_fw_join (map simple_rule_dtor rs⇩1) (map simple_rule_dtor rs⇩2))) p = Decision FinalAllow"
unfolding simple_rule_conj_def simple_action_conj_def[abs_def] using simple_fw_join by(force simp add: comp_def apsnd_def map_prod_def case_prod_unfold uncurry_def[abs_def])
text‹Using the join, it should be possible to compute any $n$-ary logical operation on firewalls.
We will use it for something somewhat different in the next section.›

subsubsection‹Translation Implementation›

text_raw‹
\begin{figure*}
\begin{framed}
›
lemma "lr_of_tran rt fw ifs ≡
if ¬ (no_oif_match fw ∧ has_default_policy fw ∧ simple_fw_valid fw	∧ valid_prefixes rt ∧ has_default_route rt ∧ distinct ifs)
then Inl ''Error in creating OpenFlow table: prerequisites not satisifed''
else (
let
nfw = map simple_rule_dtor fw;
frt = map (λr. (route2match r, output_iface (routing_action r))) rt;
nrd = generalized_fw_join frt nfw;
ard = (map (apfst of_nat) ∘ annotate_rlen) nrd
in
if length nrd < unat (max_word :: 16 word)
then Inr (pack_OF_entries ifs ard)
else Inl ''Error in creating OpenFlow table: priority number space exhausted''
)"
unfolding Let_def lr_of_tran_def lr_of_tran_fbs_def lr_of_tran_s1_def comp_def route2match_def by force

text_raw‹
\end{framed}
\caption{Function for translating a @{typ "'i::len simple_rule list"}, a @{typ "'i routing_rule list"}, and a list of interfaces to a flow table.}
\label{fig:convi}
\end{figure*}
›

text‹
This section shows the actual definition of the translation function, in Figure~\ref{fig:convi}.
Before beginning the translation, the definition checks whether the necessary preconditions are valid.
This first two steps are to convert @{term fw} and @{term rt} to lists that can be evaluated by @{const generalized_sfw}.
For @{term fw}, this is done by @{term "map simple_rule_dtor"}, which just deconstructs @{type simple_rule}s into tuples of match and action.
For @{term rt}, we made a firewall ruleset with rules that use prefix matches on the destination IP address.
The next step is to join the two rulesets.
The result of the join is a ruleset with rules @{term r} that only match if both, the corresponding firewall rule @{term fwr} and the corresponding routing rule @{term rr} matches.
The data accompanying @{term r} is the port from @{term rr} and the firewall decision from @{term fwr}.
Next, descending priorities are added to the rules using @{term "map (apfst word_of_nat) ∘ annotate_rlen"}.
If the number of rules is too large to fit into the $2^{16}$ priority classes, an error is returned.
Otherwise, the function @{const pack_OF_entries} is used to convert the @{typ "(16 word × 32 simple_match × char list × simple_action) list"} to an OpenFlow table.
While converting the @{typ "char list × simple_action"} tuple is straightforward, converting the @{type simple_match} to an equivalent list of @{typ "of_match_field set"} is non-trivial.
This is done by the function @{const simple_match_to_of_match}.
›
text‹The main difficulties for @{const simple_match_to_of_match} lie in making sure that the prerequisites are satisfied
and in the fact that a @{type simple_match} operates on slightly stronger match expressions.
\begin{itemize}
\item A @{type simple_match} allows a (string) prefix match on the input and output interfaces.
Given a list of existing interfaces on the router @{term ifs}, the function has to insert flow entries for each interface matching the prefix.
\item A @{type simple_match} can match ports by an interval. Now it becomes obvious why Section~\ref{sec:of_match} added bitmasks to @{const L4Src} and @{const L4Dst}.
Using the algorithm to split word intervals into intervals that can be represented by prefix matches from~\cite{diekmann2016verified},
we can efficiently represent the original interval by a few (32 in the worst case) prefix matches and insert flow entries for each of them.%
\footnote{It might be possible to represent the interval match more efficiently than a split into prefixes. However, that would produce overlapping matches (which is not a problem if we assing separate priorities)
and we did not have a verified implementation of an algorithm that does so.}
\end{itemize}
The following lemma characterizes @{const simple_match_to_of_match}:
›
lemma simple_match_to_of_match:
assumes
"simple_match_valid r"
"p_iiface p ∈ set ifs"
"match_iface (oiface r) (p_oiface p)"
"p_l2type p = 0x800"
shows
"simple_matches r p ⟷ (∃gr ∈ set (simple_match_to_of_match r ifs). OF_match_fields gr p = Some True)"
using assms simple_match_to_of_matchD simple_match_to_of_matchI by blast

text‹The assumptions are to be read as follows:
\begin{itemize}
\item The match @{term r} has to be valid, i.e. it has to use @{const valid_prefix} matches, and it cannot use anything other than $0$-$65535$ for the port matches unless its protocol match ensures @{const TCP}, @{const UDP} or @{const L4_Protocol.SCTP}.
\item @{const simple_match_to_of_match} cannot produce rules for packets that have input interfaces that are not named in the interface list.
\item The output interface of @{term p} has to match the output interface match of @{term r}. This is a weakened formulation of @{term "oiface r = ifaceAny"}, since @{thm[display] match_ifaceAny[no_vars]}.
We require this because OpenFlow field matches cannot be used to match on the output port --- they are supposed to match a packet and decide an output port.
\item The @{type simple_match} type was designed for IP(v4) packets, we limit ourselves to them.
\end{itemize}
The conclusion then states that the @{type simple_match} @{term r} matches iff an element of the result of @{const simple_match_to_of_match} matches.
The third assumption is part of the explanation why we did not use @{const simple_linux_router_altered}:
@{const simple_match_to_of_match} cannot deal with output interface matches.
Thus, before passing a generalized simple firewall to @{const pack_OF_entries}, we would have to set the output ports to @{const ifaceAny}.
A system replace output interface matches with destination IP addresses has already been formalized and will be published in a future version of \cite{Iptables_Semantics-AFP}.
For now, we limit ourselves to firewalls that do not do output port matching, i.e., we require @{term "no_oif_match fw"}.
›

text_raw‹\begin{figure*}
\begin{framed}
›
theorem
fixes
p :: "(32, 'a) simple_packet_ext_scheme"
assumes
"p_iiface p ∈ set ifs" and "p_l2type p = 0x800"
"lr_of_tran rt fw ifs = Inr oft"
shows
"OF_priority_match OF_match_fields_safe oft p = Action [Forward oif] ⟷ simple_linux_router_nol12 rt fw p = (Some (p⦇p_oiface := oif⦈))"
"OF_priority_match OF_match_fields_safe oft p = Action [] ⟷ simple_linux_router_nol12 rt fw p = None"
"OF_priority_match OF_match_fields_safe oft p ≠ NoAction" "OF_priority_match OF_match_fields_safe oft p ≠ Undefined"
"OF_priority_match OF_match_fields_safe oft p = Action ls ⟶ length ls ≤ 1"
"∃ls. length ls ≤ 1 ∧ OF_priority_match OF_match_fields_safe oft p = Action ls"
using assms lr_of_tran_correct by simp_all
text_raw‹
\end{framed}
\caption{Central theorem on @{const lr_of_tran}}
\label{fig:central}
\end{figure*}
›

text‹
Given discussed properties, we present the central theorem for our translation in Figure~\ref{fig:central}.
The first two assumptions are limitations on the traffic we make a statement about.
Obviously, we will never see any packets with an input interface that is not in the interface list.
Furthermore, we do not state anything about non-IPv4 traffic. (The traffic will remain unmatched in by the flow table, but we have not verified that.)
The last assumption is that the translation does not return a run-time error.
The translation will return a run-time error if the rules can not be assigned priorities from a 16 bit integer,
or when one of the following conditions on the input data is not satisifed:›
lemma "
¬ no_oif_match fw ∨
¬ has_default_policy fw ∨
¬ simple_fw_valid fw	∨
¬ valid_prefixes rt ∨
¬ has_default_route rt ∨
¬ distinct ifs ⟹
∃err. lr_of_tran rt fw ifs = Inl err" unfolding lr_of_tran_def by(simp split: if_splits)

subsubsection‹Comparison to Exodus›
text‹
We are not the first researchers to attempt automated static migration to SDN.
The (only) other attempt we are aware of is \emph{Exodus} by Nelson \emph{et al.}~\cite{nelson2015exodus}.
›
text‹
There are some fundamental differences between Exodus and our work:
\begin{itemize}
\item Exodus focuses on Cisco IOS instead of linux.
\item Exodus does not produce OpenFlow rulesets, but FlowLog~\cite{nelson2014tierless} controller programs.
\item Exodus is not limited to using a single flow table.
\item Exodus requires continuous controller interaction for some of its functions.
\item Exodus attempts to support as much functionality as possible and has implemented support for dynamic routing, VLANs and NAT.
\item Nelson \emph{et al.} reject the idea that the translation could or should be proven correct.
\end{itemize}
›

(*<*)
end
(*>*)