Theory Matching_Ternary

theory Matching_Ternary
imports "../Common/Ternary" "../Firewall_Common"
begin

section‹Packet Matching in Ternary Logic›

text‹The matcher for a primitive match expression @{typ "'a"}›
type_synonym ('a, 'packet) exact_match_tac="'a ⇒ 'packet ⇒ ternaryvalue"

text‹
If the matching is @{const TernaryUnknown}, it can be decided by the action whether this rule matches.
E.g. in doubt, we allow packets
›
type_synonym 'packet unknown_match_tac="action ⇒ 'packet ⇒ bool"

type_synonym ('a, 'packet) match_tac="(('a, 'packet) exact_match_tac × 'packet unknown_match_tac)"

text‹
For a given packet, map a firewall @{typ "'a match_expr"} to a @{typ ternaryformula}
Evaluating the formula gives whether the packet/rule matches (or unknown).
›
fun map_match_tac :: "('a, 'packet) exact_match_tac ⇒ 'packet ⇒ 'a match_expr ⇒ ternaryformula" where
"map_match_tac β p (MatchAnd m1 m2) = TernaryAnd (map_match_tac β p m1) (map_match_tac β p m2)" |
"map_match_tac β p (MatchNot m) = TernaryNot (map_match_tac β p m)" |
"map_match_tac β p (Match m) = TernaryValue (β m p)" |
"map_match_tac _ _ MatchAny = TernaryValue TernaryTrue"

context
begin
text‹the @{term ternaryformula}s we construct never have Or expressions.›
private fun ternary_has_or :: "ternaryformula ⇒ bool" where
"ternary_has_or (TernaryOr _ _) ⟷ True" |
"ternary_has_or (TernaryAnd t1 t2) ⟷ ternary_has_or t1 ∨ ternary_has_or t2" |
"ternary_has_or (TernaryNot t) ⟷ ternary_has_or t" |
"ternary_has_or (TernaryValue _) ⟷ False"
private lemma map_match_tac__does_not_use_TernaryOr: "¬ (ternary_has_or (map_match_tac β p m))"
by(induction m, simp_all)
declare ternary_has_or.simps[simp del]
end

fun ternary_to_bool_unknown_match_tac :: "'packet unknown_match_tac ⇒ action ⇒ 'packet ⇒ ternaryvalue ⇒ bool" where
"ternary_to_bool_unknown_match_tac _ _ _ TernaryTrue = True" |
"ternary_to_bool_unknown_match_tac _ _ _ TernaryFalse = False" |
"ternary_to_bool_unknown_match_tac α a p TernaryUnknown = α a p"

text‹
Matching a packet and a rule:
\begin{enumerate}
\item Translate @{typ "'a match_expr"} to ternary formula
\item Evaluate this formula
\item If @{const TernaryTrue}/@{const TernaryFalse}, return this value
\item If @{const TernaryUnknown}, apply the @{typ "'a unknown_match_tac"} to get a Boolean result
\end{enumerate}
›
definition matches :: "('a, 'packet) match_tac ⇒ 'a match_expr ⇒ action ⇒ 'packet ⇒ bool" where
"matches γ m a p ≡ ternary_to_bool_unknown_match_tac (snd γ) a p (ternary_ternary_eval (map_match_tac (fst γ) p m))"

text‹Alternative matches definitions, some more or less convenient›

lemma matches_tuple: "matches (β, α) m a p = ternary_to_bool_unknown_match_tac α a p (ternary_ternary_eval (map_match_tac β p m))"
unfolding matches_def by simp

lemma matches_case: "matches γ m a p ⟷ (case ternary_eval (map_match_tac (fst γ) p m) of None ⇒ (snd γ) a p | Some b ⇒ b)"
unfolding matches_def ternary_eval_def
by (cases "(ternary_ternary_eval (map_match_tac (fst γ) p m))") auto

