Theory SimpleFw_Semantics

theory SimpleFw_Semantics
imports SimpleFw_Syntax Prefix_Match
section‹Simple Firewall Semantics›
theory SimpleFw_Semantics
imports SimpleFw_Syntax
        IP_Addresses.IP_Address
        IP_Addresses.Prefix_Match
begin


  fun simple_match_ip :: "('i::len word × nat) ⇒ 'i::len word ⇒ bool" where
    "simple_match_ip (base, len) p_ip ⟷ p_ip ∈ ipset_from_cidr base len"

  lemma wordinterval_to_set_ipcidr_tuple_to_wordinterval_simple_match_ip_set:
    "wordinterval_to_set (ipcidr_tuple_to_wordinterval ip) = {d. simple_match_ip ip d}"
    proof -
      { fix s and d :: "'a::len word × nat"
        from wordinterval_to_set_ipcidr_tuple_to_wordinterval have
          "s ∈ wordinterval_to_set (ipcidr_tuple_to_wordinterval d) ⟷ simple_match_ip d s"
        by(cases d) auto
      } thus ?thesis by blast
    qed

  ― ‹by the way, the words do not wrap around›
  lemma "{(253::8 word) .. 8} = {}" by simp 

  fun simple_match_port :: "(16 word × 16 word) ⇒ 16 word ⇒ bool" where
    "simple_match_port (s,e) p_p ⟷ p_p ∈ {s..e}"

  fun simple_matches :: "'i::len simple_match ⇒ ('i, 'a) simple_packet_scheme ⇒ bool" where
    "simple_matches m p ⟷
      (match_iface (iiface m) (p_iiface p)) ∧
      (match_iface (oiface m) (p_oiface p)) ∧
      (simple_match_ip (src m) (p_src p)) ∧
      (simple_match_ip (dst m) (p_dst p)) ∧
      (match_proto (proto m) (p_proto p)) ∧
      (simple_match_port (sports m) (p_sport p)) ∧
      (simple_match_port (dports m) (p_dport p))"


  text‹The semantics of a simple firewall: just iterate over the rules sequentially›
  fun simple_fw :: "'i::len simple_rule list ⇒ ('i, 'a) simple_packet_scheme ⇒ state" where
    "simple_fw [] _ = Undecided" |
    "simple_fw ((SimpleRule m Accept)#rs) p = (if simple_matches m p then Decision FinalAllow else simple_fw rs p)" |
    "simple_fw ((SimpleRule m Drop)#rs) p = (if simple_matches m p then Decision FinalDeny else simple_fw rs p)"
 
  fun simple_fw_alt where
    "simple_fw_alt [] _ = Undecided" |
    "simple_fw_alt (r#rs) p = (if simple_matches (match_sel r) p then 
    	(case action_sel r of Accept ⇒ Decision FinalAllow | Drop ⇒ Decision FinalDeny) else simple_fw_alt rs p)"
 
  lemma simple_fw_alt: "simple_fw r p = simple_fw_alt r p" by(induction rule: simple_fw.induct) simp_all

  definition simple_match_any :: "'i::len simple_match" where
    "simple_match_any ≡ ⦇iiface=ifaceAny, oiface=ifaceAny, src=(0,0), dst=(0,0), proto=ProtoAny, sports=(0,65535), dports=(0,65535) ⦈"
  lemma simple_match_any: "simple_matches simple_match_any p"
    proof -
      have *: "(65535::16 word) = max_word"
        by simp
      show ?thesis
        by (simp add: simple_match_any_def ipset_from_cidr_0 match_ifaceAny *)
    qed

  text‹we specify only one empty port range›
  definition simple_match_none :: "'i::len simple_match" where
    "simple_match_none ≡
      ⦇iiface=ifaceAny, oiface=ifaceAny, src=(1,0), dst=(0,0),
       proto=ProtoAny, sports=(1,0), dports=(0,65535) ⦈"
  lemma simple_match_none: "¬ simple_matches simple_match_none p"
    proof -
      show ?thesis by(simp add: simple_match_none_def)
    qed

  fun empty_match :: "'i::len simple_match ⇒ bool" where
    "empty_match ⦇iiface=_, oiface=_, src=_, dst=_, proto=_,
                  sports=(sps1, sps2), dports=(dps1, dps2) ⦈ ⟷ (sps1 > sps2) ∨ (dps1 > dps2)"

  lemma empty_match: "empty_match m ⟷ (∀(p::('i::len, 'a) simple_packet_scheme). ¬ simple_matches m p)"
    proof
      assume "empty_match m"
      thus "∀p. ¬ simple_matches m p" by(cases m) fastforce
    next
      assume assm: "∀(p::('i::len, 'a) simple_packet_scheme). ¬ simple_matches m p"
      obtain iif oif sip dip protocol sps1 sps2 dps1 dps2 where m:
        "m = ⦇iiface = iif, oiface = oif, src = sip, dst = dip, proto = protocol, sports = (sps1, sps2), dports = (dps1, dps2)⦈"
          by(cases m) force

      show "empty_match m"
        proof(simp add: m)
          let ?x="λp. dps1 ≤ p_dport p ⟶ p_sport p ≤ sps2 ⟶ sps1 ≤ p_sport p ⟶ 
              match_proto protocol (p_proto p) ⟶ simple_match_ip dip (p_dst p) ⟶ simple_match_ip sip (p_src p) ⟶
              match_iface oif (p_oiface p) ⟶ match_iface iif (p_iiface p) ⟶ ¬ p_dport p ≤ dps2"
          from assm have nomatch: "∀(p::('i::len, 'a) simple_packet_scheme). ?x p" by(simp add: m)
          { fix ips::"'i::len word × nat"
            have "a ∈ ipset_from_cidr a n" for a::"'i::len word" and n
              using ipset_from_cidr_lowest by auto
            hence "simple_match_ip ips (fst ips)" by(cases ips) simp
          } note ips=this
          have proto: "match_proto protocol (case protocol of ProtoAny ⇒ TCP | Proto p ⇒ p)"
            by(simp split: protocol.split)
          { fix ifce
            have " match_iface ifce (iface_sel ifce)"
            by(cases ifce) (simp add: match_iface_refl)
          } note ifaces=this
          { fix p::"('i, 'a) simple_packet_scheme"
            from nomatch have "?x p" by blast
          } note pkt1=this
          obtain p::"('i, 'a) simple_packet_scheme" where [simp]:
			  "p_iiface p = iface_sel iif"
			  "p_oiface p = iface_sel oif"
			  "p_src p = fst sip"
			  "p_dst p = fst dip"
			  "p_proto p = (case protocol of ProtoAny ⇒ TCP | Proto p ⇒ p)"
			  "p_sport p = sps1"
			  "p_dport p = dps1"
			  by (meson simple_packet.select_convs)
          note pkt=pkt1[of p, simplified]
          from pkt ips proto ifaces have " sps1 ≤ sps2 ⟶ ¬ dps1 ≤ dps2" by blast
          thus "sps2 < sps1 ∨ dps2 < dps1" by fastforce
      qed
  qed
    

  lemma nomatch: "¬ simple_matches m p ⟹ simple_fw (SimpleRule m a # rs) p = simple_fw rs p"
    by(cases a, simp_all del: simple_matches.simps)

