# Theory Featherweight_OpenFlow_Comparison

```theory Featherweight_OpenFlow_Comparison
imports Semantics_OpenFlow
begin

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

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

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

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

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

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

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

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

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

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

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

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

end
```