Session Iptables_Semantics

Theory List_Misc

section‹Miscellaneous List Lemmas›
theory List_Misc
imports Main
begin

lemma list_app_singletonE:
  assumes "rs1 @ rs2 = [x]"
  obtains (first) "rs1 = [x]" "rs2 = []"
        | (second) "rs1 = []" "rs2 = [x]"
using assms
by (cases "rs1") auto

lemma list_app_eq_cases:
  assumes "xs1 @ xs2 = ys1 @ ys2"
  obtains (longer)  "xs1 = take (length xs1) ys1" "xs2 = drop (length xs1) ys1 @ ys2"
        | (shorter) "ys1 = take (length ys1) xs1" "ys2 = drop (length ys1) xs1 @ xs2"
using assms by (cases "length xs1  length ys1") (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(simp add: getPos_set)
  apply(rule iffI)
  apply(simp_all add: getPos_set getNeg_set)
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: "(isset Ms. case is of Pos i  P i | Neg i  Q i)  (iset (getPos Ms). P i)  (iset (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
imports IP_Addresses.WordInterval
  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(simp add: l2wi)
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(simp add: l2wi_intersect l2wi)
  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})"
  by(simp add: l2wi_negation_type_intersect_alt l2wi_intersect l2wi)

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(simp add: repeat_stabilize_funpow)
  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] = rs1 @ rs2 
   (rs1 = [Rule m a]  rs2 = []  P m a) 
   (rs1 = []  rs2 = [Rule m a]  P m a)  P m a"
by (cases rs1) 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"
  by(simp add: rm_LogEmpty_filter)





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 (rs1 @ rs2)  simple_ruleset rs1  simple_ruleset rs2"
    by(simp add: simple_ruleset_def, blast)







text‹Structural properties about match expressions›
  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)
  qed(simp_all add: simple_ruleset_def split: option.split)

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"
  by(simp add: optimize_matches_def optimize_matches_option_append)

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

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)"
  by(simp add: optimize_matches_def optimize_matches_option_simple_ruleset)


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)"
  by(simp add: optimize_matches_a_def simple_ruleset_def)

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)
 apply(simp add: optimize_matches_a_def)
apply(simp add: optimize_matches_a_def)
apply(simp add: simple_ruleset_def)
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)"
  by(induction rs)(simp_all add: optimize_matches_a_def)



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,
    ports, payload, ...›


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 rs1, Undecided  t; Γ,γ,p rs2, t  t'  Γ,γ,p rs1@rs2, Undecided  t'" |
call_return:  " matches γ m p; Γ chain = Some (rs1@[Rule m' Return]@rs2);
                 matches γ m' p; Γ,γ,p rs1, 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 rs1 rs2 t t'. rs = rs1 @ rs2  Γ,γ,p rs1,Undecided  t  P rs1 Undecided t  Γ,γ,p rs2,t  t'  P rs2 t t'  P rs Undecided t';
     m a chain rs1 m' rs2. matches γ m p  a = Call chain  Γ chain = Some (rs1 @ [Rule m' Return] @ rs2)  matches γ m' p  Γ,γ,p rs1,Undecided  Undecided  P rs1 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"
        | rs1 rs2 m' where "rs = rs1 @ Rule m' Return # rs2" "matches γ m' p" "Γ,γ,p rs1,s  Undecided" "t = Undecided"
  using assms
  proof (induction r s t arbitrary: rs rule: iptables_bigstep.induct)
    case (seq rs1)
    thus ?case by (cases rs1) auto
  qed auto

end

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

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