subsection‹Simple Ports›
  fun simpl_ports_conjunct :: "(16 word × 16 word) ⇒ (16 word × 16 word) ⇒ (16 word × 16 word)" where
    "simpl_ports_conjunct (p1s, p1e) (p2s, p2e) = (max p1s p2s, min p1e p2e)"

  lemma "{(p1s:: 16 word) .. p1e} ∩ {p2s .. p2e} = {max p1s p2s .. min p1e p2e}" by(simp)
  
  lemma simple_ports_conjunct_correct:
    "simple_match_port p1 pkt ∧ simple_match_port p2 pkt ⟷ simple_match_port (simpl_ports_conjunct p1 p2) pkt"
    apply(cases p1, cases p2, simp)
    by blast

  lemma simple_match_port_code[code] :"simple_match_port (s,e) p_p = (s ≤ p_p ∧ p_p ≤ e)" by simp

  lemma simple_match_port_UNIV: "{p. simple_match_port (s,e) p} = UNIV ⟷ (s = 0 ∧ e = max_word)"
    apply(simp)
    apply(rule)
     apply(case_tac "s = 0")
      using antisym_conv apply blast
     using word_le_0_iff apply blast
    using word_zero_le by blast

subsection‹Simple IPs›
  lemma simple_match_ip_conjunct:
    fixes ip1 :: "'i::len word × nat"
    shows "simple_match_ip ip1 p_ip ∧ simple_match_ip ip2 p_ip ⟷ 
            (case ipcidr_conjunct ip1 ip2 of None ⇒ False | Some ipx ⇒ simple_match_ip ipx p_ip)"
  proof -
  {
    fix b1 m1 b2 m2
    have "simple_match_ip (b1, m1) p_ip ∧ simple_match_ip (b2, m2) p_ip ⟷ 
          p_ip ∈ ipset_from_cidr b1 m1 ∩ ipset_from_cidr b2 m2"
    by simp
    also have "… ⟷ p_ip ∈ (case ipcidr_conjunct (b1, m1) (b2, m2) of None ⇒ {} | Some (bx, mx) ⇒ ipset_from_cidr bx mx)"
      using ipcidr_conjunct_correct by blast
    also have "… ⟷ (case ipcidr_conjunct (b1, m1) (b2, m2) of None ⇒ False | Some ipx ⇒ simple_match_ip ipx p_ip)"
      by(simp split: option.split)
    finally have "simple_match_ip (b1, m1) p_ip ∧ simple_match_ip (b2, m2) p_ip ⟷ 
         (case ipcidr_conjunct (b1, m1) (b2, m2) of None ⇒ False | Some ipx ⇒ simple_match_ip ipx p_ip)" .
   } thus ?thesis by(cases ip1, cases ip2, simp)
  qed

  declare simple_matches.simps[simp del]

