Theory Matching

theory Matching
imports Semantics
begin

subsection‹Boolean Matcher Algebra›

lemma MatchOr: "matches γ (MatchOr m1 m2) p ⟷ matches γ m1 p ∨ matches γ m2 p"
  by(simp add: MatchOr_def)

lemma opt_MatchAny_match_expr_correct: "matches γ (opt_MatchAny_match_expr m) = matches γ m"
 proof -
  have "matches γ (opt_MatchAny_match_expr_once m) = matches γ m" for m
   apply(simp add: fun_eq_iff)
   by(induction m rule: opt_MatchAny_match_expr_once.induct) (simp_all)
   thus ?thesis
    apply(simp add: opt_MatchAny_match_expr_def)
    apply(rule repeat_stabilize_induct)
     by(simp)+
 qed
    

lemma matcheq_matchAny: "¬ has_primitive m ⟹ matcheq_matchAny m ⟷ matches γ m p"
  by(induction m) simp_all

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

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


text‹Lemmas about matching in the @{const iptables_bigstep} semantics.›

lemma matches_rule_iptables_bigstep:
  assumes "matches γ m p ⟷ matches γ m' p"
  shows "Γ,γ,p⊢ ⟨[Rule m a], s⟩ ⇒ t ⟷ Γ,γ,p⊢ ⟨[Rule m' a], s⟩ ⇒ t" (is "?l ⟷?r")
proof -
  {
    fix m m'
    assume "Γ,γ,p⊢ ⟨[Rule m a], s⟩ ⇒ t" "matches γ m p ⟷ matches γ m' p"
    hence "Γ,γ,p⊢ ⟨[Rule m' a], s⟩ ⇒ t"
      by (induction "[Rule  m a]" s t rule: iptables_bigstep_induct)
         (auto intro: iptables_bigstep.intros simp: Cons_eq_append_conv dest: skipD)
  }
  with assms show ?thesis by blast
qed

lemma matches_rule_and_simp_help:
  assumes "matches γ m p"
  shows "Γ,γ,p⊢ ⟨[Rule (MatchAnd m m') a'], Undecided⟩ ⇒ t ⟷ Γ,γ,p⊢ ⟨[Rule m' a'], Undecided⟩ ⇒ t" (is "?l ⟷?r")
proof
  assume ?l thus ?r
    by (induction "[Rule (MatchAnd m m') a']" Undecided t rule: iptables_bigstep_induct)
       (auto intro: iptables_bigstep.intros simp: assms Cons_eq_append_conv dest: skipD)
next
  assume ?r thus ?l
    by (induction "[Rule m' a']" Undecided t rule: iptables_bigstep_induct)
       (auto intro: iptables_bigstep.intros simp: assms Cons_eq_append_conv dest: skipD)
qed

lemma matches_MatchNot_simp: 
  assumes "matches γ m p"
  shows "Γ,γ,p⊢ ⟨[Rule (MatchNot m) a], Undecided⟩ ⇒ t ⟷ Γ,γ,p⊢ ⟨[], Undecided⟩ ⇒ t" (is "?l ⟷ ?r")
proof
  assume ?l thus ?r
    by (induction "[Rule (MatchNot m) a]" "Undecided" t rule: iptables_bigstep_induct)
       (auto intro: iptables_bigstep.intros simp: assms Cons_eq_append_conv dest: skipD)
next
  assume ?r
  hence "t = Undecided"
    by (metis skipD)
  with assms show ?l
    by (fastforce intro: nomatch)
qed

lemma matches_MatchNotAnd_simp:
  assumes "matches γ m p"
  shows "Γ,γ,p⊢ ⟨[Rule (MatchAnd (MatchNot m) m') a], Undecided⟩ ⇒ t ⟷ Γ,γ,p⊢ ⟨[], Undecided⟩ ⇒ t" (is "?l ⟷ ?r")
proof
  assume ?l thus ?r
    by (induction "[Rule (MatchAnd (MatchNot m) m') a]" "Undecided" t rule: iptables_bigstep_induct)
       (auto intro: iptables_bigstep.intros simp add: assms Cons_eq_append_conv dest: skipD)
next
  assume ?r
  hence "t = Undecided"
    by (metis skipD)
  with assms show ?l
    by (fastforce intro: nomatch)
qed
  
