# Theory Fixed_Action

```theory Fixed_Action
imports Semantics_Ternary
begin

section‹Fixed Action›

text‹If firewall rules have the same action, we can focus on the matching only.›

text‹Applying a rule once or several times makes no difference.›
lemma approximating_bigstep_fun_prepend_replicate:
"n > 0 ⟹ approximating_bigstep_fun γ p (r#rs) Undecided = approximating_bigstep_fun γ p ((replicate n r)@rs) Undecided"
apply(induction n)
apply(simp)
apply(simp)
apply(case_tac r)
apply(rename_tac m a)
apply(simp split: action.split)
by fastforce

text‹utility lemmas›
context
begin
private lemma fixedaction_Log: "approximating_bigstep_fun γ p (map (λm. Rule m Log) ms) Undecided = Undecided"
by(induction ms, simp_all)

private lemma fixedaction_Empty:"approximating_bigstep_fun γ p (map (λm. Rule m Empty) ms) Undecided = Undecided"
by(induction ms, simp_all)

private lemma helperX1_Log: "matches γ m' Log p ⟹
approximating_bigstep_fun γ p (map ((λm. Rule m Log) ∘ MatchAnd m') m2' @ rs2) Undecided =
approximating_bigstep_fun γ p rs2 Undecided"
by(induction m2')(simp_all split: action.split)

private lemma helperX1_Empty: "matches γ m' Empty p ⟹
approximating_bigstep_fun γ p (map ((λm. Rule m Empty) ∘ MatchAnd m') m2' @ rs2) Undecided =
approximating_bigstep_fun γ p rs2 Undecided"
by(induction m2')(simp_all split: action.split)

private lemma helperX3: "matches γ m' a p ⟹
approximating_bigstep_fun γ p (map ((λm. Rule m a) ∘ MatchAnd m') m2' @ rs2 ) Undecided =
approximating_bigstep_fun γ p (map (λm. Rule m a) m2' @ rs2) Undecided"
proof(induction m2')
case Nil thus ?case by simp
next
case Cons thus ?case by(cases a) (simp_all add: matches_simps)
qed

lemmas fixed_action_simps = fixedaction_Log fixedaction_Empty helperX1_Log helperX1_Empty helperX3
end

lemma fixedaction_swap:
"approximating_bigstep_fun γ p (map (λm. Rule m a) (m1@m2)) s = approximating_bigstep_fun γ p (map (λm. Rule m a) (m2@m1)) s"
proof(induction s rule: just_show_all_approximating_bigstep_fun_equalities_with_start_Undecided)
case Undecided
have "approximating_bigstep_fun γ p (map (λm. Rule m a) m1 @ map (λm. Rule m a) m2) Undecided =
approximating_bigstep_fun γ p (map (λm. Rule m a) m2 @ map (λm. Rule m a) m1) Undecided"
proof(induction m1)
case Nil thus ?case by simp
next
case (Cons m m1)
{ fix m rs
have "approximating_bigstep_fun γ p ((map (λm. Rule m Log) m)@rs) Undecided =
approximating_bigstep_fun γ p rs Undecided"
by(induction m) (simp_all)
} note Log_helper=this
{ fix m rs
have "approximating_bigstep_fun γ p ((map (λm. Rule m Empty) m)@rs) Undecided =
approximating_bigstep_fun γ p rs Undecided"
by(induction m) (simp_all)
} note Empty_helper=this

show ?case
proof(cases "matches γ m a p")
case True
thus ?thesis
proof(induction m2)
case Nil thus ?case by simp
next
case Cons thus ?case
apply(simp split:action.split action.split_asm)
using Log_helper Empty_helper by fastforce+
qed
next
case False
thus ?thesis
apply(simp)
apply(induction m2)
apply(simp_all)
apply(simp split:action.split action.split_asm)
apply fastforce
done
qed
qed
thus ?thesis using Undecided by simp
qed

corollary fixedaction_reorder: "approximating_bigstep_fun γ p (map (λm. Rule m a) (m1 @ m2 @ m3)) s = approximating_bigstep_fun γ p (map (λm. Rule m a) (m2 @ m1 @ m3)) s"
proof(induction s rule: just_show_all_approximating_bigstep_fun_equalities_with_start_Undecided)
case Undecided
have "approximating_bigstep_fun γ p (map (λm. Rule m a) (m1 @ m2 @ m3)) Undecided = approximating_bigstep_fun γ p (map (λm. Rule m a) (m2 @ m1 @ m3)) Undecided"
proof(induction m3)
case Nil thus ?case using fixedaction_swap by fastforce
next
case (Cons m3'1 m3)
have "approximating_bigstep_fun γ p (map (λm. Rule m a) ((m3'1 # m3) @ m1 @ m2)) Undecided = approximating_bigstep_fun γ p (map (λm. Rule m a) ((m3'1 # m3) @ m2 @ m1)) Undecided"
apply(simp)
apply(cases "matches γ m3'1 a p")
apply(simp split: action.split action.split_asm)
apply (metis append_assoc fixedaction_swap map_append Cons.IH)
apply(simp)
by (metis append_assoc fixedaction_swap map_append Cons.IH)
hence "approximating_bigstep_fun γ p (map (λm. Rule m a) ((m1 @ m2) @ m3'1 # m3)) Undecided = approximating_bigstep_fun γ p (map (λm. Rule m a) ((m2 @ m1) @ m3'1 # m3)) Undecided"
apply(subst fixedaction_swap)
apply(subst(2) fixedaction_swap)
by simp
thus ?case
apply(subst append_assoc[symmetric])
apply(subst append_assoc[symmetric])
by simp
qed
thus ?thesis using Undecided by simp
qed

text‹If the actions are equal, the @{term set} (position and replication independent) of the match expressions can be considered.›
lemma approximating_bigstep_fun_fixaction_matchseteq: "set m1 = set m2 ⟹
approximating_bigstep_fun γ p (map (λm. Rule m a) m1) s =
approximating_bigstep_fun γ p (map (λm. Rule m a) m2) s"
proof(rule just_show_all_approximating_bigstep_fun_equalities_with_start_Undecided)
assume m1m2_seteq: "set m1 = set m2" and "s = Undecided"
from m1m2_seteq have
"approximating_bigstep_fun γ p (map (λm. Rule m a) m1) Undecided =
approximating_bigstep_fun γ p (map (λm. Rule m a) m2) Undecided"
proof(induction m1 arbitrary: m2)
case Nil thus ?case by simp
next
case (Cons m m1)
show ?case
proof (cases "m ∈ set m1")
case True
from True have "set m1 = set (m # m1)" by auto
from Cons.IH[OF ‹set m1 = set (m # m1)›] have "approximating_bigstep_fun γ p (map (λm. Rule m a) (m # m1)) Undecided = approximating_bigstep_fun γ p (map (λm. Rule m a) (m1)) Undecided" ..
thus ?thesis by (metis Cons.IH Cons.prems ‹set m1 = set (m # m1)›)
next
case False
from False have "m ∉ set m1" .
show ?thesis
proof (cases "m ∉ set m2")
case True
from True ‹m ∉ set m1› Cons.prems have "set m1 = set m2" by auto
from Cons.IH[OF this] show ?thesis by (metis Cons.IH Cons.prems ‹set m1 = set m2›)
next
case False
hence "m ∈ set m2" by simp

have repl_filter_simp: "(replicate (length [x←m2 . x = m]) m) = [x←m2 . x = m]"
by (metis (lifting, full_types) filter_set member_filter replicate_length_same)

from Cons.prems  ‹m ∉ set m1› have "set m1 = set (filter (λx. x≠m) m2)" by auto
from Cons.IH[OF this] have "approximating_bigstep_fun γ p (map (λm. Rule m a) m1) Undecided = approximating_bigstep_fun γ p (map (λm. Rule m a) [x←m2 . x ≠ m]) Undecided" .
from this have "approximating_bigstep_fun γ p (map (λm. Rule m a) (m#m1)) Undecided = approximating_bigstep_fun γ p (map (λm. Rule m a) (m#[x←m2 . x ≠ m])) Undecided"
apply(simp split: action.split)
by fast
also have "… = approximating_bigstep_fun γ p (map (λm. Rule m a) ([x←m2 . x = m]@[x←m2 . x ≠ m])) Undecided"
apply(simp only: list.map)
thm approximating_bigstep_fun_prepend_replicate[where n="length [x←m2 . x = m]"]
apply(subst approximating_bigstep_fun_prepend_replicate[where n="length [x←m2 . x = m]"])
apply (metis (full_types) False filter_empty_conv neq0_conv repl_filter_simp replicate_0)
by (metis (lifting, no_types) map_append map_replicate repl_filter_simp)
also have "… =  approximating_bigstep_fun γ p (map (λm. Rule m a) m2) Undecided"
proof(induction m2)
case Nil thus ?case by simp
next
case(Cons m2'1 m2')
have "approximating_bigstep_fun γ p (map (λm. Rule m a) [x←m2' . x = m] @ Rule m2'1 a # map (λm. Rule m a) [x←m2' . x ≠ m]) Undecided =
approximating_bigstep_fun γ p (map (λm. Rule m a) ([x←m2' . x = m] @ [m2'1] @ [x←m2' . x ≠ m])) Undecided" by fastforce
also have "… = approximating_bigstep_fun γ p (map (λm. Rule m a) ([m2'1] @ [x←m2' . x = m] @ [x←m2' . x ≠ m])) Undecided"
using fixedaction_reorder by fast
finally have XX: "approximating_bigstep_fun γ p (map (λm. Rule m a) [x←m2' . x = m] @ Rule m2'1 a # map (λm. Rule m a) [x←m2' . x ≠ m]) Undecided =
approximating_bigstep_fun γ p (Rule m2'1 a # (map (λm. Rule m a) [x←m2' . x = m] @ map (λm. Rule m a) [x←m2' . x ≠ m])) Undecided"
by fastforce
from Cons show ?case
apply(case_tac "m2'1 = m")
apply(simp split: action.split)
apply fast
apply(simp del: approximating_bigstep_fun.simps)
apply(simp only: XX)
apply(case_tac "matches γ m2'1 a p")
apply(simp)
apply(simp split: action.split)
apply(fast)
apply(simp)
done
qed
finally show ?thesis .
qed
qed
qed
thus ?thesis using ‹s = Undecided› by simp
qed

subsection‹@{term match_list}›
text‹Reducing the firewall semantics to short-circuit matching evaluation›

fun match_list :: "('a, 'packet) match_tac ⇒ 'a match_expr list ⇒ action ⇒ 'packet ⇒ bool" where
"match_list γ [] a p = False" |
"match_list γ (m#ms) a p = (if matches γ m a p then True else match_list γ ms a p)"

lemma match_list_matches: "match_list γ ms a p ⟷ (∃m ∈ set ms. matches γ m a p)"
by(induction ms, simp_all)

lemma match_list_True: "match_list γ ms a p ⟹ approximating_bigstep_fun γ p (map (λm. Rule m a) ms) Undecided = (case a of Accept ⇒ Decision FinalAllow
| Drop ⇒ Decision FinalDeny
| Reject ⇒ Decision FinalDeny
| Log ⇒ Undecided
| Empty ⇒ Undecided
― ‹unhandled cases›
)"
apply(induction ms)
apply(simp)
apply(simp split: if_split_asm action.split)
done
lemma match_list_False: "¬ match_list γ ms a p ⟹ approximating_bigstep_fun γ p (map (λm. Rule m a) ms) Undecided = Undecided"
apply(induction ms)
apply(simp)
apply(simp split: if_split_asm action.split)
done

text‹The key idea behind @{const match_list}: Reducing semantics to match list›
lemma match_list_semantics: "match_list γ ms1 a p ⟷ match_list γ ms2 a p ⟹
approximating_bigstep_fun γ p (map (λm. Rule m a) ms1) s = approximating_bigstep_fun γ p (map (λm. Rule m a) ms2) s"
apply(rule just_show_all_approximating_bigstep_fun_equalities_with_start_Undecided)
apply(simp)
apply(thin_tac "s = Undecided")
apply(induction ms2)
apply(simp)
apply(induction ms1)
apply(simp)
apply(simp split: if_split_asm)
apply(rename_tac m ms2)
apply(simp del: approximating_bigstep_fun.simps)
apply(simp split: if_split_asm del: approximating_bigstep_fun.simps)
apply(simp split: action.split add: match_list_True fixed_action_simps)
apply(simp)
done

text‹We can exploit de-morgan to get a disjunction in the match expression!›
(*but we need to normalize afterwards, which is quite slow*)
fun match_list_to_match_expr :: "'a match_expr list ⇒ 'a match_expr" where
"match_list_to_match_expr [] = MatchNot MatchAny" |
"match_list_to_match_expr (m#ms) = MatchOr m (match_list_to_match_expr ms)"
text‹@{const match_list_to_match_expr} constructs a unwieldy @{typ "'a match_expr"} from a list.
The semantics of the resulting match expression is the disjunction of the elements of the list.
This is handy because the normal match expressions do not directly support disjunction.
Use this function with care because the resulting match expression is very ugly!›
lemma match_list_to_match_expr_disjunction: "match_list γ ms a p ⟷ matches γ (match_list_to_match_expr ms) a p"
apply(induction ms rule: match_list_to_match_expr.induct)
done

lemma match_list_singleton: "match_list γ [m] a p ⟷ matches γ m a p" by(simp)

lemma match_list_append: "match_list γ (m1@m2) a p ⟷ (¬ match_list γ m1 a p ⟶ match_list γ m2 a p)"
by(induction m1) simp+

lemma match_list_helper1: "¬ matches γ m2 a p ⟹ match_list γ (map (λx. MatchAnd x m2) m1') a p ⟹ False"
apply(induction m1')
apply(simp; fail)
apply(simp split:if_split_asm)
by(auto dest: matches_dest)
lemma match_list_helper2: " ¬ matches γ m a p ⟹ ¬ match_list γ (map (MatchAnd m) m2') a p"
apply(induction m2')
apply(simp; fail)
apply(simp split:if_split_asm)
by(auto dest: matches_dest)
lemma match_list_helper3: "matches γ m a p ⟹ match_list γ m2' a p ⟹ match_list γ (map (MatchAnd m) m2') a p"
apply(induction m2')
apply(simp; fail)
apply(simp split:if_split_asm)
lemma match_list_helper4: "¬ match_list γ m2' a p ⟹ ¬ match_list γ (map (MatchAnd aa) m2') a p "
apply(induction m2')
apply(simp; fail)
apply(simp split:if_split_asm)
by(auto dest: matches_dest)
lemma match_list_helper5: " ¬ match_list γ m2' a p ⟹ ¬ match_list γ (concat (map (λx. map (MatchAnd x) m2') m1')) a p "
apply(induction m2')
apply(simp split:if_split_asm)
apply(induction m1')
apply(simp; fail)
by(auto dest: matches_dest)
lemma match_list_helper6: "¬ match_list γ m1' a p ⟹ ¬ match_list γ (concat (map (λx. map (MatchAnd x) m2') m1')) a p "
apply(induction m2')
apply(simp split:if_split_asm)
apply(induction m1')
apply(simp; fail)
by(auto dest: matches_dest)

lemmas match_list_helper = match_list_helper1 match_list_helper2 match_list_helper3 match_list_helper4 match_list_helper5 match_list_helper6
hide_fact match_list_helper1 match_list_helper2 match_list_helper3 match_list_helper4 match_list_helper5 match_list_helper6

lemma match_list_map_And1: "matches γ m1 a p = match_list γ m1' a p ⟹
matches γ (MatchAnd m1 m2) a p ⟷ match_list γ  (map (λx. MatchAnd x m2) m1') a p"
apply(induction m1')
apply(auto dest: matches_dest; fail)
apply(simp split: if_split_asm)
apply safe
apply(auto dest: match_list_helper(1))
by(auto dest: matches_dest)

lemma matches_list_And_concat: "matches γ m1 a p = match_list γ m1' a p ⟹ matches γ m2 a p = match_list γ m2' a p ⟹
matches γ (MatchAnd m1 m2) a p ⟷ match_list γ [MatchAnd x y. x <- m1', y <- m2'] a p"
apply(induction m1')
apply(auto dest: matches_dest; fail)
apply(simp split: if_split_asm)
prefer 2
apply(subgoal_tac "¬ match_list γ (map (MatchAnd aa) m2') a p")
apply(simp; fail)
apply safe
done

lemma match_list_concat: "match_list γ (concat lss) a p ⟷ (∃ls ∈ set lss. match_list γ ls a p)"
apply(induction lss)
apply(simp; fail)

lemma fixedaction_wf_ruleset: "wf_ruleset γ p (map (λm. Rule m a) ms) ⟷
¬ match_list γ ms a p ∨ ¬ (∃chain. a = Call chain) ∧ a ≠ Return ∧ ¬ (∃chain. a = Goto chain) ∧ a ≠ Unknown"
proof -
have helper: "⋀a b c. a ⟷ c ⟹ (a ⟶ b) = (c ⟶ b)" by fast
show ?thesis
apply(rule helper)
apply(induction ms)
apply(simp; fail)
apply(simp)
done
qed

lemma wf_ruleset_singleton: "wf_ruleset γ p [Rule m a] ⟷ ¬ matches γ m a p ∨ ¬ (∃chain. a = Call chain) ∧ a ≠ Return ∧ ¬ (∃chain. a = Goto chain) ∧ a ≠ Unknown"