lemma seqE:
  assumes "Γ,γ,p rs1@rs2, s  t"
  obtains ti where "Γ,γ,p rs1,s  ti" "Γ,γ,p rs2,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 "rset 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 rs1)
      thus ?case
        by (cases rs1) (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 = rs1@rs2  Γ,γ,p rs1, s  t'  Γ,γ,p rs2, t'  t"
  proof(induction arbitrary: rs1 rs2 t' rule: iptables_bigstep_induct)
    case Allow
    thus ?case
      by (cases "rs1") (auto intro: iptables_bigstep.intros dest: iptables_bigstepD)
  next
    case Deny
    thus ?case
      by (cases "rs1") (auto intro: iptables_bigstep.intros dest: iptables_bigstepD)
  next
    case Log
    thus ?case
      by (cases "rs1") (auto intro: iptables_bigstep.intros dest: iptables_bigstepD)
  next
    case Nomatch
    thus ?case
      by (cases "rs1") (auto intro: iptables_bigstep.intros dest: iptables_bigstepD)
  next
    case Decision
    thus ?case
      by (cases "rs1") (auto intro: iptables_bigstep.intros dest: iptables_bigstepD)
  next
    case(Seq rs rsa rsb t t' rs1 rs2 t'')
    hence rs: "rsa @ rsb = rs1 @ rs2" by simp
    note List.append_eq_append_conv_if[simp]
    (* TODO larsrh custom case distinction rule *)

    from rs show "Γ,γ,p rs2,t''  t'"
      proof(cases rule: list_app_eq_cases)
        case longer
        have "rs1 = take (length rsa) rs1 @ drop (length rsa) rs1"
          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 rs1)
        case (Cons r rs)
        thus ?thesis
          using Call_return
          apply(case_tac "[Rule m a] = rs2")
           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 rs1)
        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 rs1)
    thus ?case
      by (cases rs1) (auto dest: skipD)
  qed simp_all


lemma log_remove:
  assumes "Γ,γ,p rs1 @ [Rule m Log] @ rs2, s  t"
  shows "Γ,γ,p rs1 @ rs2, s  t"
  proof -
    from assms obtain t' where t': "Γ,γ,p rs1, s  t'" "Γ,γ,p [Rule m Log] @ rs2, t'  t"
      by (blast elim: seqE)
    hence "Γ,γ,p Rule m Log # rs2, t'  t"
      by simp
    then obtain t'' where "Γ,γ,p [Rule m Log], t'  t''" "Γ,γ,p rs2, 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 rs1 @ [Rule m Empty] @ rs2, s  t"
  shows "Γ,γ,p rs1 @ rs2, s  t"
  proof -
    from assms obtain t' where t': "Γ,γ,p rs1, s  t'" "Γ,γ,p [Rule m Empty] @ rs2, t'  t"
      by (blast elim: seqE)
    hence "Γ,γ,p Rule m Empty # rs2, t'  t"
      by simp
    then obtain t'' where "Γ,γ,p [Rule m Empty], t'  t''" "Γ,γ,p rs2, 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⊢' rs1, Undecided  t; p⊢' rs2, t  t'  p⊢' rs1@rs2, Undecided  t'" |
  call_return:  " matches γ m p; Γ chain = Some (rs1@[Rule m' Return]@rs2);
                   matches γ m' p; p⊢' rs1, 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"
    by(simp add: wf_Γ_def, blast)
  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)"
    apply(simp add: wf_Γ_def)
    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"
  by(simp add: wf_chain_def, blast)

lemma wf_chain_fst: "wf_chain Γ (r # rs)   wf_chain Γ (rs)"
  by(simp add: wf_chain_def)


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"
  apply(simp add: sanity_wf_ruleset_def wf_chain_def)
  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(simp add: sanity_wf_ruleset_def wf_chain_def)
 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 Γ)"
    by (simp add: dom_map_of_conv_image_fst)
  have set_map_snd: "distinct (map fst Γ)  set (map snd Γ) = ran (map_of Γ)"
    by (simp add: ran_distinct)
  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)
 by(simp add: skip)