lemma matches_case_tuple: "matches (β, α) m a p ⟷ (case ternary_eval (map_match_tac β p m) of None ⇒ α a p | Some b ⇒ b)"
by (auto simp: matches_case split: option.splits)

lemma matches_case_ternaryvalue_tuple: "matches (β, α) m a p ⟷ (case ternary_ternary_eval (map_match_tac β p m) of
TernaryUnknown ⇒ α a p |
TernaryTrue ⇒ True |
TernaryFalse ⇒ False)"
by(simp split: option.split ternaryvalue.split add: matches_case ternary_to_bool_None ternary_eval_def)
(*use together: matches_case_ternaryvalue_tuple ternaryvalue.split *)

lemma matches_casesE:
"matches (β, α) m a p ⟹
(ternary_ternary_eval (map_match_tac β p m) = TernaryUnknown ⟹ α a p ⟹ P) ⟹
(ternary_ternary_eval (map_match_tac β p m) = TernaryTrue ⟹ P)
⟹ P"
proof(induction m)
qed(auto split: option.split_asm simp: matches_case_tuple ternary_eval_def ternary_to_bool_bool_to_ternary elim: ternary_to_bool.elims)

text‹
Example: ‹¬ Unknown› is as good as ‹Unknown›
›
lemma "⟦ ternary_ternary_eval (map_match_tac β p expr) = TernaryUnknown ⟧ ⟹ matches (β, α) expr a p ⟷ matches (β, α) (MatchNot expr) a p"

"matches γ (MatchAnd m1 m2) a p ⟷ matches γ m1 a p ∧ matches γ m2 a p" (*split AND*)
"matches γ MatchAny a p" (*MatchAny is True*)
"matches γ (MatchNot MatchAny) a p ⟷ False" (*Not True*)
"matches γ (MatchNot (MatchNot m)) a p ⟷ matches γ m a p" (*idempotence*)
proof(case_tac [!] γ)
qed (simp_all split: ternaryvalue.split add: matches_case_ternaryvalue_tuple)

lemma match_raw_bool:
"matches (β, α) (Match expr) a p = (case ternary_to_bool (β expr p) of Some r ⇒ r | None ⇒ (α a p))" (*Match raw*)
lemma match_raw_ternary:
"matches (β, α) (Match expr) a p = (case (β expr p) of TernaryTrue ⇒ True | TernaryFalse ⇒ False | TernaryUnknown ⇒ (α a p))" (*Match raw explicit*)

(*kind of the DeMorgan Rule for matches*)
lemma matches_DeMorgan: "matches γ (MatchNot (MatchAnd m1 m2)) a p ⟷ (matches γ (MatchNot m1) a p) ∨ (matches γ (MatchNot m2) a p)"
by (cases γ) (simp split: ternaryvalue.split add: matches_case_ternaryvalue_tuple eval_ternary_DeMorgan)

subsection‹Ternary Matcher Algebra›

lemma matches_and_comm: "matches γ (MatchAnd m m') a p ⟷ matches γ (MatchAnd m' m) a p"
apply(cases γ, rename_tac β α, clarify)

lemma matches_not_idem: "matches γ (MatchNot (MatchNot m)) a p ⟷ matches γ m a p"

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

lemma MatchOr_MatchNot: "matches γ (MatchNot (MatchOr m1 m2)) a p ⟷ matches γ (MatchNot m1) a p ∧ matches γ (MatchNot m2) a p"

lemma "(TernaryNot (map_match_tac β p (m))) = (map_match_tac β p (MatchNot m))"
by (metis map_match_tac.simps(2))

context
begin
private lemma matches_simp1: "matches γ m a p ⟹ matches γ (MatchAnd m m') a p ⟷ matches γ m' a p"
apply(cases γ, rename_tac β α, clarify)
apply(simp split: ternaryvalue.split_asm ternaryvalue.split add: matches_case_ternaryvalue_tuple)
done

