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" "(∀fo∈set ft. ofe_prio a < ofe_prio fo ⟶ ¬ γ (ofe_fields fo) p)" 
	               "b ∈ set ft" "γ (ofe_fields b) p" "(∀fo∈set ft. ofe_prio b < ofe_prio fo ⟶ ¬ γ (ofe_fields fo) p)" by simp_all
	then have "ofe_prio a = ofe_prio b"
		by fastforce
	note goal1(1)[unfolded check_no_overlap_def] ab2(1) ab2(4) this ab2(2) ab(1) ab2(5)
	then show False by blast
qed

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

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

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

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

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

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

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

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

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

lemma no_overlapsI: "check_no_overlap γ t ⟹ distinct t ⟹ no_overlaps γ t"
unfolding check_no_overlap_alt
proof(induction t)
	case (Cons a t)
	from no_overlap_ConsI[OF Cons(2)] Cons(3,1)
	have "no_overlaps γ t" by simp
	thus ?case using Cons(2,3) unfolding check_no_overlap2_def by auto
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 "¬ (∃p∈UNIV. γ (ofe_fields a) p ∧ γ (ofe_fields b) p)" by simp
	with contr(2) show False unfolding contr(3) by simp
qed

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

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

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

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

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

end