lemma matches_rule_and_simp:
  assumes "matches γ m p"
  shows "Γ,γ,p⊢ ⟨[Rule (MatchAnd m m') a'], s⟩ ⇒ t ⟷ Γ,γ,p⊢ ⟨[Rule m' a'], s⟩ ⇒ t"
proof (cases s)
  case Undecided
  with assms show ?thesis
    by (simp add: matches_rule_and_simp_help)
next
  case Decision
  thus ?thesis by (metis decision decisionD)
qed

lemma iptables_bigstep_MatchAnd_comm:
  "Γ,γ,p⊢ ⟨[Rule (MatchAnd m1 m2) a], s⟩ ⇒ t ⟷ Γ,γ,p⊢ ⟨[Rule (MatchAnd m2 m1) a], s⟩ ⇒ t"
proof -
  { fix m1 m2
    have "Γ,γ,p⊢ ⟨[Rule (MatchAnd m1 m2) a], s⟩ ⇒ t ⟹ Γ,γ,p⊢ ⟨[Rule (MatchAnd m2 m1) a], s⟩ ⇒ t"
      proof (induction "[Rule (MatchAnd m1 m2) a]" s t rule: iptables_bigstep_induct)
        case Seq thus ?case
          by (metis Nil_is_append_conv append_Nil butlast_append butlast_snoc seq)
      qed (auto intro: iptables_bigstep.intros)
  }
  thus ?thesis by blast
qed


subsection‹Add match›

definition add_match :: "'a match_expr ⇒ 'a rule list ⇒ 'a rule list" where
  "add_match m rs = map (λr. case r of Rule m' a' ⇒ Rule (MatchAnd m m') a') rs"

lemma add_match_split: "add_match m (rs1@rs2) = add_match m rs1 @ add_match m rs2"
  unfolding add_match_def
  by (fact map_append)

lemma add_match_split_fst: "add_match m (Rule m' a' # rs) = Rule (MatchAnd m m') a' # add_match m rs"
  unfolding add_match_def
  by simp


lemma add_match_distrib:
  "Γ,γ,p⊢ ⟨add_match m1 (add_match m2 rs), s⟩ ⇒ t ⟷ Γ,γ,p⊢ ⟨add_match m2 (add_match m1 rs), s⟩ ⇒ t"
proof -
  {
    fix m1 m2
    have "Γ,γ,p⊢ ⟨add_match m1 (add_match m2 rs), s⟩ ⇒ t ⟹ Γ,γ,p⊢ ⟨add_match m2 (add_match m1 rs), s⟩ ⇒ t"
      proof (induction rs arbitrary: s)
        case Nil thus ?case by (simp add: add_match_def)
        next
        case (Cons r rs)
        from Cons obtain m a where r: "r = Rule m a" by (cases r) simp
        with Cons.prems obtain ti where 1: "Γ,γ,p⊢ ⟨[Rule (MatchAnd m1 (MatchAnd m2 m)) a], s⟩ ⇒ ti" and 2: "Γ,γ,p⊢ ⟨add_match m1 (add_match m2 rs), ti⟩ ⇒ t"
          apply(simp add: add_match_split_fst)
          apply(erule seqE_cons)
          by simp
        from 1 r have base: "Γ,γ,p⊢ ⟨[Rule (MatchAnd m2 (MatchAnd m1 m)) a], s⟩ ⇒ ti"
           by (metis matches.simps(1) matches_rule_iptables_bigstep)
        from 2 Cons.IH have IH: "Γ,γ,p⊢ ⟨add_match m2 (add_match m1 rs), ti⟩ ⇒ t" by simp
        from base IH seq'_cons have "Γ,γ,p⊢ ⟨Rule (MatchAnd m2 (MatchAnd m1 m)) a # add_match m2 (add_match m1 rs), s⟩ ⇒ t" by fast
        thus ?case using r by(simp add: add_match_split_fst[symmetric])
      qed
  }
  thus ?thesis by blast
qed

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