private lemma matches_simp11: "matches γ m a p ⟹ matches γ (MatchAnd m' m) a p ⟷ matches γ m' a p"

private lemma matches_simp2: "matches γ (MatchAnd m m') a p ⟹ ¬ matches γ m a p ⟹ False"
private lemma matches_simp22: "matches γ (MatchAnd m m') a p ⟹ ¬ matches γ m' a p ⟹ False"

(*m simplifies to MatchUnknown*)
private  lemma matches_simp3: "matches γ (MatchNot m) a p ⟹ matches γ m a p ⟹ (snd γ) a p"
apply(cases γ, rename_tac β α, clarify)
apply(simp split: ternaryvalue.split_asm ternaryvalue.split add: matches_case_ternaryvalue_tuple)
done
private lemma "matches γ (MatchNot m) a p ⟹ matches γ m a p ⟹ (ternary_eval (map_match_tac (fst γ) p m)) = None"
apply(cases γ, rename_tac β α, clarify)
apply(simp split: ternaryvalue.split_asm ternaryvalue.split add: matches_case_ternaryvalue_tuple ternary_eval_def)
done

lemmas matches_simps = matches_simp1 matches_simp11
lemmas matches_dest = matches_simp2 matches_simp22
end

lemma matches_iff_apply_f_generic: "ternary_ternary_eval (map_match_tac β p (f (β,α) a m)) = ternary_ternary_eval (map_match_tac β p m) ⟹ matches (β,α) (f (β,α) a m) a p ⟷ matches (β,α) m a p"
by(simp split: ternaryvalue.split_asm ternaryvalue.split add: matches_case_ternaryvalue_tuple)

lemma matches_iff_apply_f: "ternary_ternary_eval (map_match_tac β p (f m)) = ternary_ternary_eval (map_match_tac β p m) ⟹ matches (β,α) (f m) a p ⟷ matches (β,α) m a p"
by(fact matches_iff_apply_f_generic)

lemma opt_MatchAny_match_expr_correct: "matches γ (opt_MatchAny_match_expr m) = matches γ m"
proof(case_tac γ, rename_tac β α, clarify)
fix β α
assume "γ = (β, α)"
have "ternary_ternary_eval (map_match_tac β p (opt_MatchAny_match_expr_once m)) =
ternary_ternary_eval (map_match_tac β p m)" for p m
proof(induction m rule: opt_MatchAny_match_expr_once.induct)
thus "matches (β, α) (opt_MatchAny_match_expr m) = matches (β, α) m"
apply(clarify, rename_tac a p)
apply(rule_tac f="opt_MatchAny_match_expr" in matches_iff_apply_f)
apply(simp)
apply(rule repeat_stabilize_induct)
by(simp)+
qed

text‹An @{typ "'p unknown_match_tac"} is wf if it behaves equal for @{const Reject} and @{const Drop}›
definition wf_unknown_match_tac :: "'p unknown_match_tac ⇒ bool" where
"wf_unknown_match_tac α ≡ (α Drop = α Reject)"

lemma wf_unknown_match_tacD_False1: "wf_unknown_match_tac α ⟹ ¬ matches (β, α) m Reject p ⟹ matches (β, α) m Drop p ⟹ False"
unfolding wf_unknown_match_tac_def by(simp add: matches_case_ternaryvalue_tuple split: ternaryvalue.split_asm)

lemma wf_unknown_match_tacD_False2: "wf_unknown_match_tac α ⟹ matches (β, α) m Reject p ⟹ ¬ matches (β, α) m Drop p ⟹ False"
unfolding wf_unknown_match_tac_def by(simp add: matches_case_ternaryvalue_tuple split: ternaryvalue.split_asm)

subsection‹Removing Unknown Primitives›

definition unknown_match_all :: "'a unknown_match_tac ⇒ action ⇒ bool" where
"unknown_match_all α a = (∀p. α a p)"
definition unknown_not_match_any :: "'a unknown_match_tac ⇒ action ⇒ bool" where
"unknown_not_match_any α a = (∀p. ¬ α a p)"

