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:
	"fe1∈set ft" "x1 = ofe_action fe1" "γ (ofe_fields fe1) p" "(∀fe'∈set ft. ofe_prio fe1 < ofe_prio fe' ⟶ ¬ γ (ofe_fields fe') p)"
    "fe2∈set ft" "a  = ofe_action fe2" "γ (ofe_fields fe2) p" "(∀fe'∈set ft. ofe_prio fe2 < ofe_prio fe' ⟶ ¬ γ (ofe_fields fe') p)"
    	by blast
    from ‹x1 ≠ a› have fene: "fe1 ≠ fe2" using fes(2,6) by blast
    have pe: "ofe_prio fe1 = ofe_prio fe2" using fes(1,3-4,5,7-8) less_linear by blast
    note ‹no_overlaps γ ft›[THEN check_no_overlapI, unfolded check_no_overlap_def]
    note this[unfolded Ball_def, THEN spec, THEN mp, OF fes(1), THEN spec, THEN mp, OF fes(5),THEN spec, THEN mp, OF UNIV_I, of p] pe fene fes(3,7)
    thus False by blast
qed

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

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

text‹The above lemma does indeed not hold, the reason for this are (possibly partially) shadowed overlaps.
This is exemplified below: If there are at least three different possible actions (necessary assumption)
and a match expression that matches all packets (convenience assumption), it is possible to construct a flow 
table that is admonished by @{const check_no_overlap} but still will never run into undefined behavior.
›
(* This is not the terribly most important lemma. Feel free to delete it if the proof gives you trouble. *)
lemma
  assumes "CARD('action) ≥ 3"
  assumes "∀p. γ x p" (* with a sane γ, x = {} *)
	shows "∃ft::('a, 'action) flow_entry_match list. ¬check_no_overlap γ ft ∧
	  ¬(∃fe1 fe2 p. fe1 ∈ set ft ∧ fe2 ∈ set ft ∧ fe1 ≠ fe2 ∧ ofe_prio fe1 = ofe_prio fe2
		∧ guha_table_semantics γ ft p (Some (ofe_action fe1))
		∧ guha_table_semantics γ ft p (Some (ofe_action fe2)))"
proof -
  obtain adef aa ab :: 'action where anb[simp]: "aa ≠ ab" "adef ≠ aa" "adef ≠ ab" using assms(1) card3_eI by blast
  let ?cex = "[OFEntry 1 x adef, OFEntry 0 x aa, OFEntry 0 x ab]"
  have ol: "¬check_no_overlap γ ?cex"
    unfolding check_no_overlap_def ball_simps
    apply(rule bexI[where x = "OFEntry 0 x aa", rotated], (simp;fail))
    apply(rule bexI[where x = "OFEntry 0 x ab", rotated], (simp;fail))
    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