subsection‹Merging Simple Matches›
  text‹@{typ "'i::len simple_match"} ‹∧› @{typ "'i::len simple_match"}›
  
  fun simple_match_and :: "'i::len simple_match ⇒ 'i simple_match ⇒ 'i simple_match option" where
    "simple_match_and ⦇iiface=iif1, oiface=oif1, src=sip1, dst=dip1, proto=p1, sports=sps1, dports=dps1 ⦈ 
                      ⦇iiface=iif2, oiface=oif2, src=sip2, dst=dip2, proto=p2, sports=sps2, dports=dps2 ⦈ = 
      (case ipcidr_conjunct sip1 sip2 of None ⇒ None | Some sip ⇒ 
      (case ipcidr_conjunct dip1 dip2 of None ⇒ None | Some dip ⇒ 
      (case iface_conjunct iif1 iif2 of None ⇒ None | Some iif ⇒
      (case iface_conjunct oif1 oif2 of None ⇒ None | Some oif ⇒
      (case simple_proto_conjunct p1 p2 of None ⇒ None | Some p ⇒
      Some ⦇iiface=iif, oiface=oif, src=sip, dst=dip, proto=p,
            sports=simpl_ports_conjunct sps1 sps2, dports=simpl_ports_conjunct dps1 dps2 ⦈)))))"
  
  lemma simple_match_and_correct: "simple_matches m1 p ∧ simple_matches m2 p ⟷ 
    (case simple_match_and m1 m2 of None ⇒ False | Some m ⇒ simple_matches m p)"
    proof -
      obtain iif1 oif1 sip1 dip1 p1 sps1 dps1 where m1:
        "m1 = ⦇iiface=iif1, oiface=oif1, src=sip1, dst=dip1, proto=p1, sports=sps1, dports=dps1 ⦈" by(cases m1, blast)
      obtain iif2 oif2 sip2 dip2 p2 sps2 dps2 where m2:
        "m2 = ⦇iiface=iif2, oiface=oif2, src=sip2, dst=dip2, proto=p2, sports=sps2, dports=dps2 ⦈" by(cases m2, blast)
  
      have sip_None: "ipcidr_conjunct sip1 sip2 = None ⟹ ¬ simple_match_ip sip1 (p_src p) ∨ ¬ simple_match_ip sip2 (p_src p)"
        using simple_match_ip_conjunct[of sip1 "p_src p" sip2] by simp
      have dip_None: "ipcidr_conjunct dip1 dip2 = None ⟹ ¬ simple_match_ip dip1 (p_dst p) ∨ ¬ simple_match_ip dip2 (p_dst p)"
        using simple_match_ip_conjunct[of dip1 "p_dst p" dip2] by simp
      have sip_Some: "⋀ip. ipcidr_conjunct sip1 sip2 = Some ip ⟹
        simple_match_ip ip (p_src p) ⟷ simple_match_ip sip1 (p_src p) ∧ simple_match_ip sip2 (p_src p)"
        using simple_match_ip_conjunct[of sip1 "p_src p" sip2] by simp
      have dip_Some: "⋀ip. ipcidr_conjunct dip1 dip2 = Some ip ⟹
        simple_match_ip ip (p_dst p) ⟷ simple_match_ip dip1 (p_dst p) ∧ simple_match_ip dip2 (p_dst p)"
        using simple_match_ip_conjunct[of dip1 "p_dst p" dip2] by simp
  
      have iiface_None: "iface_conjunct iif1 iif2 = None ⟹ ¬ match_iface iif1 (p_iiface p) ∨ ¬ match_iface iif2 (p_iiface p)"
        using iface_conjunct[of iif1 "(p_iiface p)" iif2] by simp
      have oiface_None: "iface_conjunct oif1 oif2 = None ⟹ ¬ match_iface oif1 (p_oiface p) ∨ ¬ match_iface oif2 (p_oiface p)"
        using iface_conjunct[of oif1 "(p_oiface p)" oif2] by simp
      have iiface_Some: "⋀iface. iface_conjunct iif1 iif2 = Some iface ⟹ 
        match_iface iface (p_iiface p) ⟷ match_iface iif1 (p_iiface p) ∧ match_iface iif2 (p_iiface p)"
        using iface_conjunct[of iif1 "(p_iiface p)" iif2] by simp
      have oiface_Some: "⋀iface. iface_conjunct oif1 oif2 = Some iface ⟹ 
        match_iface iface (p_oiface p) ⟷ match_iface oif1 (p_oiface p) ∧ match_iface oif2 (p_oiface p)"
        using iface_conjunct[of oif1 "(p_oiface p)" oif2] by simp
  
      have proto_None: "simple_proto_conjunct p1 p2 = None ⟹ ¬ match_proto p1 (p_proto p) ∨ ¬ match_proto p2 (p_proto p)"
        using simple_proto_conjunct_correct[of p1 "(p_proto p)" p2] by simp
      have proto_Some: "⋀proto. simple_proto_conjunct p1 p2 = Some proto ⟹
        match_proto proto (p_proto p) ⟷ match_proto p1 (p_proto p) ∧ match_proto p2 (p_proto p)"
        using simple_proto_conjunct_correct[of p1 "(p_proto p)" p2] by simp
  
      have case_Some: "⋀m. Some m = simple_match_and m1 m2 ⟹
       (simple_matches m1 p ∧ simple_matches m2 p) ⟷ simple_matches m p"
       apply(simp add: m1 m2 simple_matches.simps split: option.split_asm)
       using simple_ports_conjunct_correct by(blast dest: sip_Some dip_Some iiface_Some oiface_Some proto_Some)
      have case_None: "simple_match_and m1 m2 = None ⟹ ¬ (simple_matches m1 p ∧ simple_matches m2 p)"
       apply(simp add: m1 m2 simple_matches.simps split: option.split_asm)
           apply(blast dest: sip_None dip_None iiface_None oiface_None proto_None)+
       done
      from case_Some case_None show ?thesis by(cases "simple_match_and m1 m2") simp_all
   qed
  
  lemma simple_match_and_SomeD: "simple_match_and m1 m2 = Some m ⟹
    simple_matches m p ⟷ (simple_matches m1 p ∧ simple_matches m2 p)"
    by(simp add: simple_match_and_correct)
  lemma simple_match_and_NoneD: "simple_match_and m1 m2 = None ⟹
    ¬(simple_matches m1 p ∧ simple_matches m2 p)"
    by(simp add: simple_match_and_correct)
  lemma simple_matches_andD: "simple_matches m1 p ⟹ simple_matches m2 p ⟹
    ∃m. simple_match_and m1 m2 = Some m ∧ simple_matches m p"
    by (meson option.exhaust_sel simple_match_and_NoneD simple_match_and_SomeD)