(*see upper_closure_matchexpr*)
fun remove_unknowns_generic :: "('a, 'packet) match_tac ⇒ action ⇒ 'a match_expr ⇒ 'a match_expr" where
"remove_unknowns_generic _ _ MatchAny = MatchAny" |
"remove_unknowns_generic _ _ (MatchNot MatchAny) = MatchNot MatchAny" |
"remove_unknowns_generic (β, α) a (Match A) = (if
(∀p. ternary_ternary_eval (map_match_tac β p (Match A)) = TernaryUnknown)
then
if unknown_match_all α a then MatchAny else if unknown_not_match_any α a then MatchNot MatchAny else Match A
else (Match A))" |
"remove_unknowns_generic (β, α) a (MatchNot (Match A)) = (if
(∀p. ternary_ternary_eval (map_match_tac β p (Match A)) = TernaryUnknown)
then
if unknown_match_all α a then MatchAny else if unknown_not_match_any α a then MatchNot MatchAny else MatchNot (Match A)
else MatchNot (Match A))" |
"remove_unknowns_generic (β, α) a (MatchNot (MatchNot m)) = remove_unknowns_generic (β, α) a m" |
"remove_unknowns_generic (β, α) a (MatchAnd m1 m2) = MatchAnd
(remove_unknowns_generic (β, α) a m1)
(remove_unknowns_generic (β, α) a m2)" |

― ‹@{text "¬ (a ∧ b) = ¬ b ∨ ¬ a"}   and   @{text "¬ Unknown = Unknown"}›
"remove_unknowns_generic (β, α) a (MatchNot (MatchAnd m1 m2)) =
(if (remove_unknowns_generic (β, α) a (MatchNot m1)) = MatchAny ∨
(remove_unknowns_generic (β, α) a (MatchNot m2)) = MatchAny
then MatchAny else
(if (remove_unknowns_generic (β, α) a (MatchNot m1)) = MatchNot MatchAny then
remove_unknowns_generic (β, α) a (MatchNot m2) else
if (remove_unknowns_generic (β, α) a (MatchNot m2)) = MatchNot MatchAny then
remove_unknowns_generic (β, α) a (MatchNot m1) else
MatchNot (MatchAnd (MatchNot (remove_unknowns_generic (β, α) a (MatchNot m1))) (MatchNot (remove_unknowns_generic (β, α) a (MatchNot m2)))))
)"

lemma[code_unfold]: "remove_unknowns_generic γ a (MatchNot (MatchAnd m1 m2)) =
(let m1' = remove_unknowns_generic γ  a (MatchNot m1); m2' = remove_unknowns_generic γ  a (MatchNot m2) in
(if m1' = MatchAny ∨ m2' = MatchAny
then MatchAny
else
if m1' = MatchNot MatchAny then m2' else
if m2' = MatchNot MatchAny then m1'
else
MatchNot (MatchAnd (MatchNot m1') (MatchNot m2')))
)"
by(cases γ)(simp)

lemma remove_unknowns_generic_simp_3_4_unfolded: "remove_unknowns_generic (β, α) a (Match A) = (if
(∀p. ternary_ternary_eval (map_match_tac β p (Match A)) = TernaryUnknown)
then
if (∀p. α a p) then MatchAny else if (∀p. ¬ α a p) then MatchNot MatchAny else Match A
else (Match A))"
"remove_unknowns_generic (β, α) a (MatchNot (Match A)) = (if
(∀p. ternary_ternary_eval (map_match_tac β p (Match A)) = TernaryUnknown)
then
if (∀p. α a p) then MatchAny else if (∀p. ¬ α a p) then MatchNot MatchAny else MatchNot (Match A)
else MatchNot (Match A))"

declare remove_unknowns_generic.simps[simp del]

