# Theory Semantics

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

section‹Big Step Semantics›

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

context
notes skipD[dest] list_app_singletonE[elim]
begin

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

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

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

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

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

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

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

end

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

end

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

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

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

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

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

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

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

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

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

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

text‹Showing the main theorem›

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

text‹Common Algorithms›

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

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

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

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