lemma matches_add_match_simp:
  assumes m: "matches γ m p"
  shows "Γ,γ,p⊢ ⟨add_match m rs, s⟩ ⇒ t ⟷ Γ,γ,p⊢ ⟨rs, s⟩ ⇒ t" (is "?l ⟷ ?r")
  proof
    assume ?l with m show ?r
      proof (induction rs)
        case Nil
        thus ?case
          unfolding add_match_def by simp
      next
        case (Cons r rs)
        hence IH: "Γ,γ,p⊢ ⟨add_match m rs, s⟩ ⇒ t ⟹ Γ,γ,p⊢ ⟨rs, s⟩ ⇒ t" by(simp add: add_match_split_fst)
        obtain m' a where r: "r = Rule m' a" by (cases r)
        with Cons.prems(2) obtain ti where "Γ,γ,p⊢ ⟨[Rule (MatchAnd m m') a], s⟩ ⇒ ti" and "Γ,γ,p⊢ ⟨add_match m rs, ti⟩ ⇒ t"
          by(auto elim:seqE_cons simp add: add_match_split_fst)
        with Cons.prems(1) IH have "Γ,γ,p⊢ ⟨[Rule m' a], s⟩ ⇒ ti" by(simp add: matches_rule_and_simp)
        with ‹Γ,γ,p⊢ ⟨add_match m rs, ti⟩ ⇒ t› IH r show ?case by(metis decision state.exhaust iptables_bigstep_deterministic seq_cons)
      qed
  next
    assume ?r with m show ?l
      proof (induction rs)
        case Nil
        thus ?case
          unfolding add_match_def by simp
      next
        case (Cons r rs)
        hence IH: " Γ,γ,p⊢ ⟨rs, s⟩ ⇒ t ⟹ Γ,γ,p⊢ ⟨add_match m rs, s⟩ ⇒ t" by(simp add: add_match_split_fst)
        obtain m' a where r: "r = Rule m' a" by (cases r)
        with Cons.prems(2) obtain ti where "Γ,γ,p⊢ ⟨[Rule m' a], s⟩ ⇒ ti" and "Γ,γ,p⊢ ⟨rs, ti⟩ ⇒ t"
          by(auto elim:seqE_cons simp add: add_match_split_fst)
        with Cons.prems(1) IH have "Γ,γ,p⊢ ⟨[Rule (MatchAnd m m') a], s⟩ ⇒ ti" by(simp add: matches_rule_and_simp)
        with ‹Γ,γ,p⊢ ⟨rs, ti⟩ ⇒ t› IH r show ?case 
          apply(simp add: add_match_split_fst)
          by(metis decision state.exhaust iptables_bigstep_deterministic seq_cons)
      qed
  qed