subsection‹Further Properties of a Simple Firewall›
  fun has_default_policy :: "'i::len simple_rule list ⇒ bool" where
    "has_default_policy [] = False" |
    "has_default_policy [(SimpleRule m _)] = (m = simple_match_any)" |
    "has_default_policy (_#rs) = has_default_policy rs"
  
  lemma has_default_policy: "has_default_policy rs ⟹
    simple_fw rs p = Decision FinalAllow ∨ simple_fw rs p = Decision FinalDeny"
    proof(induction rs rule: has_default_policy.induct)
    case 1 thus ?case by (simp)
    next
    case (2 m a) thus ?case by(cases a) (simp_all add: simple_match_any)
    next
    case (3 r1 r2 rs)
      from 3 obtain a m where "r1 = SimpleRule m a" by (cases r1) simp
      with 3 show ?case by (cases a) simp_all
    qed
  
  lemma has_default_policy_fst: "has_default_policy rs ⟹ has_default_policy (r#rs)"
   apply(cases r, rename_tac m a, simp)
   apply(cases rs)
    by(simp_all)


  text‹We can stop after a default rule (a rule which matches anything) is observed.›
  fun cut_off_after_match_any :: "'i::len simple_rule list ⇒ 'i simple_rule list" where
    "cut_off_after_match_any [] = []" |
    "cut_off_after_match_any (SimpleRule m a # rs) =
      (if m = simple_match_any then [SimpleRule m a] else SimpleRule m a # cut_off_after_match_any rs)"
  
  lemma cut_off_after_match_any: "simple_fw (cut_off_after_match_any rs) p = simple_fw rs p"
    apply(induction rs p rule: simple_fw.induct)
      by(simp add: simple_match_any)+
  
  lemma simple_fw_not_matches_removeAll: "¬ simple_matches m p ⟹
    simple_fw (removeAll (SimpleRule m a) rs) p = simple_fw rs p"
    apply(induction rs p rule: simple_fw.induct)
      apply(simp)
     apply(simp_all)
     apply blast+
    done


subsection‹Reality check: Validity of Simple Matches›
  text‹While it is possible to construct a ‹simple_fw› expression that only matches a source
  or destination port, such a match is not meaningful, as the presence of the port information is 
  dependent on the protocol. Thus, a match for a port should always include the match for a protocol.
  Additionally, prefixes should be zero on bits beyond the prefix length.
  ›
  
  definition "valid_prefix_fw m = valid_prefix (uncurry PrefixMatch m)"
  
  lemma ipcidr_conjunct_valid:
    "⟦valid_prefix_fw p1; valid_prefix_fw p2; ipcidr_conjunct p1 p2 = Some p⟧ ⟹ valid_prefix_fw p"
    unfolding valid_prefix_fw_def
    by(cases p; cases p1; cases p2) (simp add: ipcidr_conjunct.simps split: if_splits)
  
  definition simple_match_valid :: "('i::len, 'a) simple_match_scheme ⇒ bool" where
    "simple_match_valid m ≡ 
    ({p. simple_match_port (sports m) p} ≠ UNIV ∨ {p. simple_match_port (dports m) p} ≠ UNIV ⟶
        proto m ∈ Proto `{TCP, UDP, L4_Protocol.SCTP}) ∧
    valid_prefix_fw (src m) ∧ valid_prefix_fw (dst m)" 
  
  lemma simple_match_valid_alt[code_unfold]: "simple_match_valid = (λ m.
    (let c = (λ(s,e). (s ≠ 0 ∨ e ≠ max_word)) in (
    if c (sports m) ∨ c (dports m) then proto m = Proto TCP ∨ proto m = Proto UDP ∨ proto m = Proto L4_Protocol.SCTP else True)) ∧
  valid_prefix_fw (src m) ∧ valid_prefix_fw (dst m))" 
  proof -
    have simple_match_valid_alt_hlp1: "{p. simple_match_port x p} ≠ UNIV ⟷ (case x of (s,e) ⇒ s ≠ 0 ∨ e ≠ max_word)"
      for x using simple_match_port_UNIV by auto
    have simple_match_valid_alt_hlp2: "{p. simple_match_port x p} ≠ {} ⟷ (case x of (s,e) ⇒ s ≤ e)" for x by auto
    show ?thesis
      unfolding fun_eq_iff
      unfolding simple_match_valid_def Let_def
      unfolding simple_match_valid_alt_hlp1 simple_match_valid_alt_hlp2
      apply(clarify, rename_tac m, case_tac "sports m"; case_tac "dports m"; case_tac "proto m")
       by auto
  qed
  
  text‹Example:›
  context
  begin
    private definition "example_simple_match1 ≡
      ⦇iiface = Iface ''+'', oiface = Iface ''+'', src = (0::32 word, 0), dst = (0, 0),
       proto = Proto TCP, sports = (0, 1024), dports = (0, 1024)⦈"
  
    lemma "simple_fw [SimpleRule example_simple_match1 Drop]
      ⦇p_iiface = '''', p_oiface = '''',  p_src = (1::32 word), p_dst = 2, p_proto = TCP, p_sport = 8,
       p_dport = 9, p_tcp_flags = {}, p_payload = ''''⦈ =
        Decision FinalDeny" by eval
  
    private definition "example_simple_match2 ≡ example_simple_match1⦇ proto := ProtoAny ⦈"
    text‹Thus, ‹example_simple_match1› is valid, but if we set its protocol match to any, it isn't anymore›
    private lemma "simple_match_valid example_simple_match1" by eval
    private lemma "¬ simple_match_valid example_simple_match2" by eval
  end
  
  
  lemma simple_match_and_valid: 
    fixes m1 :: "'i::len simple_match"
    assumes mv: "simple_match_valid m1" "simple_match_valid m2"
    assumes mj: "simple_match_and m1 m2 = Some m"
    shows "simple_match_valid m"
  proof -
    have simpl_ports_conjunct_not_UNIV:
    "Collect (simple_match_port x) ≠ UNIV ⟹
      x = simpl_ports_conjunct p1 p2 ⟹
      Collect (simple_match_port p1) ≠ UNIV ∨ Collect (simple_match_port p2) ≠ UNIV" 
    for x p1 p2 by (metis Collect_cong mem_Collect_eq simple_ports_conjunct_correct)
  
    (* prefix validity. That's simple. *)
    have "valid_prefix_fw (src m1)" "valid_prefix_fw (src m2)" "valid_prefix_fw (dst m1)" "valid_prefix_fw (dst m2)"
      using mv unfolding simple_match_valid_alt by simp_all
    moreover have "ipcidr_conjunct (src m1) (src m2) = Some (src m)"
                  "ipcidr_conjunct (dst m1) (dst m2) = Some (dst m)"
      using mj by(cases m1; cases m2; cases m; simp split: option.splits)+
    ultimately have pv: "valid_prefix_fw (src m)" "valid_prefix_fw (dst m)"
      using ipcidr_conjunct_valid by blast+
  
    (* now for the source ports… *)
    define nmu where "nmu ps ⟷ {p. simple_match_port ps p} ≠ UNIV" for ps
    have "simpl_ports_conjunct (sports m1) (sports m2) = (sports m)" (is "?ph1 sports")
      using mj by(cases m1; cases m2; cases m; simp split: option.splits)
    hence sp: "nmu (sports m) ⟶ nmu (sports m1) ∨ nmu (sports m2)"
      (is "?ph2 sports")
      unfolding nmu_def using simpl_ports_conjunct_not_UNIV by metis
  
    (* dst ports: mutatis mutandem *)
    have "?ph1 dports" using mj by(cases m1; cases m2; cases m; simp split: option.splits)
    hence dp: "?ph2 dports" unfolding nmu_def using simpl_ports_conjunct_not_UNIV by metis
  
    (* And an argument for the protocol. *)
    define php where "php mr ⟷ proto mr ∈ Proto ` {TCP, UDP, L4_Protocol.SCTP}"
      for mr :: "'i simple_match"
    have pcj: "simple_proto_conjunct (proto m1) (proto m2) = Some (proto m)"
      using mj by(cases m1; cases m2; cases m; simp split: option.splits)
    hence p: "php m1 ⟹ php m"
             "php m2 ⟹ php m"
      using conjunctProtoD conjunctProtoD2 pcj unfolding php_def by auto
  
    (* Since I'm trying to trick the simplifier with these defs, I need these as explicit statements: *)
    have "⋀mx. simple_match_valid mx ⟹ nmu (sports mx) ∨ nmu (dports mx) ⟹ php mx"
      unfolding nmu_def php_def simple_match_valid_def by blast
    hence mps: "nmu (sports m1) ⟹ php m1" "nmu (dports m1) ⟹ php m1"
               "nmu (sports m2) ⟹ php m2" "nmu (dports m2) ⟹ php m2" using mv by blast+
    
    have pa: "nmu (sports m) ∨ nmu (dports m) ⟶ php m"
    (*  apply(intro impI)
      apply(elim disjE)
      apply(drule sp[THEN mp])
      apply(elim disjE)
      apply(drule mps)
      apply(elim p; fail) *)
      using sp dp mps p by fast
  
    show ?thesis
      unfolding simple_match_valid_def
      using pv pa[unfolded nmu_def php_def] by blast
  qed
      
  
  definition "simple_fw_valid ≡ list_all (simple_match_valid ∘ match_sel)"



text‹The simple firewall does not care about tcp flags, payload, or any other packet extensions.›
lemma simple_matches_extended_packet:
      "simple_matches m
        ⦇p_iiface = iifce,
         oiface = oifce,
         p_src = s, dst = d,
         p_proto = prot,
         p_sport = sport, p_dport = dport,
         tcp_flags = tcp_flags, p_payload = payload1⦈
        ⟷
       simple_matches m
        ⦇p_iiface = iifce,
         oiface = oifce,
         p_src = s, p_dst = d,
         p_proto = prot,
         p_sport = sport, p_dport = dport,
         p_tcp_flags = tcp_flags2, p_payload = payload2, … = aux⦈
        "
  by(simp add: simple_matches.simps)
end