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⊢ ⟨rs⇩1, Undecided⟩ ⇒ t; Γ,γ,p⊢ ⟨rs⇩2, t⟩ ⇒ t'⟧ ⟹ Γ,γ,p⊢ ⟨rs⇩1@rs⇩2, Undecided⟩ ⇒ t'" |
call_return:  "⟦ matches γ m p; Γ chain = Some (rs⇩1@[Rule m' Return]@rs⇩2);
                 matches γ m' p; Γ,γ,p⊢ ⟨rs⇩1, Undecided⟩ ⇒ Undecided ⟧ ⟹
               Γ,γ,p⊢ ⟨[Rule m (Call chain)], Undecided⟩ ⇒ Undecided" |
call_result:  "⟦ matches γ m p; Γ chain = Some rs; Γ,γ,p⊢ ⟨rs, Undecided⟩ ⇒ t ⟧ ⟹
               Γ,γ,p⊢ ⟨[Rule m (Call chain)], Undecided⟩ ⇒ t"

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


(*future work:
  Add abstraction function for unknown actions. At the moment, only the explicitly listed actions are supported.
  This would also require a @{text "Decision FinalUnknown"} state
  Problem: An unknown action may modify a packet.
  Assume that we have a firewall which accepts the packets A->B and rewrites the header to A->C.
  After that firewall, there is another firewall which only accepts packets for A->C.
  A can send through both firewalls.
  
  If our model says that the firewall accepts packets A->B but does not consider packet modification,
  A might not be able to pass the second firewall with this model.
  
  Luckily, our model is correct for the filtering behaviour and explicitly does not support any actions with packet modification.
  Thus, the described scenario is not a counterexample that our model is wrong but a hint for future features
  we may want to support. Luckily, we introduced the @{term "Decision state"}, which should make adding packet modification states easy.
*)

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

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

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

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

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

context
  notes skipD[dest] list_app_singletonE[elim]
begin

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

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

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

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

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

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

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

end

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

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

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

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

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

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

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


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

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

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


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

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

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


theorem iptables_bigstep_deterministic: assumes "Γ,γ,p⊢ ⟨rs, s⟩ ⇒ t" and "Γ,γ,p⊢ ⟨rs, s⟩ ⇒ t'" shows "t = t'"
proof -
  { fix r1 r2 m t
    assume a1: "Γ,γ,p⊢ ⟨r1 @ Rule m Return # r2, Undecided⟩ ⇒ t" and a2: "matches γ m p" and a3: "Γ,γ,p⊢ ⟨r1,Undecided⟩ ⇒ Undecided"
    have False
    proof -
      from a1 a3 have "Γ,γ,p⊢ ⟨Rule m Return # r2, Undecided⟩ ⇒ t"
        by (blast intro: seq_progress)
      hence "Γ,γ,p⊢ ⟨[Rule m Return] @ r2, Undecided⟩ ⇒ t"
        by simp
      from seqE[OF this] obtain ti where "Γ,γ,p⊢ ⟨[Rule m Return], Undecided⟩ ⇒ ti" by blast
      with no_free_return a2 show False by fast (*by (blast intro: no_free_return elim: seq_split)*)
    qed
  } note no_free_return_seq=this
  
  from assms show ?thesis
  proof (induction arbitrary: t' rule: iptables_bigstep_induct)
    case Seq
    thus ?case
      by (metis seq_progress)
  next
    case Call_result
    thus ?case
      by (metis no_free_return_seq callD)
  next
    case Call_return
    thus ?case
      by (metis append_Cons callD no_free_return_seq)
  qed (auto dest: iptables_bigstepD)
qed

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

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

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

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


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



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

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

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

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

  lemma wf_Γ_append: "wf_Γ (rs1@rs2) ⟷ wf_Γ rs1 ∧ wf_Γ rs2"
    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:
        "(∀x∈ran Γ. wf_chain Γ x) ⟹
         ∀rsg∈ran Γ. ∀r∈set rsg. (∀chain. get_action r ≠ Goto chain) ∧ get_action r ≠ Unknown ⟹
         ∀y m. ∀r∈set rs_called. r = Rule m (Call y) ⟶ (∃t. Γ,γ,p⊢ ⟨[Rule m (Call y)], Undecided⟩ ⇒ t) ⟹
         wf_chain Γ rs_called ⟹ 
         ∀r∈set rs_called. (∀chain. get_action r ≠ Goto chain) ∧ get_action r ≠ Unknown ⟹
         (∃t. Γ,γ,p⊢ ⟨rs_called, Undecided⟩ ⇒ t) ∨
         (∃rs_called1 rs_called2 m'.
             rs_called = (rs_called1 @ [Rule m' Return] @ rs_called2) ∧
             matches γ m' p ∧ Γ,γ,p⊢ ⟨rs_called1, Undecided⟩ ⇒ Undecided)"
  proof(induction rs_called arbitrary:)
  case Nil hence "∃t. Γ,γ,p⊢ ⟨[], Undecided⟩ ⇒ t"
     apply(rule_tac x=Undecided in exI)
     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 Γ)"
            "∀rsg∈ran Γ. wf_chain Γ rsg"
            "∀rsg∈ran Γ. ∀r∈set rsg. (∀chain. get_action r ≠ Goto chain) ∧ get_action r ≠ Unknown" by auto
        ― ‹strengthening the IH to do a well-founded induction›
        hence "matches γ m p ⟹ wf_chain Γ [Rule m (Call chain_name)] ⟹ (∃t. Γ,γ,p⊢ ⟨[Rule m (Call chain_name)], Undecided⟩ ⇒ t)"
        proof(induction arbitrary: m rule: wf_induct_rule[where r="called_by_chain Γ"])
        case (less chain_name_neu)
          from less.prems have "Γ chain_name_neu ≠ None" by(simp add: wf_chain_def)
          from this obtain rs_called where rs_called: "Γ chain_name_neu = Some rs_called" by blast
  
          from less rs_called have "wf_chain Γ rs_called" by (simp add: ranI)
          from less rs_called have "rs_called ∈ ran Γ" by (simp add: ranI)
  
          (*get good IH*)
          from less.prems rs_called have
            "∀y m. ∀r ∈ set rs_called. r = Rule m (Call y) ⟶ (y, chain_name_neu) ∈ called_by_chain Γ ∧ wf_chain Γ [Rule m (Call y)]"
             apply(simp)
             apply(intro impI allI conjI)
              apply(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. ∀r∈set rs_called. r = Rule m (Call y) ⟶ (∃t. Γ,γ,p⊢ ⟨[Rule m (Call y)], Undecided⟩ ⇒ t)"
             apply(intro allI, rename_tac y my)
             apply(case_tac "matches γ my p")
              apply blast
             apply(intro ballI impI)
             apply(rule_tac x=Undecided in exI)
             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