Session LOFT

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 "xset 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 "xset 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) = (aset 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  (yset xs. y  x)"
  by(induction xs) auto
  
  lemma sorted_descending_tail: "sorted_descending (xs@[x])  sorted_descending xs  (yset xs. x  y)"
  by(induction xs) auto
  
  lemma sorted_descending_append: "sorted_descending (xs @ ys) = 
    (sorted_descending xs  sorted_descending ys  (xset xs. yset ys. x  y))"
  by(induction xs) auto
  
  lemma sorted_descending: "sorted_descending (rev xs)  sorted xs"
  apply(induction xs)
   apply(simp)
  apply(auto simp add: sorted_descending_tail)
  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)"
    by(simp add: sort_descending_key_def sorted_descending)

  lemma sort_descending_key_distinct: "distinct xs  distinct (sort_descending_key f xs)"
    by(simp add: sort_descending_key_def)

  lemma sorted_descending_sort_descending_key: "sorted_descending (map f (sort_descending_key f xs))"
    apply(simp add: sort_descending_key_def)
    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" "(eset m. f a = f e)" "(eset n. f e < f a)" 
  				using True local.Cons by auto
  			have "a # as = a # m @ n" using mn(1) by simp
  			moreover have "eset (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  (eset m. f (hd (a # as)) = f e)  
  				(eset 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 "yset (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 "eset as. f e < f a" by simp
  			moreover have "a # as = [a] @ as  (eset [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"
  	by (simp add: sort_descending_key_def)
  	
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 )")
apply(simp_all add: le_imp_less_Suc length_dropWhile_le)
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 )")
apply(simp_all add: le_imp_less_Suc length_dropWhile_le)
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)
 by(simp_all add: id_def)

(*
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
imports IP_Addresses.Prefix_Match
        Simple_Firewall.Simple_Packet
        "HOL-Library.Monad_Syntax"
        (*"../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
  by(auto simp add: ball_Un)

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 (pp_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
  IP_Addresses.IPv4
  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›*)

(*https://www.opennetworking.org/images/stories/downloads/sdn-resources/onf-specifications/openflow/openflow-switch-v1.5.0.pdf*)

(*"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" "(foset ft. ofe_prio a < ofe_prio fo  ¬ γ (ofe_fields fo) p)" 
	               "b  set ft" "γ (ofe_fields b) p" "(foset 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  (eset 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  (foset (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  (foset (a # ft). ofe_prio f < ofe_prio fo  ¬ γ (ofe_fields fo) p)}"
		hence as: "x  set (a # ft)  γ (ofe_fields x) p  (foset (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 "(foset ft. ofe_prio x < ofe_prio fo  ¬ γ (ofe_fields fo) p)" by simp
		ultimately show "x  {f  set ft. γ (ofe_fields f) p  (foset 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  (foset ft. ofe_prio f < ofe_prio fo  ¬ γ (ofe_fields fo) p)}"
		hence as: "x  set ft" "γ (ofe_fields x) p" "(foset 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 "(foset (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  (foset (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" "eset m. ofe_prio a = ofe_prio e" "eset 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  
			(foset (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" 
				"(foset m. ofe_prio x < ofe_prio fo  ¬ γ (ofe_fields fo) p)"
				"(foset 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. (foset (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  (foset (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
qed (simp add: OF_same_priority_match2_def)

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)}
  	  )"
by(auto simp add: Let_def)
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
  	  )"
by(auto simp add: Let_def)

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: "[xs. 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
qed (simp add: check_no_overlap2_def)

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
qed (simp add: check_no_overlap2_def)

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 "¬ (pUNIV. γ (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 = [ffe . γ (ofe_fields f) p] in [fm . foset 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  eset 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
        IP_Addresses.Lib_Word_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]"
lemma "serialize_mac 0xdeadbeefcafe = ''de:ad:be:ef:ca:fe''" by eval

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''"
  by(simp add: serialize_actions_def)

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)))"
by (simp add: serialize_of_matches_def)

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] |
	   simp add: m)+
	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(simp add: guha_equal_Action[OF no])
	apply(simp add: guha_equal_NoAction[OF no])
	apply(subgoal_tac False, simp)
	apply(simp add: no no_overlaps_not_unefined)
done

lemma guha_deterministic1: "guha_table_semantics γ ft p (Some x1)  ¬ guha_table_semantics γ ft p None" 
by(auto simp add: guha_table_semantics.simps)

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:
	"fe1set ft" "x1 = ofe_action fe1" "γ (ofe_fields fe1) p" "(fe'set ft. ofe_prio fe1 < ofe_prio fe'  ¬ γ (ofe_fields fe') p)"
    "fe2set 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))
    apply(simp add: assms)
  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(clarsimp simp add: List.neq_Nil_conv)
    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
imports IP_Addresses.CIDR_Split
  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"
src :: "(ipv4addr × nat) " --"source IP address"
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_src :: ipv4addr
p_dst :: ipv4addr
p_proto :: primitive_protocol
p_sport :: "16 word"
p_dport :: "16 word"
p_tcp_flags :: "tcp_flag set"
p_payload :: string
*)

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 
	   simp add: toprefixmatch_def ipset_from_cidr_def pfxm_mask_def fun_eq_iff
	            prefix_match_semantics_ipset_from_netmask[OF vld] NOT_mask_shifted_lenword[symmetric]
	   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"
