# Theory List_Misc

section‹Miscellaneous List Lemmas›
theory List_Misc
imports Main
begin

lemma list_app_singletonE:
assumes "rs⇩1 @ rs⇩2 = [x]"
obtains (first) "rs⇩1 = [x]" "rs⇩2 = []"
| (second) "rs⇩1 = []" "rs⇩2 = [x]"
using assms
by (cases "rs⇩1") auto

lemma list_app_eq_cases:
assumes "xs⇩1 @ xs⇩2 = ys⇩1 @ ys⇩2"
obtains (longer)  "xs⇩1 = take (length xs⇩1) ys⇩1" "xs⇩2 = drop (length xs⇩1) ys⇩1 @ ys⇩2"
| (shorter) "ys⇩1 = take (length ys⇩1) xs⇩1" "ys⇩2 = drop (length ys⇩1) xs⇩1 @ xs⇩2"
using assms by (cases "length xs⇩1 ≤ length ys⇩1") (metis append_eq_append_conv_if)+

lemma empty_concat: "concat (map (λx. []) ms) = []" by simp
end


# Theory Negation_Type

section‹Negation Type›
theory Negation_Type
imports Main
begin

text‹Store some @{typ 'a} and remember symbolically whether you mean just @{term a} or @{term "¬ a"}.›

text‹Only negated or non-negated literals›
datatype 'a negation_type = Pos 'a | Neg 'a

fun getPos :: "'a negation_type list ⇒ 'a list" where
"getPos [] = []" |
"getPos ((Pos x)#xs) = x#(getPos xs)" |
"getPos (_#xs) = getPos xs"

fun getNeg :: "'a negation_type list ⇒ 'a list" where
"getNeg [] = []" |
"getNeg ((Neg x)#xs) = x#(getNeg xs)" |
"getNeg (_#xs) = getNeg xs"

lemma getPos_append: "getPos (as@bs) = getPos as @ getPos bs"
by(induct as rule: getPos.induct) simp+

lemma getNeg_append: "getNeg (as@bs) = getNeg as @ getNeg bs"
by(induct as rule: getNeg.induct) simp+

text‹If there is @{typ "'a negation_type"}, then apply a @{term map} only to @{typ 'a}.
I.e. keep @{term Neg} and @{term Pos}›
fun NegPos_map :: "('a ⇒ 'b) ⇒ 'a negation_type list ⇒ 'b negation_type list" where
"NegPos_map _ [] = []" |
"NegPos_map f ((Pos a)#as) = (Pos (f a))#NegPos_map f as" |
"NegPos_map f ((Neg a)#as) = (Neg (f a))#NegPos_map f as"

text‹Example›
lemma "NegPos_map (λx::nat. x+1) [Pos 0, Neg 1] = [Pos 1, Neg 2]" by eval

lemma getPos_NegPos_map_simp: "(getPos (NegPos_map X (map Pos src))) = map X src"
by(induction src) (simp_all)
lemma getNeg_NegPos_map_simp: "(getNeg (NegPos_map X (map Neg src))) = map X src"
by(induction src) (simp_all)
lemma getNeg_Pos_empty: "(getNeg (NegPos_map X (map Pos src))) = []"
by(induction src) (simp_all)
lemma getNeg_Neg_empty: "(getPos (NegPos_map X (map Neg src))) = []"
by(induction src) (simp_all)
lemma getPos_NegPos_map_simp2: "(getPos (NegPos_map X src)) = map X (getPos src)"
by(induction src rule: getPos.induct) (simp_all)
lemma getNeg_NegPos_map_simp2: "(getNeg (NegPos_map X src)) = map X (getNeg src)"
by(induction src rule: getPos.induct) (simp_all)
lemma getPos_id: "getPos (map Pos xs) = xs"
by(induction xs) (simp_all)
lemma getNeg_id: "getNeg (map Neg xs) = xs"
by(induction xs) (simp_all)
lemma getPos_empty2: "(getPos (map Neg src)) = []"
by(induction src) (simp_all)
lemma getNeg_empty2: "(getNeg (map Pos src)) = []"
by(induction src) (simp_all)

lemmas NegPos_map_simps = getPos_NegPos_map_simp getNeg_NegPos_map_simp getNeg_Pos_empty getNeg_Neg_empty getPos_NegPos_map_simp2
getNeg_NegPos_map_simp2 getPos_id getNeg_id getPos_empty2 getNeg_empty2

lemma NegPos_map_map_Neg: "NegPos_map C (map Neg as) = map Neg (map C as)"
by(induction as) (simp_all)
lemma NegPos_map_map_Pos: "NegPos_map C (map Pos as) = map Pos (map C as)"
by(induction as) (simp_all)

lemma NegPos_map_append: "NegPos_map C (as @ bs) = NegPos_map C as @ NegPos_map C bs"
by(induction as rule: getNeg.induct) (simp_all)

lemma getPos_set: "Pos a ∈ set x ⟷ a ∈ set (getPos x)"
apply(induction x rule: getPos.induct)
apply(auto)
done
lemma getNeg_set: "Neg a ∈ set x ⟷ a ∈ set (getNeg x)"
apply(induction x rule: getPos.induct)
apply(auto)
done
lemma getPosgetNeg_subset: "set x ⊆ set x' ⟷  set (getPos x) ⊆ set (getPos x') ∧ set (getNeg x) ⊆ set (getNeg x')"
apply(induction x rule: getPos.induct)
apply(simp)
apply(rule iffI)
done
lemma set_Pos_getPos_subset: "Pos  set (getPos x) ⊆ set x"
apply(induction x rule: getPos.induct)
apply(simp_all)
apply blast+
done
lemma set_Neg_getNeg_subset: "Neg  set (getNeg x) ⊆ set x"
apply(induction x rule: getNeg.induct)
apply(simp_all)
apply blast+
done
lemmas NegPos_set = getPos_set getNeg_set getPosgetNeg_subset set_Pos_getPos_subset set_Neg_getNeg_subset
hide_fact getPos_set getNeg_set getPosgetNeg_subset set_Pos_getPos_subset set_Neg_getNeg_subset

lemma negation_type_forall_split: "(∀is∈set Ms. case is of Pos i ⇒ P i | Neg i ⇒ Q i) ⟷ (∀i∈set (getPos Ms). P i) ∧ (∀i∈set (getNeg Ms). Q i)"
apply(rule)
apply(simp split: negation_type.split_asm)
using NegPos_set(1) NegPos_set(2) apply force
apply(simp split: negation_type.split)
using NegPos_set(1) NegPos_set(2) by fastforce

fun invert :: "'a negation_type ⇒ 'a negation_type" where
"invert (Pos x) = Neg x" |
"invert (Neg x) = Pos x"

lemma invert_invert_id: "invert ∘ invert = id"
apply(clarsimp simp add: fun_eq_iff, rename_tac x, case_tac x)
by simp+

end


# Theory WordInterval_Lists

theory WordInterval_Lists
Negation_Type
begin

fun l2wi_negation_type_union :: "('a::len word × 'a::len word) negation_type list ⇒ 'a::len wordinterval" where
"l2wi_negation_type_union [] = Empty_WordInterval" |
"l2wi_negation_type_union ((Pos (s,e))#ls) = wordinterval_union (WordInterval s e) (l2wi_negation_type_union ls)" |
"l2wi_negation_type_union ((Neg (s,e))#ls) = wordinterval_union (wordinterval_invert (WordInterval s e)) (l2wi_negation_type_union ls)"

lemma l2wi_negation_type_union: "wordinterval_to_set (l2wi_negation_type_union l) =
(⋃ (i,j) ∈ set (getPos l). {i .. j}) ∪ (⋃ (i,j) ∈ set (getNeg l). - {i .. j})"
apply(induction l rule: l2wi_negation_type_union.induct)
apply(simp_all)
apply fast+
done

definition l2wi_intersect :: "('a::len word × 'a::len word) list ⇒ 'a::len wordinterval" where
"l2wi_intersect = foldl (λ acc (s,e). wordinterval_intersection (WordInterval s e) acc) wordinterval_UNIV"

lemma l2wi_intersect: "wordinterval_to_set (l2wi_intersect l) = (⋂ (i,j) ∈ set l. {i .. j})"
proof -
{ fix U ― ‹@{const wordinterval_UNIV} generalized›
have "wordinterval_to_set (foldl (λacc (s, e). wordinterval_intersection (WordInterval s e) acc) U l) = (wordinterval_to_set U) ∩ (⋂(i, j)∈set l. {i..j})"
apply(induction l arbitrary: U)
apply(simp)
by force
} thus ?thesis
unfolding l2wi_intersect_def by simp
qed

fun l2wi_negation_type_intersect :: "('a::len word × 'a::len word) negation_type list ⇒ 'a::len wordinterval" where
"l2wi_negation_type_intersect [] = wordinterval_UNIV" |
"l2wi_negation_type_intersect ((Pos (s,e))#ls) = wordinterval_intersection (WordInterval s e) (l2wi_negation_type_intersect ls)" |
"l2wi_negation_type_intersect ((Neg (s,e))#ls) = wordinterval_intersection (wordinterval_invert (WordInterval s e)) (l2wi_negation_type_intersect ls)"

lemma l2wi_negation_type_intersect_alt: "wordinterval_to_set (l2wi_negation_type_intersect l) =
wordinterval_to_set (wordinterval_setminus (l2wi_intersect (getPos l)) (l2wi (getNeg l)))"
apply(induction l rule :l2wi_negation_type_intersect.induct)
apply(simp_all)
apply(fast)+
done

lemma l2wi_negation_type_intersect: "wordinterval_to_set (l2wi_negation_type_intersect l) =
(⋂ (i,j) ∈ set (getPos l). {i .. j}) - (⋃ (i,j) ∈ set (getNeg l). {i .. j})"

end


# Theory Repeat_Stabilize

section‹Repeat finitely Until it Stabilizes›
theory Repeat_Stabilize
imports Main
begin

text‹Repeating something a number of times›

text‹Iterating a function at most @{term n} times (first parameter) until it stabilizes.›
fun repeat_stabilize :: "nat ⇒ ('a ⇒ 'a) ⇒ 'a ⇒ 'a" where
"repeat_stabilize 0 _ v = v" |
"repeat_stabilize (Suc n) f v = (let v_new = f v in if v = v_new then v else repeat_stabilize n f v_new)"

lemma repeat_stabilize_funpow: "repeat_stabilize n f v = (f^^n) v"
proof(induction n arbitrary: v)
case (Suc n)
have "f v = v ⟹ (f^^n) v = v" by(induction n) simp_all
with Suc show ?case by(simp add: Let_def funpow_swap1)
qed(simp)

lemma repeat_stabilize_induct: "(P m) ⟹ (⋀m. P m ⟹ P (f m)) ⟹ P (repeat_stabilize n f m)"
apply(induction n)
by(simp)+

end


# Theory Firewall_Common

section‹Firewall Basic Syntax›
theory Firewall_Common
imports Main Simple_Firewall.Firewall_Common_Decision_State
"Common/Repeat_Stabilize"
begin

text‹
Our firewall model supports the following actions.
›
datatype action = Accept | Drop | Log | Reject | Call string | Return | Goto string | Empty | Unknown

text‹
We support the following algebra over primitives of type @{typ 'a}.
The type parameter @{typ 'a} denotes the primitive match condition. For example, matching
on source IP address or on protocol.
We lift the primitives to an algebra. Note that we do not have an Or expression.
›
datatype 'a match_expr = Match 'a
| MatchNot "'a match_expr"
| MatchAnd "'a match_expr" "'a match_expr"
| MatchAny

definition MatchOr :: "'a match_expr ⇒ 'a match_expr ⇒ 'a match_expr" where
"MatchOr m1 m2 = MatchNot (MatchAnd (MatchNot m1) (MatchNot m2))"

text‹A firewall rule consists of a match expression and an action.›
datatype 'a rule = Rule (get_match: "'a match_expr") (get_action: action)

lemma rules_singleton_rev_E:
"[Rule m a] = rs⇩1 @ rs⇩2 ⟹
(rs⇩1 = [Rule m a] ⟹ rs⇩2 = [] ⟹ P m a) ⟹
(rs⇩1 = [] ⟹ rs⇩2 = [Rule m a] ⟹ P m a) ⟹ P m a"
by (cases rs⇩1) auto

section‹Basic Algorithms›
text‹These algorithms should be valid for all firewall semantics.
The corresponding proofs follow once the semantics are defined.›

text‹The actions Log and Empty do not modify the packet processing in any way. They can be removed.›
fun rm_LogEmpty :: "'a rule list ⇒ 'a rule list" where
"rm_LogEmpty [] = []" |
"rm_LogEmpty ((Rule _ Empty)#rs) = rm_LogEmpty rs" |
"rm_LogEmpty ((Rule _ Log)#rs) = rm_LogEmpty rs" |
"rm_LogEmpty (r#rs) = r # rm_LogEmpty rs"

lemma rm_LogEmpty_filter: "rm_LogEmpty rs = filter (λr. get_action r ≠ Log ∧ get_action r ≠ Empty) rs"
by(induction rs rule: rm_LogEmpty.induct) (simp_all)

lemma rm_LogEmpty_seq: "rm_LogEmpty (rs1@rs2) = rm_LogEmpty rs1 @ rm_LogEmpty rs2"

text‹Optimize away MatchAny matches›
fun opt_MatchAny_match_expr_once :: "'a match_expr ⇒ 'a match_expr" where
"opt_MatchAny_match_expr_once MatchAny = MatchAny" |
"opt_MatchAny_match_expr_once (Match a) = (Match a)" |
"opt_MatchAny_match_expr_once (MatchNot (MatchNot m)) = (opt_MatchAny_match_expr_once m)" |
"opt_MatchAny_match_expr_once (MatchNot m) = MatchNot (opt_MatchAny_match_expr_once m)" |
"opt_MatchAny_match_expr_once (MatchAnd MatchAny MatchAny) = MatchAny" |
"opt_MatchAny_match_expr_once (MatchAnd MatchAny m) = (opt_MatchAny_match_expr_once m)" |
(*note: remove recursive call to opt_MatchAny_match_expr_once to make it probably faster*)
"opt_MatchAny_match_expr_once (MatchAnd m MatchAny) = (opt_MatchAny_match_expr_once m)" |
"opt_MatchAny_match_expr_once (MatchAnd _ (MatchNot MatchAny)) = (MatchNot MatchAny)" |
"opt_MatchAny_match_expr_once (MatchAnd (MatchNot MatchAny) _) = (MatchNot MatchAny)" |
"opt_MatchAny_match_expr_once (MatchAnd m1 m2) = MatchAnd (opt_MatchAny_match_expr_once m1) (opt_MatchAny_match_expr_once m2)"
(* without recursive call: need to apply multiple times until it stabelizes *)

text‹It is still a good idea to apply @{const opt_MatchAny_match_expr_once} multiple times. Example:›
lemma "MatchNot (opt_MatchAny_match_expr_once (MatchAnd MatchAny (MatchNot MatchAny))) = MatchNot (MatchNot MatchAny)" by simp
lemma "m = (MatchAnd (MatchAnd MatchAny MatchAny) (MatchAnd MatchAny MatchAny)) ⟹
(opt_MatchAny_match_expr_once^^2) m ≠ opt_MatchAny_match_expr_once m" by(simp add: funpow_def)

definition opt_MatchAny_match_expr :: "'a match_expr ⇒ 'a match_expr" where
"opt_MatchAny_match_expr m ≡ repeat_stabilize 2 opt_MatchAny_match_expr_once m"

text‹Rewrite @{const Reject} actions to @{const Drop} actions.
If we just care about the filtering decision (@{const FinalAllow} or @{const FinalDeny}), they should be equal.›
fun rw_Reject :: "'a rule list ⇒ 'a rule list" where
"rw_Reject [] = []" |
"rw_Reject ((Rule m Reject)#rs) = (Rule m Drop)#rw_Reject rs" |
"rw_Reject (r#rs) = r # rw_Reject rs"

text‹We call a ruleset simple iff the only actions are @{const Accept} and @{const Drop}›
definition simple_ruleset :: "'a rule list ⇒ bool" where
"simple_ruleset rs ≡ ∀r ∈ set rs. get_action r = Accept ∨ get_action r = Drop"

lemma simple_ruleset_tail: "simple_ruleset (r#rs) ⟹ simple_ruleset rs" by (simp add: simple_ruleset_def)

lemma simple_ruleset_append: "simple_ruleset (rs⇩1 @ rs⇩2) ⟷ simple_ruleset rs⇩1 ∧ simple_ruleset rs⇩2"

fun has_primitive :: "'a match_expr ⇒ bool" where
"has_primitive MatchAny = False" |
"has_primitive (Match a) = True" |
"has_primitive (MatchNot m) = has_primitive m" |
"has_primitive (MatchAnd m1 m2) = (has_primitive m1 ∨ has_primitive m2)"

text‹Is a match expression equal to the @{const MatchAny} expression?
Only applicable if no primitives are in the expression.›
fun matcheq_matchAny :: "'a match_expr ⇒ bool" where
"matcheq_matchAny MatchAny ⟷ True" |
"matcheq_matchAny (MatchNot m) ⟷ ¬ (matcheq_matchAny m)" |
"matcheq_matchAny (MatchAnd m1 m2) ⟷ matcheq_matchAny m1 ∧ matcheq_matchAny m2" |
"matcheq_matchAny (Match _) = undefined"

fun matcheq_matchNone :: "'a match_expr ⇒ bool" where
"matcheq_matchNone MatchAny = False" |
"matcheq_matchNone (Match _) = False" |
"matcheq_matchNone (MatchNot MatchAny) = True" |
"matcheq_matchNone (MatchNot (Match _)) = False" |
"matcheq_matchNone (MatchNot (MatchNot m)) = matcheq_matchNone m" |
"matcheq_matchNone (MatchNot (MatchAnd m1 m2)) ⟷ matcheq_matchNone (MatchNot m1) ∧ matcheq_matchNone (MatchNot m2)" |
"matcheq_matchNone (MatchAnd m1 m2) ⟷  matcheq_matchNone m1 ∨ matcheq_matchNone m2"

lemma matachAny_matchNone: "¬ has_primitive m ⟹ matcheq_matchAny m ⟷ ¬ matcheq_matchNone m"
by(induction m rule: matcheq_matchNone.induct)(simp_all)

lemma matcheq_matchNone_no_primitive: "¬ has_primitive m ⟹ matcheq_matchNone (MatchNot m) ⟷ ¬ matcheq_matchNone m"
by(induction m rule: matcheq_matchNone.induct) (simp_all)

text‹optimizing match expressions›

fun optimize_matches_option :: "('a match_expr ⇒ 'a match_expr option) ⇒ 'a rule list ⇒ 'a rule list" where
"optimize_matches_option _ [] = []" |
"optimize_matches_option f (Rule m a#rs) = (case f m of None ⇒ optimize_matches_option f rs | Some m ⇒ (Rule m a)#optimize_matches_option f rs)"

lemma optimize_matches_option_simple_ruleset: "simple_ruleset rs ⟹ simple_ruleset (optimize_matches_option f rs)"
proof(induction rs rule:optimize_matches_option.induct)

lemma optimize_matches_option_preserves:
"(⋀ r m. r ∈ set rs ⟹ f (get_match r) = Some m ⟹ P m) ⟹
∀ r ∈ set (optimize_matches_option f rs). P (get_match r)"
apply(induction rs rule: optimize_matches_option.induct)
apply(simp; fail)
apply(simp split: option.split)
by fastforce
(*
lemma optimize_matches_option_preserves':
"∀ m ∈ set rs. P (get_match m) ⟹ ∀m. P m ⟶ (∀m'. f m = Some m' ⟶ P m') ⟹ ∀m ∈ set (optimize_matches_option f rs). P (get_match m)"
using optimize_matches_option_preserves[simplified] by metis
*)
lemma optimize_matches_option_append: "optimize_matches_option f (rs1@rs2) = optimize_matches_option f rs1 @ optimize_matches_option f rs2"
proof(induction rs1 rule: optimize_matches_option.induct)
qed(simp_all split: option.split)

definition optimize_matches :: "('a match_expr ⇒ 'a match_expr) ⇒ 'a rule list ⇒ 'a rule list" where
"optimize_matches f rs =  optimize_matches_option (λm. (if matcheq_matchNone (f m) then None else Some (f m))) rs"

lemma optimize_matches_append: "optimize_matches f (rs1@rs2) = optimize_matches f rs1 @ optimize_matches f rs2"

(*Warning: simplifier loops with this lemma*)
lemma optimize_matches_fst: "optimize_matches f (r#rs) = optimize_matches f [r]@optimize_matches f rs"

lemma optimize_matches_preserves: "(⋀ r. r ∈ set rs ⟹ P (f (get_match r))) ⟹
∀ r ∈ set (optimize_matches f rs). P (get_match r)"
unfolding optimize_matches_def
apply(rule optimize_matches_option_preserves)
by(auto split: if_split_asm)

lemma optimize_matches_simple_ruleset: "simple_ruleset rs ⟹ simple_ruleset (optimize_matches f rs)"

definition optimize_matches_a :: "(action ⇒ 'a match_expr ⇒ 'a match_expr) ⇒ 'a rule list ⇒ 'a rule list" where
"optimize_matches_a f rs = map (λr. Rule (f (get_action r) (get_match r)) (get_action r)) rs"

lemma optimize_matches_a_simple_ruleset: "simple_ruleset rs ⟹ simple_ruleset (optimize_matches_a f rs)"

lemma optimize_matches_a_simple_ruleset_eq:
"simple_ruleset rs ⟹ (⋀ m a. a = Accept ∨ a = Drop ⟹ f1 a m = f2 a m) ⟹ optimize_matches_a f1 rs = optimize_matches_a f2 rs"
apply(induction rs)
done

lemma optimize_matches_a_preserves: "(⋀ r. r ∈ set rs ⟹ P (f (get_action r) (get_match r)))
⟹ ∀ r ∈ set (optimize_matches_a f rs). P (get_match r)"

end


# Theory Semantics

theory Semantics
imports Main Firewall_Common "Common/List_Misc" "HOL-Library.LaTeXsugar"
begin

section‹Big Step Semantics›

text‹
The assumption we apply in general is that the firewall does not alter any packets.
›

text‹A firewall ruleset is a map of chain names
(e.g., INPUT, OUTPUT, FORWARD, arbitrary-user-defined-chain) to a list of rules.
The list of rules is processed sequentially.›
type_synonym 'a ruleset = "string ⇀ 'a rule list"

text‹A matcher (parameterized by the type of primitive @{typ 'a} and packet @{typ 'p})
is a function which just tells whether a given primitive and packet matches.›
type_synonym ('a, 'p) matcher = "'a ⇒ 'p ⇒ bool"

text‹Example: Assume a network packet only has a destination street number
(for simplicity, of type @{typ "nat"}) and we only support the following match expression:
Is the packet's street number within a certain range?
The type for the primitive could then be @{typ "nat × nat"} and a possible implementation
for @{typ "(nat × nat, nat) matcher"} could be
@{term "match_street_number (a,b) p ⟷ p ∈ {a .. b}"}.
Usually, the primitives are a datatype which supports interfaces, IP addresses, protocols,

text‹Given an @{typ "('a, 'p) matcher"} and a match expression, does a packet of type @{typ 'p}
match the match expression?›
fun matches :: "('a, 'p) matcher ⇒ 'a match_expr ⇒ 'p ⇒ bool" where
"matches γ (MatchAnd e1 e2) p ⟷ matches γ e1 p ∧ matches γ e2 p" |
"matches γ (MatchNot me) p ⟷ ¬ matches γ me p" |
"matches γ (Match e) p ⟷ γ e p" |
"matches _ MatchAny _ ⟷ True"

(*Note: "matches γ (MatchNot me) p ⟷ ¬ matches γ me p" does not work for ternary logic.
Here, we have Boolean logic and everything is fine.*)

inductive iptables_bigstep :: "'a ruleset ⇒ ('a, 'p) matcher ⇒ 'p ⇒ 'a rule list ⇒ state ⇒ state ⇒ bool"
("_,_,_⊢ ⟨_, _⟩ ⇒ _"  [60,60,60,20,98,98] 89)
for Γ and γ and p where
skip:    "Γ,γ,p⊢ ⟨[], t⟩ ⇒ t" |
accept:  "matches γ m p ⟹ Γ,γ,p⊢ ⟨[Rule m Accept], Undecided⟩ ⇒ Decision FinalAllow" |
drop:    "matches γ m p ⟹ Γ,γ,p⊢ ⟨[Rule m Drop], Undecided⟩ ⇒ Decision FinalDeny" |
reject:  "matches γ m p ⟹  Γ,γ,p⊢ ⟨[Rule m Reject], Undecided⟩ ⇒ Decision FinalDeny" |
log:     "matches γ m p ⟹ Γ,γ,p⊢ ⟨[Rule m Log], Undecided⟩ ⇒ Undecided" |
(*empty does not do anything to the packet. It could update the internal firewall state, e.g. marking a packet for later-on rate limiting*)
empty:   "matches γ m p ⟹ Γ,γ,p⊢ ⟨[Rule m Empty], Undecided⟩ ⇒ Undecided" |
nomatch: "¬ matches γ m p ⟹ Γ,γ,p⊢ ⟨[Rule m a], Undecided⟩ ⇒ Undecided" |
decision: "Γ,γ,p⊢ ⟨rs, Decision X⟩ ⇒ Decision X" |
seq:      "⟦Γ,γ,p⊢ ⟨rs⇩1, Undecided⟩ ⇒ t; Γ,γ,p⊢ ⟨rs⇩2, t⟩ ⇒ t'⟧ ⟹ Γ,γ,p⊢ ⟨rs⇩1@rs⇩2, Undecided⟩ ⇒ t'" |
call_return:  "⟦ matches γ m p; Γ chain = Some (rs⇩1@[Rule m' Return]@rs⇩2);
matches γ m' p; Γ,γ,p⊢ ⟨rs⇩1, Undecided⟩ ⇒ Undecided ⟧ ⟹
Γ,γ,p⊢ ⟨[Rule m (Call chain)], Undecided⟩ ⇒ Undecided" |
call_result:  "⟦ matches γ m p; Γ chain = Some rs; Γ,γ,p⊢ ⟨rs, Undecided⟩ ⇒ t ⟧ ⟹
Γ,γ,p⊢ ⟨[Rule m (Call chain)], Undecided⟩ ⇒ t"

text‹
The semantic rules again in pretty format:
\begin{center}
@{thm[mode=Axiom] skip [no_vars]}\\[1ex]
@{thm[mode=Rule] accept [no_vars]}\\[1ex]
@{thm[mode=Rule] drop [no_vars]}\\[1ex]
@{thm[mode=Rule] reject [no_vars]}\\[1ex]
@{thm[mode=Rule] log [no_vars]}\\[1ex]
@{thm[mode=Rule] empty [no_vars]}\\[1ex]
@{thm[mode=Rule] nomatch [no_vars]}\\[1ex]
@{thm[mode=Rule] decision [no_vars]}\\[1ex]
@{thm[mode=Rule] seq [no_vars]} \\[1ex]
@{thm[mode=Rule] call_return [no_vars]}\\[1ex]
@{thm[mode=Rule] call_result [no_vars]}
\end{center}
›

(*future work:
Add abstraction function for unknown actions. At the moment, only the explicitly listed actions are supported.
This would also require a @{text "Decision FinalUnknown"} state
Problem: An unknown action may modify a packet.
Assume that we have a firewall which accepts the packets A->B and rewrites the header to A->C.
After that firewall, there is another firewall which only accepts packets for A->C.
A can send through both firewalls.

If our model says that the firewall accepts packets A->B but does not consider packet modification,
A might not be able to pass the second firewall with this model.

Luckily, our model is correct for the filtering behaviour and explicitly does not support any actions with packet modification.
Thus, the described scenario is not a counterexample that our model is wrong but a hint for future features
we may want to support. Luckily, we introduced the @{term "Decision state"}, which should make adding packet modification states easy.
*)

lemma deny:
"matches γ m p ⟹ a = Drop ∨ a = Reject ⟹ iptables_bigstep Γ γ p [Rule m a] Undecided (Decision FinalDeny)"
by (auto intro: drop reject)

lemma seq_cons:
assumes "Γ,γ,p⊢ ⟨[r],Undecided⟩ ⇒ t" and "Γ,γ,p⊢ ⟨rs,t⟩ ⇒ t'"
shows "Γ,γ,p⊢ ⟨r#rs, Undecided⟩ ⇒ t'"
proof -
from assms have "Γ,γ,p⊢ ⟨[r] @ rs, Undecided⟩ ⇒ t'" by (rule seq)
thus ?thesis by simp
qed

lemma iptables_bigstep_induct
[case_names Skip Allow Deny Log Nomatch Decision Seq Call_return Call_result,
induct pred: iptables_bigstep]:
"⟦ Γ,γ,p⊢ ⟨rs,s⟩ ⇒ t;
⋀t. P [] t t;
⋀m a. matches γ m p ⟹ a = Accept ⟹ P [Rule m a] Undecided (Decision FinalAllow);
⋀m a. matches γ m p ⟹ a = Drop ∨ a = Reject ⟹ P [Rule m a] Undecided (Decision FinalDeny);
⋀m a. matches γ m p ⟹ a = Log ∨ a = Empty ⟹ P [Rule m a] Undecided Undecided;
⋀m a. ¬ matches γ m p ⟹ P [Rule m a] Undecided Undecided;
⋀rs X. P rs (Decision X) (Decision X);
⋀rs rs⇩1 rs⇩2 t t'. rs = rs⇩1 @ rs⇩2 ⟹ Γ,γ,p⊢ ⟨rs⇩1,Undecided⟩ ⇒ t ⟹ P rs⇩1 Undecided t ⟹ Γ,γ,p⊢ ⟨rs⇩2,t⟩ ⇒ t' ⟹ P rs⇩2 t t' ⟹ P rs Undecided t';
⋀m a chain rs⇩1 m' rs⇩2. matches γ m p ⟹ a = Call chain ⟹ Γ chain = Some (rs⇩1 @ [Rule m' Return] @ rs⇩2) ⟹ matches γ m' p ⟹ Γ,γ,p⊢ ⟨rs⇩1,Undecided⟩ ⇒ Undecided ⟹ P rs⇩1 Undecided Undecided ⟹ P [Rule m a] Undecided Undecided;
⋀m a chain rs t. matches γ m p ⟹ a = Call chain ⟹ Γ chain = Some rs ⟹ Γ,γ,p⊢ ⟨rs,Undecided⟩ ⇒ t ⟹ P rs Undecided t ⟹ P [Rule m a] Undecided t ⟧ ⟹
P rs s t"
by (induction rule: iptables_bigstep.induct) auto

lemma skipD: "Γ,γ,p⊢ ⟨r, s⟩ ⇒ t ⟹ r = [] ⟹ s = t"
by (induction rule: iptables_bigstep.induct) auto

lemma decisionD: "Γ,γ,p⊢ ⟨r, s⟩ ⇒ t ⟹ s = Decision X ⟹ t = Decision X"
by (induction rule: iptables_bigstep_induct) auto

context
notes skipD[dest] list_app_singletonE[elim]
begin

lemma acceptD: "Γ,γ,p⊢ ⟨r, s⟩ ⇒ t ⟹ r = [Rule m Accept] ⟹ matches γ m p ⟹ s = Undecided ⟹ t = Decision FinalAllow"
by (induction rule: iptables_bigstep.induct) auto

lemma dropD: "Γ,γ,p⊢ ⟨r, s⟩ ⇒ t ⟹ r = [Rule m Drop] ⟹ matches γ m p ⟹ s = Undecided ⟹ t = Decision FinalDeny"
by (induction rule: iptables_bigstep.induct) auto

lemma rejectD: "Γ,γ,p⊢ ⟨r, s⟩ ⇒ t ⟹ r = [Rule m Reject] ⟹ matches γ m p ⟹ s = Undecided ⟹ t = Decision FinalDeny"
by (induction rule: iptables_bigstep.induct) auto

lemma logD: "Γ,γ,p⊢ ⟨r, s⟩ ⇒ t ⟹ r = [Rule m Log] ⟹ matches γ m p ⟹ s = Undecided ⟹ t = Undecided"
by (induction rule: iptables_bigstep.induct) auto

lemma emptyD: "Γ,γ,p⊢ ⟨r, s⟩ ⇒ t ⟹ r = [Rule m Empty] ⟹ matches γ m p ⟹ s = Undecided ⟹ t = Undecided"
by (induction rule: iptables_bigstep.induct) auto

lemma nomatchD: "Γ,γ,p⊢ ⟨r, s⟩ ⇒ t ⟹ r = [Rule m a] ⟹ s = Undecided ⟹ ¬ matches γ m p ⟹ t = Undecided"
by (induction rule: iptables_bigstep.induct) auto

lemma callD:
assumes "Γ,γ,p⊢ ⟨r, s⟩ ⇒ t" "r = [Rule m (Call chain)]" "s = Undecided" "matches γ m p" "Γ chain = Some rs"
obtains "Γ,γ,p⊢ ⟨rs,s⟩ ⇒ t"
| rs⇩1 rs⇩2 m' where "rs = rs⇩1 @ Rule m' Return # rs⇩2" "matches γ m' p" "Γ,γ,p⊢ ⟨rs⇩1,s⟩ ⇒ Undecided" "t = Undecided"
using assms
proof (induction r s t arbitrary: rs rule: iptables_bigstep.induct)
case (seq rs⇩1)
thus ?case by (cases rs⇩1) auto
qed auto

end

lemmas iptables_bigstepD = skipD acceptD dropD rejectD logD emptyD nomatchD decisionD callD

lemma seq':
assumes "rs = rs⇩1 @ rs⇩2" "Γ,γ,p⊢ ⟨rs⇩1,s⟩ ⇒ t" "Γ,γ,p⊢ ⟨rs⇩2,t⟩ ⇒ t'"
shows "Γ,γ,p⊢ ⟨rs,s⟩ ⇒ t'"
using assms by (cases s) (auto intro: seq decision dest: decisionD)

lemma seq'_cons: "Γ,γ,p⊢ ⟨[r],s⟩ ⇒ t ⟹ Γ,γ,p⊢ ⟨rs,t⟩ ⇒ t' ⟹ Γ,γ,p⊢ ⟨r#rs, s⟩ ⇒ t'"
by (metis decision decisionD state.exhaust seq_cons)

lemma seq_split:
assumes "Γ,γ,p⊢ ⟨rs, s⟩ ⇒ t" "rs = rs⇩1@rs⇩2"
obtains t' where "Γ,γ,p⊢ ⟨rs⇩1,s⟩ ⇒ t'" "Γ,γ,p⊢ ⟨rs⇩2,t'⟩ ⇒ t"
using assms
proof (induction rs s t arbitrary: rs⇩1 rs⇩2 thesis rule: iptables_bigstep_induct)
case Allow thus ?case by (cases rs⇩1) (auto intro: iptables_bigstep.intros)
next
case Deny thus ?case by (cases rs⇩1) (auto intro: iptables_bigstep.intros)
next
case Log thus ?case by (cases rs⇩1) (auto intro: iptables_bigstep.intros)
next
case Nomatch thus ?case by (cases rs⇩1) (auto intro: iptables_bigstep.intros)
next
case (Seq rs rsa rsb t t')
hence rs: "rsa @ rsb = rs⇩1 @ rs⇩2" by simp
note List.append_eq_append_conv_if[simp]
from rs show ?case
proof (cases rule: list_app_eq_cases)
case longer
with Seq have t1: "Γ,γ,p⊢ ⟨take (length rsa) rs⇩1, Undecided⟩ ⇒ t"
by simp
from Seq longer obtain t2
where t2a: "Γ,γ,p⊢ ⟨drop (length rsa) rs⇩1,t⟩ ⇒ t2"
and rs2_t2: "Γ,γ,p⊢ ⟨rs⇩2,t2⟩ ⇒ t'"
by blast
with t1 rs2_t2 have "Γ,γ,p⊢ ⟨take (length rsa) rs⇩1 @ drop (length rsa) rs⇩1,Undecided⟩ ⇒ t2"
by (blast intro: iptables_bigstep.seq)
with Seq rs2_t2 show ?thesis
by simp
next
case shorter
with rs have rsa': "rsa = rs⇩1 @ take (length rsa - length rs⇩1) rs⇩2"
by (metis append_eq_conv_conj length_drop)
from shorter rs have rsb': "rsb = drop (length rsa - length rs⇩1) rs⇩2"
by (metis append_eq_conv_conj length_drop)
from Seq rsa' obtain t1
where t1a: "Γ,γ,p⊢ ⟨rs⇩1,Undecided⟩ ⇒ t1"
and t1b: "Γ,γ,p⊢ ⟨take (length rsa - length rs⇩1) rs⇩2,t1⟩ ⇒ t"
by blast
from rsb' Seq.hyps have t2: "Γ,γ,p⊢ ⟨drop (length rsa - length rs⇩1) rs⇩2,t⟩ ⇒ t'"
by blast
with seq' t1b have "Γ,γ,p⊢ ⟨rs⇩2,t1⟩ ⇒ t'"
by fastforce
with Seq t1a show ?thesis
by fast
qed
next
case Call_return
hence "Γ,γ,p⊢ ⟨rs⇩1, Undecided⟩ ⇒ Undecided" "Γ,γ,p⊢ ⟨rs⇩2, Undecided⟩ ⇒ Undecided"
by (case_tac [!] rs⇩1) (auto intro: iptables_bigstep.skip iptables_bigstep.call_return)
thus ?case by fact
next
case (Call_result _ _ _ _ t)
show ?case
proof (cases rs⇩1)
case Nil
with Call_result have "Γ,γ,p⊢ ⟨rs⇩1, Undecided⟩ ⇒ Undecided" "Γ,γ,p⊢ ⟨rs⇩2, Undecided⟩ ⇒ t"
by (auto intro: iptables_bigstep.intros)
thus ?thesis by fact
next
case Cons
with Call_result have "Γ,γ,p⊢ ⟨rs⇩1, Undecided⟩ ⇒ t" "Γ,γ,p⊢ ⟨rs⇩2, t⟩ ⇒ t"
by (auto intro: iptables_bigstep.intros)
thus ?thesis by fact
qed
qed (auto intro: iptables_bigstep.intros)

lemma seqE:
assumes "Γ,γ,p⊢ ⟨rs⇩1@rs⇩2, s⟩ ⇒ t"
obtains ti where "Γ,γ,p⊢ ⟨rs⇩1,s⟩ ⇒ ti" "Γ,γ,p⊢ ⟨rs⇩2,ti⟩ ⇒ t"
using assms by (force elim: seq_split)

lemma seqE_cons:
assumes "Γ,γ,p⊢ ⟨r#rs, s⟩ ⇒ t"
obtains ti where "Γ,γ,p⊢ ⟨[r],s⟩ ⇒ ti" "Γ,γ,p⊢ ⟨rs,ti⟩ ⇒ t"
using assms by (metis append_Cons append_Nil seqE)

lemma nomatch':
assumes "⋀r. r ∈ set rs ⟹ ¬ matches γ (get_match r) p"
shows "Γ,γ,p⊢ ⟨rs, s⟩ ⇒ s"
proof(cases s)
case Undecided
have "∀r∈set rs. ¬ matches γ (get_match r) p ⟹ Γ,γ,p⊢ ⟨rs, Undecided⟩ ⇒ Undecided"
proof(induction rs)
case Nil
thus ?case by (fast intro: skip)
next
case (Cons r rs)
hence "Γ,γ,p⊢ ⟨[r], Undecided⟩ ⇒ Undecided"
by (cases r) (auto intro: nomatch)
with Cons show ?case
by (fastforce intro: seq_cons)
qed
with assms Undecided show ?thesis by simp
qed (blast intro: decision)

text‹there are only two cases when there can be a Return on top-level:

▪ the firewall is in a Decision state
▪ the return does not match

In both cases, it is not applied!
›
lemma no_free_return: assumes "Γ,γ,p⊢ ⟨[Rule m Return], Undecided⟩ ⇒ t" and "matches γ m p" shows "False"
proof -
{ fix a s
have no_free_return_hlp: "Γ,γ,p⊢ ⟨a,s⟩ ⇒ t ⟹ matches γ m p ⟹  s = Undecided ⟹ a = [Rule m Return] ⟹ False"
proof (induction rule: iptables_bigstep.induct)
case (seq rs⇩1)
thus ?case
by (cases rs⇩1) (auto dest: skipD)
qed simp_all
} with assms show ?thesis by blast
qed

(* seq_split is elim, seq_progress is dest *)
lemma seq_progress: "Γ,γ,p⊢ ⟨rs, s⟩ ⇒ t ⟹ rs = rs⇩1@rs⇩2 ⟹ Γ,γ,p⊢ ⟨rs⇩1, s⟩ ⇒ t' ⟹ Γ,γ,p⊢ ⟨rs⇩2, t'⟩ ⇒ t"
proof(induction arbitrary: rs⇩1 rs⇩2 t' rule: iptables_bigstep_induct)
case Allow
thus ?case
by (cases "rs⇩1") (auto intro: iptables_bigstep.intros dest: iptables_bigstepD)
next
case Deny
thus ?case
by (cases "rs⇩1") (auto intro: iptables_bigstep.intros dest: iptables_bigstepD)
next
case Log
thus ?case
by (cases "rs⇩1") (auto intro: iptables_bigstep.intros dest: iptables_bigstepD)
next
case Nomatch
thus ?case
by (cases "rs⇩1") (auto intro: iptables_bigstep.intros dest: iptables_bigstepD)
next
case Decision
thus ?case
by (cases "rs⇩1") (auto intro: iptables_bigstep.intros dest: iptables_bigstepD)
next
case(Seq rs rsa rsb t t' rs⇩1 rs⇩2 t'')
hence rs: "rsa @ rsb = rs⇩1 @ rs⇩2" by simp
note List.append_eq_append_conv_if[simp]
(* TODO larsrh custom case distinction rule *)

from rs show "Γ,γ,p⊢ ⟨rs⇩2,t''⟩ ⇒ t'"
proof(cases rule: list_app_eq_cases)
case longer
have "rs⇩1 = take (length rsa) rs⇩1 @ drop (length rsa) rs⇩1"
by auto
with Seq longer show ?thesis
by (metis append_Nil2 skipD seq_split)
next
case shorter
with Seq(7) Seq.hyps(3) Seq.IH(1) rs show ?thesis
by (metis seq' append_eq_conv_conj)
qed
next
case(Call_return m a chain rsa m' rsb)
have xx: "Γ,γ,p⊢ ⟨[Rule m (Call chain)], Undecided⟩ ⇒ t' ⟹ matches γ m p ⟹
Γ chain = Some (rsa @ Rule m' Return # rsb) ⟹
matches γ m' p ⟹
Γ,γ,p⊢ ⟨rsa, Undecided⟩ ⇒ Undecided ⟹
t' = Undecided"
apply(erule callD)
apply(simp_all)
apply(erule seqE)
apply(erule seqE_cons)
by (metis Call_return.IH no_free_return self_append_conv skipD)

show ?case
proof (cases rs⇩1)
case (Cons r rs)
thus ?thesis
using Call_return
apply(case_tac "[Rule m a] = rs⇩2")
apply(simp)
apply(simp)
using xx by blast
next
case Nil
moreover hence "t' = Undecided"
by (metis Call_return.hyps(1) Call_return.prems(2) append.simps(1) decision no_free_return seq state.exhaust)
moreover have "⋀m. Γ,γ,p⊢ ⟨[Rule m a], Undecided⟩ ⇒ Undecided"
by (metis (no_types) Call_return(2) Call_return.hyps(3) Call_return.hyps(4) Call_return.hyps(5) call_return nomatch)
ultimately show ?thesis
using Call_return.prems(1) by auto
qed
next
case(Call_result m a chain rs t)
thus ?case
proof (cases rs⇩1)
case Cons
thus ?thesis
using Call_result
apply(auto simp add: iptables_bigstep.skip iptables_bigstep.call_result dest: skipD)
apply(drule callD, simp_all)
apply blast
by (metis Cons_eq_appendI append_self_conv2 no_free_return seq_split)
qed (fastforce intro: iptables_bigstep.intros dest: skipD)
qed (auto dest: iptables_bigstepD)

theorem iptables_bigstep_deterministic: assumes "Γ,γ,p⊢ ⟨rs, s⟩ ⇒ t" and "Γ,γ,p⊢ ⟨rs, s⟩ ⇒ t'" shows "t = t'"
proof -
{ fix r1 r2 m t
assume a1: "Γ,γ,p⊢ ⟨r1 @ Rule m Return # r2, Undecided⟩ ⇒ t" and a2: "matches γ m p" and a3: "Γ,γ,p⊢ ⟨r1,Undecided⟩ ⇒ Undecided"
have False
proof -
from a1 a3 have "Γ,γ,p⊢ ⟨Rule m Return # r2, Undecided⟩ ⇒ t"
by (blast intro: seq_progress)
hence "Γ,γ,p⊢ ⟨[Rule m Return] @ r2, Undecided⟩ ⇒ t"
by simp
from seqE[OF this] obtain ti where "Γ,γ,p⊢ ⟨[Rule m Return], Undecided⟩ ⇒ ti" by blast
with no_free_return a2 show False by fast (*by (blast intro: no_free_return elim: seq_split)*)
qed
} note no_free_return_seq=this

from assms show ?thesis
proof (induction arbitrary: t' rule: iptables_bigstep_induct)
case Seq
thus ?case
by (metis seq_progress)
next
case Call_result
thus ?case
by (metis no_free_return_seq callD)
next
case Call_return
thus ?case
by (metis append_Cons callD no_free_return_seq)
qed (auto dest: iptables_bigstepD)
qed

lemma iptables_bigstep_to_undecided: "Γ,γ,p⊢ ⟨rs, s⟩ ⇒ Undecided ⟹ s = Undecided"
by (metis decisionD state.exhaust)

lemma iptables_bigstep_to_decision: "Γ,γ,p⊢ ⟨rs, Decision Y⟩ ⇒ Decision X ⟹ Y = X"
by (metis decisionD state.inject)

lemma Rule_UndecidedE:
assumes "Γ,γ,p⊢ ⟨[Rule m a], Undecided⟩ ⇒ Undecided"
obtains (nomatch) "¬ matches γ m p"
| (log) "a = Log ∨ a = Empty"
| (call) c where "a = Call c" "matches γ m p"
using assms
proof (induction "[Rule m a]" Undecided Undecided rule: iptables_bigstep_induct)
case Seq
thus ?case
by (metis append_eq_Cons_conv append_is_Nil_conv iptables_bigstep_to_undecided)
qed simp_all

lemma Rule_DecisionE:
assumes "Γ,γ,p⊢ ⟨[Rule m a], Undecided⟩ ⇒ Decision X"
obtains (call) chain where "matches γ m p" "a = Call chain"
| (accept_reject) "matches γ m p" "X = FinalAllow ⟹ a = Accept" "X = FinalDeny ⟹ a = Drop ∨ a = Reject"
using assms
proof (induction "[Rule m a]" Undecided "Decision X" rule: iptables_bigstep_induct)
case (Seq rs⇩1)
thus ?case
by (cases rs⇩1) (auto dest: skipD)
qed simp_all

lemma log_remove:
assumes "Γ,γ,p⊢ ⟨rs⇩1 @ [Rule m Log] @ rs⇩2, s⟩ ⇒ t"
shows "Γ,γ,p⊢ ⟨rs⇩1 @ rs⇩2, s⟩ ⇒ t"
proof -
from assms obtain t' where t': "Γ,γ,p⊢ ⟨rs⇩1, s⟩ ⇒ t'" "Γ,γ,p⊢ ⟨[Rule m Log] @ rs⇩2, t'⟩ ⇒ t"
by (blast elim: seqE)
hence "Γ,γ,p⊢ ⟨Rule m Log # rs⇩2, t'⟩ ⇒ t"
by simp
then obtain t'' where "Γ,γ,p⊢ ⟨[Rule m Log], t'⟩ ⇒ t''" "Γ,γ,p⊢ ⟨rs⇩2, t''⟩ ⇒ t"
by (blast elim: seqE_cons)
with t' show ?thesis
by (metis state.exhaust iptables_bigstep_deterministic decision log nomatch seq)
qed
lemma empty_empty:
assumes "Γ,γ,p⊢ ⟨rs⇩1 @ [Rule m Empty] @ rs⇩2, s⟩ ⇒ t"
shows "Γ,γ,p⊢ ⟨rs⇩1 @ rs⇩2, s⟩ ⇒ t"
proof -
from assms obtain t' where t': "Γ,γ,p⊢ ⟨rs⇩1, s⟩ ⇒ t'" "Γ,γ,p⊢ ⟨[Rule m Empty] @ rs⇩2, t'⟩ ⇒ t"
by (blast elim: seqE)
hence "Γ,γ,p⊢ ⟨Rule m Empty # rs⇩2, t'⟩ ⇒ t"
by simp
then obtain t'' where "Γ,γ,p⊢ ⟨[Rule m Empty], t'⟩ ⇒ t''" "Γ,γ,p⊢ ⟨rs⇩2, t''⟩ ⇒ t"
by (blast elim: seqE_cons)
with t' show ?thesis
by (metis state.exhaust iptables_bigstep_deterministic decision empty nomatch seq)
qed

lemma Unknown_actions_False: "Γ,γ,p⊢ ⟨r # rs, Undecided⟩ ⇒ t ⟹ r = Rule m a ⟹ matches γ m p ⟹ a = Unknown ∨ (∃chain. a = Goto chain) ⟹ False"
proof -
have 1: "Γ,γ,p⊢ ⟨[Rule m Unknown], Undecided⟩ ⇒ t ⟹ matches γ m p ⟹ False"
by (induction "[Rule m Unknown]" Undecided t rule: iptables_bigstep.induct)
(auto elim: list_app_singletonE dest: skipD)

{ fix chain
have "Γ,γ,p⊢ ⟨[Rule m (Goto chain)], Undecided⟩ ⇒ t ⟹ matches γ m p ⟹ False"
by (induction "[Rule m (Goto chain)]" Undecided t rule: iptables_bigstep.induct)
(auto elim: list_app_singletonE dest: skipD)
}note 2=this
show "Γ,γ,p⊢ ⟨r # rs, Undecided⟩ ⇒ t ⟹ r = Rule m a ⟹ matches γ m p ⟹ a = Unknown ∨ (∃chain. a = Goto chain) ⟹ False"
apply(erule seqE_cons)
apply(case_tac ti)
apply(simp_all)
using Rule_UndecidedE apply fastforce
by (metis "1" "2" decision iptables_bigstep_deterministic)
qed

text‹
The notation we prefer in the paper. The semantics are defined for fixed ‹Γ› and ‹γ›
›
locale iptables_bigstep_fixedbackground =
fixes Γ::"'a ruleset"
and γ::"('a, 'p) matcher"
begin

inductive iptables_bigstep' :: "'p ⇒ 'a rule list ⇒ state ⇒ state ⇒ bool"
("_⊢'' ⟨_, _⟩ ⇒ _"  [60,20,98,98] 89)
for p where
skip:    "p⊢' ⟨[], t⟩ ⇒ t" |
accept:  "matches γ m p ⟹ p⊢' ⟨[Rule m Accept], Undecided⟩ ⇒ Decision FinalAllow" |
drop:    "matches γ m p ⟹ p⊢' ⟨[Rule m Drop], Undecided⟩ ⇒ Decision FinalDeny" |
reject:  "matches γ m p ⟹  p⊢' ⟨[Rule m Reject], Undecided⟩ ⇒ Decision FinalDeny" |
log:     "matches γ m p ⟹ p⊢' ⟨[Rule m Log], Undecided⟩ ⇒ Undecided" |
empty:   "matches γ m p ⟹ p⊢' ⟨[Rule m Empty], Undecided⟩ ⇒ Undecided" |
nomatch: "¬ matches γ m p ⟹ p⊢' ⟨[Rule m a], Undecided⟩ ⇒ Undecided" |
decision: "p⊢' ⟨rs, Decision X⟩ ⇒ Decision X" |
seq:      "⟦p⊢' ⟨rs⇩1, Undecided⟩ ⇒ t; p⊢' ⟨rs⇩2, t⟩ ⇒ t'⟧ ⟹ p⊢' ⟨rs⇩1@rs⇩2, Undecided⟩ ⇒ t'" |
call_return:  "⟦ matches γ m p; Γ chain = Some (rs⇩1@[Rule m' Return]@rs⇩2);
matches γ m' p; p⊢' ⟨rs⇩1, Undecided⟩ ⇒ Undecided ⟧ ⟹
p⊢' ⟨[Rule m (Call chain)], Undecided⟩ ⇒ Undecided" |
call_result:  "⟦ matches γ m p; p⊢' ⟨the (Γ chain), Undecided⟩ ⇒ t ⟧ ⟹
p⊢' ⟨[Rule m (Call chain)], Undecided⟩ ⇒ t"

definition wf_Γ:: "'a rule list ⇒ bool" where
"wf_Γ rs ≡ ∀rsg ∈ ran Γ ∪ {rs}. (∀r ∈ set rsg. ∀ chain. get_action r = Call chain ⟶ Γ chain ≠ None)"

lemma wf_Γ_append: "wf_Γ (rs1@rs2) ⟷ wf_Γ rs1 ∧ wf_Γ rs2"
lemma wf_Γ_tail: "wf_Γ (r # rs) ⟹ wf_Γ rs" by(simp add: wf_Γ_def)
lemma wf_Γ_Call: "wf_Γ [Rule m (Call chain)] ⟹ wf_Γ (the (Γ chain)) ∧ (∃rs. Γ chain = Some rs)"
by (metis option.collapse ranI)

lemma "wf_Γ rs ⟹ p⊢' ⟨rs, s⟩ ⇒ t ⟷ Γ,γ,p⊢ ⟨rs, s⟩ ⇒ t"
apply(rule iffI)
apply(rotate_tac 1)
apply(induction rs s t rule: iptables_bigstep'.induct)
apply(auto intro: iptables_bigstep.intros simp: wf_Γ_append dest!: wf_Γ_Call)[11]
apply(rotate_tac 1)
apply(induction rs s t rule: iptables_bigstep.induct)
apply(auto intro: iptables_bigstep'.intros simp: wf_Γ_append dest!: wf_Γ_Call)[11]
done

end

text‹Showing that semantics are defined.
For rulesets which can be loaded by the Linux kernel. The kernel does not allow loops.›

text‹
We call a ruleset well-formed (wf) iff all @{const Call}s are into actually existing chains.
›
definition wf_chain :: "'a ruleset ⇒ 'a rule list ⇒ bool" where
"wf_chain Γ rs ≡ (∀r ∈ set rs. ∀ chain. get_action r = Call chain ⟶ Γ chain ≠ None)"
lemma wf_chain_append: "wf_chain Γ (rs1@rs2) ⟷ wf_chain Γ rs1 ∧ wf_chain Γ rs2"

lemma wf_chain_fst: "wf_chain Γ (r # rs) ⟹  wf_chain Γ (rs)"

text‹This is what our tool will check at runtime›
definition sanity_wf_ruleset :: "(string × 'a rule list) list ⇒ bool" where
"sanity_wf_ruleset Γ ≡ distinct (map fst Γ) ∧
(∀ rs ∈ ran (map_of Γ). (∀r ∈ set rs. case get_action r of Accept ⇒ True
| Drop ⇒ True
| Reject ⇒ True
| Log ⇒ True
| Empty ⇒ True
| Call chain ⇒ chain ∈ dom (map_of Γ)
| Goto chain ⇒ chain ∈ dom (map_of Γ)
| Return ⇒ True
| _ ⇒ False))"

lemma sanity_wf_ruleset_wf_chain: "sanity_wf_ruleset Γ ⟹ rs ∈ ran (map_of Γ) ⟹ wf_chain (map_of Γ) rs"
by fastforce

lemma sanity_wf_ruleset_start: "sanity_wf_ruleset Γ ⟹ chain_name ∈ dom (map_of Γ) ⟹
default_action = Accept ∨ default_action = Drop ⟹
wf_chain (map_of Γ) [Rule MatchAny (Call chain_name), Rule MatchAny default_action]"
apply(safe)
apply(simp_all)
apply blast+
done

lemma [code]: "sanity_wf_ruleset Γ =
(let dom = map fst Γ;
ran = map snd Γ
in distinct dom ∧
(∀ rs ∈ set ran. (∀r ∈ set rs. case get_action r of Accept ⇒ True
| Drop ⇒ True
| Reject ⇒ True
| Log ⇒ True
| Empty ⇒ True
| Call chain ⇒ chain ∈ set dom
| Goto chain ⇒ chain ∈ set dom
| Return ⇒ True
| _ ⇒ False)))"
proof -
have set_map_fst: "set (map fst Γ) = dom (map_of Γ)"
have set_map_snd: "distinct (map fst Γ) ⟹ set (map snd Γ) = ran (map_of Γ)"
show ?thesis
unfolding sanity_wf_ruleset_def Let_def
apply(subst set_map_fst)+
apply(rule iffI)
apply(elim conjE)
apply(subst set_map_snd)
apply(simp)
apply(simp)
apply(elim conjE)
apply(subst(asm) set_map_snd)
apply(simp_all)
done
qed

lemma semantics_bigstep_defined1: assumes "∀rsg ∈ ran Γ ∪ {rs}. wf_chain Γ rsg"
and "∀rsg ∈ ran Γ ∪ {rs}. ∀ r ∈ set rsg. (∀chain. get_action r ≠ Goto chain) ∧ get_action r ≠ Unknown"
and "∀ r ∈ set rs. get_action r ≠ Return" (*no toplevel return*)
and "(∀name ∈ dom Γ. ∃t. Γ,γ,p⊢ ⟨the (Γ name), Undecided⟩ ⇒ t)" (*defined for all chains in the background ruleset*)
shows "∃t. Γ,γ,p⊢ ⟨rs, s⟩ ⇒ t"
using assms proof(induction rs)
case Nil thus ?case
apply(rule_tac x=s in exI)
next
case (Cons r rs)
from Cons.prems Cons.IH obtain t' where t': "Γ,γ,p⊢ ⟨rs, s⟩ ⇒ t'"
apply simp
apply(elim conjE)
by blast

obtain m a where r: "r = Rule m a" by(cases r) blast

show ?case
proof(cases "matches γ m p")
case False
hence "Γ,γ,p⊢ ⟨[r], s⟩ ⇒ s"
apply(cases s)
thus ?thesis
apply(rule_tac x=t' in exI)
apply(rule_tac t=s in seq'_cons)
apply assumption
using t' by(simp)
next
case True
show ?thesis
proof(cases s)
case (Decision X) thus ?thesis
apply(rule_tac x="Decision X" in exI)
next
case Undecided
have "∃t. Γ,γ,p⊢ ⟨Rule m a # rs, Undecided⟩ ⇒ t"
proof(cases a)
case Accept with True show ?thesis
apply(rule_tac x="Decision FinalAllow" in exI)
apply(rule_tac t="Decision FinalAllow" in seq'_cons)
by(auto intro: iptables_bigstep.intros)
next
case Drop with True show ?thesis
apply(rule_tac x="Decision FinalDeny" in exI)
apply(rule_tac t="Decision FinalDeny" in seq'_cons)
by(auto intro: iptables_bigstep.intros)
next
case Log with True t' Undecided show ?thesis
apply(rule_tac x=t' in exI)
apply(rule_tac t=Undecided in seq'_cons)
by(auto intro: iptables_bigstep.intros)
next
case Reject with True show ?thesis
apply(rule_tac x="Decision FinalDeny" in exI)
apply(rule_tac t="Decision FinalDeny" in seq'_cons)
by(auto intro: iptables_bigstep.intros)[2]
next
case Return with Cons.prems(3)[simplified r] show ?thesis by simp
next
case Goto with Cons.prems(2)[simplified r] show ?thesis by auto
next
case (Call chain_name)
from Call Cons.prems(1) obtain rs' where 1: "Γ chain_name = Some rs'" by(simp add: r wf_chain_def) blast
with Cons.prems(4) obtain t'' where 2: "Γ,γ,p⊢ ⟨the (Γ chain_name), Undecided⟩ ⇒ t''" by blast
from 1 2 True have "Γ,γ,p⊢ ⟨[Rule m (Call chain_name)], Undecided⟩ ⇒ t''" by(auto dest: call_result)
with Call t' Undecided show ?thesis
apply(cases t'')
apply simp
apply(rule_tac x=t' in exI)
apply(rule_tac t=Undecided in seq'_cons)
apply(auto intro: iptables_bigstep.intros)[2]
apply(simp)
apply(rule_tac x=t'' in exI)
apply(rule_tac t=t'' in seq'_cons)
apply(auto intro: iptables_bigstep.intros)
done
next
case Empty  with True t' Undecided show ?thesis
apply(rule_tac x=t' in exI)
apply(rule_tac t=Undecided in seq'_cons)
by(auto intro: iptables_bigstep.intros)
next
case Unknown with Cons.prems(2)[simplified r] show ?thesis by(simp)
qed
thus ?thesis
unfolding r Undecided by simp
qed
qed
qed

text‹Showing the main theorem›

context
begin
private lemma iptables_bigstep_defined_if_singleton_rules:
"∀ r ∈ set rs. (∃t. Γ,γ,p⊢ ⟨[r], s⟩ ⇒ t) ⟹ ∃t. Γ,γ,p⊢ ⟨rs, s⟩ ⇒ t"
proof(induction rs arbitrary: s)
case Nil hence "Γ,γ,p⊢ ⟨[], s⟩ ⇒ s" by(simp add: skip)
thus ?case by blast
next
case(Cons r rs s)
from Cons.prems obtain t where t: "Γ,γ,p⊢ ⟨[r], s⟩ ⇒ t" by simp blast
with Cons show ?case
proof(cases t)
case Decision with t show ?thesis by (meson decision seq'_cons)
next
case Undecided
from Cons obtain t' where t': "Γ,γ,p⊢ ⟨rs, s⟩ ⇒ t'" by simp blast
with Undecided t show ?thesis
apply(rule_tac x=t' in exI)
apply(rule seq'_cons)
apply(simp)
using iptables_bigstep_to_undecided by fastforce
qed
qed

text‹well founded relation.›
definition calls_chain :: "'a ruleset ⇒ (string × string) set" where
"calls_chain Γ = {(r, s). case Γ r of Some rs ⇒ ∃m. Rule m (Call s) ∈ set rs | None ⇒ False}"

lemma calls_chain_def2: "calls_chain Γ = {(caller, callee). ∃rs m. Γ caller = Some rs ∧ Rule m (Call callee) ∈ set rs}"
unfolding calls_chain_def
apply(safe)
apply(simp split: option.split_asm)
apply(simp)
by blast

text‹example›
private lemma "calls_chain [
''FORWARD'' ↦ [(Rule m1 Log), (Rule m2 (Call ''foo'')), (Rule m3 Accept), (Rule m' (Call ''baz''))],
''foo'' ↦ [(Rule m4 Log), (Rule m5 Return), (Rule m6 (Call ''bar''))],
''bar'' ↦ [],
''baz'' ↦ []] =
{(''FORWARD'', ''foo''), (''FORWARD'', ''baz''), (''foo'', ''bar'')}"
unfolding calls_chain_def by(auto split: option.split_asm if_split_asm)

private lemma "wf (calls_chain [
''FORWARD'' ↦ [(Rule m1 Log), (Rule m2 (Call ''foo'')), (Rule m3 Accept), (Rule m' (Call ''baz''))],
''foo'' ↦ [(Rule m4 Log), (Rule m5 Return), (Rule m6 (Call ''bar''))],
''bar'' ↦ [],
''baz'' ↦ []])"
proof -
have g: "calls_chain [''FORWARD'' ↦ [(Rule m1 Log), (Rule m2 (Call ''foo'')), (Rule m3 Accept), (Rule m' (Call ''baz''))],
''foo'' ↦ [(Rule m4 Log), (Rule m5 Return), (Rule m6 (Call ''bar''))],
''bar'' ↦ [],
''baz'' ↦ []] = {(''FORWARD'', ''foo''), (''FORWARD'', ''baz''), (''foo'', ''bar'')}"
by(auto simp add: calls_chain_def split: option.split_asm if_split_asm)
show ?thesis
unfolding g
apply(simp)
apply safe
apply(erule rtranclE, simp_all)
apply(erule rtranclE, simp_all)
done
qed

text‹In our proof, we will need the reverse.›
private definition called_by_chain :: "'a ruleset ⇒ (string × string) set" where
"called_by_chain Γ = {(callee, caller). case Γ caller of Some rs ⇒ ∃m. Rule m (Call callee) ∈ set rs | None ⇒ False}"
private lemma called_by_chain_converse: "calls_chain Γ = converse (called_by_chain Γ)"
by blast
private lemma wf_called_by_chain: "finite (calls_chain Γ) ⟹ wf (calls_chain Γ) ⟹ wf (called_by_chain Γ)"
apply(frule Wellfounded.wf_acyclic)
apply(drule(1) Wellfounded.finite_acyclic_wf_converse)
done

private lemma helper_cases_call_subchain_defined_or_return:
"(∀x∈ran Γ. wf_chain Γ x) ⟹
∀rsg∈ran Γ. ∀r∈set rsg. (∀chain. get_action r ≠ Goto chain) ∧ get_action r ≠ Unknown ⟹
∀y m. ∀r∈set rs_called. r = Rule m (Call y) ⟶ (∃t. Γ,γ,p⊢ ⟨[Rule m (Call y)], Undecided⟩ ⇒ t) ⟹
wf_chain Γ rs_called ⟹
∀r∈set rs_called. (∀chain. get_action r ≠ Goto chain) ∧ get_action r ≠ Unknown ⟹
(∃t. Γ,γ,p⊢ ⟨rs_called, Undecided⟩ ⇒ t) ∨
(∃rs_called1 rs_called2 m'.
rs_called = (rs_called1 @ [Rule m' Return] @ rs_called2) ∧
matches γ m' p ∧ Γ,γ,p⊢ ⟨rs_called1, Undecided⟩ ⇒ Undecided)"
proof(induction rs_called arbitrary:)
case Nil hence "∃t. Γ,γ,p⊢ ⟨[], Undecided⟩ ⇒ t"
apply(rule_tac x=Undecided in exI)
thus ?case by simp
next
case (Cons r rs)
from Cons.prems have "wf_chain Γ [r]" by(simp add: wf_chain_def)
from Cons.prems have IH:"(∃t'. Γ,γ,p⊢ ⟨rs, Undecided⟩ ⇒ t') ∨
(∃rs_called1 rs_called2 m'.
rs = (rs_called1 @ [Rule m' Return] @ rs_called2) ∧
matches γ m' p ∧ Γ,γ,p⊢ ⟨rs_called1, Undecided⟩ ⇒ Undecided)"
apply -
apply(rule Cons.IH)
apply(auto dest: wf_chain_fst)
done

from Cons.prems have case_call: "r = Rule m (Call y) ⟹ (∃t. Γ,γ,p⊢ ⟨[Rule m (Call y)], Undecided⟩ ⇒ t)" for y m
by(simp)

obtain m a where r: "r = Rule m a" by(cases r) simp

from Cons.prems have a_not: "(∀chain. a ≠ Goto chain) ∧ a ≠ Unknown" by(simp add: r)

have ex_neq_ret: "a ≠ Return ⟹ ∃t. Γ,γ,p⊢ ⟨[Rule m a], Undecided⟩ ⇒ t"
proof(cases "matches γ m p")
case False thus ?thesis by(rule_tac x=Undecided in exI)(simp add: nomatch; fail)
next
case True
assume "a ≠ Return"
show ?thesis
proof(cases a)
case Accept with True show ?thesis
by(rule_tac x="Decision FinalAllow" in exI) (simp add: accept; fail)
next
case Drop with True show ?thesis
by(rule_tac x="Decision FinalDeny" in exI) (simp add: drop; fail)
next
case Log with True show ?thesis
by(rule_tac x="Undecided" in exI)(simp add: log; fail)
next
case Reject with True show ?thesis
by(rule_tac x="Decision FinalDeny" in exI) (simp add: reject; fail)
next
case Call with True show ?thesis
apply(simp)
apply(rule case_call)
done
next
case Empty with True show ?thesis by(rule_tac x="Undecided" in exI) (simp add: empty; fail)
next
case Return with ‹a ≠ Return› show ?thesis by simp
qed

have *: "?case"
if pre: "rs = rs_called1 @ Rule m' Return # rs_called2 ∧ matches γ m' p ∧ Γ,γ,p⊢ ⟨rs_called1, Undecided⟩ ⇒ Undecided"
for rs_called1 m' rs_called2
proof(cases "matches γ m p")
case False thus ?thesis
apply -
apply(rule disjI2)
apply(rule_tac x="r#rs_called1" in exI)
apply(rule_tac x=rs_called2 in exI)
apply(rule_tac x=m' in exI)
apply(rule_tac t=Undecided in seq_cons)
done
next
case True
from pre have rule_case_dijs1: "∃X. Γ,γ,p⊢ ⟨[Rule m a], Undecided⟩ ⇒ Decision X ⟹ ?thesis"
apply -
apply(rule disjI1)
apply(elim exE conjE, rename_tac X)
apply(simp)
apply(rule_tac x="Decision X" in exI)
apply(rule_tac t="Decision X" in seq_cons)
done

from pre have rule_case_dijs2: "Γ,γ,p⊢ ⟨[Rule m a], Undecided⟩ ⇒ Undecided ⟹ ?thesis"
apply -
apply(rule disjI2)
apply(rule_tac x="r#rs_called1" in exI)
apply(rule_tac x=rs_called2 in exI)
apply(rule_tac x=m' in exI)
apply(rule_tac t=Undecided in seq_cons)
apply(simp; fail)
apply(simp;fail)
done

show ?thesis
proof(cases a)
case Accept show ?thesis
apply(rule rule_case_dijs1)
apply(rule_tac x="FinalAllow" in exI)
using True pre Accept by(simp add: accept)
next
case Drop show ?thesis
apply(rule rule_case_dijs1)
apply(rule_tac x="FinalDeny" in exI)
using True Drop by(simp add: deny)
next
case Log show ?thesis
apply(rule rule_case_dijs2)
using Log True by(simp add: log)
next
case Reject show ?thesis
apply(rule rule_case_dijs1)
apply(rule_tac x="FinalDeny" in exI)
using Reject True by(simp add: reject)
next
case (Call x5)
have "∃t. Γ,γ,p⊢ ⟨[Rule m (Call x5)], Undecided⟩ ⇒ t" by(rule case_call) (simp add: r Call)
with Call pre True show ?thesis
apply(simp)
apply(elim exE, rename_tac t_called)
apply(case_tac t_called)
apply(simp)
apply(rule disjI2)
apply(rule_tac x="r#rs_called1" in exI)
apply(rule_tac x=rs_called2 in exI)
apply(rule_tac x=m' in exI)
apply(rule_tac t=Undecided in seq_cons)
apply(simp; fail)
apply(rule disjI1)
apply(rule_tac x=t_called in exI)
apply(rule_tac t=t_called in seq_cons)
done
next
case Empty show ?thesis
apply(rule rule_case_dijs2)
using Empty True by(simp add: pre empty)
next
case Return show ?thesis
apply(rule disjI2)
apply(rule_tac x="[]" in exI)
apply(rule_tac x="rs_called1 @ Rule m' Return # rs_called2" in exI)
apply(rule_tac x=m in exI)
using Return True pre by(simp add: skip r)
qed

from IH have **: "a ≠ Return ⟶ (∃t. Γ,γ,p⊢ ⟨[Rule m a], Undecided⟩ ⇒ t) ⟹ ?case"
proof(elim disjE, goal_cases)
case 2
from this obtain rs_called1 m' rs_called2 where
a1: "rs = rs_called1 @ [Rule m' Return] @ rs_called2" and
a2: "matches γ m' p" and a3: "Γ,γ,p⊢ ⟨rs_called1, Undecided⟩ ⇒ Undecided" by blast
show ?case
apply(rule *)
using a1 a2 a3 by simp
next
case 1 thus ?case
proof(cases "a ≠ Return")
case True
with 1 obtain t1 t2 where t1: "Γ,γ,p⊢ ⟨[Rule m a], Undecided⟩ ⇒ t1"
and t2: "Γ,γ,p⊢ ⟨rs, Undecided⟩ ⇒ t2" by blast
from t1 t2 show ?thesis
apply -
apply(rule disjI1)
apply(cases t1)
apply(simp_all)
apply(rule_tac x=t2 in exI)
apply(rule_tac seq'_cons)
apply(simp_all)
apply (meson decision seq_cons)
done
next
case False show ?thesis
proof(cases "matches γ m p")
assume "¬ matches γ m p" with 1 show ?thesis
apply -
apply(rule disjI1)
apply(elim exE)
apply(rename_tac t')
apply(rule_tac x=t' in exI)
apply(rule_tac t=Undecided in seq_cons)
by(simp)
next
assume "matches γ m p" with False show ?thesis
apply -
apply(rule disjI2)
apply(rule_tac x="[]" in exI)
apply(rule_tac x=rs in exI)
apply(rule_tac x=m in exI)
done
qed
qed
qed
thus ?case using ex_neq_ret by blast
qed

lemma helper_defined_single:
assumes "wf (called_by_chain Γ)"
and "∀rsg ∈ ran Γ ∪ {[Rule m a]}. wf_chain Γ rsg"
and "∀rsg ∈ ran Γ ∪ {[Rule m a]}. ∀ r ∈ set rsg. (¬(∃chain. get_action r = Goto chain)) ∧ get_action r ≠ Unknown"
and "a ≠ Return" (*no toplevel Return*)
shows "∃t. Γ,γ,p⊢ ⟨[Rule m a], s⟩ ⇒ t"
proof(cases s)
case (Decision decision) thus ?thesis
apply(rule_tac x="Decision decision" in exI)
apply(simp)
using iptables_bigstep.decision by fast
next
case Undecided
have "∃t. Γ,γ,p⊢ ⟨[Rule m a], Undecided⟩ ⇒ t"
proof(cases "matches γ m p")
case False with assms show ?thesis
apply(rule_tac x=Undecided in exI)
apply(rule_tac t=Undecided in seq'_cons)
apply (metis empty_iff empty_set insert_iff list.simps(15) nomatch' rule.sel(1))
done
next
case True
show ?thesis
proof(cases a)
case Unknown with assms(3) show ?thesis by simp
next
case Goto with assms(3) show ?thesis by auto
next
case Accept with True show ?thesis by(auto intro: iptables_bigstep.intros)
next
case Drop with True show ?thesis by(auto intro: iptables_bigstep.intros)
next
case Reject with True show ?thesis by(auto intro: iptables_bigstep.intros)
next
case Log with True show ?thesis by(auto intro: iptables_bigstep.intros)
next
case Empty with True show ?thesis by(auto intro: iptables_bigstep.intros)
next
case Return with assms show ?thesis by simp
next
case (Call chain_name)
thm wf_induct_rule[where r="(calls_chain Γ)" and P="λx. ∃t. Γ,γ,p⊢ ⟨[Rule m (Call x)], Undecided⟩ ⇒ t"]
― ‹Only the assumptions we will need›
from assms have "wf (called_by_chain Γ)"
"∀rsg∈ran Γ. wf_chain Γ rsg"
"∀rsg∈ran Γ. ∀r∈set rsg. (∀chain. get_action r ≠ Goto chain) ∧ get_action r ≠ Unknown" by auto
― ‹strengthening the IH to do a well-founded induction›
hence "matches γ m p ⟹ wf_chain Γ [Rule m (Call chain_name)] ⟹ (∃t. Γ,γ,p⊢ ⟨[Rule m (Call chain_name)], Undecided⟩ ⇒ t)"
proof(induction arbitrary: m rule: wf_induct_rule[where r="called_by_chain Γ"])
case (less chain_name_neu)
from less.prems have "Γ chain_name_neu ≠ None" by(simp add: wf_chain_def)
from this obtain rs_called where rs_called: "Γ chain_name_neu = Some rs_called" by blast

from less rs_called have "wf_chain Γ rs_called" by (simp add: ranI)
from less rs_called have "rs_called ∈ ran Γ" by (simp add: ranI)

(*get good IH*)
from less.prems rs_called have
"∀y m. ∀r ∈ set rs_called. r = Rule m (Call y) ⟶ (y, chain_name_neu) ∈ called_by_chain Γ ∧ wf_chain Γ [Rule m (Call y)]"
apply(simp)
apply(intro impI allI conjI)
apply blast
apply (meson ranI rule.sel(2))
done
with less have "∀y m. ∀r∈set rs_called. r = Rule m (Call y) ⟶ (∃t. Γ,γ,p⊢ ⟨[Rule m (Call y)], Undecided⟩ ⇒ t)"
apply(intro allI, rename_tac y my)
apply(case_tac "matches γ my p")
apply blast
apply(intro ballI impI)
apply(rule_tac x=Undecided in exI)
done
from less.prems(4) rs_called ‹rs_called ∈ ran Γ›
helper_cases_call_subchain_defined_or_return[OF less.prems(3) less.prems(4) this ‹wf_chain Γ rs_called›] have
"(∃t. Γ,γ,p⊢ ⟨rs_called, Undecided⟩ ⇒ t) ∨
(∃rs_called1 rs_called2 m'.
Γ chain_name_neu = Some (rs_called1@[Rule m' Return]@rs_called2) ∧
matches γ m' p ∧ Γ,γ,p⊢ ⟨rs_called1, Undecided⟩ ⇒ Undecided)" by simp
thus ?case
proof(elim disjE exE conjE)
fix t
assume a: "Γ,γ,p⊢ ⟨rs_called, Undecided⟩ ⇒ t" show ?case
using call_result[OF less.prems(1) rs_called a] by(blast)
next
fix m' rs_called1 rs_called2
assume a1: "Γ chain_name_neu = Some (rs_called1 @ [Rule m' Return] @ rs_called2)"
and a2: "matches γ m' p" and a3: "Γ,γ,p⊢ ⟨rs_called1, Undecided⟩ ⇒ Undecided"
show ?case using call_return[OF less.prems(1) a1 a2 a3 ] by(blast)
qed
qed
with True assms Call show ?thesis by simp
qed
qed
with Undecided show ?thesis by simp
qed

private lemma helper_defined_ruleset_calledby: "wf (called_by_chain Γ) ⟹
∀rsg ∈ ran Γ ∪ {rs}. wf_chain Γ rsg ⟹
∀rsg ∈ ran Γ ∪ {rs}. ∀ r ∈ set rsg. (¬(∃chain. get_action r = Goto chain)) ∧ get_action r ≠ Unknown ⟹
∀ r ∈ set rs. get_action r ≠ Return ⟹
∃t. Γ,γ,p⊢ ⟨rs, s⟩ ⇒ t"
apply(rule iptables_bigstep_defined_if_singleton_rules)
apply(intro ballI, rename_tac r, case_tac r, rename_tac m a, simp)
apply(rule helper_defined_single)
apply(simp; fail)
apply fastforce
apply fastforce
done

corollary semantics_bigstep_defined: "finite (calls_chain Γ) ⟹ wf (calls_chain Γ) ⟹ ― ‹call relation finite and terminating›
∀rsg ∈ ran Γ ∪ {rs}. wf_chain Γ rsg ⟹ ― ‹All calls to defined chains›
∀rsg ∈ ran Γ ∪ {rs}. ∀ r ∈ set rsg. (∀x. get_action r ≠ Goto x) ∧ get_action r ≠ Unknown ⟹ ― ‹no bad actions›
∀ r ∈ set rs. get_action r ≠ Return ― ‹no toplevel return› ⟹
∃t. Γ,γ,p⊢ ⟨rs, s⟩ ⇒ t"
apply(drule(1) wf_called_by_chain)
apply(thin_tac "wf (calls_chain Γ)")
apply(rule helper_defined_ruleset_calledby)
apply(simp_all)
done
end

text‹Common Algorithms›

lemma iptables_bigstep_rm_LogEmpty: "Γ,γ,p⊢ ⟨rm_LogEmpty rs, s⟩ ⇒ t ⟷ Γ,γ,p⊢ ⟨rs, s⟩ ⇒ t"
proof(induction rs arbitrary: s)
case Nil thus ?case by(simp)
next
case (Cons r rs)
have step_IH: "(⋀s. Γ,γ,p⊢ ⟨rs1, s⟩ ⇒ t = Γ,γ,p⊢ ⟨rs2, s⟩ ⇒ t) ⟹
Γ,γ,p⊢ ⟨r#rs1, s⟩ ⇒ t = Γ,γ,p⊢ ⟨r#rs2, s⟩ ⇒ t" for rs1 rs2 r
by (meson seq'_cons seqE_cons)
have case_log: "Γ,γ,p⊢ ⟨Rule m Log # rs, s⟩ ⇒ t ⟷ Γ,γ,p⊢ ⟨rs, s⟩ ⇒ t" for m
apply(rule iffI)
apply(erule seqE_cons)
apply (metis append_Nil log_remove seq')
apply(rule_tac t=s in seq'_cons)
apply(cases s)
apply(cases "matches γ m p")
apply simp
done
have case_empty: "Γ,γ,p⊢ ⟨Rule m Empty # rs, s⟩ ⇒ t ⟷ Γ,γ,p⊢ ⟨rs, s⟩ ⇒ t" for m
apply(rule iffI)
apply(erule seqE_cons)
apply (metis append_Nil empty_empty seq')
apply(rule_tac t=s in seq'_cons)
apply(cases s)
apply(cases "matches γ m p")
apply simp
done

from Cons show ?case
apply(cases r, rename_tac m a)
apply(case_tac a)
apply(simp_all)
apply(simp_all cong: step_IH)
done
qed

lemma iptables_bigstep_rw_Reject: "Γ,γ,p⊢ ⟨rw_Reject rs, s⟩ ⇒ t ⟷ Γ,γ,p⊢ ⟨rs, s⟩ ⇒ t"
proof(induction rs arbitrary: s)
case Nil thus ?case by(simp)
next
case (Cons r rs)
have step_IH: "(⋀s. Γ,γ,p⊢ ⟨rs1, s⟩ ⇒ t = Γ,γ,p⊢ ⟨rs2, s⟩ ⇒ t) ⟹
Γ,γ,p⊢ ⟨r#rs1, s⟩ ⇒ t = Γ,γ,p⊢ ⟨r#rs2, s⟩ ⇒ t" for rs1 rs2 r
by (meson seq'_cons seqE_cons)
have fst_rule: "(⋀t. Γ,γ,p⊢ ⟨[r1], s⟩ ⇒ t ⟷ Γ,γ,p⊢ ⟨[r2], s⟩ ⇒ t) ⟹
Γ,γ,p⊢ ⟨r1 # rs, s⟩ ⇒ t ⟷ Γ,γ,p⊢ ⟨r2 # rs, s⟩ ⇒ t" for r1 r2 rs s t
by (meson seq'_cons seqE_cons)
have dropreject: "Γ,γ,p⊢ ⟨[Rule m Drop], s⟩ ⇒ t = Γ,γ,p⊢ ⟨[Rule m Reject], s⟩ ⇒ t" for m t
apply(cases s)
apply(cases "matches γ m p")
using drop reject dropD rejectD apply fast
using nomatch nomatchD apply fast
using decision decisionD apply fast
done

from Cons show ?case
apply(cases r, rename_tac m a)
apply simp
apply(case_tac a)
apply(simp_all)
apply(simp_all cong: step_IH)
apply(rule fst_rule)
done
qed

end


# Theory Matching

theory Matching
imports Semantics
begin

subsection‹Boolean Matcher Algebra›

lemma MatchOr: "matches γ (MatchOr m1 m2) p ⟷ matches γ m1 p ∨ matches γ m2 p"

lemma opt_MatchAny_match_expr_correct: "matches γ (opt_MatchAny_match_expr m) = matches γ m"
proof -
have "matches γ (opt_MatchAny_match_expr_once m) = matches γ m" for m
by(induction m rule: opt_MatchAny_match_expr_once.induct) (simp_all)
thus ?thesis
apply(rule repeat_stabilize_induct)
by(simp)+
qed

lemma matcheq_matchAny: "¬ has_primitive m ⟹ matcheq_matchAny m ⟷ matches γ m p"
by(induction m) simp_all

lemma matcheq_matchNone: "¬ has_primitive m ⟹ matcheq_matchNone m ⟷ ¬ matches γ m p"
by(auto dest: matcheq_matchAny matachAny_matchNone)

lemma matcheq_matchNone_not_matches: "matcheq_matchNone m ⟹ ¬ matches γ m p"
by(induction m rule: matcheq_matchNone.induct) auto

text‹Lemmas about matching in the @{const iptables_bigstep} semantics.›

lemma matches_rule_iptables_bigstep:
assumes "matches γ m p ⟷ matches γ m' p"
shows "Γ,γ,p⊢ ⟨[Rule m a], s⟩ ⇒ t ⟷ Γ,γ,p⊢ ⟨[Rule m' a], s⟩ ⇒ t" (is "?l ⟷?r")
proof -
{
fix m m'
assume "Γ,γ,p⊢ ⟨[Rule m a], s⟩ ⇒ t" "matches γ m p ⟷ matches γ m' p"
hence "Γ,γ,p⊢ ⟨[Rule m' a], s⟩ ⇒ t"
by (induction "[Rule  m a]" s t rule: iptables_bigstep_induct)
(auto intro: iptables_bigstep.intros simp: Cons_eq_append_conv dest: skipD)
}
with assms show ?thesis by blast
qed

lemma matches_rule_and_simp_help:
assumes "matches γ m p"
shows "Γ,γ,p⊢ ⟨[Rule (MatchAnd m m') a'], Undecided⟩ ⇒ t ⟷ Γ,γ,p⊢ ⟨[Rule m' a'], Undecided⟩ ⇒ t" (is "?l ⟷?r")
proof
assume ?l thus ?r
by (induction "[Rule (MatchAnd m m') a']" Undecided t rule: iptables_bigstep_induct)
(auto intro: iptables_bigstep.intros simp: assms Cons_eq_append_conv dest: skipD)
next
assume ?r thus ?l
by (induction "[Rule m' a']" Undecided t rule: iptables_bigstep_induct)
(auto intro: iptables_bigstep.intros simp: assms Cons_eq_append_conv dest: skipD)
qed

lemma matches_MatchNot_simp:
assumes "matches γ m p"
shows "Γ,γ,p⊢ ⟨[Rule (MatchNot m) a], Undecided⟩ ⇒ t ⟷ Γ,γ,p⊢ ⟨[], Undecided⟩ ⇒ t" (is "?l ⟷ ?r")
proof
assume ?l thus ?r
by (induction "[Rule (MatchNot m) a]" "Undecided" t rule: iptables_bigstep_induct)
(auto intro: iptables_bigstep.intros simp: assms Cons_eq_append_conv dest: skipD)
next
assume ?r
hence "t = Undecided"
by (metis skipD)
with assms show ?l
by (fastforce intro: nomatch)
qed

lemma matches_MatchNotAnd_simp:
assumes "matches γ m p"
shows "Γ,γ,p⊢ ⟨[Rule (MatchAnd (MatchNot m) m') a], Undecided⟩ ⇒ t ⟷ Γ,γ,p⊢ ⟨[], Undecided⟩ ⇒ t" (is "?l ⟷ ?r")
proof
assume ?l thus ?r
by (induction "[Rule (MatchAnd (MatchNot m) m') a]" "Undecided" t rule: iptables_bigstep_induct)
(auto intro: iptables_bigstep.intros simp add: assms Cons_eq_append_conv dest: skipD)
next
assume ?r
hence "t = Undecided"
by (metis skipD)
with assms show ?l
by (fastforce intro: nomatch)
qed

lemma matches_rule_and_simp:
assumes "matches γ m p"
shows "Γ,γ,p⊢ ⟨[Rule (MatchAnd m m') a'], s⟩ ⇒ t ⟷ Γ,γ,p⊢ ⟨[Rule m' a'], s⟩ ⇒ t"
proof (cases s)
case Undecided
with assms show ?thesis
next
case Decision
thus ?thesis by (metis decision decisionD)
qed

lemma iptables_bigstep_MatchAnd_comm:
"Γ,γ,p⊢ ⟨[Rule (MatchAnd m1 m2) a], s⟩ ⇒ t ⟷ Γ,γ,p⊢ ⟨[Rule (MatchAnd m2 m1) a], s⟩ ⇒ t"
proof -
{ fix m1 m2
have "Γ,γ,p⊢ ⟨[Rule (MatchAnd m1 m2) a], s⟩ ⇒ t ⟹ Γ,γ,p⊢ ⟨[Rule (MatchAnd m2 m1) a], s⟩ ⇒ t"
proof (induction "[Rule (MatchAnd m1 m2) a]" s t rule: iptables_bigstep_induct)
case Seq thus ?case
by (metis Nil_is_append_conv append_Nil butlast_append butlast_snoc seq)
qed (auto intro: iptables_bigstep.intros)
}
thus ?thesis by blast
qed

definition add_match :: "'a match_expr ⇒ 'a rule list ⇒ 'a rule list" where
"add_match m rs = map (λr. case r of Rule m' a' ⇒ Rule (MatchAnd m m') a') rs"

by (fact map_append)

lemma add_match_split_fst: "add_match m (Rule m' a' # rs) = Rule (MatchAnd m m') a' # add_match m rs"
by simp

proof -
{
fix m1 m2
proof (induction rs arbitrary: s)
next
case (Cons r rs)
from Cons obtain m a where r: "r = Rule m a" by (cases r) simp
with Cons.prems obtain ti where 1: "Γ,γ,p⊢ ⟨[Rule (MatchAnd m1 (MatchAnd m2 m)) a], s⟩ ⇒ ti" and 2: "Γ,γ,p⊢ ⟨add_match m1 (add_match m2 rs), ti⟩ ⇒ t"
apply(erule seqE_cons)
by simp
from 1 r have base: "Γ,γ,p⊢ ⟨[Rule (MatchAnd m2 (MatchAnd m1 m)) a], s⟩ ⇒ ti"
by (metis matches.simps(1) matches_rule_iptables_bigstep)
from 2 Cons.IH have IH: "Γ,γ,p⊢ ⟨add_match m2 (add_match m1 rs), ti⟩ ⇒ t" by simp
from base IH seq'_cons have "Γ,γ,p⊢ ⟨Rule (MatchAnd m2 (MatchAnd m1 m)) a # add_match m2 (add_match m1 rs), s⟩ ⇒ t" by fast
qed
}
thus ?thesis by blast
qed

assumes m: "matches γ m p"
shows "Γ,γ,p⊢ ⟨add_match m rs, s⟩ ⇒ t ⟷ Γ,γ,p⊢ ⟨rs, s⟩ ⇒ t" (is "?l ⟷ ?r")
proof
assume ?l with m show ?r
proof (induction rs)
case Nil
thus ?case
next
case (Cons r rs)
hence IH: "Γ,γ,p⊢ ⟨add_match m rs, s⟩ ⇒ t ⟹ Γ,γ,p⊢ ⟨rs, s⟩ ⇒ t" by(simp add: add_match_split_fst)
obtain m' a where r: "r = Rule m' a" by (cases r)
with Cons.prems(2) obtain ti where "Γ,γ,p⊢ ⟨[Rule (MatchAnd m m') a], s⟩ ⇒ ti" and "Γ,γ,p⊢ ⟨add_match m rs, ti⟩ ⇒ t"
with Cons.prems(1) IH have "Γ,γ,p⊢ ⟨[Rule m' a], s⟩ ⇒ ti" by(simp add: matches_rule_and_simp)
with ‹Γ,γ,p⊢ ⟨add_match m rs, ti⟩ ⇒ t› IH r show ?case by(metis decision state.exhaust iptables_bigstep_deterministic seq_cons)
qed
next
assume ?r with m show ?l
proof (induction rs)
case Nil
thus ?case
next
case (Cons r rs)
hence IH: " Γ,γ,p⊢ ⟨rs, s⟩ ⇒ t ⟹ Γ,γ,p⊢ ⟨add_match m rs, s⟩ ⇒ t" by(simp add: add_match_split_fst)
obtain m' a where r: "r = Rule m' a" by (cases r)
with Cons.prems(2) obtain ti where "Γ,γ,p⊢ ⟨[Rule m' a], s⟩ ⇒ ti" and "Γ,γ,p⊢ ⟨rs, ti⟩ ⇒ t"
with Cons.prems(1) IH have "Γ,γ,p⊢ ⟨[Rule (MatchAnd m m') a], s⟩ ⇒ ti" by(simp add: matches_rule_and_simp)
with ‹Γ,γ,p⊢ ⟨rs, ti⟩ ⇒ t› IH r show ?case
by(metis decision state.exhaust iptables_bigstep_deterministic seq_cons)
qed
qed

assumes m: "matches γ m p"
shows "Γ,γ,p⊢ ⟨add_match (MatchNot m) rs, s⟩ ⇒ t ⟷ Γ,γ,p⊢ ⟨[], s⟩ ⇒ t" (is "?l s ⟷ ?r s")
proof (cases s)
case Undecided
have "?l Undecided ⟷ ?r Undecided"
proof
assume "?l Undecided" with m show "?r Undecided"
proof (induction rs)
case Nil
thus ?case
next
case (Cons r rs)
thus ?case
by (cases r) (metis matches_MatchNotAnd_simp skipD seqE_cons add_match_split_fst)
qed
next
assume "?r Undecided" with m show "?l Undecided"
proof (induction rs)
case Nil
thus ?case
next
case (Cons r rs)
thus ?case
by (cases r) (metis matches_MatchNotAnd_simp skipD seq'_cons add_match_split_fst)
qed
qed
with Undecided show ?thesis by fast
next
case (Decision d)
thus ?thesis
by(metis decision decisionD)
qed

assumes "¬ matches γ m p"
shows "Γ,γ,p⊢ ⟨add_match m rs, Undecided⟩ ⇒ t ⟷ Γ,γ,p⊢ ⟨[], Undecided⟩ ⇒ t"
proof(induction rs)
case Nil
thus ?case
next
case (Cons r rs)
thus ?case
by (cases r) (metis assms add_match_split_fst matches.simps(1) nomatch seq'_cons nomatchD seqE_cons)
qed

"Γ,γ,p⊢ ⟨add_match (MatchNot (MatchNot m)) rs, s⟩ ⇒ t ⟷ Γ,γ,p⊢ ⟨add_match m rs, s⟩ ⇒ t"
proof(induction rs)
case Nil
thus ?case
next
case (Cons r rs)
thus ?case
by (cases r)
qed

"Γ,γ,p⊢ ⟨add_match (MatchNot m) rs, Undecided⟩ ⇒ Undecided ⟹ matches γ m p ∨ Γ,γ,p⊢ ⟨rs, Undecided⟩ ⇒ Undecided"

"¬ matches γ m p ⟹ Γ,γ,p⊢ ⟨add_match (MatchNot m) rs, s⟩ ⇒ t ⟷ Γ,γ,p⊢ ⟨rs, s⟩ ⇒ t"

"Γ,γ,p⊢ ⟨add_match m1 (add_match m2 rs), s⟩ ⇒ t ⟷ Γ,γ,p⊢ ⟨add_match (MatchAnd m1 m2) rs, s⟩ ⇒ t"
proof(induction rs arbitrary: s t)
case Nil
thus ?case
next
case(Cons r rs)
show ?case
proof (cases r, simp only: add_match_split_fst)
fix m a
show "Γ,γ,p⊢ ⟨Rule (MatchAnd m1 (MatchAnd m2 m)) a # add_match m1 (add_match m2 rs), s⟩ ⇒ t ⟷ Γ,γ,p⊢ ⟨Rule (MatchAnd (MatchAnd m1 m2) m) a # add_match (MatchAnd m1 m2) rs, s⟩ ⇒ t" (is "?l ⟷ ?r")
proof
assume ?l with Cons.IH show ?r
apply -
apply(erule seqE_cons)
apply(case_tac s)
apply(case_tac ti)
apply (metis matches.simps(1) matches_rule_and_simp matches_rule_and_simp_help nomatch seq'_cons)
apply (metis decision decisionD)
done
next
assume ?r with Cons.IH show ?l
apply -
apply(erule seqE_cons)
apply(case_tac s)
apply(case_tac ti)
apply (metis matches.simps(1) matches_rule_and_simp matches_rule_and_simp_help nomatch seq'_cons)
apply (metis decision decisionD)
done
qed
qed
qed

lemma optimize_matches_option_generic:
assumes "∀ r ∈ set rs. P (get_match r)"
and "(⋀m m'. P m ⟹ f m = Some m' ⟹ matches γ m' p = matches γ m p)"
and "(⋀m. P m ⟹ f m = None ⟹ ¬ matches γ m p)"
shows "Γ,γ,p⊢ ⟨optimize_matches_option f rs, s⟩ ⇒ t ⟷ Γ,γ,p⊢ ⟨rs, s⟩ ⇒ t"
(is "?lhs ⟷ ?rhs")
proof
assume ?rhs
from this assms show ?lhs
apply(induction rs s t rule: iptables_bigstep_induct)
apply(auto simp: optimize_matches_option_append intro: iptables_bigstep.intros split: option.split)
done
next
assume ?lhs
from this assms show ?rhs
apply(induction f rs arbitrary: s rule: optimize_matches_option.induct)
apply(simp; fail)
apply(simp split: option.split_asm)
apply(subgoal_tac "¬ matches γ m p")
prefer 2 apply blast
apply (metis decision nomatch seq'_cons state.exhaust)
apply(erule seqE_cons)
apply(rule_tac t=ti in seq'_cons)
apply (meson matches_rule_iptables_bigstep)
by blast
qed

lemma optimize_matches_generic: "∀ r ∈ set rs. P (get_match r) ⟹
(⋀m. P m ⟹ matches γ (f m) p = matches γ m p) ⟹
Γ,γ,p⊢ ⟨optimize_matches f rs, s⟩ ⇒ t ⟷ Γ,γ,p⊢ ⟨rs, s⟩ ⇒ t"
unfolding optimize_matches_def
apply(rule optimize_matches_option_generic)
apply(simp; fail)
apply(simp split: if_split_asm)
apply blast
apply(simp split: if_split_asm)
using matcheq_matchNone_not_matches by fast
end


# Theory Ruleset_Update

theory Ruleset_Update
imports Matching
begin

lemma free_return_not_match: "Γ,γ,p⊢ ⟨[Rule m Return], Undecided⟩ ⇒ t ⟹ ¬ matches γ m p"
using no_free_return by fast

subsection‹Background Ruleset Updating›
lemma update_Gamma_nomatch:
assumes "¬ matches γ m p"
shows "Γ(chain ↦ Rule m a # rs),γ,p⊢ ⟨rs', s⟩ ⇒ t ⟷ Γ(chain ↦ rs),γ,p⊢ ⟨rs', s⟩ ⇒ t" (is "?l ⟷ ?r")
proof
assume ?l thus ?r
proof (induction rs' s t rule: iptables_bigstep_induct)
case (Call_return m a chain' rs⇩1 m' rs⇩2)
thus ?case
proof (cases "chain' = chain")
case True
with Call_return show ?thesis
apply simp
apply(cases "rs⇩1")
using assms apply fastforce
apply(rule_tac rs⇩1="list" and m'="m'" and rs⇩2="rs⇩2" in call_return)
apply(simp)
apply(simp)
apply(simp)
apply(simp)
apply(erule seqE_cons[where Γ="(λa. if a = chain then Some rs else Γ a)"])
apply(frule iptables_bigstep_to_undecided[where Γ="(λa. if a = chain then Some rs else Γ a)"])
apply(simp)
done
qed (auto intro: call_return)
next
case (Call_result m' a' chain' rs' t')
have "Γ(chain ↦ rs),γ,p⊢ ⟨[Rule m' (Call chain')], Undecided⟩ ⇒ t'"
proof (cases "chain' = chain")
case True
with Call_result have "Rule m a # rs = rs'" "(Γ(chain ↦ rs)) chain' = Some rs"
by simp+
with assms Call_result show ?thesis
by (metis call_result nomatchD seqE_cons)
next
case False
with Call_result show ?thesis
by (metis call_result fun_upd_apply)
qed
with Call_result show ?case
by fast
qed (auto intro: iptables_bigstep.intros)
next
assume ?r thus ?l
proof (induction rs' s t rule: iptables_bigstep_induct)
case (Call_return m' a' chain' rs⇩1)
thus ?case
proof (cases "chain' = chain")
case True
with Call_return show ?thesis
using assms
by (auto intro: seq_cons nomatch intro!: call_return[where rs⇩1 = "Rule m a # rs⇩1"])
qed (auto intro: call_return)
next
case (Call_result m' a' chain' rs')
thus ?case
proof (cases "chain' = chain")
case True
with Call_result show ?thesis
using assms by (auto intro: seq_cons nomatch intro!: call_result)
qed (auto intro: call_result)
qed (auto intro: iptables_bigstep.intros)
qed

lemma update_Gamma_log_empty:
assumes "a = Log ∨ a = Empty"
shows "Γ(chain ↦ Rule m a # rs),γ,p⊢ ⟨rs', s⟩ ⇒ t ⟷
Γ(chain ↦ rs),γ,p⊢ ⟨rs', s⟩ ⇒ t" (is "?l ⟷ ?r")
proof
assume ?l thus ?r
proof (induction rs' s t rule: iptables_bigstep_induct)
case (Call_return m' a' chain' rs⇩1 m'' rs⇩2)
(*it seems that Isabelle has problems to apply @{thm fun_upd_apply} at the semantics if it appears in the goal without @{text λ}*)
note [simp] = fun_upd_apply[abs_def]

from Call_return have "Γ(chain ↦ rs),γ,p⊢ ⟨[Rule m' (Call chain')], Undecided⟩ ⇒ Undecided" (is ?Call_return_case)
proof(cases "chain' = chain")
case True with Call_return show ?Call_return_case
― ‹@{term rs⇩1} cannot be empty›
proof(cases "rs⇩1")
case Nil with Call_return(3) ‹chain' = chain› assms have "False" by simp
thus ?Call_return_case by simp
next
case (Cons r⇩1 rs⇩1s)
from Cons Call_return have "Γ(chain ↦ rs),γ,p⊢ ⟨r⇩1 # rs⇩1s, Undecided⟩ ⇒ Undecided" by blast
with seqE_cons[where Γ="Γ(chain ↦ rs)"] obtain ti where
"Γ(chain ↦ rs),γ,p⊢ ⟨[r⇩1], Undecided⟩ ⇒ ti" and "Γ(chain ↦ rs),γ,p⊢ ⟨rs⇩1s, ti⟩ ⇒ Undecided" by metis
with iptables_bigstep_to_undecided[where Γ="Γ(chain ↦ rs)"] have "Γ(chain ↦ rs),γ,p⊢ ⟨rs⇩1s, Undecided⟩ ⇒ Undecided" by fast
with Cons Call_return ‹chain' = chain› show ?Call_return_case
apply(rule_tac rs⇩1="rs⇩1s" and m'="m''" and rs⇩2="rs⇩2" in call_return)
apply(simp_all)
done
qed
next
case False with Call_return show ?Call_return_case
by (auto intro: call_return)
qed
thus ?case using Call_return by blast
next
case (Call_result m' a' chain' rs' t')
thus ?case
proof (cases "chain' = chain")
case True
with Call_result have "rs' = [] @ [Rule m a] @ rs"
by simp
with Call_result assms have "Γ(chain ↦ rs),γ,p⊢ ⟨[] @ rs, Undecided⟩ ⇒ t'"
using log_remove empty_empty by fast
hence "Γ(chain ↦ rs),γ,p⊢ ⟨rs, Undecided⟩ ⇒ t'"
by simp
with Call_result True show ?thesis
by (metis call_result fun_upd_same)
qed (fastforce intro: call_result)
qed (auto intro: iptables_bigstep.intros)
next
have cases_a: "⋀P. (a = Log ⟹ P a) ⟹ (a = Empty ⟹ P a) ⟹ P a" using assms by blast
assume ?r thus ?l
proof (induction rs' s t rule: iptables_bigstep_induct)
case (Call_return m' a' chain' rs⇩1 m'' rs⇩2)
from Call_return have xx: "Γ(chain ↦ Rule m a # rs),γ,p⊢ ⟨Rule m a # rs⇩1, Undecided⟩ ⇒ Undecided"
apply -
apply(rule cases_a)
apply (auto intro: nomatch seq_cons intro!: log empty simp del: fun_upd_apply)
done
with Call_return show ?case
proof(cases "chain' = chain")
case False
with Call_return have x: "(Γ(chain ↦ Rule m a # rs)) chain' = Some (rs⇩1 @ Rule m'' Return # rs⇩2)"
by(simp)
with Call_return have "Γ(chain ↦ Rule m a # rs),γ,p⊢ ⟨[Rule m' (Call chain')], Undecided⟩ ⇒ Undecided"
apply -
apply(rule call_return[where rs⇩1="rs⇩1" and m'="m''" and rs⇩2="rs⇩2"])
apply(simp_all add: x xx del: fun_upd_apply)
done
thus "Γ(chain ↦ Rule m a # rs),γ,p⊢ ⟨[Rule m' a'], Undecided⟩ ⇒ Undecided" using Call_return by simp
next
case True
with Call_return have x: "(Γ(chain ↦ Rule m a # rs)) chain' = Some (Rule m a # rs⇩1 @ Rule m'' Return # rs⇩2)"
by(simp)
with Call_return have "Γ(chain ↦ Rule m a # rs),γ,p⊢ ⟨[Rule m' (Call chain')], Undecided⟩ ⇒ Undecided"
apply -
apply(rule call_return[where rs⇩1="Rule m a#rs⇩1" and m'="m''" and rs⇩2="rs⇩2"])
apply(simp_all add: x xx del: fun_upd_apply)
done
thus "Γ(chain ↦ Rule m a # rs),γ,p⊢ ⟨[Rule m' a'], Undecided⟩ ⇒ Undecided" using Call_return by simp
qed
next
case (Call_result ma a chaina rs t)
thus ?case
apply (cases "chaina = chain")
apply(rule cases_a)
apply (auto intro: nomatch seq_cons intro!: log empty call_result)[2]
by (auto intro!: call_result)[1]
qed (auto intro: iptables_bigstep.intros)
qed

lemma map_update_chain_if: "(λb. if b = chain then Some rs else Γ b) = Γ(chain ↦ rs)"
by auto

lemma no_recursive_calls_helper:
assumes "Γ,γ,p⊢ ⟨[Rule m (Call chain)], Undecided⟩ ⇒ t"
and     "matches γ m p"
and     "Γ chain = Some [Rule m (Call chain)]"
shows   False
using assms
proof (induction "[Rule m (Call chain)]" Undecided t rule: iptables_bigstep_induct)
case Seq
thus ?case
by (metis Cons_eq_append_conv append_is_Nil_conv skipD)
next
case (Call_return chain' rs⇩1 m' rs⇩2)
hence "rs⇩1 @ Rule m' Return # rs⇩2 = [Rule m (Call chain')]"
by simp
thus ?case
by (cases "rs⇩1") auto
next
case Call_result
thus ?case
by simp
qed (auto intro: iptables_bigstep.intros)

lemma no_recursive_calls:
"Γ(chain ↦ [Rule m (Call chain)]),γ,p⊢ ⟨[Rule m (Call chain)], Undecided⟩ ⇒ t ⟹ matches γ m p ⟹ False"
by (fastforce intro: no_recursive_calls_helper)

lemma no_recursive_calls2:
assumes "Γ(chain ↦ (Rule m (Call chain)) # rs''),γ,p⊢ ⟨(Rule m (Call chain)) # rs', Undecided⟩ ⇒ Undecided"
and     "matches γ m p"
shows   False
using assms
proof (induction "(Rule m (Call chain)) # rs'" Undecided Undecided arbitrary: rs' rule: iptables_bigstep_induct)
case (Seq rs⇩1 rs⇩2 t)
thus ?case
by (cases rs⇩1) (auto elim: seqE_cons simp add: iptables_bigstep_to_undecided)
qed (auto intro: iptables_bigstep.intros simp: Cons_eq_append_conv)

lemma update_Gamma_nochange1:
assumes "Γ(chain ↦ rs),γ,p⊢ ⟨[Rule m a], Undecided⟩ ⇒ Undecided"
and     "Γ(chain ↦ Rule m a # rs),γ,p⊢ ⟨rs', s⟩ ⇒ t"
shows   "Γ(chain ↦ rs),γ,p⊢ ⟨rs', s⟩ ⇒ t"
using assms(2) proof (induction rs' s t rule: iptables_bigstep_induct)
case (Call_return m a chaina rs⇩1 m' rs⇩2)
thus ?case
proof (cases "chaina = chain")
case True
with Call_return show ?thesis
apply simp
apply(cases "rs⇩1")
apply(simp)
using assms apply (metis no_free_return) (*gives False*)
apply(rule_tac rs⇩1="list" and m'="m'" and rs⇩2="rs⇩2" in call_return)
apply(simp)
apply(simp)
apply(simp)
apply(simp)
apply(erule seqE_cons[where Γ="(λa. if a = chain then Some rs else Γ a)"])
apply(frule iptables_bigstep_to_undecided[where Γ="(λa. if a = chain then Some rs else Γ a)"])
apply(simp)
done
qed (auto intro: call_return)
next
case (Call_result m a chaina rsa t)
thus ?case
proof (cases "chaina = chain")
case True
with Call_result show ?thesis
apply(simp)
apply(cases "rsa")
apply(simp)
apply(rule_tac rs=rs in call_result)
apply(simp_all)
apply(erule_tac seqE_cons[where Γ="(λb. if b = chain then Some rs else Γ b)"])
apply(case_tac t)
apply(simp)
apply(frule iptables_bigstep_to_undecided[where Γ="(λb. if b = chain then Some rs else Γ b)"])
apply(simp)
apply(simp)
apply(subgoal_tac "ti = Undecided")
apply(simp)
using assms(1)[simplified map_update_chain_if[symmetric]] iptables_bigstep_deterministic apply fast
done
qed (fastforce intro: call_result)
qed (auto intro: iptables_bigstep.intros)

lemma update_gamme_remove_Undecidedpart:
assumes "Γ(chain ↦ rs'),γ,p⊢ ⟨rs', Undecided⟩ ⇒ Undecided"
and     "Γ(chain ↦ rs1@rs'),γ,p⊢ ⟨rs, Undecided⟩ ⇒ Undecided"
shows   "Γ(chain ↦rs'),γ,p⊢ ⟨rs, Undecided⟩ ⇒ Undecided"
using assms(2) proof (induction rs Undecided Undecided rule: iptables_bigstep_induct)
case Seq
thus ?case
by (auto simp: iptables_bigstep_to_undecided intro: seq)
next
case (Call_return m a chaina rs⇩1 m' rs⇩2)
thus ?case
apply(cases "chaina = chain")
apply(simp)
apply(cases "length rs1 ≤ length rs⇩1")
apply(rule_tac rs⇩1="drop (length rs1) rs⇩1" and m'=m' and rs⇩2=rs⇩2 in call_return)
apply(simp_all)[3]
apply(subgoal_tac "rs⇩1 = (take (length rs1) rs⇩1) @ drop (length rs1) rs⇩1")
prefer 2 apply (metis append_take_drop_id)
apply(clarify)
apply(subgoal_tac "Γ(chain ↦ drop (length rs1) rs⇩1 @ Rule m' Return # rs⇩2),γ,p⊢
⟨(take (length rs1) rs⇩1) @ drop (length rs1) rs⇩1, Undecided⟩ ⇒ Undecided")
prefer 2 apply(auto)[1]
apply(erule_tac rs⇩1="take (length rs1) rs⇩1" and rs⇩2="drop (length rs1) rs⇩1" in seqE)
apply(simp)
apply(frule_tac rs="drop (length rs1) rs⇩1" in iptables_bigstep_to_undecided)
apply(simp; fail) (*oh wow*)
using assms apply (auto intro: call_result call_return)
done
next
case (Call_result _ _ chain' rsa)
thus ?case
apply(cases "chain' = chain")
apply(simp)
apply(rule call_result)
apply(simp_all)[2]
apply (metis iptables_bigstep_to_undecided seqE)
apply (auto intro: call_result)
done
qed (auto intro: iptables_bigstep.intros)

lemma update_Gamma_nocall:
assumes "¬ (∃chain. a = Call chain)"
shows "Γ,γ,p⊢ ⟨[Rule m a], s⟩ ⇒ t ⟷ Γ',γ,p⊢ ⟨[Rule m a], s⟩ ⇒ t"
proof -
{
fix Γ Γ'
have "Γ,γ,p⊢ ⟨[Rule m a], s⟩ ⇒ t ⟹ Γ',γ,p⊢ ⟨[Rule m a], s⟩ ⇒ t"
proof (induction "[Rule m a]" s t rule: iptables_bigstep_induct)
case Seq
thus ?case by (metis (lifting, no_types) list_app_singletonE[where x = "Rule m a"] skipD)
next
case Call_return thus ?case using assms by metis
next
case Call_result thus ?case using assms by metis
qed (auto intro: iptables_bigstep.intros)
}
thus ?thesis
by blast
qed

lemma update_Gamma_call:
assumes "Γ chain = Some rs" and "Γ' chain = Some rs'"
assumes "Γ,γ,p⊢ ⟨rs, Undecided⟩ ⇒ Undecided" and "Γ',γ,p⊢ ⟨rs', Undecided⟩ ⇒ Undecided"
shows "Γ,γ,p⊢ ⟨[Rule m (Call chain)], s⟩ ⇒ t ⟷ Γ',γ,p⊢ ⟨[Rule m (Call chain)], s⟩ ⇒ t"
proof -
{
fix Γ Γ' rs rs'
assume assms:
"Γ chain = Some rs" "Γ' chain = Some rs'"
"Γ,γ,p⊢ ⟨rs, Undecided⟩ ⇒ Undecided" "Γ',γ,p⊢ ⟨rs', Undecided⟩ ⇒ Undecided"
have "Γ,γ,p⊢ ⟨[Rule m (Call chain)], s⟩ ⇒ t ⟹ Γ',γ,p⊢ ⟨[Rule m (Call chain)], s⟩ ⇒ t"
proof (induction "[Rule m (Call chain)]" s t rule: iptables_bigstep_induct)
case Seq
thus ?case by (metis (lifting, no_types) list_app_singletonE[where x = "Rule m (Call chain)"] skipD)
next
case Call_result
thus ?case
using assms by (metis call_result iptables_bigstep_deterministic)
qed (auto intro: iptables_bigstep.intros assms)
}
note * = this
show ?thesis
using *[OF assms(1-4)] *[OF assms(2,1,4,3)] by blast
qed

lemma update_Gamma_remove_call_undecided:
assumes "Γ(chain ↦ Rule m (Call foo) # rs'),γ,p⊢ ⟨rs, Undecided⟩ ⇒ Undecided"
and     "matches γ m p"
shows "Γ(chain ↦ rs'),γ,p⊢ ⟨rs, Undecided⟩ ⇒ Undecided"
using assms
proof (induction rs Undecided Undecided arbitrary: rule: iptables_bigstep_induct)
case Seq
thus ?case
by (force simp: iptables_bigstep_to_undecided intro: seq')
next
case (Call_return m a chaina rs⇩1 m' rs⇩2)
thus ?case
apply(cases "chaina = chain")
apply(cases "rs⇩1")
apply(force intro: call_return)
apply(simp)
apply(erule_tac Γ="Γ(chain ↦ list @ Rule m' Return # rs⇩2)" in seqE_cons)
apply(frule_tac Γ="Γ(chain ↦ list @ Rule m' Return # rs⇩2)" in iptables_bigstep_to_undecided)
apply(auto intro: call_return)
done
next
case (Call_result m a chaina rsa)
thus ?case
apply(cases "chaina = chain")
apply(simp)
apply (metis call_result fun_upd_same iptables_bigstep_to_undecided seqE_cons)
apply (auto intro: call_result)
done
qed (auto intro: iptables_bigstep.intros)

lemma all_return_subchain:
assumes a1: "Γ chain = Some rs"
and     a2: "matches γ m p"
and     a3: "∀r∈set rs. get_action r = Return"
shows "Γ,γ,p⊢ ⟨[Rule m (Call chain)], Undecided⟩ ⇒ Undecided"
proof (cases "∃r ∈ set rs. matches γ (get_match r) p")
case True
hence "(∃rs1 r rs2. rs = rs1 @ r # rs2 ∧ matches γ (get_match r) p ∧ (∀r'∈set rs1. ¬ matches γ (get_match r') p))"
by (subst split_list_first_prop_iff[symmetric])
then obtain rs1 r rs2
where *: "rs = rs1 @ r # rs2" "matches γ (get_match r) p" "∀r'∈set rs1. ¬ matches γ (get_match r') p"
by auto

with a3 obtain m' where "r = Rule m' Return"
by (cases r) simp
with * assms show ?thesis
by (fastforce intro: call_return nomatch')
next
case False
hence "Γ,γ,p⊢ ⟨rs, Undecided⟩ ⇒ Undecided"
by (blast intro: nomatch')
with a1 a2 show ?thesis
by (metis call_result)
qed

lemma get_action_case_simp: "get_action (case r of Rule m' x ⇒ Rule (MatchAnd m m') x) = get_action r"
by (metis rule.case_eq_if rule.sel(2))

lemma updategamma_insert_new: "Γ,γ,p⊢ ⟨rs, s⟩ ⇒ t ⟹ chain ∉ dom Γ ⟹ Γ(chain ↦ rs'),γ,p⊢ ⟨rs, s⟩ ⇒ t"
proof(induction rule: iptables_bigstep_induct)
case (Call_result m a chain' rs t)
thus ?case by (metis call_result domI fun_upd_def)
next
case Call_return
thus ?case by (metis call_return domI fun_upd_def)
qed(auto intro: iptables_bigstep.intros)

end


# Theory Call_Return_Unfolding

theory Call_Return_Unfolding
imports Matching Ruleset_Update
"Common/Repeat_Stabilize"
begin

section‹@{term Call} @{term Return} Unfolding›

text‹Remove @{term Return}s›
fun process_ret :: "'a rule list ⇒ 'a rule list" where
"process_ret [] = []" |
"process_ret (Rule m Return # rs) = add_match (MatchNot m) (process_ret rs)" |
"process_ret (r#rs) = r # process_ret rs"

text‹Remove @{term Call}s›
fun process_call :: "'a ruleset ⇒ 'a rule list ⇒ 'a rule list" where
"process_call Γ [] = []" |
"process_call Γ (Rule m (Call chain) # rs) = add_match m (process_ret (the (Γ chain))) @ process_call Γ rs" |
"process_call Γ (r#rs) = r # process_call Γ rs"

lemma process_ret_split_fst_Return:
"a = Return ⟹ process_ret (Rule m a # rs) = add_match (MatchNot m) (process_ret rs)"
by auto

lemma process_ret_split_fst_NeqReturn:
"a ≠ Return ⟹ process_ret((Rule m a) # rs) = (Rule m a) # (process_ret rs)"
by (cases a) auto

lemma add_match_simp: "add_match m = map (λr. Rule (MatchAnd m (get_match r)) (get_action r))"
by (auto simp: add_match_def cong: map_cong split: rule.split)

definition add_missing_ret_unfoldings :: "'a rule list ⇒ 'a rule list ⇒ 'a rule list" where
foldr (λrf acc. add_match (MatchNot (get_match rf)) ∘ acc) [r←rs1. get_action r = Return] id rs2"

fun MatchAnd_foldr :: "'a match_expr list ⇒ 'a match_expr" where
"MatchAnd_foldr [] = undefined" | (*error, semantically, MatchAny would match*)
"MatchAnd_foldr [e] = e" |
"MatchAnd_foldr (e # es) = MatchAnd e (MatchAnd_foldr es)"
fun add_match_MatchAnd_foldr :: "'a match_expr list ⇒ ('a rule list ⇒ 'a rule list)" where

"Γ,γ,p⊢ ⟨add_match m (add_match_MatchAnd_foldr ms rs2), s⟩ ⇒ t = Γ,γ,p⊢ ⟨add_match (MatchAnd_foldr (m#ms)) rs2, s⟩ ⇒ t"
proof (induction ms)
case Nil
next
case Cons
qed

Γ,γ,p⊢ ⟨(add_match_MatchAnd_foldr (map (λr. MatchNot (get_match r)) [r←rs1. get_action r = Return])) rs2, s ⟩ ⇒ t"
proof(induction rs1)
case Nil
thus ?case
next
case (Cons r rs)
from Cons obtain m a where "r = Rule m a" by(cases r) (simp)
with Cons show ?case
apply(cases "matches γ m p")
done
qed

Γ,γ,p⊢ ⟨add_missing_ret_unfoldings (Rule (MatchNot m) Return#rs1) rs2, s⟩ ⇒ t"

subsection‹Completeness›
lemma process_ret_split_obvious: "process_ret (rs⇩1 @ rs⇩2) =
(process_ret rs⇩1) @ (add_missing_ret_unfoldings rs⇩1 (process_ret rs⇩2))"
proof (induction rs⇩1 arbitrary: rs⇩2)
case (Cons r rs)
from Cons obtain m a where "r = Rule m a" by (cases r) simp
with Cons.IH show ?case
apply(cases a)
done
qed simp

lemma process_call_split: "process_call Γ (rs1 @ rs2) = process_call Γ rs1 @ process_call Γ rs2"
proof (induction rs1)
case (Cons r rs1)
thus ?case
apply(cases r, rename_tac m a)
apply(case_tac a)
apply(simp_all)
done
qed simp

lemma process_call_split_fst: "process_call Γ (a # rs) = process_call Γ [a] @ process_call Γ rs"

lemma iptables_bigstep_process_ret_undecided: "Γ,γ,p⊢ ⟨rs, Undecided⟩ ⇒ t ⟹ Γ,γ,p⊢ ⟨process_ret rs, Undecided⟩ ⇒ t"
proof (induction rs)
case (Cons r rs)
show ?case
proof (cases r)
case (Rule m' a')
show "Γ,γ,p⊢ ⟨process_ret (r # rs), Undecided⟩ ⇒ t"
proof (cases a')
case Accept
with Cons Rule show ?thesis
by simp (metis acceptD decision decisionD nomatchD seqE_cons seq_cons)
next
case Drop
with Cons Rule show ?thesis
by simp (metis decision decisionD dropD nomatchD seqE_cons seq_cons)
next
case Log
with Cons Rule show ?thesis
by simp (metis logD nomatchD seqE_cons seq_cons)
next
case Reject
with Cons Rule show ?thesis
by simp (metis decision decisionD nomatchD rejectD seqE_cons seq_cons)
next
case (Call chain)
from Cons.prems obtain ti where 1:"Γ,γ,p⊢ ⟨[r], Undecided⟩ ⇒ ti" and 2: "Γ,γ,p⊢ ⟨rs, ti⟩ ⇒ t" using seqE_cons by metis
thus ?thesis
proof(cases ti)
case Undecided
with Cons.IH 2 have IH: "Γ,γ,p⊢ ⟨process_ret rs, Undecided⟩ ⇒ t" by simp
from Undecided 1 Call Rule have "Γ,γ,p⊢ ⟨[Rule m' (Call chain)], Undecided⟩ ⇒ Undecided" by simp
with IH  have" Γ,γ,p⊢ ⟨Rule m' (Call chain) # process_ret rs, Undecided⟩ ⇒ t" using seq'_cons by fast
thus ?thesis using Rule Call by force
next
case (Decision X)
with 1 Rule Call have "Γ,γ,p⊢ ⟨[Rule m' (Call chain)], Undecided⟩ ⇒ Decision X" by simp
moreover from 2 Decision have "t = Decision X" using decisionD by fast
moreover from decision have "Γ,γ,p⊢ ⟨process_ret rs, Decision X⟩ ⇒ Decision X" by fast
ultimately show ?thesis using seq_cons by (metis Call Rule process_ret.simps(7))
qed
next
case Return
with Cons Rule show ?thesis
by simp (metis matches.simps(2) matches_add_match_simp no_free_return nomatchD seqE_cons)
next
case Empty
show ?thesis
apply (insert Empty Cons Rule)
apply(erule seqE_cons)
apply (rename_tac ti)
apply(case_tac ti)
apply (metis Rule_DecisionE emptyD state.distinct(1))
done
next
case Unknown
show ?thesis using Unknown_actions_False
by (metis Cons.IH Cons.prems Rule Unknown nomatchD process_ret.simps(10) seqE_cons seq_cons)
next
case Goto thus ?thesis  using Unknown_actions_False
by (metis Cons.IH Cons.prems Rule Goto nomatchD process_ret.simps(8) seqE_cons seq_cons)
qed
qed
qed simp

apply(cases "map (λr. MatchNot (get_match r)) [r←rs1 . (get_action r) = Return]")
done

text ‹Completeness›
theorem unfolding_complete: "Γ,γ,p⊢ ⟨rs,s⟩ ⇒ t  ⟹  Γ,γ,p⊢ ⟨process_call Γ rs,s⟩ ⇒ t"
proof (induction rule: iptables_bigstep_induct)
case (Nomatch m a)
thus ?case
next
case Seq
thus ?case
next
case (Call_return m a chain rs⇩1 m' rs⇩2)
hence "Γ,γ,p⊢ ⟨rs⇩1, Undecided⟩ ⇒ Undecided"
by simp
hence "Γ,γ,p⊢ ⟨process_ret rs⇩1, Undecided⟩ ⇒ Undecided"
by (rule iptables_bigstep_process_ret_undecided)
with Call_return have "Γ,γ,p⊢ ⟨process_ret rs⇩1 @ add_missing_ret_unfoldings rs⇩1 (add_match (MatchNot m') (process_ret rs⇩2)), Undecided⟩ ⇒ Undecided"
with Call_return show ?case
next
case Call_result
thus ?case
qed (auto intro: iptables_bigstep.intros)

lemma process_ret_cases:
"process_ret rs = rs ∨ (∃rs⇩1 rs⇩2 m. rs = rs⇩1@[Rule m Return]@rs⇩2 ∧ (process_ret rs) = rs⇩1@(process_ret ([Rule m Return]@rs⇩2)))"
proof (induction rs)
case (Cons r rs)
thus ?case
apply(cases r, rename_tac m' a')
apply(case_tac a')
apply(simp_all)
apply(erule disjE,simp,rule disjI2,elim exE,simp add: process_ret_split_obvious,
metis append_Cons process_ret_split_obvious process_ret.simps(2))+
apply(rule disjI2)
apply(rule_tac x="[]" in exI)
apply(rule_tac x="rs" in exI)
apply(rule_tac x="m'" in exI)
apply(simp)
apply(erule disjE,simp,rule disjI2,elim exE,simp add: process_ret_split_obvious,
metis append_Cons process_ret_split_obvious process_ret.simps(2))+
done
qed simp

lemma process_ret_splitcases:
obtains (id) "process_ret rs = rs"
| (split) rs⇩1 rs⇩2 m where "rs = rs⇩1@[Rule m Return]@rs⇩2" and "process_ret rs = rs⇩1@(process_ret ([Rule m Return]@rs⇩2))"
by (metis process_ret_cases)

lemma iptables_bigstep_process_ret_cases3:
assumes "Γ,γ,p⊢ ⟨process_ret rs, Undecided⟩ ⇒ Undecided"
obtains (noreturn) "Γ,γ,p⊢ ⟨rs, Undecided⟩ ⇒ Undecided"
| (return) rs⇩1 rs⇩2 m where "rs = rs⇩1@[Rule m Return]@rs⇩2" "Γ,γ,p⊢ ⟨rs⇩1, Undecided⟩ ⇒ Undecided" "matches γ m p"
proof -
have "Γ,γ,p⊢ ⟨process_ret rs, Undecided⟩ ⇒ Undecided ⟹
(Γ,γ,p⊢ ⟨rs, Undecided⟩ ⇒ Undecided) ∨
(∃rs⇩1 rs⇩2 m. rs = rs⇩1@[Rule m Return]@rs⇩2 ∧ Γ,γ,p⊢ ⟨rs⇩1, Undecided⟩ ⇒ Undecided ∧ matches γ m p)"
proof (induction rs)
case Nil thus ?case by simp
next
case (Cons r rs)
from Cons obtain m a where r: "r = Rule m a" by (cases r) simp
from r Cons show ?case
proof(cases "a ≠ Return")
case True
with r Cons.prems have prems_r: "Γ,γ,p⊢ ⟨[Rule m a], Undecided⟩ ⇒ Undecided " and prems_rs: "Γ,γ,p⊢ ⟨process_ret rs, Undecided⟩ ⇒ Undecided"
apply(erule seqE_cons, frule iptables_bigstep_to_undecided, simp)+
done
from prems_rs Cons.IH have "Γ,γ,p⊢ ⟨rs, Undecided⟩ ⇒ Undecided ∨
(∃rs⇩1 rs⇩2 m. rs = rs⇩1 @ [Rule m Return] @ rs⇩2 ∧ Γ,γ,p⊢ ⟨rs⇩1, Undecided⟩ ⇒ Undecided ∧ matches γ m p)" by simp
thus "Γ,γ,p⊢ ⟨r # rs, Undecided⟩ ⇒ Undecided ∨ (∃rs⇩1 rs⇩2 m. r # rs = rs⇩1 @ [Rule m Return] @ rs⇩2 ∧ Γ,γ,p⊢ ⟨rs⇩1, Undecided⟩ ⇒ Undecided ∧ matches γ m p)"
proof(elim disjE)
assume "Γ,γ,p⊢ ⟨rs, Undecided⟩ ⇒ Undecided"
hence "Γ,γ,p⊢ ⟨r # rs, Undecided⟩ ⇒ Undecided" using prems_r by (metis r seq'_cons)
thus ?thesis by simp
next
assume "(∃rs⇩1 rs⇩2 m. rs = rs⇩1 @ [Rule m Return] @ rs⇩2 ∧ Γ,γ,p⊢ ⟨rs⇩1, Undecided⟩ ⇒ Undecided ∧ matches γ m p)"
from this obtain rs⇩1 rs⇩2 m' where "rs = rs⇩1 @ [Rule m' Return] @ rs⇩2" and "Γ,γ,p⊢ ⟨rs⇩1, Undecided⟩ ⇒ Undecided" and "matches γ m' p" by blast
hence "∃rs⇩1 rs⇩2 m. r # rs = rs⇩1 @ [Rule m Return] @ rs⇩2 ∧ Γ,γ,p⊢ ⟨rs⇩1, Undecided⟩ ⇒ Undecided ∧ matches γ m p"
apply(rule_tac x="Rule m a # rs⇩1" in exI)
apply(rule_tac x=rs⇩2 in exI)
apply(rule_tac x=m' in exI)
using prems_r seq'_cons by fast
thus ?thesis by simp
qed
next
case False
hence "a = Return" by simp
with Cons.prems r have prems: "Γ,γ,p⊢ ⟨add_match (MatchNot m) (process_ret rs), Undecided⟩ ⇒ Undecided" by simp
show "Γ,γ,p⊢ ⟨r # rs, Undecided⟩ ⇒ Undecided ∨ (∃rs⇩1 rs⇩2 m. r # rs = rs⇩1 @ [Rule m Return] @ rs⇩2 ∧ Γ,γ,p⊢ ⟨rs⇩1, Undecided⟩ ⇒ Undecided ∧ matches γ m p)"
proof(cases "matches γ m p")
case True
(*the Cons premises are useless in this case*)
hence "∃rs⇩1 rs⇩2 m. r # rs = rs⇩1 @ Rule m Return # rs⇩2 ∧ Γ,γ,p⊢ ⟨rs⇩1, Undecided⟩ ⇒ Undecided ∧ matches γ m p"
apply(rule_tac x="[]" in exI)
apply(rule_tac x="rs" in exI)
apply(rule_tac x="m" in exI)
apply(simp add: skip r ‹a = Return›)
done
thus ?thesis by simp
next
case False
with nomatch seq_cons False r have r_nomatch: "⋀rs. Γ,γ,p⊢ ⟨rs, Undecided⟩ ⇒ Undecided ⟹ Γ,γ,p⊢ ⟨r # rs, Undecided⟩ ⇒ Undecided" by fast
note r_nomatch'=r_nomatch[simplified r ‹a = Return›] ― ‹r unfolded›
from False not_matches_add_matchNot_simp prems have "Γ,γ,p⊢ ⟨process_ret rs, Undecided⟩ ⇒ Undecided" by fast
with Cons.IH have IH: "Γ,γ,p⊢ ⟨rs, Undecided⟩ ⇒ Undecided ∨ (∃rs⇩1 rs⇩2 m. rs = rs⇩1 @ [Rule m Return] @ rs⇩2 ∧ Γ,γ,p⊢ ⟨rs⇩1, Undecided⟩ ⇒ Undecided ∧ matches γ m p)" .
thus ?thesis
proof(elim disjE)
assume "Γ,γ,p⊢ ⟨rs, Undecided⟩ ⇒ Undecided"
hence "Γ,γ,p⊢ ⟨r # rs, Undecided⟩ ⇒ Undecided" using r_nomatch by simp
thus ?thesis by simp
next
assume "∃rs⇩1 rs⇩2 m. rs = rs⇩1 @ [Rule m Return] @ rs⇩2 ∧ Γ,γ,p⊢ ⟨rs⇩1, Undecided⟩ ⇒ Undecided ∧ matches γ m p"
from this obtain rs⇩1 rs⇩2 m' where "rs = rs⇩1 @ [Rule m' Return] @ rs⇩2" and "Γ,γ,p⊢ ⟨rs⇩1, Undecided⟩ ⇒ Undecided" and "matches γ m' p" by blast
hence "∃rs⇩1 rs⇩2 m. r # rs = rs⇩1 @ [Rule m Return] @ rs⇩2 ∧ Γ,γ,p⊢ ⟨rs⇩1, Undecided⟩ ⇒ Undecided ∧ matches γ m p"
apply(rule_tac x="Rule m Return # rs⇩1" in exI)
apply(rule_tac x="rs⇩2" in exI)
apply(rule_tac x="m'" in exI)
by(simp add:  ‹a = Return› False r r_nomatch')
thus ?thesis by simp
qed
qed
qed
qed
with assms noreturn return show ?thesis by auto
qed

lemma iptables_bigstep_process_ret_DecisionD: "Γ,γ,p⊢ ⟨process_ret rs, s⟩ ⇒ Decision X ⟹ Γ,γ,p⊢ ⟨rs, s⟩ ⇒ Decision X"
proof (induction rs arbitrary: s)
case (Cons r rs)
thus ?case
apply(cases r, rename_tac m a)
apply(clarify)

apply(case_tac "a ≠ Return")
apply(erule seqE_cons)

apply(simp) (*case a = AReturn*)

apply(case_tac "matches γ m p")
apply (metis decision skipD)

(*case ¬ matches*)
by (metis decision state.exhaust nomatch seq'_cons)
qed simp

subsection‹@{const process_ret} correctness›
lemma process_ret_add_match_dist1: "Γ,γ,p⊢ ⟨process_ret (add_match m rs), s⟩ ⇒ t ⟹ Γ,γ,p⊢ ⟨add_match m (process_ret rs), s⟩ ⇒ t"
apply(induction rs arbitrary: s t)
apply(rename_tac r rs s t)
apply(case_tac r)
apply(rename_tac m' a')
apply(simp)
apply(case_tac a')
apply(erule seqE_cons)
using seq' apply(fastforce)
apply(erule seqE_cons)
using seq' apply(fastforce)
apply(erule seqE_cons)
using seq' apply(fastforce)
apply(erule seqE_cons)
using seq' apply(fastforce)
apply(erule seqE_cons)
using seq' apply(fastforce)
defer
apply(erule seqE_cons)
using seq' apply(fastforce)
apply(erule seqE_cons)
using seq' apply(fastforce)
apply(case_tac "matches γ (MatchNot (MatchAnd m m')) p")
apply(simp)
apply (meson seq'_cons seqE_cons)
apply (meson seq'_cons seqE_cons)

lemma process_ret_add_match_dist2: "Γ,γ,p⊢ ⟨add_match m (process_ret rs), s⟩ ⇒ t ⟹ Γ,γ,p⊢ ⟨process_ret (add_match m rs), s⟩ ⇒ t"
apply(induction rs arbitrary: s t)
apply(rename_tac r rs s t)
apply(case_tac r)
apply(rename_tac m' a')
apply(simp)
apply(case_tac a')
apply(erule seqE_cons)
using seq' apply(fastforce)
apply(erule seqE_cons)
using seq' apply(fastforce)
apply(erule seqE_cons)
using seq' apply(fastforce)
apply(erule seqE_cons)
using seq' apply(fastforce)
apply(erule seqE_cons)
using seq' apply(fastforce)
defer
apply(erule seqE_cons)
using seq' apply(fastforce)
apply(erule seqE_cons)
using seq' apply(fastforce)
apply(case_tac "matches γ (MatchNot (MatchAnd m m')) p")
apply(simp)
apply (meson seq'_cons seqE_cons)
apply (meson seq'_cons seqE_cons)

(*such fuckup*)
lemma process_ret_add_match_dist: "Γ,γ,p⊢ ⟨process_ret (add_match m rs), s⟩ ⇒ t ⟷ Γ,γ,p⊢ ⟨add_match m (process_ret rs), s⟩ ⇒ t"

lemma process_ret_Undecided_sound:
assumes "Γ(chain ↦ rs),γ,p⊢ ⟨process_ret (add_match m rs), Undecided⟩ ⇒ Undecided"
shows "Γ(chain ↦ rs),γ,p⊢ ⟨[Rule m (Call chain)], Undecided⟩ ⇒ Undecided"
proof (cases "matches γ m p")
case False
thus ?thesis
by (metis nomatch)
next
case True
note matches = this
show ?thesis
using assms proof (induction rs)
case Nil
from call_result[OF matches, where Γ="Γ(chain ↦ [])"]
have "(Γ(chain ↦ [])) chain = Some [] ⟹ Γ(chain ↦ []),γ,p⊢ ⟨[], Undecided⟩ ⇒ Undecided ⟹ Γ(chain ↦ []),γ,p⊢ ⟨[Rule m (Call chain)], Undecided⟩ ⇒ Undecided"
by simp
thus ?case
by (fastforce intro: skip)
next
case (Cons r rs)
obtain m' a' where r: "r = Rule m' a'" by (cases r) blast

with Cons.prems have prems: "Γ(chain ↦ Rule m' a' # rs),γ,p⊢ ⟨process_ret (add_match m (Rule m' a' # rs)), Undecided⟩ ⇒ Undecided"
by fast
hence prems_simplified: "Γ(chain ↦ Rule m' a' # rs),γ,p⊢ ⟨process_ret (Rule m' a' # rs), Undecided⟩ ⇒ Undecided"

have "Γ(chain ↦ Rule m' a' # rs),γ,p⊢ ⟨[Rule m (Call chain)], Undecided⟩ ⇒ Undecided"
proof (cases "a' = Return")
case True
note a' = this
have "Γ(chain ↦ Rule m' Return # rs),γ,p⊢ ⟨[Rule m (Call chain)], Undecided⟩ ⇒ Undecided"
proof (cases "matches γ m' p")
case True
with matches show ?thesis
by (fastforce intro: call_return skip)
next
case False
note matches' = this
hence "Γ(chain ↦ rs),γ,p⊢ ⟨process_ret (Rule m' a' # rs), Undecided⟩ ⇒ Undecided"
by (metis prems_simplified update_Gamma_nomatch)
with a' have "Γ(chain ↦ rs),γ,p⊢ ⟨add_match (MatchNot m') (process_ret rs), Undecided⟩ ⇒ Undecided"
by simp
with matches matches' have "Γ(chain ↦ rs),γ,p⊢ ⟨add_match m (process_ret rs), Undecided⟩ ⇒ Undecided"
with matches' Cons.IH show ?thesis
qed
with a' show ?thesis
by simp
next
case False
note a' = this
with prems_simplified have "Γ(chain ↦ Rule m' a' # rs),γ,p⊢ ⟨Rule m' a' # process_ret rs, Undecided⟩ ⇒ Undecided"
hence step: "Γ(chain ↦ Rule m' a' # rs),γ,p⊢ ⟨[Rule m' a'], Undecided⟩ ⇒ Undecided"
and   IH_pre: "Γ(chain ↦ Rule m' a' # rs),γ,p⊢ ⟨process_ret rs, Undecided⟩ ⇒ Undecided"
by (metis seqE_cons iptables_bigstep_to_undecided)+

from step have "Γ(chain ↦ rs),γ,p⊢ ⟨process_ret rs, Undecided⟩ ⇒ Undecided"
proof (cases rule: Rule_UndecidedE)
case log thus ?thesis
using IH_pre by (metis empty iptables_bigstep.log update_Gamma_nochange1 update_Gamma_nomatch)
next
case call thus ?thesis
using IH_pre by (metis update_Gamma_remove_call_undecided)
next
case nomatch thus ?thesis
using IH_pre by (metis update_Gamma_nomatch)
qed

hence "Γ(chain ↦ rs),γ,p⊢ ⟨process_ret (add_match m rs), Undecided⟩ ⇒ Undecided"
with Cons.IH have IH: "Γ(chain ↦ rs),γ,p⊢ ⟨[Rule m (Call chain)], Undecided⟩ ⇒ Undecided"
by fast

from step show ?thesis
proof (cases rule: Rule_UndecidedE)
case log thus ?thesis using IH
next
case nomatch
thus ?thesis
using IH by (metis update_Gamma_nomatch)
next
case (call c)
let ?Γ' = "Γ(chain ↦ Rule m' a' # rs)"
from IH_pre show ?thesis
proof (cases rule: iptables_bigstep_process_ret_cases3)
case noreturn
with call have "?Γ',γ,p⊢ ⟨Rule m' (Call c) # rs, Undecided⟩ ⇒ Undecided"
by (metis step seq_cons)
from call have "?Γ' chain = Some (Rule m' (Call c) # rs)"
by simp
from matches show ?thesis
by (rule call_result) fact+
next
case (return rs⇩1 rs⇩2 new_m')
with call have "?Γ' chain = Some ((Rule m' (Call c) # rs⇩1) @ [Rule new_m' Return] @ rs⇩2)"
by simp
from call return step have "?Γ',γ,p⊢ ⟨Rule m' (Call c) # rs⇩1, Undecided⟩ ⇒ Undecided"
using IH_pre by (auto intro: seq_cons)
from matches show ?thesis
by (rule call_return) fact+
qed
qed
qed
thus ?case
by (metis r)
qed
qed

lemma process_ret_Decision_sound:
assumes "Γ(chain ↦ rs),γ,p⊢ ⟨process_ret (add_match m rs), Undecided⟩ ⇒ Decision X"
shows "Γ(chain ↦ rs),γ,p⊢ ⟨[Rule m (Call chain)], Undecided⟩ ⇒ Decision X"
proof (cases "matches γ m p")
case False
next
case True
note matches = this
show ?thesis
using assms proof (induction rs)
case Nil
hence False by (metis add_match_split append_self_conv state.distinct(1) process_ret.simps(1) skipD)
thus ?case by simp
next
case (Cons r rs)
obtain m' a' where r: "r = Rule m' a'" by (cases r) blast

with Cons.prems have prems: "Γ(chain ↦ Rule m' a' # rs),γ,p⊢ ⟨process_ret (add_match m (Rule m' a' # rs)), Undecided⟩ ⇒ Decision X"
by fast
hence prems_simplified: "Γ(chain ↦ Rule m' a' # rs),γ,p⊢ ⟨process_ret (Rule m' a' # rs), Undecided⟩ ⇒ Decision X"

have "Γ(chain ↦ Rule m' a' # rs),γ,p⊢ ⟨[Rule m (Call chain)], Undecided⟩ ⇒ Decision X"
proof (cases "a' = Return")
case True
note a' = this
have "Γ(chain ↦ Rule m' Return # rs),γ,p⊢ ⟨[Rule m (Call chain)], Undecided⟩ ⇒ Decision X"
proof (cases "matches γ m' p")
case True
with matches prems_simplified a' show ?thesis
by (auto simp: not_matches_add_match_simp dest: skipD)
next
case False
note matches' = this
with prems_simplified have "Γ(chain ↦ rs),γ,p⊢ ⟨process_ret (Rule m' a' # rs), Undecided⟩ ⇒ Decision X"
by (metis update_Gamma_nomatch)
with a' matches matches' have "Γ(chain ↦ rs),γ,p⊢ ⟨add_match m (process_ret rs), Undecided⟩ ⇒ Decision X"
with matches matches' Cons.IH show ?thesis
qed
with a' show ?thesis
by simp
next
case False
with prems_simplified obtain ti
where step: "Γ(chain ↦ Rule m' a' # rs),γ,p⊢ ⟨[Rule m' a'], Undecided⟩ ⇒ ti"
and IH_pre: "Γ(chain ↦ Rule m' a' # rs),γ,p⊢ ⟨process_ret rs, ti⟩ ⇒ Decision X"
by (auto simp: process_ret_split_fst_NeqReturn elim: seqE_cons)

hence "Γ(chain ↦ Rule m' a' # rs),γ,p⊢ ⟨rs, ti⟩ ⇒ Decision X"
by (metis iptables_bigstep_process_ret_DecisionD)

thus ?thesis
using matches step by (force intro: call_result seq'_cons)
qed
thus ?case
by (metis r)
qed
qed

lemma process_ret_result_empty: "[] = process_ret rs ⟹ ∀r ∈ set rs. get_action r = Return"
proof (induction rs)
case (Cons r rs)
thus ?case
apply(simp)
apply(case_tac r)
apply(rename_tac m a)
apply(case_tac a)
done
qed simp

lemma process_ret_sound':
assumes "Γ(chain ↦ rs),γ,p⊢ ⟨process_ret (add_match m rs), Undecided⟩ ⇒ t"
shows "Γ(chain ↦ rs),γ,p⊢ ⟨[Rule m (Call chain)], Undecided⟩ ⇒ t"
using assms by (metis state.exhaust process_ret_Undecided_sound process_ret_Decision_sound)

lemma wf_chain_process_ret: "wf_chain Γ rs ⟹ wf_chain Γ (process_ret rs)"
apply(induction rs)
apply(case_tac a)
apply(case_tac "x2 ≠ Return")
using wf_chain_append apply (metis Cons_eq_appendI append_Nil)
done

subsection‹Soundness›
theorem unfolding_sound: "wf_chain Γ rs ⟹ Γ,γ,p⊢ ⟨process_call Γ rs, s⟩ ⇒ t ⟹ Γ,γ,p⊢ ⟨rs, s⟩ ⇒ t"
proof (induction rs arbitrary: s t)
case (Cons r rs)
thus ?case
apply -
apply(subst(asm) process_call_split_fst)
apply(erule seqE)

unfolding wf_chain_def
apply(case_tac r, rename_tac m a)
apply(case_tac a)

apply(case_tac s)
defer
apply (metis decision decisionD)
apply(case_tac "matches γ m p")
defer
apply(drule skipD, simp)
apply (metis nomatch seq_cons)
apply(clarify)
apply(rule_tac t=ti in seq_cons)
apply(simp_all)

using process_ret_sound'
qed simp

corollary unfolding_sound_complete: "wf_chain Γ rs ⟹ Γ,γ,p⊢ ⟨process_call Γ rs, s⟩ ⇒ t ⟷ Γ,γ,p⊢ ⟨rs, s⟩ ⇒ t"
by (metis unfolding_complete unfolding_sound)

corollary unfolding_n_sound_complete: "∀rsg ∈ ran Γ ∪ {rs}. wf_chain Γ rsg ⟹ Γ,γ,p⊢ ⟨((process_call Γ)^^n) rs, s⟩ ⇒ t ⟷ Γ,γ,p⊢ ⟨rs, s⟩ ⇒ t"
proof(induction n arbitrary: rs)
case 0 thus ?case by simp
next
case (Suc n)
from Suc have "Γ,γ,p⊢ ⟨(process_call Γ ^^ n) rs, s⟩ ⇒ t = Γ,γ,p⊢ ⟨rs, s⟩ ⇒ t" by blast
from Suc.prems have "∀a∈ran Γ ∪ {process_call Γ rs}. wf_chain Γ a"
proof(induction rs)
case Nil thus ?case by simp
next
case(Cons r rs)
from Cons.prems have "∀a∈ran Γ. wf_chain Γ a" by blast
from Cons.prems have "wf_chain Γ [r]"
apply(simp)
apply(clarify)
done
from Cons.prems have "wf_chain Γ rs"
apply(simp)
apply(clarify)
done
from this Cons.prems Cons.IH have "wf_chain Γ (process_call Γ rs)" by blast
from this ‹wf_chain Γ [r]›have "wf_chain Γ (r # (process_call Γ rs))" by(simp add: wf_chain_def)
from this Cons.prems have "wf_chain Γ (process_call Γ (r#rs))"
apply(cases r)
apply(rename_tac m a, clarify)
apply(case_tac a)
apply(simp_all)
apply(clarify)
apply(simp add: ‹wf_chain Γ (process_call Γ rs)›)
apply(rule wf_chain_process_ret)
apply(clarify)
by (metis ranI option.sel)
from this ‹∀a∈ran Γ. wf_chain Γ a› show ?case by simp
qed
from this Suc.IH[of "((process_call Γ) rs)"] have
"Γ,γ,p⊢ ⟨(process_call Γ ^^ n) (process_call Γ rs), s⟩ ⇒ t = Γ,γ,p⊢ ⟨process_call Γ rs, s⟩ ⇒ t"
by simp
from this show ?case by (simp add: Suc.prems funpow_swap1 unfolding_sound_complete)
qed

text_raw‹
\begin{verbatim}
loops in the linux kernel:
http://lxr.linux.no/linux+v3.2/net/ipv4/netfilter/ip_tables.c#L464
/* Figures out from what hook each rule can be called: returns 0 if
there are loops.  Puts hook bitmask in comefrom. */
static int mark_source_chains(const struct xt_table_info *newinfo,
unsigned int valid_hooks, void *entry0)

discussion: http://marc.info/?l=netfilter-devel&m=105190848425334&w=2
\end{verbatim}
›

text‹Example›
lemma "process_call [''X'' ↦ [Rule (Match b) Return, Rule (Match c) Accept]] [Rule (Match a) (Call ''X'')] =
[Rule (MatchAnd (Match a) (MatchAnd (MatchNot (Match b)) (Match c))) Accept]" by (simp add: add_match_def)

text‹This is how a firewall processes a ruleset.
It starts at a certain chain, usually INPUT, FORWARD, or OUTPUT (called @{term chain_name} in the lemma).
The firewall has a default action of accept or drop.
We can check @{const sanity_wf_ruleset} and the other assumptions at runtime.
Consequently, we can apply @{const repeat_stabilize} as often as we want.
›

theorem repeat_stabilize_process_call:
assumes "sanity_wf_ruleset Γ" and "chain_name ∈ set (map fst Γ)" and "default_action = Accept ∨ default_action = Drop"
shows "(map_of Γ),γ,p⊢ ⟨repeat_stabilize n (process_call (map_of Γ)) [Rule MatchAny (Call chain_name), Rule MatchAny default_action], s⟩ ⇒ t ⟷
(map_of Γ),γ,p⊢ ⟨[Rule MatchAny (Call chain_name), Rule MatchAny default_action], s⟩ ⇒ t"
proof -
have x: "sanity_wf_ruleset Γ ⟹ rs ∈ ran (map_of Γ) ⟹ wf_chain (map_of Γ) rs" for Γ and rs::"'a rule list"
by fastforce

from assms(1) have 1: "∀rsg ∈ ran (map_of Γ). wf_chain (map_of Γ) rsg"
apply(intro ballI)
apply(drule x, simp)
apply(simp)
done
let ?rs="[Rule MatchAny (Call chain_name), Rule MatchAny default_action]::'a rule list"
from assms(2,3) have 2: "wf_chain (map_of Γ) ?rs"
by blast

have "∀rsg ∈ ran Γ ∪ {rs}. wf_chain Γ rsg ⟹
Γ,γ,p⊢ ⟨repeat_stabilize n (process_call Γ) rs, s⟩ ⇒ t ⟷ Γ,γ,p⊢ ⟨rs, s⟩ ⇒ t" for Γ rs
moreover from 1 2 have "∀rsg ∈ ran (map_of Γ) ∪ {?rs}. wf_chain (map_of Γ) rsg" by simp
ultimately show ?thesis by simp
qed

definition unfold_optimize_ruleset_CHAIN
:: "('a match_expr ⇒ 'a match_expr) ⇒ string ⇒ action ⇒ 'a ruleset ⇒ 'a rule list option"
where
"unfold_optimize_ruleset_CHAIN optimize chain_name default_action rs = (let rs =
(repeat_stabilize 1000 (optimize_matches opt_MatchAny_match_expr)
(optimize_matches optimize
(rw_Reject (rm_LogEmpty (repeat_stabilize 10000 (process_call rs)
[Rule MatchAny (Call chain_name), Rule MatchAny default_action]
)))))
in if simple_ruleset rs then Some rs else None)"

lemma unfold_optimize_ruleset_CHAIN:
assumes "sanity_wf_ruleset Γ" and "chain_name ∈ set (map fst Γ)"
and "default_action = Accept ∨ default_action = Drop"
and "⋀m. matches γ (optimize m) p = matches γ m p"
and "unfold_optimize_ruleset_CHAIN optimize chain_name default_action (map_of Γ) = Some rs"
shows "(map_of Γ),γ,p⊢ ⟨rs, s⟩ ⇒ t ⟷
(map_of Γ),γ,p⊢ ⟨[Rule MatchAny (Call chain_name), Rule MatchAny default_action], s⟩ ⇒ t"
proof -
from assms(5) have rs: "rs = repeat_stabilize 1000 (optimize_matches opt_MatchAny_match_expr)
(optimize_matches optimize
(rw_Reject
(rm_LogEmpty
(repeat_stabilize 10000 (process_call (map_of Γ)) [Rule MatchAny (Call chain_name), Rule MatchAny default_action]))))"
by(simp add: unfold_optimize_ruleset_CHAIN_def Let_def split: if_split_asm)

have optimize_matches_generic_funpow_helper: "(⋀m. matches γ (f m) p = matches γ m p) ⟹
Γ,γ,p⊢ ⟨(optimize_matches f ^^ n) rs, s⟩ ⇒ t ⟷ Γ,γ,p⊢ ⟨rs, s⟩ ⇒ t"
for Γ f n rs
proof(induction n arbitrary:)
case 0 thus ?case by simp
next
case (Suc n) thus ?case
apply(simp)
apply(subst optimize_matches_generic[where P="λ_. True"])
by simp_all
qed

have "(map_of Γ),γ,p⊢ ⟨rs, s⟩ ⇒ t ⟷ map_of Γ,γ,p⊢ ⟨repeat_stabilize 10000 (process_call (map_of Γ))
[Rule MatchAny (Call chain_name), Rule MatchAny default_action], s⟩ ⇒ t"
apply(subst optimize_matches_generic_funpow_helper)
apply(subst optimize_matches_generic[where P="λ_. True"], simp_all add: assms(4))
done
also have "… ⟷ (map_of Γ),γ,p⊢ ⟨[Rule MatchAny (Call chain_name), Rule MatchAny default_action], s⟩ ⇒ t"
using assms(1,2,3) by(intro repeat_stabilize_process_call[of Γ chain_name default_action γ p 10000 s t]) simp_all
finally show ?thesis .
qed

end


# Theory Ternary

section‹Ternary Logic›
theory Ternary
imports Main
begin

text‹Kleene logic›

datatype ternaryvalue = TernaryTrue | TernaryFalse | TernaryUnknown
datatype ternaryformula = TernaryAnd ternaryformula ternaryformula
| TernaryOr ternaryfor