lemmas remove_unknowns_generic_simps2 = remove_unknowns_generic.simps(1) remove_unknowns_generic.simps(2)
remove_unknowns_generic_simp_3_4_unfolded
remove_unknowns_generic.simps(5) remove_unknowns_generic.simps(6) remove_unknowns_generic.simps(7)

lemma "matches (β, α) (remove_unknowns_generic (β, α) a (MatchNot (Match A))) a p = matches (β, α) (MatchNot (Match A)) a p"

lemma remove_unknowns_generic: "matches γ (remove_unknowns_generic γ a m) a = matches γ m a"
proof -
have "matches γ (remove_unknowns_generic γ a m) a p = matches γ m a p"
for p
proof(induction γ a m rule: remove_unknowns_generic.induct)
case 3 thus ?case
next
case 4 thus ?case
next
case 7 thus ?case
by fastforce
qed

fun has_unknowns :: " ('a, 'p) exact_match_tac ⇒ 'a match_expr ⇒ bool" where
"has_unknowns β (Match A) = (∃p. ternary_ternary_eval (map_match_tac β p (Match A)) = TernaryUnknown)" |
"has_unknowns β (MatchNot m) = has_unknowns β m" |
"has_unknowns β MatchAny = False" |
"has_unknowns β (MatchAnd m1 m2) = (has_unknowns β m1 ∨ has_unknowns β m2)"

(* assumes simple_ruleset, thus we only care about Accept/Drop *)
definition packet_independent_α :: "'p unknown_match_tac ⇒ bool" where
"packet_independent_α α = (∀a p1 p2. a = Accept ∨ a = Drop ⟶ α a p1 ⟷ α a p2)"

lemma packet_independent_unknown_match: "a = Accept ∨ a = Drop ⟹ packet_independent_α α ⟹ ¬ unknown_not_match_any α a ⟷ unknown_match_all α a"
by(auto simp add: packet_independent_α_def unknown_match_all_def unknown_not_match_any_def)

text‹If for some type the exact matcher returns unknown, then it returns unknown for all these types›
definition packet_independent_β_unknown :: "('a, 'packet) exact_match_tac ⇒ bool" where
"packet_independent_β_unknown β ≡ ∀A. (∃p. β A p ≠ TernaryUnknown) ⟶ (∀p. β A p ≠ TernaryUnknown)"

lemma remove_unknowns_generic_specification: "a = Accept ∨ a = Drop ⟹ packet_independent_α α ⟹
packet_independent_β_unknown β ⟹
¬ has_unknowns β (remove_unknowns_generic (β, α) a m)"
proof(induction "(β, α)" a m rule: remove_unknowns_generic.induct)
case 3 thus ?case by(simp add: packet_independent_unknown_match packet_independent_β_unknown_def remove_unknowns_generic.simps)
next
case 4 thus ?case by(simp add: packet_independent_unknown_match packet_independent_β_unknown_def remove_unknowns_generic.simps)

text‹Checking is something matches unconditionally›
context
begin
private lemma no_primitives_no_unknown: "¬ has_primitive m  ⟹ (ternary_ternary_eval (map_match_tac β p m)) ≠ TernaryUnknown"
proof(induction m)
case Match thus ?case by auto
next
case MatchAny thus ?case by simp
next
case MatchAnd thus ?case by(auto elim: eval_ternary_And.elims)
next
case MatchNot thus ?case by(auto dest: eval_ternary_Not_UnknownD)
qed

private lemma no_primitives_matchNot: assumes "¬ has_primitive m" shows "matches γ (MatchNot m) a p ⟷ ¬ matches γ m a p"
proof -
obtain β α where "(β, α) = γ" by (cases γ, simp)
thm no_primitives_no_unknown
from assms have "matches (β, α) (MatchNot m) a p ⟷ ¬ matches (β, α) m a p"
apply(induction m)
apply(simp_all add: matches_case_ternaryvalue_tuple split: ternaryvalue.split )
apply(rename_tac m1 m2)
by(simp split: ternaryvalue.split_asm)
with ‹(β, α) = γ› assms show ?thesis by simp
qed