by(cases "(src r)") (simp add: prefix_match_semantics_ipset_from_netmask2 prefix_to_wordset_ipset_from_cidr simple_match_valid_def valid_prefix_fw_def)
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"
by(cases "(dst r)") (simp add: prefix_match_semantics_ipset_from_netmask2 prefix_to_wordset_ipset_from_cidr simple_match_valid_def valid_prefix_fw_def)

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
					apply(simp add: pfxm_mask_def prefix_match_dtor_def Set.image_iff 
					           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
					apply(simp add: pfxm_mask_def prefix_match_dtor_def Set.image_iff 
					           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"
        by(clarsimp simp: prefix_match_semantics_def pfxm_mask_def word_bw_comms;fail)
      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"
        by(clarsimp simp: prefix_match_semantics_def pfxm_mask_def word_bw_comms;fail)
      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
					add: simple_match_to_of_match_single_def OF_match_fields_unsafe_def spm
					     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"
  by (simp add: valid_prefix_def zero_prefix_match_all)

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
      by(simp add: prefix_match_semantics_def word_bw_comms;fail)
    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")
			 apply (simp add: match_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(clarsimp simp add: option2set_def;fail)
			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" "eset 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 eset (a # as). e  unat max_word› by fastforce
		have a_reprbl: "a  {0..unat ?mmw}" using eset (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)  eset (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_anyoiface := Iface oif, iiface := Iface iif, simple_action.Accept). oif  ifs, iif  ifs, oif  iif]"
definition "oif_ne_iif_p2 ifs = [(simple_match_anyoiface := 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

lemma mask_inj_hlp1: "inj_on (mask :: nat  16 word) {0..16}"
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)"
         unfolding mask_bl of_bl_rep_False .
  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)
  subgoal by(simp_all add: smtoms_eq_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
  by(erule no_overlaps_lroft_hlp2, simp add: distinct_simple_match_to_of_match)

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)
    apply(simp add: split3_def;fail)
  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])
	subgoal by(simp add: assms)
	subgoal by(simp add: o_assoc)
done

lemma sorted_lr_of_tran_s3_hlp: "xset f. fst x  a  b  set (lr_of_tran_s3 s f)  fst b  a" 
	by(auto simp add: lr_of_tran_s3_def)

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)
	 subgoal by(simp add: lr_of_tran_s3_def)
	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(simp add: fst_def[symmetric])
	apply(rule sorted_lr_of_tran_s3)
	apply(drule sorted_annotated[OF less_or_eq_imp_le, OF disjI1])
	apply(simp add: o_assoc)
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)"
by(simp add: route2match_def simple_matches.simps match_ifaceAny match_iface_refl ipset_from_cidr_0 prefix_match_semantics_ipset_from_netmask2)

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)
	 apply(simp add: valid_prefix_def pfxm_mask_def prefix_match_semantics_def generalized_sfw_def 
	       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)
     apply(simp add: generalized_sfw_def lr_of_tran_s1_def route2match_correct;fail)
    apply(simp add: route2match_def simple_matches.simps prefix_match_semantics_ipset_from_netmask2 
                    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(simp add: split3_def)
      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)
   subgoal by(simp add: generalized_sfw_simps)
  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(clarsimp simp add: comp_def)
    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 = ad])
     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(simp add: OF_match_linear_append OF_match_fields_safe_def comp_def)
   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)
   apply(simp add: match_ifaceAny;fail)
  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
    apply(simp add: valid_prefixes_alt_def)
  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(simp add: list_all_iff)
  apply(clarsimp)
  apply(drule simple_match_valid_fbs_rlen[rotated])
    apply(simp add: list_all_iff;fail)
   apply(simp add: list_all_iff;fail)
  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. [foft . OF_match_fields_unsafe (ofe_fields f) packet] = [foft . OF_match_fields_safe (ofe_fields f) packet]"
    apply(clarsimp simp add: list_all_iff of_match_fields_safe_eq) 
  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 (pp_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 (pp_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 (pp_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 (pp_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 (pp_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 (pp_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 (pp_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 (pp_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 (pp_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 = pp_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_match`set (upper_closure (packet_assume_new unfolded)). normalized_nnf_match m" by eval
lemma "m  get_match`set (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
value "dotdecimal_of_ipv4addr 0xA0D2500"
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  [
	⌦‹(''s1-lan'', (ipv4addr_of_dotdecimal (10,0,1,1), 0x3)),›
	(''s1-lan'', (ipv4addr_of_dotdecimal (10,0,1,2), 0x1)),
	(''s1-lan'', (ipv4addr_of_dotdecimal (10,0,1,3), 0x2)),
	(''s1-wan'', (ipv4addr_of_dotdecimal (10,0,2,1), 0x3))
	⌦‹(''s1-wan'', (ipv4addr_of_dotdecimal (10,0,2,4), 0xeabad0152059))›
]"

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_match`set (upper_closure (packet_assume_new unfolded)). normalized_nnf_match m" by eval
lemma "m  get_match`set (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 = pp_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 (pp_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 = pp_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 = pp_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. pp_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)" 
  by (simp add: valid_prefix_def pfxm_mask_def mask_eq_decr_exp and.commute)
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 "pd  {(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"
by (simp add: guha_equal no_overlapsI)
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 fw1} makes the decision @{term a} (where @{term a} is the second element of the result tuple from @{const generalized_sfw}) and @{term fw2} 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 fw1 fw2) p = Some (u, d1,d2)  (r1 r2. generalized_sfw fw1 p = Some (r1,d1)  generalized_sfw fw2 p = Some (r2,d2)  Some u = simple_match_and r1 r2)"
  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 rs1 p = Decision FinalAllow  simple_fw rs2 p = Decision FinalAllow 
simple_fw (map simple_rule_conj (generalized_fw_join (map simple_rule_dtor rs1) (map simple_rule_dtor rs2))) 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 (pp_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
(*>*)