next
case (Cons r rs)
  from Cons.prems Cons.IH obtain t' where t': "Γ,γ,p rs, s  t'"
    apply simp
    apply(elim conjE)
    apply(simp add: wf_chain_fst)
    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)
       apply(simp add: nomatch r)
      by(simp add: decision)
    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)
      by(simp add: decision)
    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(simp add: r)
          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 Γ)"
    apply(simp add: calls_chain_def called_by_chain_def)
    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)
    apply(simp add: called_by_chain_converse)
    done
  
  
  private lemma helper_cases_call_subchain_defined_or_return:
        "(xran Γ. wf_chain Γ x) 
         rsgran Γ. rset rsg. (chain. get_action r  Goto chain)  get_action r  Unknown 
         y m. rset rs_called. r = Rule m (Call y)  (t. Γ,γ,p [Rule m (Call y)], Undecided  t) 
         wf_chain Γ rs_called  
         rset 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)
     by(simp add: skip)
   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)
        apply(simp add: r; fail)
        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(simp_all add: a_not)
    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(simp add: r pre)
      apply(rule_tac t=Undecided in seq_cons)
       apply(simp add: r nomatch; fail)
      apply(simp add: pre; fail)
      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)
         apply(simp add: r; fail)
        apply(simp add: decision; fail)
        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(simp add: r)
        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(simp add: r)
         apply(rule_tac t=Undecided in seq_cons)
          apply(simp add: r; fail)
         apply(simp; fail)
        apply(rule disjI1)
        apply(rule_tac x=t_called in exI)
        apply(rule_tac t=t_called in seq_cons)
         apply(simp add: r; fail)
        apply(simp add: decision; fail)
        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(simp_all add: a_not)
    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(simp add: r)
        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)
             apply(simp add: r nomatch; fail)
            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)
            apply(simp add: r skip; fail)
            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)) 
      apply(simp add: skip; fail)
      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 Γ)"
            "rsgran Γ. wf_chain Γ rsg"
            "rsgran Γ. rset 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(simp add: called_by_chain_def)
              apply blast
             apply(simp add: wf_chain_def)
             apply (meson ranI rule.sel(2))
             done
          with less have "y m. rset 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)
             apply(simp add: nomatch; fail)
             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(simp add: wf_chain_def; 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 add: log; fail)
      apply(simp add: nomatch; fail)
     apply(simp add: decision; fail)
    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 add: empty; fail)
      apply(simp add: nomatch; fail)
     apply(simp add: decision; fail)
    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)
   apply(simp_all add: case_log case_empty)
  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)
   apply(simp add: dropreject)
  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"
  by(simp add: MatchOr_def)

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
   apply(simp add: fun_eq_iff)
   by(induction m rule: opt_MatchAny_match_expr_once.induct) (simp_all)
   thus ?thesis
    apply(simp add: opt_MatchAny_match_expr_def)
    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
    by (simp add: matches_rule_and_simp_help)
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


subsection‹Add match›

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"

lemma add_match_split: "add_match m (rs1@rs2) = add_match m rs1 @ add_match m rs2"
  unfolding add_match_def
  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"
  unfolding add_match_def
  by simp


lemma add_match_distrib:
  "Γ,γ,p add_match m1 (add_match m2 rs), s  t  Γ,γ,p add_match m2 (add_match m1 rs), s  t"
proof -
  {
    fix m1 m2
    have "Γ,γ,p add_match m1 (add_match m2 rs), s  t  Γ,γ,p add_match m2 (add_match m1 rs), s  t"
      proof (induction rs arbitrary: s)
        case Nil thus ?case by (simp add: add_match_def)
        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(simp add: add_match_split_fst)
          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
        thus ?case using r by(simp add: add_match_split_fst[symmetric])
      qed
  }
  thus ?thesis by blast
qed

lemma add_match_split_fst': "add_match m (a # rs) = add_match m [a] @ add_match m rs"
  by (simp add: add_match_split[symmetric])



lemma matches_add_match_simp:
  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
          unfolding add_match_def by simp
      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"
          by(auto elim:seqE_cons simp add: add_match_split_fst)
        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
          unfolding add_match_def by simp
      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"
          by(auto elim:seqE_cons simp add: add_match_split_fst)
        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 
          apply(simp add: add_match_split_fst)
          by(metis decision state.exhaust iptables_bigstep_deterministic seq_cons)
      qed
  qed

lemma matches_add_match_MatchNot_simp:
  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
              unfolding add_match_def by simp
          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
              unfolding add_match_def by simp
          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

lemma not_matches_add_match_simp:
  assumes "¬ matches γ m p"
  shows "Γ,γ,p add_match m rs, Undecided  t  Γ,γ,p [], Undecided  t"
  proof(induction rs)
    case Nil
    thus ?case
      unfolding add_match_def by simp
  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

lemma iptables_bigstep_add_match_notnot_simp: 
  "Γ,γ,p add_match (MatchNot (MatchNot m)) rs, s  t  Γ,γ,p add_match m rs, s  t"
  proof(induction rs)
    case Nil
    thus ?case
      unfolding add_match_def by simp
  next
    case (Cons r rs)
    thus ?case
      by (cases r)
         (metis decision decisionD state.exhaust matches.simps(2) matches_add_match_simp not_matches_add_match_simp)
  qed


lemma add_match_match_not_cases:
  "Γ,γ,p add_match (MatchNot m) rs, Undecided  Undecided  matches γ m p  Γ,γ,p rs, Undecided  Undecided"
  by (metis matches.simps(2) matches_add_match_simp)