lemma matches_add_match_MatchNot_simp:
  assumes m: "matches γ m p"
  shows "Γ,γ,p⊢ ⟨add_match (MatchNot m) rs, s⟩ ⇒ t ⟷ Γ,γ,p⊢ ⟨[], s⟩ ⇒ t" (is "?l s ⟷ ?r s")
  proof (cases s)
    case Undecided
    have "?l Undecided ⟷ ?r Undecided"
      proof
        assume "?l Undecided" with m show "?r Undecided"
          proof (induction rs)
            case Nil
            thus ?case
              unfolding add_match_def by simp
          next
            case (Cons r rs)
            thus ?case
              by (cases r) (metis matches_MatchNotAnd_simp skipD seqE_cons add_match_split_fst)
          qed
      next
        assume "?r Undecided" with m show "?l Undecided"
          proof (induction rs)
            case Nil
            thus ?case
              unfolding add_match_def by simp
          next
            case (Cons r rs)
            thus ?case
              by (cases r) (metis matches_MatchNotAnd_simp skipD seq'_cons add_match_split_fst)
          qed
      qed
    with Undecided show ?thesis by fast
  next
    case (Decision d)
    thus ?thesis
      by(metis decision decisionD)
  qed

lemma not_matches_add_match_simp:
  assumes "¬ matches γ m p"
  shows "Γ,γ,p⊢ ⟨add_match m rs, Undecided⟩ ⇒ t ⟷ Γ,γ,p⊢ ⟨[], Undecided⟩ ⇒ t"
  proof(induction rs)
    case Nil
    thus ?case
      unfolding add_match_def by simp
  next
    case (Cons r rs)
    thus ?case
      by (cases r) (metis assms add_match_split_fst matches.simps(1) nomatch seq'_cons nomatchD seqE_cons)
  qed

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


lemma add_match_match_not_cases:
  "Γ,γ,p⊢ ⟨add_match (MatchNot m) rs, Undecided⟩ ⇒ Undecided ⟹ matches γ m p ∨ Γ,γ,p⊢ ⟨rs, Undecided⟩ ⇒ Undecided"
  by (metis matches.simps(2) matches_add_match_simp)


lemma not_matches_add_matchNot_simp:
  "¬ matches γ m p ⟹ Γ,γ,p⊢ ⟨add_match (MatchNot m) rs, s⟩ ⇒ t ⟷ Γ,γ,p⊢ ⟨rs, s⟩ ⇒ t"
  by (simp add: matches_add_match_simp)

lemma iptables_bigstep_add_match_and:
  "Γ,γ,p⊢ ⟨add_match m1 (add_match m2 rs), s⟩ ⇒ t ⟷ Γ,γ,p⊢ ⟨add_match (MatchAnd m1 m2) rs, s⟩ ⇒ t"
  proof(induction rs arbitrary: s t)
    case Nil
    thus ?case
      unfolding add_match_def by simp
  next
    case(Cons r rs)
    show ?case
    proof (cases r, simp only: add_match_split_fst)
      fix m a
      show "Γ,γ,p⊢ ⟨Rule (MatchAnd m1 (MatchAnd m2 m)) a # add_match m1 (add_match m2 rs), s⟩ ⇒ t ⟷ Γ,γ,p⊢ ⟨Rule (MatchAnd (MatchAnd m1 m2) m) a # add_match (MatchAnd m1 m2) rs, s⟩ ⇒ t" (is "?l ⟷ ?r")
      proof
        assume ?l with Cons.IH show ?r
          apply -
          apply(erule seqE_cons)
          apply(case_tac s)
          apply(case_tac ti)
          apply (metis matches.simps(1) matches_rule_and_simp matches_rule_and_simp_help nomatch seq'_cons)
          apply (metis add_match_split_fst matches.simps(1) matches_add_match_simp not_matches_add_match_simp seq_cons)
          apply (metis decision decisionD)
          done
      next
        assume ?r with Cons.IH show ?l
          apply -
          apply(erule seqE_cons)
          apply(case_tac s)
          apply(case_tac ti)
          apply (metis matches.simps(1) matches_rule_and_simp matches_rule_and_simp_help nomatch seq'_cons)
          apply (metis add_match_split_fst matches.simps(1) matches_add_match_simp not_matches_add_match_simp seq_cons)
          apply (metis decision decisionD)
          done
        qed
    qed
  qed


lemma optimize_matches_option_generic:
  assumes "∀ r ∈ set rs. P (get_match r)"
      and "(⋀m m'. P m ⟹ f m = Some m' ⟹ matches γ m' p = matches γ m p)"
      and "(⋀m. P m ⟹ f m = None ⟹ ¬ matches γ m p)"
  shows "Γ,γ,p⊢ ⟨optimize_matches_option f rs, s⟩ ⇒ t ⟷ Γ,γ,p⊢ ⟨rs, s⟩ ⇒ t"
      (is "?lhs ⟷ ?rhs")
  proof
    assume ?rhs
    from this assms show ?lhs
    apply(induction rs s t rule: iptables_bigstep_induct)
    apply(auto simp: optimize_matches_option_append intro: iptables_bigstep.intros split: option.split)
    done
  next
    assume ?lhs
    from this assms show ?rhs
    apply(induction f rs arbitrary: s rule: optimize_matches_option.induct)
     apply(simp; fail)
    apply(simp split: option.split_asm)
     apply(subgoal_tac "¬ matches γ m p")
     prefer 2 apply blast
    apply (metis decision nomatch seq'_cons state.exhaust)
    apply(erule seqE_cons)
    apply(rule_tac t=ti in seq'_cons)
     apply (meson matches_rule_iptables_bigstep)
    by blast
  qed

lemma optimize_matches_generic: "∀ r ∈ set rs. P (get_match r) ⟹ 
      (⋀m. P m ⟹ matches γ (f m) p = matches γ m p) ⟹
      Γ,γ,p⊢ ⟨optimize_matches f rs, s⟩ ⇒ t ⟷ Γ,γ,p⊢ ⟨rs, s⟩ ⇒ t"
  unfolding optimize_matches_def
  apply(rule optimize_matches_option_generic)
    apply(simp; fail)
   apply(simp split: if_split_asm)
   apply blast
  apply(simp split: if_split_asm)
  using matcheq_matchNone_not_matches by fast
end