Theory Semantics_Goto
theory Semantics_Goto
imports Main Firewall_Common "Common/List_Misc" "HOL-Library.LaTeXsugar"
begin
section‹Big Step Semantics with Goto›
text‹
We extend the iptables semantics to support the goto action.
A goto directly continues processing at the start of the called chain.
It does not change the call stack.
In contrast to calls, goto does not return.
Consequently, everything behind a matching goto cannot be reached.
›
text‹
This theory is structured as follows.
Fist, the goto semantics are introduced.
Then, we show that those semantics are deterministic.
Finally, we present two methods to remove gotos.
The first unfolds goto.
The second replaces gotos with calls.
Finally, since the goto rules makes all proofs quite ugly, we never mention the goto semantics again.
As we have shown, we can get rid of the gotos easily, thus, we stick to the nicer iptables semantics without goto.
›
context
begin
subsection‹Semantics›
private type_synonym 'a ruleset = "string ⇀ 'a rule list"
private type_synonym ('a, 'p) matcher = "'a ⇒ 'p ⇒ bool"
qualified 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"
qualified fun no_matching_Goto :: "('a, 'p) matcher ⇒ 'p ⇒ 'a rule list ⇒ bool" where
"no_matching_Goto _ _ [] ⟷ True" |
"no_matching_Goto γ p ((Rule m (Goto _))#rs) ⟷ ¬ matches γ m p ∧ no_matching_Goto γ p rs" |
"no_matching_Goto γ p (_#rs) ⟷ no_matching_Goto γ p rs"
inductive iptables_goto_bigstep :: "'a ruleset ⇒ ('a, 'p) matcher ⇒ 'p ⇒ 'a rule list ⇒ state ⇒ state ⇒ bool"
("_,_,_⊢⇩g ⟨_, _⟩ ⇒ _" [60,60,60,20,98,98] 89)
for Γ and γ and p where
skip: "Γ,γ,p⊢⇩g ⟨[], t⟩ ⇒ t" |
accept: "matches γ m p ⟹ Γ,γ,p⊢⇩g ⟨[Rule m Accept], Undecided⟩ ⇒ Decision FinalAllow" |
drop: "matches γ m p ⟹ Γ,γ,p⊢⇩g ⟨[Rule m Drop], Undecided⟩ ⇒ Decision FinalDeny" |
reject: "matches γ m p ⟹ Γ,γ,p⊢⇩g ⟨[Rule m Reject], Undecided⟩ ⇒ Decision FinalDeny" |
log: "matches γ m p ⟹ Γ,γ,p⊢⇩g ⟨[Rule m Log], Undecided⟩ ⇒ Undecided" |
empty: "matches γ m p ⟹ Γ,γ,p⊢⇩g ⟨[Rule m Empty], Undecided⟩ ⇒ Undecided" |
nomatch: "¬ matches γ m p ⟹ Γ,γ,p⊢⇩g ⟨[Rule m a], Undecided⟩ ⇒ Undecided" |
decision: "Γ,γ,p⊢⇩g ⟨rs, Decision X⟩ ⇒ Decision X" |
seq: "⟦Γ,γ,p⊢⇩g ⟨rs⇩1, Undecided⟩ ⇒ t; Γ,γ,p⊢⇩g ⟨rs⇩2, t⟩ ⇒ t'; no_matching_Goto γ p rs⇩1⟧ ⟹ Γ,γ,p⊢⇩g ⟨rs⇩1@rs⇩2, Undecided⟩ ⇒ t'" |
call_return: "⟦ matches γ m p; Γ chain = Some (rs⇩1@[Rule m' Return]@rs⇩2);
matches γ m' p; Γ,γ,p⊢⇩g ⟨rs⇩1, Undecided⟩ ⇒ Undecided;
no_matching_Goto γ p rs⇩1⟧ ⟹
Γ,γ,p⊢⇩g ⟨[Rule m (Call chain)], Undecided⟩ ⇒ Undecided" |
call_result: "⟦ matches γ m p; Γ chain = Some rs; Γ,γ,p⊢⇩g ⟨rs, Undecided⟩ ⇒ t ⟧ ⟹
Γ,γ,p⊢⇩g ⟨[Rule m (Call chain)], Undecided⟩ ⇒ t" |
goto_decision: "⟦ matches γ m p; Γ chain = Some rs; Γ,γ,p⊢⇩g ⟨rs, Undecided⟩ ⇒ Decision X ⟧ ⟹
Γ,γ,p⊢⇩g ⟨(Rule m (Goto chain))#rest, Undecided⟩ ⇒ Decision X" |
goto_no_decision: "⟦ matches γ m p; Γ chain = Some rs; Γ,γ,p⊢⇩g ⟨rs, Undecided⟩ ⇒ Undecided ⟧ ⟹
Γ,γ,p⊢⇩g ⟨(Rule m (Goto chain))#rest, Undecided⟩ ⇒ Undecided"
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]}\\[1ex]
@{thm[mode=Rule] goto_decision [no_vars]}\\[1ex]
@{thm[mode=Rule] goto_no_decision [no_vars]}
\end{center}
›
private lemma deny:
"matches γ m p ⟹ a = Drop ∨ a = Reject ⟹ iptables_goto_bigstep Γ γ p [Rule m a] Undecided (Decision FinalDeny)"
by (auto intro: drop reject)
private lemma iptables_goto_bigstep_induct
[case_names
Skip Allow Deny Log Nomatch Decision Seq Call_return Call_result Goto_Decision Goto_no_Decision,
induct pred: iptables_goto_bigstep]:
"⟦ Γ,γ,p⊢⇩g ⟨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⊢⇩g ⟨rs⇩1,Undecided⟩ ⇒ t ⟹ P rs⇩1 Undecided t ⟹
Γ,γ,p⊢⇩g ⟨rs⇩2,t⟩ ⇒ t' ⟹ P rs⇩2 t t' ⟹ no_matching_Goto γ p rs⇩1 ⟹
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⊢⇩g ⟨rs⇩1,Undecided⟩ ⇒ Undecided ⟹
no_matching_Goto γ p rs⇩1 ⟹ 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⊢⇩g ⟨rs,Undecided⟩ ⇒ t ⟹ P rs Undecided t ⟹ P [Rule m a] Undecided t;
⋀m a chain rs rest X. matches γ m p ⟹ a = Goto chain ⟹ Γ chain = Some rs ⟹
Γ,γ,p⊢⇩g ⟨rs,Undecided⟩ ⇒ (Decision X) ⟹ P rs Undecided (Decision X) ⟹
P (Rule m a#rest) Undecided (Decision X);
⋀m a chain rs rest. matches γ m p ⟹ a = Goto chain ⟹ Γ chain = Some rs ⟹
Γ,γ,p⊢⇩g ⟨rs,Undecided⟩ ⇒ Undecided ⟹ P rs Undecided Undecided ⟹
P (Rule m a#rest) Undecided Undecided⟧ ⟹
P rs s t"
by (induction rule: iptables_goto_bigstep.induct) auto
subsubsection‹Forward reasoning›
private lemma decisionD: "Γ,γ,p⊢⇩g ⟨r, s⟩ ⇒ t ⟹ s = Decision X ⟹ t = Decision X"
by (induction rule: iptables_goto_bigstep_induct) auto
private lemma iptables_goto_bigstep_to_undecided: "Γ,γ,p⊢⇩g ⟨rs, s⟩ ⇒ Undecided ⟹ s = Undecided"
by (metis decisionD state.exhaust)
private lemma iptables_goto_bigstep_to_decision: "Γ,γ,p⊢⇩g ⟨rs, Decision Y⟩ ⇒ Decision X ⟹ Y = X"
by (metis decisionD state.inject)
private lemma skipD: "Γ,γ,p⊢⇩g ⟨r, s⟩ ⇒ t ⟹ r = [] ⟹ s = t"
by (induction rule: iptables_goto_bigstep.induct) auto
private lemma gotoD: "Γ,γ,p⊢⇩g ⟨r, s⟩ ⇒ t ⟹ r = [Rule m (Goto chain)] ⟹ s = Undecided ⟹ matches γ m p ⟹
∃ rs. Γ chain = Some rs ∧ Γ,γ,p⊢⇩g ⟨rs,s⟩ ⇒ t"
by (induction rule: iptables_goto_bigstep.induct) (auto dest: skipD elim: list_app_singletonE)
private lemma not_no_matching_Goto_singleton_cases: "¬ no_matching_Goto γ p [Rule m a] ⟷ (∃ chain. a = (Goto chain)) ∧ matches γ m p"
by(case_tac a) (simp_all)
private lemma no_matching_Goto_Cons: "no_matching_Goto γ p [r] ⟹ no_matching_Goto γ p rs ⟹ no_matching_Goto γ p (r#rs)"
by(cases r)(rename_tac m a, case_tac a, simp_all)
private lemma no_matching_Goto_head: "no_matching_Goto γ p (r#rs) ⟹ no_matching_Goto γ p [r]"
by(cases r)(rename_tac m a, case_tac a, simp_all)
private lemma no_matching_Goto_tail: "no_matching_Goto γ p (r#rs) ⟹ no_matching_Goto γ p rs"
by(cases r)(rename_tac m a, case_tac a, simp_all)
private lemma not_no_matching_Goto_cases:
assumes "¬ no_matching_Goto γ p rs" "rs ≠ []"
shows "∃rs1 m chain rs2. rs = rs1@(Rule m (Goto chain))#rs2 ∧ no_matching_Goto γ p rs1 ∧ matches γ m p"
using assms
proof(induction rs)
case Nil thus ?case by simp
next
case (Cons r rs)
note Cons_outer=this
from Cons have "¬ no_matching_Goto γ p (r # rs)" by simp
show ?case
proof(cases rs)
case Nil
obtain m a where "r = Rule m a" by (cases r) simp
with ‹¬ no_matching_Goto γ p (r # rs)› Nil not_no_matching_Goto_singleton_cases have "(∃ chain. a = (Goto chain)) ∧ matches γ m p" by metis
from this obtain chain where "a = (Goto chain)" and "matches γ m p" by blast
have "r # rs = [] @ Rule m (Goto chain) # []" "no_matching_Goto γ p []" "matches γ m p"
by (simp_all add: ‹a = Goto chain› ‹r = Rule m a› Nil ‹matches γ m p›)
thus ?thesis by blast
next
case(Cons r' rs')
with Cons_outer have "r # rs = r # r' # rs'" by simp
show ?thesis
proof(cases"no_matching_Goto γ p [r]")
case True
with ‹¬ no_matching_Goto γ p (r # rs)› have "¬ no_matching_Goto γ p rs" by (meson no_matching_Goto_Cons)
have "rs ≠ []" using Cons by simp
from Cons_outer(1)[OF ‹¬ no_matching_Goto γ p rs› ‹rs ≠ []›]
obtain rs1 m chain rs2 where "rs = rs1 @ Rule m (Goto chain) # rs2" "no_matching_Goto γ p rs1" "matches γ m p" by blast
with ‹r # rs = r # r' # rs'› ‹no_matching_Goto γ p [r]› no_matching_Goto_Cons
have "r # rs = r # rs1 @ Rule m (Goto chain) # rs2 ∧ no_matching_Goto γ p (r#rs1) ∧ matches γ m p" by fast
thus ?thesis
apply(rule_tac x="r#rs1" in exI)
by auto
next
case False
obtain m a where "r = Rule m a" by (cases r) simp
with False not_no_matching_Goto_singleton_cases have "(∃ chain. a = (Goto chain)) ∧ matches γ m p" by metis
from this obtain chain where "a = (Goto chain)" and "matches γ m p" by blast
have "r # rs = [] @ Rule m (Goto chain) # rs" "no_matching_Goto γ p []" "matches γ m p"
by (simp_all add: ‹a = Goto chain› ‹r = Rule m a› ‹matches γ m p›)
thus ?thesis by blast
qed
qed
qed
private lemma seq_cons_Goto_Undecided:
assumes "Γ,γ,p⊢⇩g ⟨[Rule m (Goto chain)], Undecided⟩ ⇒ Undecided"
and "¬ matches γ m p ⟹ Γ,γ,p⊢⇩g ⟨rs, Undecided⟩ ⇒ Undecided"
shows "Γ,γ,p⊢⇩g ⟨Rule m (Goto chain) # rs, Undecided⟩ ⇒ Undecided"
proof(cases "matches γ m p")
case True
from True assms have "∃rs. Γ chain = Some rs ∧ Γ,γ,p⊢⇩g ⟨rs, Undecided⟩ ⇒ Undecided" by(auto dest: gotoD)
with True show ?thesis using goto_no_decision by fast
next
case False
with assms have " Γ,γ,p⊢⇩g ⟨[Rule m (Goto chain)] @ rs, Undecided⟩ ⇒ Undecided" by(auto dest: seq)
with False show ?thesis by simp
qed
private lemma seq_cons_Goto_t:
"Γ,γ,p⊢⇩g ⟨[Rule m (Goto chain)], Undecided⟩ ⇒ t ⟹ matches γ m p ⟹ Γ,γ,p⊢⇩g ⟨Rule m (Goto chain) # rs, Undecided⟩ ⇒ t"
apply(frule gotoD)
apply(simp_all)
apply(clarify)
apply(cases t)
apply(auto intro: iptables_goto_bigstep.intros)
done
private lemma no_matching_Goto_append: "no_matching_Goto γ p (rs1@rs2) ⟷ no_matching_Goto γ p rs1 ∧ no_matching_Goto γ p rs2"
by(induction γ p rs1 rule: no_matching_Goto.induct) (simp_all)
private lemma no_matching_Goto_append1: "no_matching_Goto γ p (rs1@rs2) ⟹ no_matching_Goto γ p rs1"
using no_matching_Goto_append by fast
private lemma no_matching_Goto_append2: "no_matching_Goto γ p (rs1@rs2) ⟹ no_matching_Goto γ p rs2"
using no_matching_Goto_append by fast
private lemma seq_cons:
assumes "Γ,γ,p⊢⇩g ⟨[r],Undecided⟩ ⇒ t" and "Γ,γ,p⊢⇩g ⟨rs,t⟩ ⇒ t'" and "no_matching_Goto γ p [r]"
shows "Γ,γ,p⊢⇩g ⟨r#rs, Undecided⟩ ⇒ t'"
proof -
from assms have "Γ,γ,p⊢⇩g ⟨[r] @ rs, Undecided⟩ ⇒ t'" by (rule seq)
thus ?thesis by simp
qed
context
notes skipD[dest] list_app_singletonE[elim]
begin
lemma acceptD: "Γ,γ,p⊢⇩g ⟨r, s⟩ ⇒ t ⟹ r = [Rule m Accept] ⟹ matches γ m p ⟹ s = Undecided ⟹ t = Decision FinalAllow"
by (induction rule: iptables_goto_bigstep.induct) auto
lemma dropD: "Γ,γ,p⊢⇩g ⟨r, s⟩ ⇒ t ⟹ r = [Rule m Drop] ⟹ matches γ m p ⟹ s = Undecided ⟹ t = Decision FinalDeny"
by (induction rule: iptables_goto_bigstep.induct) auto
lemma rejectD: "Γ,γ,p⊢⇩g ⟨r, s⟩ ⇒ t ⟹ r = [Rule m Reject] ⟹ matches γ m p ⟹ s = Undecided ⟹ t = Decision FinalDeny"
by (induction rule: iptables_goto_bigstep.induct) auto
lemma logD: "Γ,γ,p⊢⇩g ⟨r, s⟩ ⇒ t ⟹ r = [Rule m Log] ⟹ matches γ m p ⟹ s = Undecided ⟹ t = Undecided"
by (induction rule: iptables_goto_bigstep.induct) auto
lemma emptyD: "Γ,γ,p⊢⇩g ⟨r, s⟩ ⇒ t ⟹ r = [Rule m Empty] ⟹ matches γ m p ⟹ s = Undecided ⟹ t = Undecided"
by (induction rule: iptables_goto_bigstep.induct) auto
lemma nomatchD: "Γ,γ,p⊢⇩g ⟨r, s⟩ ⇒ t ⟹ r = [Rule m a] ⟹ s = Undecided ⟹ ¬ matches γ m p ⟹ t = Undecided"
by (induction rule: iptables_goto_bigstep.induct) auto
lemma callD:
assumes "Γ,γ,p⊢⇩g ⟨r, s⟩ ⇒ t" "r = [Rule m (Call chain)]" "s = Undecided" "matches γ m p" "Γ chain = Some rs"
obtains "Γ,γ,p⊢⇩g ⟨rs,s⟩ ⇒ t"
| rs⇩1 rs⇩2 m' where "rs = rs⇩1 @ Rule m' Return # rs⇩2" "matches γ m' p" "Γ,γ,p⊢⇩g ⟨rs⇩1,s⟩ ⇒ Undecided" "no_matching_Goto γ p rs⇩1" "t = Undecided"
using assms
proof (induction r s t arbitrary: rs rule: iptables_goto_bigstep.induct)
case (seq rs⇩1)
thus ?case by (cases rs⇩1) auto
qed auto
end
private lemmas iptables_goto_bigstepD = skipD acceptD dropD rejectD logD emptyD nomatchD decisionD callD gotoD
private lemma seq':
assumes "rs = rs⇩1 @ rs⇩2" "Γ,γ,p⊢⇩g ⟨rs⇩1,s⟩ ⇒ t" "Γ,γ,p⊢⇩g ⟨rs⇩2,t⟩ ⇒ t'" and "no_matching_Goto γ p rs⇩1"
shows "Γ,γ,p⊢⇩g ⟨rs,s⟩ ⇒ t'"
using assms by (cases s) (auto intro: seq decision dest: decisionD)
private lemma seq'_cons: "Γ,γ,p⊢⇩g ⟨[r],s⟩ ⇒ t ⟹ Γ,γ,p⊢⇩g ⟨rs,t⟩ ⇒ t' ⟹ no_matching_Goto γ p [r] ⟹ Γ,γ,p⊢⇩g ⟨r#rs, s⟩ ⇒ t'"
by (metis decision decisionD state.exhaust seq_cons)
private lemma no_matching_Goto_take: "no_matching_Goto γ p rs ⟹ no_matching_Goto γ p (take n rs)"
apply(induction n arbitrary: rs)
apply(simp_all)
apply(rename_tac r rs)
apply(case_tac rs)
apply(simp_all)
apply(rename_tac r' rs')
apply(case_tac r')
apply(simp)
apply(rename_tac m a)
by(case_tac a) (simp_all)
private lemma seq_split:
assumes "Γ,γ,p⊢⇩g ⟨rs, s⟩ ⇒ t" "rs = rs⇩1@rs⇩2"
obtains (no_matching_Goto) t' where "Γ,γ,p⊢⇩g ⟨rs⇩1,s⟩ ⇒ t'" "Γ,γ,p⊢⇩g ⟨rs⇩2,t'⟩ ⇒ t" "no_matching_Goto γ p rs⇩1"
| (matching_Goto) "Γ,γ,p⊢⇩g ⟨rs⇩1,s⟩ ⇒ t" "¬ no_matching_Goto γ p rs⇩1"
proof -
have "(∃t'. Γ,γ,p⊢⇩g ⟨rs⇩1,s⟩ ⇒ t' ∧ Γ,γ,p⊢⇩g ⟨rs⇩2,t'⟩ ⇒ t ∧ no_matching_Goto γ p rs⇩1) ∨ (Γ,γ,p⊢⇩g ⟨rs⇩1,s⟩ ⇒ t ∧ ¬ no_matching_Goto γ p rs⇩1)"
using assms
proof (induction rs s t arbitrary: rs⇩1 rs⇩2 rule: iptables_goto_bigstep_induct)
case Skip thus ?case by (auto intro: iptables_goto_bigstep.intros simp add: accept)
next
case Allow thus ?case by (cases rs⇩1) (auto intro: iptables_goto_bigstep.intros simp add: accept)
next
case Deny thus ?case by (cases rs⇩1) (auto intro: iptables_goto_bigstep.intros simp add: deny)
next
case Log thus ?case by (cases rs⇩1) (auto intro: iptables_goto_bigstep.intros simp add: log empty)
next
case Nomatch thus ?case by (cases rs⇩1)
(auto intro: iptables_goto_bigstep.intros simp add: not_no_matching_Goto_singleton_cases, meson nomatch not_no_matching_Goto_singleton_cases skip)
next
case Decision thus ?case by (auto intro: iptables_goto_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⊢⇩g ⟨take (length rsa) rs⇩1, Undecided⟩ ⇒ t"
by simp
from Seq.IH(2)[OF longer(2)] have IH:
"(∃t'a. Γ,γ,p⊢⇩g ⟨drop (length rsa) rs⇩1, t⟩ ⇒ t'a ∧ Γ,γ,p⊢⇩g ⟨rs⇩2, t'a⟩ ⇒ t' ∧ no_matching_Goto γ p (drop (length rsa) rs⇩1)) ∨
Γ,γ,p⊢⇩g ⟨drop (length rsa) rs⇩1, t⟩ ⇒ t' ∧ ¬ no_matching_Goto γ p (drop (length rsa) rs⇩1)" (is "?IH_no_Goto ∨ ?IH_Goto") by simp
thus ?thesis
proof(rule disjE)
assume IH: ?IH_no_Goto
from IH obtain t2
where t2a: "Γ,γ,p⊢⇩g ⟨drop (length rsa) rs⇩1,t⟩ ⇒ t2"
and rs_part2: "Γ,γ,p⊢⇩g ⟨rs⇩2,t2⟩ ⇒ t'"
and "no_matching_Goto γ p (drop (length rsa) rs⇩1)"
by blast
with t1 rs_part2 have rs_part1: "Γ,γ,p⊢⇩g ⟨take (length rsa) rs⇩1 @ drop (length rsa) rs⇩1, Undecided⟩ ⇒ t2"
using Seq.hyps(4) longer(1) seq by fastforce
have "no_matching_Goto γ p (take (length rsa) rs⇩1 @ drop (length rsa) rs⇩1)"
using Seq.hyps(4) ‹no_matching_Goto γ p (drop (length rsa) rs⇩1)› longer(1)
no_matching_Goto_append by fastforce
with Seq rs_part1 rs_part2 show ?thesis by auto
next
assume ?IH_Goto
thus ?thesis by (metis Seq.hyps(2) Seq.hyps(4) append_take_drop_id longer(1) no_matching_Goto_append2 seq')
qed
next
case shorter
from shorter 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.hyps(4) rsa' no_matching_Goto_append2 have
no_matching_Goto_rs2: "no_matching_Goto γ p (take (length rsa - length rs⇩1) rs⇩2)" by metis
from rsb' Seq.hyps have t2: "Γ,γ,p⊢⇩g ⟨drop (length rsa - length rs⇩1) rs⇩2,t⟩ ⇒ t'"
by blast
from Seq.IH(1)[OF rsa'] have IH:
"(∃t'. Γ,γ,p⊢⇩g ⟨rs⇩1, Undecided⟩ ⇒ t' ∧ Γ,γ,p⊢⇩g ⟨take (length rsa - length rs⇩1) rs⇩2, t'⟩ ⇒ t ∧ no_matching_Goto γ p rs⇩1) ∨
Γ,γ,p⊢⇩g ⟨rs⇩1, Undecided⟩ ⇒ t ∧ ¬ no_matching_Goto γ p rs⇩1" (is "?IH_no_Goto ∨ ?IH_Goto") by simp
thus ?thesis
proof(rule disjE)
assume IH: ?IH_no_Goto
from IH obtain t1
where t1a: "Γ,γ,p⊢⇩g ⟨rs⇩1,Undecided⟩ ⇒ t1"
and t1b: "Γ,γ,p⊢⇩g ⟨take (length rsa - length rs⇩1) rs⇩2,t1⟩ ⇒ t"
and "no_matching_Goto γ p rs⇩1"
by blast
from no_matching_Goto_rs2 t2 seq' t1b have rs2: "Γ,γ,p⊢⇩g ⟨rs⇩2,t1⟩ ⇒ t'"
by fastforce
from t1a rs2 ‹no_matching_Goto γ p rs⇩1› show ?thesis by fast
next
assume ?IH_Goto
thus ?thesis by (metis Seq.hyps(4) no_matching_Goto_append1 rsa')
qed
qed
next
case Call_return
hence "Γ,γ,p⊢⇩g ⟨rs⇩1, Undecided⟩ ⇒ Undecided" "Γ,γ,p⊢⇩g ⟨rs⇩2, Undecided⟩ ⇒ Undecided"
by (case_tac [!] rs⇩1) (auto intro: iptables_goto_bigstep.skip iptables_goto_bigstep.call_return)
thus ?case by fast
next
case (Call_result _ _ _ _ t)
show ?case
proof (cases rs⇩1)
case Nil
with Call_result have "Γ,γ,p⊢⇩g ⟨rs⇩1, Undecided⟩ ⇒ Undecided" "Γ,γ,p⊢⇩g ⟨rs⇩2, Undecided⟩ ⇒ t"
by (auto intro: iptables_goto_bigstep.intros)
thus ?thesis using local.Nil by auto
next
case Cons
with Call_result have "Γ,γ,p⊢⇩g ⟨rs⇩1, Undecided⟩ ⇒ t" "Γ,γ,p⊢⇩g ⟨rs⇩2, t⟩ ⇒ t"
by (auto intro: iptables_goto_bigstep.intros)
thus ?thesis by fast
qed
next
case (Goto_Decision m a chain rs rest X)
thus ?case
proof (cases rs⇩1)
case Nil
with Goto_Decision have "Γ,γ,p⊢⇩g ⟨rs⇩1, Undecided⟩ ⇒ Undecided" "Γ,γ,p⊢⇩g ⟨rs⇩2, Undecided⟩ ⇒ Decision X"
by (auto intro: iptables_goto_bigstep.intros)
thus ?thesis using local.Nil by auto
next
case Cons
with Goto_Decision have "Γ,γ,p⊢⇩g ⟨rs⇩1, Undecided⟩ ⇒ Decision X" "Γ,γ,p⊢⇩g ⟨rs⇩2, Decision X⟩ ⇒ Decision X"
by (auto intro: iptables_goto_bigstep.intros)
thus ?thesis by fast
qed
next
case (Goto_no_Decision m a chain rs rest rs⇩1)
from Goto_no_Decision have rs1rs2: "Rule m (Goto chain) # rest = rs⇩1 @ rs⇩2" by simp
from goto_no_decision[OF Goto_no_Decision(1)] Goto_no_Decision(3) Goto_no_Decision(4)
have x: "⋀rest. Γ,γ,p⊢⇩g ⟨Rule m (Goto chain) # rest, Undecided⟩ ⇒ Undecided" by simp
show ?case
proof (cases rs⇩1)
case Nil
with Goto_no_Decision have "Γ,γ,p⊢⇩g ⟨rs⇩1, Undecided⟩ ⇒ Undecided" "Γ,γ,p⊢⇩g ⟨rs⇩2, Undecided⟩ ⇒ Undecided"
by (auto intro: iptables_goto_bigstep.intros)
thus ?thesis by fast
next
case (Cons rs⇩1a rs⇩1s)
with rs1rs2 have "rs⇩1 = Rule m (Goto chain) # (take (length rs⇩1s) rest)" by simp
from Cons rs1rs2 have"rs⇩2 = drop (length rs⇩1s) rest" by simp
from Cons Goto_no_Decision have 1: "Γ,γ,p⊢⇩g ⟨rs⇩1, Undecided⟩ ⇒ Undecided"
using x by auto[1]
have 2: "¬ no_matching_Goto γ p rs⇩1"
by (simp add: Goto_no_Decision.hyps(1) ‹rs⇩1 = Rule m (Goto chain) # take (length rs⇩1s) rest›)
from 1 2 show ?thesis by fast
qed
qed
thus ?thesis using matching_Goto no_matching_Goto by blast
qed
private lemma seqE:
assumes "Γ,γ,p⊢⇩g ⟨rs⇩1@rs⇩2, s⟩ ⇒ t"
obtains (no_matching_Goto) ti where "Γ,γ,p⊢⇩g ⟨rs⇩1,s⟩ ⇒ ti" "Γ,γ,p⊢⇩g ⟨rs⇩2,ti⟩ ⇒ t" "no_matching_Goto γ p rs⇩1"
| (matching_Goto) "Γ,γ,p⊢⇩g ⟨rs⇩1,s⟩ ⇒ t" "¬ no_matching_Goto γ p rs⇩1"
using assms by (force elim: seq_split)
private lemma seqE_cons:
assumes "Γ,γ,p⊢⇩g ⟨r#rs, s⟩ ⇒ t"
obtains (no_matching_Goto) ti where "Γ,γ,p⊢⇩g ⟨[r],s⟩ ⇒ ti" "Γ,γ,p⊢⇩g ⟨rs,ti⟩ ⇒ t" "no_matching_Goto γ p [r]"
| (matching_Goto) "Γ,γ,p⊢⇩g ⟨[r],s⟩ ⇒ t" "¬ no_matching_Goto γ p [r]"
using assms by (metis append_Cons append_Nil seqE)
private lemma seqE_cons_Undecided:
assumes "Γ,γ,p⊢⇩g ⟨r#rs, Undecided⟩ ⇒ t"
obtains (no_matching_Goto) ti where "Γ,γ,p⊢⇩g ⟨[r],Undecided⟩ ⇒ ti" and "Γ,γ,p⊢⇩g ⟨rs,ti⟩ ⇒ t" and "no_matching_Goto γ p [r]"
| (matching_Goto) m chain rs' where "r = Rule m (Goto chain)" and "Γ,γ,p⊢⇩g ⟨[Rule m (Goto chain)],Undecided⟩ ⇒ t" and "matches γ m p" "Γ chain = Some rs'"
using assms
proof(cases rule: seqE_cons)
case no_matching_Goto thus ?thesis using local.that by simp
next
case matching_Goto
from this(2) not_no_matching_Goto_singleton_cases[of γ p "(get_match r)" "(get_action r)", simplified] have
"((∃chain. (get_action r) = Goto chain) ∧ matches γ (get_match r) p)" by simp
from this obtain chain m where r: "r = Rule m (Goto chain)" "matches γ m p" by(cases r) auto
from matching_Goto r have "Γ,γ,p⊢⇩g ⟨[Rule m (Goto chain)],Undecided⟩ ⇒ t" by simp
from gotoD[OF matching_Goto(1)] r ‹matches γ m p› obtain rs' where "Γ chain = Some rs'" by blast
from local.that
show ?thesis using ‹Γ chain = Some rs'› ‹Γ,γ,p⊢⇩g ⟨[Rule m (Goto chain)], Undecided⟩ ⇒ t› r(1) r(2) by blast
qed
private lemma nomatch':
assumes "⋀r. r ∈ set rs ⟹ ¬ matches γ (get_match r) p"
shows "Γ,γ,p⊢⇩g ⟨rs, s⟩ ⇒ s"
proof(cases s)
case Undecided
have "∀r∈set rs. ¬ matches γ (get_match r) p ⟹ Γ,γ,p⊢⇩g ⟨rs, Undecided⟩ ⇒ Undecided"
proof(induction rs)
case Nil
thus ?case by (fast intro: skip)
next
case (Cons r rs)
hence "Γ,γ,p⊢⇩g ⟨[r], Undecided⟩ ⇒ Undecided"
by (cases r) (auto intro: nomatch)
with Cons show ?case
by (metis list.set_intros(1) list.set_intros(2) not_no_matching_Goto_singleton_cases rule.collapse seq'_cons)
qed
with assms Undecided show ?thesis by simp
qed (blast intro: decision)
private lemma no_free_return: assumes "Γ,γ,p⊢⇩g ⟨[Rule m Return], Undecided⟩ ⇒ t" and "matches γ m p" shows "False"
proof -
{ fix a s
have no_free_return_hlp: "Γ,γ,p⊢⇩g ⟨a,s⟩ ⇒ t ⟹ matches γ m p ⟹ s = Undecided ⟹ a = [Rule m Return] ⟹ False"
proof (induction rule: iptables_goto_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
subsection‹Determinism›
private lemma iptables_goto_bigstep_Undecided_Undecided_deterministic:
"Γ,γ,p⊢⇩g ⟨rs, Undecided⟩ ⇒ Undecided ⟹ Γ,γ,p⊢⇩g ⟨rs, Undecided⟩ ⇒ t ⟹ t = Undecided"
proof(induction rs Undecided Undecided arbitrary: t rule: iptables_goto_bigstep_induct)
case Skip thus ?case by(fastforce dest: skipD logD emptyD nomatchD decisionD)
next
case Log thus ?case by(fastforce dest: skipD logD emptyD nomatchD decisionD)
next
case Nomatch thus ?case by(fastforce dest: skipD logD emptyD nomatchD decisionD)
next
case Seq thus ?case by (metis iptables_goto_bigstep_to_undecided seqE)
next
case (Call_return m a chain rs⇩1 m' rs⇩2)
from Call_return have " Γ,γ,p⊢⇩g ⟨[Rule m (Call chain)], Undecided⟩ ⇒ Undecided"
apply(frule_tac rs⇩1=rs⇩1 and m'=m' and chain=chain in call_return)
by(simp_all)
with Call_return show ?case
apply simp
apply (metis callD no_free_return seqE seqE_cons)
done
next
case Call_result thus ?case by (meson callD)
next
case Goto_no_Decision thus ?case by (metis gotoD no_matching_Goto.simps(2) option.sel seqE_cons)
qed
private lemma iptables_goto_bigstep_Undecided_deterministic:
"Γ,γ,p⊢⇩g ⟨rs, Undecided⟩ ⇒ t ⟹ Γ,γ,p⊢⇩g ⟨rs, Undecided⟩ ⇒ t' ⟹ t' = t"
proof(induction rs Undecided t arbitrary: t' rule: iptables_goto_bigstep_induct)
case Skip thus ?case by(fastforce dest: skipD logD emptyD nomatchD decisionD)
next
case Allow thus ?case by (auto dest: iptables_goto_bigstepD)
next
case Deny thus ?case by (auto dest: iptables_goto_bigstepD)
next
case Log thus ?case by (auto dest: iptables_goto_bigstepD)
next
case Nomatch thus ?case by (auto dest: iptables_goto_bigstepD)
next
case Seq thus ?case by (metis decisionD seqE state.exhaust)
next
case Call_return thus ?case by (meson call_return iptables_goto_bigstep_Undecided_Undecided_deterministic)
next
case Call_result thus ?case by (metis callD call_result iptables_goto_bigstep_Undecided_Undecided_deterministic)
next
case Goto_Decision thus ?case by (metis gotoD no_matching_Goto.simps(2) option.sel seqE_cons)
next
case Goto_no_Decision thus ?case by (meson goto_no_decision iptables_goto_bigstep_Undecided_Undecided_deterministic)
qed
qualified theorem iptables_goto_bigstep_deterministic: assumes "Γ,γ,p⊢⇩g ⟨rs, s⟩ ⇒ t" and "Γ,γ,p⊢⇩g ⟨rs, s⟩ ⇒ t'" shows "t = t'"
using assms
apply(cases s)
apply(simp add: iptables_goto_bigstep_Undecided_deterministic)
by(auto dest: decisionD)
subsection‹Matching›
private lemma matches_rule_and_simp_help:
assumes "matches γ m p"
shows "Γ,γ,p⊢⇩g ⟨[Rule (MatchAnd m m') a'], s⟩ ⇒ t ⟷ Γ,γ,p⊢⇩g ⟨[Rule m' a'], s⟩ ⇒ t" (is "?l ⟷?r")
proof
assume ?l thus ?r
by (induction "[Rule (MatchAnd m m') a']" s t rule: iptables_goto_bigstep_induct)
(auto intro: iptables_goto_bigstep.intros simp: assms Cons_eq_append_conv dest: skipD)
next
assume ?r thus ?l
by (induction "[Rule m' a']" s t rule: iptables_goto_bigstep_induct)
(auto intro: iptables_goto_bigstep.intros simp: assms Cons_eq_append_conv dest: skipD)
qed
private lemma matches_MatchNot_simp:
assumes "matches γ m p"
shows "Γ,γ,p⊢⇩g ⟨[Rule (MatchNot m) a], Undecided⟩ ⇒ t ⟷ Γ,γ,p⊢⇩g ⟨[], Undecided⟩ ⇒ t" (is "?l ⟷ ?r")
proof
assume ?l thus ?r
by (induction "[Rule (MatchNot m) a]" "Undecided" t rule: iptables_goto_bigstep_induct)
(auto intro: iptables_goto_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
private lemma matches_MatchNotAnd_simp:
assumes "matches γ m p"
shows "Γ,γ,p⊢⇩g ⟨[Rule (MatchAnd (MatchNot m) m') a], Undecided⟩ ⇒ t ⟷ Γ,γ,p⊢⇩g ⟨[], Undecided⟩ ⇒ t" (is "?l ⟷ ?r")
proof
assume ?l thus ?r
by (induction "[Rule (MatchAnd (MatchNot m) m') a]" "Undecided" t rule: iptables_goto_bigstep_induct)
(auto intro: iptables_goto_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
private lemma matches_rule_and_simp:
assumes "matches γ m p"
shows "Γ,γ,p⊢⇩g ⟨[Rule (MatchAnd m m') a'], s⟩ ⇒ t ⟷ Γ,γ,p⊢⇩g ⟨[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
qualified 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"
private 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)
private 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
private lemma matches_add_match_no_matching_Goto_simp: "matches γ m p ⟹ no_matching_Goto γ p (add_match m rs) ⟹ no_matching_Goto γ p rs"
apply(induction rs)
apply(simp_all)
apply(rename_tac r rs)
apply(case_tac r)
apply(simp add: add_match_split_fst no_matching_Goto_tail)
apply(drule no_matching_Goto_head)
apply(rename_tac m' a')
apply(case_tac a')
apply simp_all
done
private lemma matches_add_match_no_matching_Goto_simp2: "matches γ m p ⟹ no_matching_Goto γ p rs ⟹ no_matching_Goto γ p (add_match m rs)"
apply(induction rs)
apply(simp add: add_match_def)
apply(rename_tac r rs)
apply(case_tac r)
apply(simp add: add_match_split_fst no_matching_Goto_tail)
apply(rename_tac m' a')
apply(case_tac a')
apply simp_all
done
private lemma matches_add_match_MatchNot_no_matching_Goto_simp: "¬ matches γ m p ⟹ no_matching_Goto γ p (add_match m rs)"
apply(induction rs)
apply(simp add: add_match_def)
apply(rename_tac r rs)
apply(case_tac r)
apply(simp add: add_match_split_fst no_matching_Goto_tail)
apply(rename_tac m' a')
apply(case_tac a')
apply simp_all
done
private lemma not_matches_add_match_simp:
assumes "¬ matches γ m p"
shows "Γ,γ,p⊢⇩g ⟨add_match m rs, Undecided⟩ ⇒ t ⟷ Γ,γ,p⊢⇩g ⟨[], Undecided⟩ ⇒ t"
proof(induction rs)
case Nil thus ?case unfolding add_match_def by simp
next
case (Cons r rs)
obtain m' a where r: "r = Rule m' a" by(cases r, simp)
let ?lhs="Γ,γ,p⊢⇩g ⟨Rule (MatchAnd m m') a # add_match m rs, Undecided⟩ ⇒ t"
let ?rhs="Γ,γ,p⊢⇩g ⟨[], Undecided⟩ ⇒ t"
{ assume ?lhs
from ‹?lhs› Cons have ?rhs
proof(cases Γ γ p "Rule (MatchAnd m m') a" "add_match m rs" t rule: seqE_cons_Undecided)
case (no_matching_Goto ti)
hence "ti = Undecided" by (simp add: assms nomatchD)
with no_matching_Goto Cons show ?thesis by simp
next
case (matching_Goto) with Cons assms show ?thesis by force
qed
} note 1=this
{ assume ?rhs
hence "t = Undecided" using skipD by metis
with Cons.IH ‹?rhs› have ?lhs
by (meson assms matches.simps(1) nomatch not_no_matching_Goto_singleton_cases seq_cons)
} with 1 show ?case by(auto simp add: r add_match_split_fst)
qed
private lemma matches_add_match_MatchNot_simp:
assumes m: "matches γ m p"
shows "Γ,γ,p⊢⇩g ⟨add_match (MatchNot m) rs, s⟩ ⇒ t ⟷ Γ,γ,p⊢⇩g ⟨[], 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)
hence "t = Undecided" using skipD by metis
with Cons show ?case
apply (cases r)
apply(simp add: add_match_split_fst)
by (metis matches.simps(1) matches.simps(2) matches_MatchNotAnd_simp not_no_matching_Goto_singleton_cases seq_cons)
qed
qed
with Undecided show ?thesis by fast
next
case (Decision d)
thus ?thesis
by(metis decision decisionD)
qed
private lemma just_show_all_bigstep_semantics_equalities_with_start_Undecided:
"Γ,γ,p⊢⇩g ⟨rs1, Undecided⟩ ⇒ t ⟷ Γ,γ,p⊢⇩g ⟨rs2, Undecided⟩ ⇒ t ⟹
Γ,γ,p⊢⇩g ⟨rs1, s⟩ ⇒ t ⟷ Γ,γ,p⊢⇩g ⟨rs2, s⟩ ⇒ t"
apply(cases s)
apply(simp)
apply(simp)
using decision decisionD by fastforce
private lemma matches_add_match_simp_helper:
assumes m: "matches γ m p"
shows "Γ,γ,p⊢⇩g ⟨add_match m rs, Undecided⟩ ⇒ t ⟷ Γ,γ,p⊢⇩g ⟨rs, Undecided⟩ ⇒ 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)
obtain m' a where r: "r = Rule m' a" by(cases r, simp)
from Cons have " Γ,γ,p⊢⇩g ⟨Rule (MatchAnd m m') a # add_match m rs, Undecided⟩ ⇒ t"
by(simp add: r add_match_split_fst)
from this Cons have "Γ,γ,p⊢⇩g ⟨Rule m' a # rs, Undecided⟩ ⇒ t"
proof(cases rule: seqE_cons_Undecided)
case (no_matching_Goto ti)
from no_matching_Goto(3) Cons.prems(1) not_no_matching_Goto_singleton_cases
have "no_matching_Goto γ p [Rule m' a]" by (metis matches.simps(1))
with no_matching_Goto Cons show ?thesis
apply(simp add: matches_rule_and_simp)
apply(cases ti)
apply (simp add: seq'_cons)
by (metis decision decisionD seq'_cons)
next
case (matching_Goto) with Cons show ?thesis
apply(clarify)
apply(simp add: matches_rule_and_simp_help)
by (simp add: seq_cons_Goto_t)
qed
thus ?case by(simp add: r)
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)
obtain m' a where r: "r = Rule m' a" by(cases r, simp)
from Cons have "Γ,γ,p⊢⇩g ⟨Rule m' a # rs, Undecided⟩ ⇒ t" by(simp add: r)
from this have "Γ,γ,p⊢⇩g ⟨Rule (MatchAnd m m') a # add_match m rs, Undecided⟩ ⇒ t"
proof(cases Γ γ p "Rule m' a" rs t rule: seqE_cons_Undecided)
case (no_matching_Goto ti)
from no_matching_Goto Cons.prems matches_rule_and_simp[symmetric] have
"Γ,γ,p⊢⇩g ⟨[Rule (MatchAnd m m') a], Undecided⟩ ⇒ ti" by fast
with Cons.prems Cons.IH no_matching_Goto show ?thesis
apply(cases ti)
apply (metis matches.simps(1) not_no_matching_Goto_singleton_cases seq_cons)
apply (metis decision decisionD matches.simps(1) not_no_matching_Goto_singleton_cases seq_cons)
done
next
case (matching_Goto) with Cons show ?thesis
by (simp add: matches_rule_and_simp_help seq_cons_Goto_t)
qed
thus ?case by(simp add: r add_match_split_fst)
qed
qed
private lemma matches_add_match_simp:
"matches γ m p ⟹ Γ,γ,p⊢⇩g ⟨add_match m rs, s⟩ ⇒ t ⟷ Γ,γ,p⊢⇩g ⟨rs, s⟩ ⇒ t"
apply(rule just_show_all_bigstep_semantics_equalities_with_start_Undecided)
by(simp add: matches_add_match_simp_helper)
private lemma not_matches_add_matchNot_simp:
"¬ matches γ m p ⟹ Γ,γ,p⊢⇩g ⟨add_match (MatchNot m) rs, s⟩ ⇒ t ⟷ Γ,γ,p⊢⇩g ⟨rs, s⟩ ⇒ t"
by (simp add: matches_add_match_simp)
subsection‹Goto Unfolding›
private lemma unfold_Goto_Undecided:
assumes chain_defined: "Γ chain = Some rs" and no_matching_Goto_rs: "no_matching_Goto γ p rs"
shows "Γ,γ,p⊢⇩g ⟨(Rule m (Goto chain))#rest, Undecided⟩ ⇒ t ⟷ Γ,γ,p⊢⇩g ⟨add_match m rs @ add_match (MatchNot m) rest, Undecided⟩ ⇒ t"
(is "?l ⟷ ?r")
proof
assume ?l
thus ?r
proof(cases rule: seqE_cons_Undecided)
case (no_matching_Goto ti)
from no_matching_Goto have "¬ matches γ m p" by simp
with no_matching_Goto have ti: "ti = Undecided" using nomatchD by metis
from ‹¬ matches γ m p› have "Γ,γ,p⊢⇩g ⟨add_match m rs, Undecided⟩ ⇒ Undecided"
using not_matches_add_match_simp skip by fast
from ‹¬ matches γ m p› matches_add_match_MatchNot_no_matching_Goto_simp have "no_matching_Goto γ p (add_match m rs)" by force
from no_matching_Goto ti have "Γ,γ,p⊢⇩g ⟨rest, Undecided⟩ ⇒ t" by simp
with not_matches_add_matchNot_simp[OF ‹¬ matches γ m p›] have "Γ,γ,p⊢⇩g ⟨add_match (MatchNot m) rest, Undecided⟩ ⇒ t" by simp
show ?thesis
by (meson ‹Γ,γ,p⊢⇩g ⟨add_match (MatchNot m) rest, Undecided⟩ ⇒ t› ‹Γ,γ,p⊢⇩g ⟨add_match m rs, Undecided⟩ ⇒ Undecided› ‹no_matching_Goto γ p (add_match m rs)› seq)
next
case (matching_Goto m chain rs')
from matching_Goto gotoD assms have "Γ,γ,p⊢⇩g ⟨rs, Undecided⟩ ⇒ t" by fastforce
hence 1: "Γ,γ,p⊢⇩g ⟨add_match m rs, Undecided⟩ ⇒ t" by (simp add: matches_add_match_simp matching_Goto(3))
have 2: "Γ,γ,p⊢⇩g ⟨add_match (MatchNot m) rest, t⟩ ⇒ t" by (simp add: matches_add_match_MatchNot_simp matching_Goto(3) skip)
from no_matching_Goto_rs matches_add_match_no_matching_Goto_simp2 matching_Goto have 3: "no_matching_Goto γ p (add_match m rs)" by fast
from 1 2 3 show ?thesis using matching_Goto(1) seq by fastforce
qed
next
assume ?r
thus ?l
proof(cases "matches γ m p")
case True
have "Γ,γ,p⊢⇩g ⟨rs, Undecided⟩ ⇒ t"
by (metis True ‹Γ,γ,p⊢⇩g ⟨add_match m rs @ add_match (MatchNot m) rest, Undecided⟩ ⇒ t›
matches_add_match_MatchNot_simp matches_add_match_simp_helper self_append_conv seq' seqE)
show ?l
apply(cases t)
using goto_no_decision[OF True] chain_defined apply (metis ‹Γ,γ,p⊢⇩g ⟨rs, Undecided⟩ ⇒ t›)
using goto_decision[OF True, of Γ chain rs _ rest] chain_defined apply (metis ‹Γ,γ,p⊢⇩g ⟨rs, Undecided⟩ ⇒ t›)
done
next
case False
with ‹?r› have "Γ,γ,p⊢⇩g ⟨add_match (MatchNot m) rest, Undecided⟩ ⇒ t"
by (metis matches_add_match_MatchNot_no_matching_Goto_simp not_matches_add_match_simp seqE skipD)
with False have "Γ,γ,p⊢⇩g ⟨rest, Undecided⟩ ⇒ t" by (meson not_matches_add_matchNot_simp)
show ?l by (meson False ‹Γ,γ,p⊢⇩g ⟨rest, Undecided⟩ ⇒ t› nomatch not_no_matching_Goto_singleton_cases seq_cons)
qed
qed
qualified theorem unfold_Goto:
assumes chain_defined: "Γ chain = Some rs" and no_matching_Goto_rs: "no_matching_Goto γ p rs"
shows "Γ,γ,p⊢⇩g ⟨(Rule m (Goto chain))#rest, s⟩ ⇒ t ⟷ Γ,γ,p⊢⇩g ⟨add_match m rs @ add_match (MatchNot m) rest, s⟩ ⇒ t"
apply(rule just_show_all_bigstep_semantics_equalities_with_start_Undecided)
using assms unfold_Goto_Undecided by fast
text‹A chain that will definitely come to a direct decision›
qualified fun terminal_chain :: "'a rule list ⇒ bool" where
"terminal_chain [] = False" |
"terminal_chain [Rule MatchAny Accept] = True" |
"terminal_chain [Rule MatchAny Drop] = True" |
"terminal_chain [Rule MatchAny Reject] = True" |
"terminal_chain ((Rule _ (Goto _))#rs) = False" |
"terminal_chain ((Rule _ (Call _))#rs) = False" |
"terminal_chain ((Rule _ Return)#rs) = False" |
"terminal_chain ((Rule _ Unknown)#rs) = False" |
"terminal_chain (_#rs) = terminal_chain rs"
private lemma terminal_chain_no_matching_Goto: "terminal_chain rs ⟹ no_matching_Goto γ p rs"
by(induction rs rule: terminal_chain.induct) simp_all
text‹A terminal chain means (if the semantics are actually defined) that the chain will
ultimately yield a final filtering decision, for all packets.›
qualified lemma "terminal_chain rs ⟹ Γ,γ,p⊢⇩g ⟨rs, Undecided⟩ ⇒ t ⟹ ∃X. t = Decision X"
apply(induction rs)
apply(simp)
apply(rename_tac r rs)
apply(case_tac r)
apply(rename_tac m a)
apply(simp)
apply(frule_tac γ=γ and p=p in terminal_chain_no_matching_Goto)
apply(case_tac a)
apply(simp_all)
apply(erule seqE_cons, simp_all,
metis iptables_goto_bigstepD matches.elims terminal_chain.simps terminal_chain.simps terminal_chain.simps)+
done
private lemma replace_Goto_with_Call_in_terminal_chain_Undecided:
assumes chain_defined: "Γ chain = Some rs" and terminal_chain: "terminal_chain rs"
shows "Γ,γ,p⊢⇩g ⟨[Rule m (Goto chain)], Undecided⟩ ⇒ t ⟷ Γ,γ,p⊢⇩g ⟨[Rule m (Call chain)], Undecided⟩ ⇒ t"
(is "?l ⟷ ?r")
proof
assume ?l
thus ?r
proof(cases rule: seqE_cons_Undecided)
case (no_matching_Goto ti)
from no_matching_Goto have "¬ matches γ m p" by simp
with nomatch have 1: "Γ,γ,p⊢⇩g ⟨[Rule m (Goto chain)], Undecided⟩ ⇒ Undecided" by fast
from ‹¬ matches γ m p› nomatch have 2: "Γ,γ,p⊢⇩g ⟨[Rule m (Call chain)], Undecided⟩ ⇒ Undecided" by fast
from 1 2 show ?thesis
using ‹?l› iptables_goto_bigstep_Undecided_Undecided_deterministic by fastforce
next
case (matching_Goto m chain rs')
from matching_Goto gotoD assms have "Γ,γ,p⊢⇩g ⟨rs, Undecided⟩ ⇒ t" by fastforce
from call_result[OF ‹matches γ m p› chain_defined ‹Γ,γ,p⊢⇩g ⟨rs, Undecided⟩ ⇒ t›] show ?thesis
by (metis matching_Goto(1) rule.sel(1))
qed
next
assume ?r
thus ?l
proof(cases "matches γ m p")
case True
{fix rs1::"'a rule list" and m' and rs2
have "terminal_chain (rs1 @ Rule m' Return # rs2) ⟹ False"
apply(induction rs1)
apply(simp_all)
apply(rename_tac r' rs')
apply(case_tac r')
apply(rename_tac m a)
apply(simp_all)
apply(case_tac a)
apply(simp_all)
apply (metis append_is_Nil_conv hd_Cons_tl terminal_chain.simps)+
done
} note no_return=this
have "Γ,γ,p⊢⇩g ⟨rs, Undecided⟩ ⇒ t"
apply(rule callD[OF ‹?r› _ _ True chain_defined])
apply(simp_all)
using no_return terminal_chain by blast
show ?l
apply(cases t)
using goto_no_decision[OF True] chain_defined apply (metis ‹Γ,γ,p⊢⇩g ⟨rs, Undecided⟩ ⇒ t›)
using goto_decision[OF True, of Γ chain rs _ "[]"] chain_defined apply (metis ‹Γ,γ,p⊢⇩g ⟨rs, Undecided⟩ ⇒ t›)
done
next
case False
show ?l using False ‹Γ,γ,p⊢⇩g ⟨[Rule m (Call chain)], Undecided⟩ ⇒ t› nomatch nomatchD by fastforce
qed
qed
qualified theorem replace_Goto_with_Call_in_terminal_chain:
assumes chain_defined: "Γ chain = Some rs" and terminal_chain: "terminal_chain rs"
shows "Γ,γ,p⊢⇩g ⟨[Rule m (Goto chain)], s⟩ ⇒ t ⟷ Γ,γ,p⊢⇩g ⟨[Rule m (Call chain)], s⟩ ⇒ t"
apply(rule just_show_all_bigstep_semantics_equalities_with_start_Undecided)
using assms replace_Goto_with_Call_in_terminal_chain_Undecided by fast
qualified fun rewrite_Goto_chain_safe :: "(string ⇀ 'a rule list) ⇒ 'a rule list ⇒ ('a rule list) option" where
"rewrite_Goto_chain_safe _ [] = Some []" |
"rewrite_Goto_chain_safe Γ ((Rule m (Goto chain))#rs) =
(case (Γ chain) of None ⇒ None
| Some rs' ⇒ (if
¬ terminal_chain rs'
then
None
else
map_option (λrs. Rule m (Call chain) # rs) (rewrite_Goto_chain_safe Γ rs)
)
)" |
"rewrite_Goto_chain_safe Γ (r#rs) = map_option (λrs. r # rs) (rewrite_Goto_chain_safe Γ rs)"
private fun rewrite_Goto_safe_internal
:: "(string × 'a rule list) list ⇒ (string × 'a rule list) list ⇒ (string × 'a rule list) list option" where
"rewrite_Goto_safe_internal _ [] = Some []" |
"rewrite_Goto_safe_internal Γ ((chain_name, rs)#cs) =
(case rewrite_Goto_chain_safe (map_of Γ) rs of
None ⇒ None
| Some rs' ⇒ map_option (λrst. (chain_name, rs')#rst) (rewrite_Goto_safe_internal Γ cs)
)"
qualified fun rewrite_Goto_safe :: "(string × 'a rule list) list ⇒ (string × 'a rule list) list option" where
"rewrite_Goto_safe cs = rewrite_Goto_safe_internal cs cs"
qualified definition rewrite_Goto :: "(string × 'a rule list) list ⇒ (string × 'a rule list) list" where
"rewrite_Goto cs = the (rewrite_Goto_safe cs)"
private lemma step_IH_cong: "(⋀s. Γ,γ,p⊢⇩g ⟨rs1, s⟩ ⇒ t = Γ,γ,p⊢⇩g ⟨rs2, s⟩ ⇒ t) ⟹
Γ,γ,p⊢⇩g ⟨r#rs1, s⟩ ⇒ t = Γ,γ,p⊢⇩g ⟨r#rs2, s⟩ ⇒ t"
apply(rule iffI)
apply(erule seqE_cons)
apply(rule seq'_cons)
apply simp_all
apply(drule not_no_matching_Goto_cases)
apply(simp; fail)
apply(elim exE conjE, rename_tac rs1a m chain rs2a)
apply(subgoal_tac "r = Rule m (Goto chain)")
prefer 2
subgoal by (simp add: Cons_eq_append_conv)
apply(thin_tac "[r] = _ @ Rule m (Goto chain) # _")
apply simp
apply (metis decision decisionD seq_cons_Goto_t state.exhaust)
apply(erule seqE_cons)
apply(rule seq'_cons)
apply simp_all
apply(drule not_no_matching_Goto_cases)
apply(simp; fail)
apply(elim exE conjE, rename_tac rs1a m chain rs2a)
apply(subgoal_tac "r = Rule m (Goto chain)")
prefer 2
subgoal by (simp add: Cons_eq_append_conv)
apply(thin_tac "[r] = _ @ Rule m (Goto chain) # _")
apply simp
apply (metis decision decisionD seq_cons_Goto_t state.exhaust)
done
private lemma terminal_chain_decision:
"terminal_chain rs ⟹ Γ,γ,p⊢⇩g ⟨rs, Undecided⟩ ⇒ t ⟹ ∃X. t = Decision X"
apply(induction rs arbitrary: t rule: terminal_chain.induct)
apply simp_all
apply(auto dest: iptables_goto_bigstepD)[3]
apply(erule seqE_cons, simp_all, blast dest: iptables_goto_bigstepD)+
done
private lemma terminal_chain_Goto_decision: "Γ chain = Some rs ⟹ terminal_chain rs ⟹ matches γ m p ⟹
Γ,γ,p⊢⇩g ⟨[Rule m (Goto chain)], s⟩ ⇒ t ⟹ ∃X. t = Decision X"
apply(cases s)
apply(drule gotoD, simp_all)
apply(elim exE conjE, simp_all)
using terminal_chain_decision apply fast
by (meson decisionD)
qualified theorem rewrite_Goto_chain_safe:
"rewrite_Goto_chain_safe Γ rs = Some rs' ⟹ Γ,γ,p⊢⇩g ⟨rs', s⟩ ⇒ t ⟷ Γ,γ,p⊢⇩g ⟨rs, s⟩ ⇒ t"
proof(induction Γ rs arbitrary: rs' s rule: rewrite_Goto_chain_safe.induct)
case 1 thus ?case by (simp split: option.split_asm if_split_asm)
next
case (2 Γ m chain rs)
from 2(2) obtain z x2 where "Γ chain = Some x2" and "terminal_chain x2"
and "rs' = Rule m (Call chain) # z"
and "Some z = rewrite_Goto_chain_safe Γ rs"
by(auto split: option.split_asm if_split_asm)
from 2(1) ‹Γ chain = Some x2› ‹terminal_chain x2› ‹Some z = rewrite_Goto_chain_safe Γ rs›
have IH: "Γ,γ,p⊢⇩g ⟨z, s⟩ ⇒ t = Γ,γ,p⊢⇩g ⟨rs, s⟩ ⇒ t" for s by simp
have "Γ,γ,p⊢⇩g ⟨Rule m (Call chain) # z, Undecided⟩ ⇒ t ⟷ Γ,γ,p⊢⇩g ⟨Rule m (Goto chain) # rs, Undecided⟩ ⇒ t"
(is "?lhs ⟷ ?rhs")
proof(intro iffI)
assume ?lhs
with IH obtain ti where ti1: "Γ,γ,p⊢⇩g ⟨[Rule m (Call chain)], Undecided⟩ ⇒ ti" and ti2: "Γ,γ,p⊢⇩g ⟨rs, ti⟩ ⇒ t"
by(auto elim: seqE_cons)
show ?rhs
proof(cases "matches γ m p")
case False
from replace_Goto_with_Call_in_terminal_chain ‹Γ chain = Some x2› ‹terminal_chain x2›
have " Γ,γ,p⊢⇩g ⟨[Rule m (Call chain)], Undecided⟩ ⇒ ti ⟷ Γ,γ,p⊢⇩g ⟨[Rule m (Goto chain)], Undecided⟩ ⇒ ti"
by fast
with False ti1 ti2 show ?thesis by(rule_tac t=ti in seq'_cons) simp+
next
case True
from ti1 ‹Γ chain = Some x2› ‹terminal_chain x2›
have g: "Γ,γ,p⊢⇩g ⟨[Rule m (Goto chain)], Undecided⟩ ⇒ ti"
by(subst(asm) replace_Goto_with_Call_in_terminal_chain[symmetric]) simp+
with True ‹Γ chain = Some x2› ‹terminal_chain x2› obtain X where X: "ti = Decision X"
by(blast dest: terminal_chain_Goto_decision)
with this ti2 have "t = Decision X"
by(simp add: decisionD)
with g X True ti2 ‹Γ chain = Some x2› ‹terminal_chain x2› show ?thesis
apply(simp)
apply(rule seq_cons_Goto_t, simp_all)
done
qed
next
assume ?rhs
with IH ‹Γ chain = Some x2› ‹terminal_chain x2› ‹Some z = rewrite_Goto_chain_safe Γ rs› show ?lhs
apply -
apply(erule seqE_cons)
subgoal for ti
apply simp_all
apply(rule_tac t=ti in seq'_cons)
apply simp_all
using replace_Goto_with_Call_in_terminal_chain by fast
apply simp
apply(frule(3) terminal_chain_Goto_decision)
apply(subst(asm) replace_Goto_with_Call_in_terminal_chain, simp_all)
apply(rule seq'_cons, simp_all)
apply(elim exE)
by (simp add: decision)
qed
with ‹rs' = Rule m (Call chain) # z› show ?case
apply -
apply(rule just_show_all_bigstep_semantics_equalities_with_start_Undecided)
by simp
qed(auto cong: step_IH_cong)
text‹Example: The semantics are actually defined (for this example).›
lemma defines "γ ≡ (λ_ _. True)" and "m ≡ MatchAny"
shows "[''FORWARD'' ↦ [Rule m Log, Rule m (Call ''foo''), Rule m Drop],
''foo'' ↦ [Rule m Log, Rule m (Goto ''bar''), Rule m Reject],
''bar'' ↦ [Rule m (Goto ''baz''), Rule m Reject],
''baz'' ↦ [(Rule m Accept)]],
γ,p⊢⇩g⟨[Rule MatchAny (Call ''FORWARD'')], Undecided⟩ ⇒ (Decision FinalAllow)"
apply(subgoal_tac "matches γ m p")
prefer 2
apply(simp add: γ_def m_def; fail)
apply(rule call_result)
apply(auto)
apply(rule_tac t=Undecided in seq_cons)
apply(auto intro: log)
apply(rule_tac t="Decision FinalAllow" in seq_cons)
apply(auto intro: decision)
apply(rule call_result)
apply(simp)+
apply(rule_tac t=Undecided in seq_cons)
apply(auto intro: log)
apply(rule goto_decision)
apply(simp)+
apply(rule goto_decision)
apply(simp)+
apply(auto intro: accept)
done
end
end