lemma not_matches_add_matchNot_simp:
  "¬ matches γ m p  Γ,γ,p add_match (MatchNot m) rs, s  t  Γ,γ,p rs, s  t"
  by (simp add: matches_add_match_simp)

lemma iptables_bigstep_add_match_and:
  "Γ,γ,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
      unfolding add_match_def by simp
  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 add_match_split_fst matches.simps(1) matches_add_match_simp not_matches_add_match_simp 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 add_match_split_fst matches.simps(1) matches_add_match_simp not_matches_add_match_simp 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' rs1 m' rs2)
        thus ?case
          proof (cases "chain' = chain")
            case True
            with Call_return show ?thesis
              apply simp
              apply(cases "rs1")
              using assms apply fastforce
              apply(rule_tac rs1="list" and m'="m'" and rs2="rs2" 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' rs1)
        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 rs1 = "Rule m a # rs1"])
          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' rs1 m'' rs2)
        (*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 rs1} cannot be empty›
            proof(cases "rs1")
            case Nil with Call_return(3) chain' = chain assms have "False" by simp
              thus ?Call_return_case by simp
            next
            case (Cons r1 rs1s)
            from Cons Call_return have "Γ(chain  rs),γ,p r1 # rs1s, Undecided  Undecided" by blast
            with seqE_cons[where Γ="Γ(chain  rs)"] obtain ti where 
              "Γ(chain  rs),γ,p [r1], Undecided  ti" and "Γ(chain  rs),γ,p rs1s, ti  Undecided" by metis
            with iptables_bigstep_to_undecided[where Γ="Γ(chain  rs)"] have "Γ(chain  rs),γ,p rs1s, Undecided  Undecided" by fast
            with Cons Call_return chain' = chain show ?Call_return_case
               apply(rule_tac rs1="rs1s" and m'="m''" and rs2="rs2" 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' rs1 m'' rs2)
        from Call_return have xx: "Γ(chain  Rule m a # rs),γ,p Rule m a # rs1, 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 (rs1 @ Rule m'' Return # rs2)"
              by(simp)
            with Call_return have "Γ(chain  Rule m a # rs),γ,p [Rule m' (Call chain')], Undecided  Undecided"
             apply -
             apply(rule call_return[where rs1="rs1" and m'="m''" and rs2="rs2"])
                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 # rs1 @ Rule m'' Return # rs2)"
              by(simp)
            with Call_return have "Γ(chain  Rule m a # rs),γ,p [Rule m' (Call chain')], Undecided  Undecided"
             apply -
             apply(rule call_return[where rs1="Rule m a#rs1" and m'="m''" and rs2="rs2"])
                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' rs1 m' rs2)
    hence "rs1 @ Rule m' Return # rs2 = [Rule m (Call chain')]"
      by simp
    thus ?case
      by (cases "rs1") 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 rs1 rs2 t)
    thus ?case
      by (cases rs1) (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 rs1 m' rs2)
    thus ?case
      proof (cases "chaina = chain")
        case True
        with Call_return show ?thesis
          apply simp
          apply(cases "rs1")
          apply(simp)
          using assms apply (metis no_free_return) (*gives False*)
          apply(rule_tac rs1="list" and m'="m'" and rs2="rs2" 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 rs1 m' rs2)
    thus ?case
      apply(cases "chaina = chain")
       apply(simp)
       apply(cases "length rs1  length rs1")
        apply(simp add: List.append_eq_append_conv_if)
        apply(rule_tac rs1="drop (length rs1) rs1" and m'=m' and rs2=rs2 in call_return)
          apply(simp_all)[3]
        apply(subgoal_tac "rs1 = (take (length rs1) rs1) @ drop (length rs1) rs1")
         prefer 2 apply (metis append_take_drop_id)
        apply(clarify)
        apply(subgoal_tac "Γ(chain  drop (length rs1) rs1 @ Rule m' Return # rs2),γ,p 
            (take (length rs1) rs1) @ drop (length rs1) rs1, Undecided  Undecided")
         prefer 2 apply(auto)[1]
        apply(erule_tac rs1="take (length rs1) rs1" and rs2="drop (length rs1) rs1" in seqE)
        apply(simp)
        apply(frule_tac rs="drop (length rs1) rs1" 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 rs1 m' rs2)
    thus ?case
      apply(cases "chaina = chain")
      apply(cases "rs1")
      apply(force intro: call_return)
      apply(simp)
      apply(erule_tac Γ="Γ(chain  list @ Rule m' Return # rs2)" in seqE_cons)
      apply(frule_tac Γ="Γ(chain  list @ Rule m' Return # rs2)" 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: "rset 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
  "add_missing_ret_unfoldings rs1 rs2  
  foldr (λrf acc. add_match (MatchNot (get_match rf))  acc) [rrs1. 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
  "add_match_MatchAnd_foldr [] = id" |
  "add_match_MatchAnd_foldr es = add_match (MatchAnd_foldr es)"

lemma add_match_add_match_MatchAnd_foldr:
  "Γ,γ,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
    show ?case by (simp add: add_match_def)
  next
    case Cons
    thus ?case by (simp add: iptables_bigstep_add_match_and)
  qed

lemma add_match_MatchAnd_foldr_empty_rs2: "add_match_MatchAnd_foldr ms [] = []"
  by (induction ms) (simp_all add: add_match_def)

lemma add_missing_ret_unfoldings_alt: "Γ,γ,p add_missing_ret_unfoldings rs1 rs2, s  t 
  Γ,γ,p (add_match_MatchAnd_foldr (map (λr. MatchNot (get_match r)) [rrs1. get_action r = Return])) rs2, s   t"
  proof(induction rs1)
    case Nil
    thus ?case
      unfolding add_missing_ret_unfoldings_def by simp
  next
    case (Cons r rs)
    from Cons obtain m a where "r = Rule m a" by(cases r) (simp)
    with Cons show ?case
      unfolding add_missing_ret_unfoldings_def
      apply(cases "matches γ m p")
       apply (simp_all add: matches_add_match_simp matches_add_match_MatchNot_simp add_match_add_match_MatchAnd_foldr[symmetric])
      done
  qed

lemma add_match_add_missing_ret_unfoldings_rot:
  "Γ,γ,p add_match m (add_missing_ret_unfoldings rs1 rs2), s  t =  
   Γ,γ,p add_missing_ret_unfoldings (Rule (MatchNot m) Return#rs1) rs2, s  t"
  by(simp add: add_missing_ret_unfoldings_def iptables_bigstep_add_match_notnot_simp)


subsection‹Completeness›
lemma process_ret_split_obvious: "process_ret (rs1 @ rs2) = 
  (process_ret rs1) @ (add_missing_ret_unfoldings rs1 (process_ret rs2))"
  unfolding add_missing_ret_unfoldings_def
  proof (induction rs1 arbitrary: rs2)
    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)
             apply(simp_all add: add_match_split)
      done
  qed simp

lemma add_missing_ret_unfoldings_emptyrs2: "add_missing_ret_unfoldings rs1 [] = []"
  unfolding add_missing_ret_unfoldings_def
  by (induction rs1) (simp_all add: add_match_def)

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"
  by (simp add: process_call_split[symmetric])


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 (simp add: seq_cons)
            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


lemma add_match_rot_add_missing_ret_unfoldings:
  "Γ,γ,p add_match m (add_missing_ret_unfoldings rs1 rs2), Undecided  Undecided =
   Γ,γ,p add_missing_ret_unfoldings rs1 (add_match m rs2), Undecided  Undecided"
apply(simp add: add_missing_ret_unfoldings_alt add_match_add_missing_ret_unfoldings_rot add_match_add_match_MatchAnd_foldr[symmetric] iptables_bigstep_add_match_notnot_simp)
apply(cases "map (λr. MatchNot (get_match r)) [rrs1 . (get_action r) = Return]")
 apply(simp_all add: add_match_distrib)
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
      by (cases a) (auto intro: iptables_bigstep.intros simp add: not_matches_add_match_simp skip)
  next
    case Seq
    thus ?case
      by(simp add: process_call_split seq')
  next
    case (Call_return m a chain rs1 m' rs2)
    hence "Γ,γ,p rs1, Undecided  Undecided"
      by simp
    hence "Γ,γ,p process_ret rs1, Undecided  Undecided"
      by (rule iptables_bigstep_process_ret_undecided)
    with Call_return have "Γ,γ,p process_ret rs1 @ add_missing_ret_unfoldings rs1 (add_match (MatchNot m') (process_ret rs2)), Undecided  Undecided"
      by (metis matches_add_match_MatchNot_simp skip add_match_rot_add_missing_ret_unfoldings seq')
    with Call_return show ?case
      by (simp add: matches_add_match_simp process_ret_split_obvious)
  next
    case Call_result
    thus ?case
      by (simp add: matches_add_match_simp iptables_bigstep_process_ret_undecided)
  qed (auto intro: iptables_bigstep.intros)



lemma process_ret_cases:
  "process_ret rs = rs  (rs1 rs2 m. rs = rs1@[Rule m Return]@rs2  (process_ret rs) = rs1@(process_ret ([Rule m Return]@rs2)))"
  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) rs1 rs2 m where "rs = rs1@[Rule m Return]@rs2" and "process_ret rs = rs1@(process_ret ([Rule m Return]@rs2))"
 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) rs1 rs2 m where "rs = rs1@[Rule m Return]@rs2" "Γ,γ,p rs1, Undecided  Undecided" "matches γ m p"
proof -
  have "Γ,γ,p process_ret rs, Undecided  Undecided  
    (Γ,γ,p rs, Undecided  Undecided) 
    (rs1 rs2 m. rs = rs1@[Rule m Return]@rs2  Γ,γ,p rs1, 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(simp_all add: process_ret_split_fst_NeqReturn)
         apply(erule seqE_cons, frule iptables_bigstep_to_undecided, simp)+
         done
        from prems_rs Cons.IH have "Γ,γ,p rs, Undecided  Undecided 
                      (rs1 rs2 m. rs = rs1 @ [Rule m Return] @ rs2  Γ,γ,p rs1, Undecided  Undecided  matches γ m p)" by simp
        thus "Γ,γ,p r # rs, Undecided  Undecided  (rs1 rs2 m. r # rs = rs1 @ [Rule m Return] @ rs2  Γ,γ,p rs1, 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 "(rs1 rs2 m. rs = rs1 @ [Rule m Return] @ rs2  Γ,γ,p rs1, Undecided  Undecided  matches γ m p)"
            from this obtain rs1 rs2 m' where "rs = rs1 @ [Rule m' Return] @ rs2" and "Γ,γ,p rs1, Undecided  Undecided" and "matches γ m' p" by blast
            hence "rs1 rs2 m. r # rs = rs1 @ [Rule m Return] @ rs2  Γ,γ,p rs1, Undecided  Undecided  matches γ m p"
              apply(rule_tac x="Rule m a # rs1" in exI)
              apply(rule_tac x=rs2 in exI)
              apply(rule_tac x=m' in exI)
              apply(simp add: r)
              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  (rs1 rs2 m. r # rs = rs1 @ [Rule m Return] @ rs2  Γ,γ,p rs1, Undecided  Undecided  matches γ m p)"
          proof(cases "matches γ m p")
          case True
            (*the Cons premises are useless in this case*)
            hence "rs1 rs2 m. r # rs = rs1 @ Rule m Return # rs2  Γ,γ,p rs1, 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  (rs1 rs2 m. rs = rs1 @ [Rule m Return] @ rs2  Γ,γ,p rs1, 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 "rs1 rs2 m. rs = rs1 @ [Rule m Return] @ rs2  Γ,γ,p rs1, Undecided  Undecided  matches γ m p"
                from this obtain rs1 rs2 m' where "rs = rs1 @ [Rule m' Return] @ rs2" and "Γ,γ,p rs1, Undecided  Undecided" and "matches γ m' p" by blast
                hence "rs1 rs2 m. r # rs = rs1 @ [Rule m Return] @ rs2  Γ,γ,p rs1, Undecided  Undecided  matches γ m p" 
                  apply(rule_tac x="Rule m Return # rs1" in exI)
                  apply(rule_tac x="rs2" 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(simp add: process_ret_split_fst_NeqReturn)
    apply(erule seqE_cons)
    apply(simp add: seq'_cons)

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

    apply(case_tac "matches γ m p")
    apply(simp add: matches_add_match_MatchNot_simp skip) (*the prems becomes useless in this case*)
    apply (metis decision skipD)

    (*case ¬ matches*)
    apply(simp add: not_matches_add_matchNot_simp) (*get IH*)
    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(simp add: add_match_def)
apply(rename_tac r rs s t)
apply(case_tac r)
apply(rename_tac m' a')
apply(simp)
apply(case_tac a')
        apply(simp_all add: add_match_split_fst)
        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)
by (metis decision decisionD matches.simps(1) matches_add_match_MatchNot_simp matches_add_match_simp
  not_matches_add_matchNot_simp not_matches_add_match_simp state.exhaust)

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(simp add: add_match_def)
apply(rename_tac r rs s t)
apply(case_tac r)
apply(rename_tac m' a')
apply(simp)
apply(case_tac a')
        apply(simp_all add: add_match_split_fst)
        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)
by (metis decision decisionD matches.simps(1) matches_add_match_MatchNot_simp matches_add_match_simp
  not_matches_add_matchNot_simp not_matches_add_match_simp state.exhaust)

(*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"
by (metis process_ret_add_match_dist1 process_ret_add_match_dist2)


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"
          using matches by (metis matches_add_match_simp process_ret_add_match_dist)

        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" 
                  by (simp add: matches_add_match_simp not_matches_add_matchNot_simp)
                with matches' Cons.IH show ?thesis
                  by (fastforce simp: update_Gamma_nomatch process_ret_add_match_dist)
              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"
              by (simp add: process_ret_split_fst_NeqReturn)
            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"
              by (metis matches matches_add_match_simp process_ret_add_match_dist)
            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
                   by (simp add: update_Gamma_log_empty)
              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 rs1 rs2 new_m')
                    with call have "?Γ' chain = Some ((Rule m' (Call c) # rs1) @ [Rule new_m' Return] @ rs2)"
                      by simp
                    from call return step have "?Γ',γ,p Rule m' (Call c) # rs1, 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
    thus ?thesis by (metis assms state.distinct(1) not_matches_add_match_simp process_ret_add_match_dist1 skipD)
  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"
          using matches by (metis matches_add_match_simp process_ret_add_match_dist)

        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" 
                  by (simp add: matches_add_match_simp not_matches_add_matchNot_simp)
                with matches matches' Cons.IH show ?thesis
                  by (fastforce simp: update_Gamma_nomatch process_ret_add_match_dist matches_add_match_simp not_matches_add_matchNot_simp)
              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)
              apply(simp_all add: add_match_def)
      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(simp add: wf_chain_def add_match_def)
  apply(case_tac a)
  apply(case_tac "x2  Return")
   apply(simp add: process_ret_split_fst_NeqReturn)
   using wf_chain_append apply (metis Cons_eq_appendI append_Nil)
  apply(simp add: process_ret_split_fst_Return)
  apply(simp add: wf_chain_def add_match_def get_action_case_simp)
  done
lemma wf_chain_add_match: "wf_chain Γ rs  wf_chain Γ (add_match m rs)"
  by(induction rs) (simp_all add: wf_chain_def add_match_def get_action_case_simp)

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(simp_all add: seq'_cons)

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

    using process_ret_sound'
    by (metis fun_upd_triv matches_add_match_simp process_ret_add_match_dist)
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 "aran Γ  {process_call Γ rs}. wf_chain Γ a"
        proof(induction rs)
          case Nil thus ?case by simp
        next
          case(Cons r rs)
            from Cons.prems have "aran Γ. wf_chain Γ a" by blast
            from Cons.prems have "wf_chain Γ [r]"
              apply(simp)
              apply(clarify)
              apply(simp add: wf_chain_def)
              done
            from Cons.prems have "wf_chain Γ rs"
              apply(simp)
              apply(clarify)
              apply(simp add: wf_chain_def)
              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(simp add: wf_chain_append)
              apply(clarify)
              apply(simp add: ‹wf_chain Γ (process_call Γ rs))
              apply(rule wf_chain_add_match)
              apply(rule wf_chain_process_ret)
              apply(simp add: wf_chain_def)
              apply(clarify)
              by (metis ranI option.sel)
          from this aran Γ. 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"
  apply(simp add: sanity_wf_ruleset_def wf_chain_def)
  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"
    apply(simp add: wf_chain_def domD dom_map_of_conv_image_fst)
    by blast

  have "rsg  ran Γ  {rs}. wf_chain Γ rsg  
    Γ,γ,p repeat_stabilize n (process_call Γ) rs, s  t  Γ,γ,p rs, s  t" for Γ rs
  by(simp add: repeat_stabilize_funpow unfolding_n_sound_complete)
  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(simp add: rs repeat_stabilize_funpow)
    apply(subst optimize_matches_generic_funpow_helper)
     apply (simp add: opt_MatchAny_match_expr_correct; fail)
    apply(subst optimize_matches_generic[where P="λ_. True"], simp_all add: assms(4))
    apply(simp add: iptables_bigstep_rw_Reject iptables_bigstep_rm_LogEmpty)
    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