lemma matcheq_matchAny: "¬ has_primitive m ⟹ matcheq_matchAny m ⟷ matches γ m a p"
proof(induction m)
case Match hence False by auto
thus ?case ..
next
case (MatchNot m)
from MatchNot.prems have "¬ has_primitive m" by simp
with no_primitives_matchNot have "matches γ (MatchNot m) a p = (¬ matches γ m a p)" by metis
with MatchNot show ?case by(simp)
next
case (MatchAnd m1 m2)
next
qed

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

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

end

text‹Lemmas about @{const MatchNot} in ternary logic.›

lemma matches_MatchNot_no_unknowns:
assumes "¬ has_unknowns β m"
shows "matches (β,α) (MatchNot m) a p ⟷ ¬ matches (β,α) m a p"
proof -
{ fix m have "¬ has_unknowns β m ⟹
ternary_to_bool (ternary_ternary_eval (map_match_tac β p m)) ≠ None"
apply(induction m)
apply(simp_all)
using ternary_to_bool.elims apply blast
using ternary_to_bool_Some apply fastforce
using ternary_lift(6) ternary_to_bool_Some by auto
} note no_unknowns_ternary_to_bool_Some=this
from assms show ?thesis
by(auto split: option.split_asm
simp: matches_case_tuple no_unknowns_ternary_to_bool_Some ternary_to_bool_Some  ternary_eval_def ternary_to_bool_bool_to_ternary
elim: ternary_to_bool.elims)
qed

lemma MatchNot_ternary_ternary_eval: "(ternary_ternary_eval (map_match_tac β p m')) = (ternary_ternary_eval (map_match_tac β p m)) ⟹
matches (β,α) (MatchNot m') a p = matches (β,α) (MatchNot m) a p"

text‹For our @{typ "'p unknown_match_tac"}s ‹in_doubt_allow› and ‹in_doubt_deny›,
when doing an induction over some function that modifies @{term "m::'a match_expr"},
we get the @{const MatchNot} case for free (if we can set arbitrary @{term "p::'p"}).
This does not hold for arbitrary @{typ "'p unknown_match_tac"}s.›
lemma matches_induction_case_MatchNot:
assumes "α Drop ≠ α Accept" and "packet_independent_α α"
and     "∀ a. matches (β,α) m' a p = matches (β,α) m a p"
shows   "matches (β,α) (MatchNot m') a p = matches (β,α) (MatchNot m) a p"
proof -
from assms(1) assms(2) have xxxx_xxX: "⋀b. ∀a. α a p = (¬ b) ⟹ False"
apply(case_tac "α Accept p")
apply(simp_all)
apply(case_tac [!] "α Drop p")
apply blast+
done

have xx2: "⋀t. ternary_eval (TernaryNot t) = None ⟹ ternary_eval t = None"
by (simp add: eval_ternary_Not_UnknownD ternary_eval_def ternary_to_bool_None)

have xx3: "⋀t b. ternary_eval (TernaryNot t) = Some b ⟹  ternary_eval t = Some (¬ b)"
by (metis eval_ternary_Not.simps(1) eval_ternary_Not.simps(2) ternary_eval_def ternary_ternary_eval.simps(3) ternary_ternary_eval_idempotence_Not ternary_to_bool_Some)

from assms show ?thesis
apply(case_tac "ternary_eval (TernaryNot (map_match_tac β p m'))")
apply(case_tac [!] "ternary_eval (TernaryNot (map_match_tac β p m))")
apply(simp_all)
apply(drule xx2)
apply(drule xx3)
apply(simp)
using xxxx_xxX apply metis
apply(drule xx2)
apply(drule xx3)
apply(simp)
using xxxx_xxX apply metis
apply(drule xx3)+
apply(simp)
done
qed

end