Session Simple_Firewall

Theory Lib_Enum_toString

section‹Enum toString Functions›
theory Lib_Enum_toString
imports Main IP_Addresses.Lib_List_toString
begin

fun bool_toString :: "bool  string" where
  "bool_toString True = ''True''" |
  "bool_toString False = ''False''"

subsection‹Enum set to string›
  fun enum_set_get_one :: "'a list  'a set  'a option" where
    "enum_set_get_one []     S = None" |
    "enum_set_get_one (s#ss) S = (if s  S then Some s else enum_set_get_one ss S)"

  lemma enum_set_get_one_empty: "enum_set_get_one ss {} = None"
    by(induction ss) simp_all
  
  lemma enum_set_get_one_None: "S  set ss  enum_set_get_one ss S = None  S = {}"
    apply(induction ss)
     apply(simp; fail)
    apply(simp)
    apply(intro conjI)
     apply blast
    by fast
 
  lemma enum_set_get_one_Some: "S  set ss  enum_set_get_one ss S = Some x  x  S"
    apply(induction ss)
     apply(simp; fail)
    apply(simp split: if_split_asm)
    apply(blast)
    done
  corollary enum_set_get_one_enum_Some: "enum_set_get_one enum_class.enum S = Some x  x  S"
    using enum_set_get_one_Some[where ss=enum_class.enum, simplified enum_UNIV] by auto

  lemma enum_set_get_one_Ex_Some: "S  set ss  S  {}  x. enum_set_get_one ss S = Some x"
    apply(induction ss)
     apply(simp; fail)
    apply(simp split: if_split_asm)
    apply(blast)
    done
  corollary enum_set_get_one_enum_Ex_Some:
    "S  {}  x. enum_set_get_one enum_class.enum S = Some x"
    using enum_set_get_one_Ex_Some[where ss=enum_class.enum, simplified enum_UNIV] by auto
  
  function enum_set_to_list :: "('a::enum) set  'a list" where
    "enum_set_to_list S = (if S = {} then [] else
      case enum_set_get_one Enum.enum S of None  []
                                        |  Some a  a#enum_set_to_list (S - {a}))"
  by(pat_completeness) auto
  
  termination enum_set_to_list
    apply(relation "measure (λ(S). card S)")
     apply(simp_all add: card_gt_0_iff)
    apply(drule enum_set_get_one_enum_Some)
    apply(subgoal_tac "finite S")
     prefer 2
     apply force
    apply (meson card_Diff1_less)
    done

  (*this definition is simpler*)
  lemma enum_set_to_list_simps: "enum_set_to_list S =
      (case enum_set_get_one (Enum.enum) S of None  []
                                           |  Some a  a#enum_set_to_list (S - {a}))"
   by(simp add: enum_set_get_one_empty)
  declare enum_set_to_list.simps[simp del]

  lemma enum_set_to_list: "set (enum_set_to_list A) = A"
    apply(induction A rule: enum_set_to_list.induct)
    apply(case_tac "S = {}")
     apply(simp add: enum_set_to_list.simps; fail)
    apply(simp)
    apply(subst enum_set_to_list_simps)
    apply(simp)
    apply(drule enum_set_get_one_enum_Ex_Some)
    apply(clarify)
    apply(simp)
    apply(drule enum_set_get_one_enum_Some)
    by blast
  
lemma "list_toString bool_toString (enum_set_to_list {True, False}) = ''[False, True]''" by eval

end

Theory L4_Protocol

theory L4_Protocol
imports "../Common/Lib_Enum_toString" "HOL-Library.Word"
begin

section‹Transport Layer Protocols›
type_synonym primitive_protocol = "8 word"

definition "ICMP  1 :: 8 word"
definition "TCP  6 :: 8 word"
definition "UDP  17 :: 8 word"
context begin (*let's not pollute the namespace too much*)
qualified definition "SCTP  132  :: 8 word"
qualified definition "IGMP  2 :: 8 word"
qualified definition "GRE  47 :: 8 word"
qualified definition "ESP  50 :: 8 word"
qualified definition "AH  51 :: 8 word"
qualified definition "IPv6ICMP  58 :: 8 word"
end
(* turn http://www.iana.org/assignments/protocol-numbers/protocol-numbers.xhtml into a separate file or so? *)

datatype protocol = ProtoAny | Proto "primitive_protocol"

fun match_proto :: "protocol  primitive_protocol  bool" where
  "match_proto ProtoAny _  True" |
  "match_proto (Proto (p)) p_p  p_p = p"

  fun simple_proto_conjunct :: "protocol  protocol  protocol option" where
    "simple_proto_conjunct ProtoAny proto = Some proto" |
    "simple_proto_conjunct proto ProtoAny = Some proto" |
    "simple_proto_conjunct (Proto p1) (Proto p2) = (if p1 = p2 then Some (Proto p1) else None)"
  lemma simple_proto_conjunct_asimp[simp]: "simple_proto_conjunct proto ProtoAny = Some proto"
    by(cases proto) simp_all

  lemma simple_proto_conjunct_correct: "match_proto p1 pkt  match_proto p2 pkt  
    (case simple_proto_conjunct p1 p2 of None  False | Some proto  match_proto proto pkt)"
    apply(cases p1)
     apply(simp_all)
    apply(cases p2)
     apply(simp_all)
    done

  lemma simple_proto_conjunct_Some: "simple_proto_conjunct p1 p2 = Some proto  
    match_proto proto pkt  match_proto p1 pkt  match_proto p2 pkt"
    using simple_proto_conjunct_correct by simp
  lemma simple_proto_conjunct_None: "simple_proto_conjunct p1 p2 = None  
    ¬ (match_proto p1 pkt  match_proto p2 pkt)"
    using simple_proto_conjunct_correct by simp

  lemma conjunctProtoD:
    "simple_proto_conjunct a (Proto b) = Some x  x = Proto b  (a = ProtoAny  a = Proto b)"
  by(cases a) (simp_all split: if_splits)
  lemma conjunctProtoD2:
    "simple_proto_conjunct (Proto b) a = Some x  x = Proto b  (a = ProtoAny  a = Proto b)"
  by(cases a) (simp_all split: if_splits)

  text‹Originally, there was a @{typ nat} in the protocol definition, allowing infinitely many protocols 
        This was intended behavior. We want to prevent things such as @{term "¬TCP = UDP"}.
        So be careful with what you prove...›
  lemma primitive_protocol_Ex_neq: "p = Proto pi  p'. p'  pi" for pi
  proof
  	show "pi + 1  pi" by simp
  qed
  lemma protocol_Ex_neq: "p'. Proto p'  p"
    by(cases p) (simp_all add: primitive_protocol_Ex_neq)

section‹TCP flags›
  datatype tcp_flag = TCP_SYN | TCP_ACK | TCP_FIN | TCP_RST | TCP_URG | TCP_PSH (*| TCP_ALL | TCP_NONE*)

  lemma UNIV_tcp_flag: "UNIV = {TCP_SYN, TCP_ACK, TCP_FIN, TCP_RST, TCP_URG, TCP_PSH}" using tcp_flag.exhaust by auto 
  instance tcp_flag :: finite
  proof
    from UNIV_tcp_flag show "finite (UNIV:: tcp_flag set)" using finite.simps by auto 
  qed
  instantiation "tcp_flag" :: enum
  begin
    definition "enum_tcp_flag = [TCP_SYN, TCP_ACK, TCP_FIN, TCP_RST, TCP_URG, TCP_PSH]"
  
    definition "enum_all_tcp_flag P  P TCP_SYN  P TCP_ACK  P TCP_FIN  P TCP_RST  P TCP_URG  P TCP_PSH"
    
    definition "enum_ex_tcp_flag P  P TCP_SYN  P TCP_ACK  P TCP_FIN  P TCP_RST  P TCP_URG  P TCP_PSH"
  instance proof
    show "UNIV = set (enum_class.enum :: tcp_flag list)"
      by(simp add: UNIV_tcp_flag enum_tcp_flag_def)
    next
    show "distinct (enum_class.enum :: tcp_flag list)"
      by(simp add: enum_tcp_flag_def)
    next
    show "P. (enum_class.enum_all :: (tcp_flag  bool)  bool) P = Ball UNIV P"
      by(simp add: UNIV_tcp_flag enum_all_tcp_flag_def)
    next
    show "P. (enum_class.enum_ex :: (tcp_flag  bool)  bool) P = Bex UNIV P"
      by(simp add: UNIV_tcp_flag enum_ex_tcp_flag_def)
  qed
  end

subsection‹TCP Flags to String›
  fun tcp_flag_toString :: "tcp_flag  string" where
    "tcp_flag_toString TCP_SYN = ''TCP_SYN''" |
    "tcp_flag_toString TCP_ACK = ''TCP_ACK''" |
    "tcp_flag_toString TCP_FIN = ''TCP_FIN''" |
    "tcp_flag_toString TCP_RST = ''TCP_RST''" |
    "tcp_flag_toString TCP_URG = ''TCP_URG''" |
    "tcp_flag_toString TCP_PSH = ''TCP_PSH''"


  definition ipt_tcp_flags_toString :: "tcp_flag set  char list" where
    "ipt_tcp_flags_toString flags  list_toString tcp_flag_toString (enum_set_to_list flags)"

  lemma "ipt_tcp_flags_toString {TCP_SYN,TCP_SYN,TCP_ACK} = ''[TCP_SYN, TCP_ACK]''" by eval


end

Theory Simple_Packet

section‹Simple Packet›
theory Simple_Packet
imports "Primitives/L4_Protocol"
begin

  text‹Packet constants are prefixed with p›

  text@{typ "'i::len word"} is an IP address of variable length. 32bit for IPv4, 128bit for IPv6›

  text‹A simple packet with IP addresses and layer four ports.
             Also has the following phantom fields:
             Input and Output network interfaces›

  record (overloaded) 'i simple_packet = p_iiface :: string
                         p_oiface :: string
                         p_src :: "'i::len word"
                         p_dst :: "'i::len word"
                         p_proto :: primitive_protocol
                         p_sport :: "16 word"
                         p_dport :: "16 word"
                         p_tcp_flags :: "tcp_flag set"
                         p_payload :: string


  value [nbe] " 
          p_iiface = ''eth1'', p_oiface = '''', 
          p_src = 0, p_dst = 0, 
          p_proto = TCP, p_sport = 0, p_dport = 0, 
          p_tcp_flags = {TCP_SYN},
          p_payload = ''arbitrary payload''
         "

  text‹We suggest to use @{typ "('i,'pkt_ext) simple_packet_scheme"} instead of 
        @{typ "'i simple_packet"} because of its extensibility which naturally 
        models any payload›

  
  definition simple_packet_unext :: "('i::len, 'a) simple_packet_scheme  'i simple_packet" where
    "simple_packet_unext p 
      p_iiface = p_iiface p, p_oiface = p_oiface p, p_src = p_src p, p_dst = p_dst p, p_proto = p_proto p, 
       p_sport = p_sport p, p_dport = p_dport p, p_tcp_flags = p_tcp_flags p, 
       p_payload = p_payload p"

  text‹An extended simple packet with MAC addresses and VLAN header›
  
  record (overloaded) 'i simple_packet_ext = "'i::len simple_packet" +
    p_l2type :: "16 word"
    p_l2src :: "48 word"
    p_l2dst :: "48 word"
    p_vlanid :: "16 word"
    p_vlanprio :: "16 word"

end

Theory Firewall_Common_Decision_State

section‹The state of a firewall, abstracted only to the packet filtering outcome›
theory Firewall_Common_Decision_State
imports Main
begin

datatype final_decision = FinalAllow | FinalDeny

text‹
The state during packet processing. If undecided, there are some remaining rules to process. If
decided, there is an action which applies to the packet
›
datatype state = Undecided | Decision final_decision

end

Theory Iface

section‹Network Interfaces›
theory Iface
imports "HOL-Library.Char_ord" (*WARNING: importing char ord*)
begin

text‹Network interfaces, e.g. \texttt{eth0}, \texttt{wlan1}, ...

iptables supports wildcard matching, e.g. \texttt{eth+} will match \texttt{eth}, \texttt{eth1}, \texttt{ethFOO}, ...
The character `+' is only a wildcard if it appears at the end.
›

datatype iface = Iface (iface_sel: "string")  ― ‹no negation supported, but wildcards›


text‹Just a normal lexicographical ordering on the interface strings. Used only for optimizing code.
     WARNING: not a semantic ordering.›
(*We cannot use List_lexord because it clashed with the Word_Lib imported ordering!*)
instantiation iface :: linorder
begin
  function (sequential) less_eq_iface :: "iface  iface  bool" where
    "(Iface [])  (Iface _)  True" |
    "(Iface _)  (Iface [])  False" |
    "(Iface (a#as))  (Iface (b#bs))  (if a = b then Iface as  Iface bs else a  b)"
   by(pat_completeness) auto
  termination "less_eq :: iface  _  bool"
    apply(relation "measure (λis. size (iface_sel (fst is)) + size (iface_sel (snd is)))")
    apply(rule wf_measure, unfold in_measure comp_def)
    apply(simp)
    done
  
  lemma Iface_less_eq_empty: "Iface x  Iface []  x = []"
    by(induction "Iface x" "Iface []" rule: less_eq_iface.induct) auto
  lemma less_eq_empty: "Iface []  q"
    by(induction "Iface []" q rule: less_eq_iface.induct) auto
  lemma iface_cons_less_eq_i:
    "Iface (b # bs)  i   q qs. i=Iface (q#qs)  (b < q  (Iface bs)  (Iface qs))"
    apply(induction "Iface (b # bs)" i rule: less_eq_iface.induct)
     apply(simp_all split: if_split_asm)
    apply(clarify)
    apply(simp)
    done

  function (sequential) less_iface :: "iface  iface  bool" where
    "(Iface []) < (Iface [])  False" |
    "(Iface []) < (Iface _)  True" |
    "(Iface _) < (Iface [])  False" |
    "(Iface (a#as)) < (Iface (b#bs))  (if a = b then Iface as < Iface bs else a < b)"
   by(pat_completeness) auto
  termination "less :: iface  _  bool"
    apply(relation "measure (λis. size (iface_sel (fst is)) + size (iface_sel (snd is)))")
    apply(rule wf_measure, unfold in_measure comp_def)
    apply(simp)
    done
instance
  proof
    fix n m :: iface
    show "n < m  n  m  ¬ m  n"
      proof(induction rule: less_iface.induct)
      case 4 thus ?case by simp fastforce
      qed(simp+)
  next
    fix n :: iface have "n = m  n  m" for m
      by(induction n m rule: less_eq_iface.induct) simp+
    thus "n  n" by simp
  next
    fix n m :: iface
    show "n  m  m  n  n = m"
      proof(induction n m rule: less_eq_iface.induct)
      case 1 thus ?case using Iface_less_eq_empty by blast
      next
      case 3 thus ?case by (simp split: if_split_asm)
      qed(simp)+
  next
    fix n m q :: iface show "n  m  m  q  n  q" 
      proof(induction n q arbitrary: m rule: less_eq_iface.induct)
      case 1 thus ?case by simp
      next
      case 2 thus ?case
        apply simp
        apply(drule iface_cons_less_eq_i)
        apply(elim exE conjE disjE)
         apply(simp; fail)
        by fastforce
      next
      case 3 thus ?case
        apply simp
        apply(frule iface_cons_less_eq_i)
         by(auto split: if_split_asm)
      qed
  next
    fix n m :: iface show "n  m  m  n"
      apply(induction n m rule: less_eq_iface.induct)
        apply(simp_all)
      by fastforce
  qed
end

definition ifaceAny :: iface where
  "ifaceAny  Iface ''+''"
(* there is no IfaceFalse, proof below *)

text‹If the interface name ends in a ``+'', then any interface which begins with this name will match.
  (man iptables)

Here is how iptables handles this wildcard on my system.
A packet for the loopback interface \texttt{lo} is matched by the following expressions
   lo
   lo+
   l+
   +

It is not matched by the following expressions
   lo++
   lo+++
   lo1+
   lo1

By the way: \texttt{Warning: weird characters in interface ` ' ('/' and ' ' are not allowed by the kernel).}
However, happy snowman and shell colors are fine.
›


context
begin
  subsection‹Helpers for the interface name (@{typ string})›
    (*Do not use outside this thy! Type is really misleading.*)
    text‹
      argument 1: interface as in firewall rule - Wildcard support
      argument 2: interface a packet came from - No wildcard support›
    fun internal_iface_name_match :: "string  string  bool" where
      "internal_iface_name_match []     []          True" |
      "internal_iface_name_match (i#is) []          (i = CHR ''+''  is = [])" |
      "internal_iface_name_match []     (_#_)       False" |
      "internal_iface_name_match (i#is) (p_i#p_is)  (if (i = CHR ''+''  is = []) then True else (
            (p_i = i)  internal_iface_name_match is p_is
      ))"
    
    (*<*)
    ― ‹Examples›
      lemma "internal_iface_name_match ''lo'' ''lo''" by eval
      lemma "internal_iface_name_match ''lo+'' ''lo''" by eval
      lemma "internal_iface_name_match ''l+'' ''lo''" by eval
      lemma "internal_iface_name_match ''+'' ''lo''" by eval
      lemma "¬ internal_iface_name_match ''lo++'' ''lo''" by eval
      lemma "¬ internal_iface_name_match ''lo+++'' ''lo''" by eval
      lemma "¬ internal_iface_name_match ''lo1+'' ''lo''" by eval
      lemma "¬ internal_iface_name_match ''lo1'' ''lo''" by eval
      text‹The wildcard interface name›
      lemma "internal_iface_name_match ''+'' ''''" by eval (*>*)
  
  
    fun iface_name_is_wildcard :: "string  bool" where
      "iface_name_is_wildcard []  False" |
      "iface_name_is_wildcard [s]  s = CHR ''+''" |
      "iface_name_is_wildcard (_#ss)  iface_name_is_wildcard ss"
    private lemma iface_name_is_wildcard_alt: "iface_name_is_wildcard eth  eth  []  last eth = CHR ''+''"
      proof(induction eth rule: iface_name_is_wildcard.induct)
      qed(simp_all)
    private lemma iface_name_is_wildcard_alt': "iface_name_is_wildcard eth  eth  []  hd (rev eth) = CHR ''+''"
      unfolding iface_name_is_wildcard_alt by (simp add: hd_rev)
    private lemma iface_name_is_wildcard_fst: "iface_name_is_wildcard (i # is)  is  []  iface_name_is_wildcard is"
      by(simp add: iface_name_is_wildcard_alt)
  
    private fun internal_iface_name_to_set :: "string  string set" where
      "internal_iface_name_to_set i = (if ¬ iface_name_is_wildcard i
        then
          {i}
        else
          {(butlast i)@cs | cs. True})"
    private lemma "{(butlast i)@cs | cs. True} = (λs. (butlast i)@s) ` (UNIV::string set)" by fastforce
    private lemma internal_iface_name_to_set: "internal_iface_name_match i p_iface  p_iface  internal_iface_name_to_set i"
      proof(induction i p_iface rule: internal_iface_name_match.induct)
      case 4 thus ?case
        apply(simp)
        apply(safe)
               apply(simp_all add: iface_name_is_wildcard_fst)
         apply (metis (full_types) iface_name_is_wildcard.simps(3) list.exhaust)
        by (metis append_butlast_last_id)
      qed(simp_all)
    private lemma internal_iface_name_to_set2: "internal_iface_name_to_set ifce = {i. internal_iface_name_match ifce i}"
      by (simp add: internal_iface_name_to_set)
      
  
    private lemma internal_iface_name_match_refl: "internal_iface_name_match i i"
     proof -
     { fix i j
       have "i=j  internal_iface_name_match i j"
         by(induction i j rule: internal_iface_name_match.induct)(simp_all)
     } thus ?thesis by simp
     qed
  
  subsection‹Matching›
    fun match_iface :: "iface  string  bool" where
      "match_iface (Iface i) p_iface  internal_iface_name_match i p_iface"
    
    ― ‹Examples›
      lemma "  match_iface (Iface ''lo'')    ''lo''"
            "  match_iface (Iface ''lo+'')   ''lo''"
            "  match_iface (Iface ''l+'')    ''lo''"
            "  match_iface (Iface ''+'')     ''lo''"
            "¬ match_iface (Iface ''lo++'')  ''lo''"
            "¬ match_iface (Iface ''lo+++'') ''lo''"
            "¬ match_iface (Iface ''lo1+'')  ''lo''"
            "¬ match_iface (Iface ''lo1'')   ''lo''"
            "  match_iface (Iface ''+'')     ''eth0''"
            "  match_iface (Iface ''+'')     ''eth0''"
            "  match_iface (Iface ''eth+'')  ''eth0''"
            "¬ match_iface (Iface ''lo+'')   ''eth0''"
            "  match_iface (Iface ''lo+'')   ''loX''"
            "¬ match_iface (Iface '''')      ''loX''"
            (*<*)by eval+(*>*)
  
    lemma match_ifaceAny: "match_iface ifaceAny i"
      by(cases i, simp_all add: ifaceAny_def)
    lemma match_IfaceFalse: "¬( IfaceFalse. (i. ¬ match_iface IfaceFalse i))"
      apply(simp)
      apply(intro allI, rename_tac IfaceFalse)
      apply(case_tac IfaceFalse, rename_tac name)
      apply(rule_tac x="name" in exI)
      by(simp add: internal_iface_name_match_refl)
      

    ― ‹@{const match_iface} explained by the individual cases›
    lemma match_iface_case_nowildcard: "¬ iface_name_is_wildcard i  match_iface (Iface i) p_i  i = p_i"
      proof(induction i p_i rule: internal_iface_name_match.induct)
      qed(auto simp add: iface_name_is_wildcard_alt split: if_split_asm)
    lemma match_iface_case_wildcard_prefix:
      "iface_name_is_wildcard i  match_iface (Iface i) p_i  butlast i = take (length i - 1) p_i"
      apply(induction i p_i rule: internal_iface_name_match.induct)
         apply(simp; fail)
        apply(simp add: iface_name_is_wildcard_alt split: if_split_asm; fail)
       apply(simp; fail)
      apply(simp)
      apply(intro conjI)
       apply(simp add: iface_name_is_wildcard_alt split: if_split_asm; fail)
      apply(simp add: iface_name_is_wildcard_fst)
      by (metis One_nat_def length_0_conv list.sel(1) list.sel(3) take_Cons')
    lemma match_iface_case_wildcard_length: "iface_name_is_wildcard i  match_iface (Iface i) p_i  length p_i  (length i - 1)"
      proof(induction i p_i rule: internal_iface_name_match.induct)
      qed(simp_all add: iface_name_is_wildcard_alt split: if_split_asm)
    corollary match_iface_case_wildcard:
      "iface_name_is_wildcard i  match_iface (Iface i) p_i  butlast i = take (length i - 1) p_i  length p_i  (length i - 1)"
      using match_iface_case_wildcard_length match_iface_case_wildcard_prefix by blast
  
  
    lemma match_iface_set: "match_iface (Iface i) p_iface  p_iface  internal_iface_name_to_set i"
      using internal_iface_name_to_set by simp
  
    private definition internal_iface_name_wildcard_longest :: "string  string  string option" where
      "internal_iface_name_wildcard_longest i1 i2 = (
        if 
          take (min (length i1 - 1) (length i2 - 1)) i1 = take (min (length i1 - 1) (length i2 - 1)) i2
        then
          Some (if length i1  length i2 then i2 else i1)
        else
          None)"
    private lemma "internal_iface_name_wildcard_longest ''eth+'' ''eth3+'' = Some ''eth3+''" by eval
    private lemma "internal_iface_name_wildcard_longest ''eth+'' ''e+'' = Some ''eth+''" by eval
    private lemma "internal_iface_name_wildcard_longest ''eth+'' ''lo'' = None" by eval
  
    private  lemma internal_iface_name_wildcard_longest_commute: "iface_name_is_wildcard i1  iface_name_is_wildcard i2  
      internal_iface_name_wildcard_longest i1 i2 = internal_iface_name_wildcard_longest i2 i1"
      apply(simp add: internal_iface_name_wildcard_longest_def)
      apply(safe)
        apply(simp_all add: iface_name_is_wildcard_alt)
        apply (metis One_nat_def append_butlast_last_id butlast_conv_take)
       by (metis min.commute)+
    private  lemma internal_iface_name_wildcard_longest_refl: "internal_iface_name_wildcard_longest i i = Some i"
      by(simp add: internal_iface_name_wildcard_longest_def)
  
  
    private lemma internal_iface_name_wildcard_longest_correct:
      "iface_name_is_wildcard i1  iface_name_is_wildcard i2  
       match_iface (Iface i1) p_i  match_iface (Iface i2) p_i 
       (case internal_iface_name_wildcard_longest i1 i2 of None  False | Some x  match_iface (Iface x) p_i)"
    proof -
      assume assm1: "iface_name_is_wildcard i1"
         and assm2: "iface_name_is_wildcard i2"
      { assume assm3: "internal_iface_name_wildcard_longest i1 i2 = None" 
        have "¬ (internal_iface_name_match i1 p_i  internal_iface_name_match i2 p_i)"
        proof -
          from match_iface_case_wildcard_prefix[OF assm1] have 1:
            "internal_iface_name_match i1 p_i = (take (length i1 - 1) i1 = take (length i1 - 1) p_i)" by(simp add: butlast_conv_take)
          from match_iface_case_wildcard_prefix[OF assm2] have 2:
            "internal_iface_name_match i2 p_i = (take (length i2 - 1) i2 = take (length i2 - 1) p_i)" by(simp add: butlast_conv_take)
          from assm3 have 3: "take (min (length i1 - 1) (length i2 - 1)) i1  take (min (length i1 - 1) (length i2 - 1)) i2"
           by(simp add: internal_iface_name_wildcard_longest_def split: if_split_asm)
          from 3 show ?thesis using 1 2 min.commute take_take by metis
        qed
      } note internal_iface_name_wildcard_longest_correct_None=this
    
      { fix X
        assume assm3: "internal_iface_name_wildcard_longest i1 i2 = Some X"
        have "(internal_iface_name_match i1 p_i  internal_iface_name_match i2 p_i)  internal_iface_name_match X p_i"
        proof -
          from assm3 have assm3': "take (min (length i1 - 1) (length i2 - 1)) i1 = take (min (length i1 - 1) (length i2 - 1)) i2"
            unfolding internal_iface_name_wildcard_longest_def by(simp split: if_split_asm)
      
          { fix i1 i2
            assume iw1: "iface_name_is_wildcard i1" and iw2: "iface_name_is_wildcard i2" and len: "length i1  length i2" and
                   take_i1i2: "take (length i1 - 1) i1 = take (length i1 - 1) i2"
            from len have len': "length i1 - 1  length i2 - 1" by fastforce
            { fix x::string
             from len' have "take (length i1 - 1) x = take (length i1 - 1) (take (length i2 - 1) x)" by(simp add: min_def)
            } note takei1=this
        
            { fix m::nat and n::nat and a::string and b c
              have "m  n  take n a = take n b  take m a = take m c  take m c = take m b" by (metis min_absorb1 take_take)
            } note takesmaller=this
        
            from match_iface_case_wildcard_prefix[OF iw1, simplified] have 1:
                "internal_iface_name_match i1 p_i  take (length i1 - 1) i1 = take (length i1 - 1) p_i" by(simp add: butlast_conv_take)
            also have "  take (length i1 - 1) (take (length i2 - 1) i1) = take (length i1 - 1) (take (length i2 - 1) p_i)" using takei1 by simp
            finally have  "internal_iface_name_match i1 p_i = (take (length i1 - 1) (take (length i2 - 1) i1) = take (length i1 - 1) (take (length i2 - 1) p_i))" .
            from match_iface_case_wildcard_prefix[OF iw2, simplified] have 2:
                "internal_iface_name_match i2 p_i  take (length i2 - 1) i2 = take (length i2 - 1) p_i" by(simp add: butlast_conv_take)
        
            have "internal_iface_name_match i2 p_i  internal_iface_name_match i1 p_i"
              unfolding 1 2 
              apply(rule takesmaller[of "(length i1 - 1)" "(length i2 - 1)" i2 p_i])
                using len' apply (simp; fail)
               apply (simp; fail)
              using take_i1i2 by simp
          } note longer_iface_imp_shorter=this
        
         show ?thesis
          proof(cases "length i1  length i2")
          case True
            with assm3 have "X = i2" unfolding internal_iface_name_wildcard_longest_def by(simp split: if_split_asm)
            from True assm3' have take_i1i2: "take (length i1 - 1) i1 = take (length i1 - 1) i2" by linarith
            from longer_iface_imp_shorter[OF assm1 assm2 True take_i1i2] X = i2
            show "(internal_iface_name_match i1 p_i  internal_iface_name_match i2 p_i)  internal_iface_name_match X p_i" by fastforce
          next
          case False
            with assm3 have "X = i1" unfolding internal_iface_name_wildcard_longest_def by(simp split: if_split_asm)
            from False assm3' have take_i1i2: "take (length i2 - 1) i2 = take (length i2 - 1) i1" by (metis min_def min_diff)
            from longer_iface_imp_shorter[OF assm2 assm1 _ take_i1i2] False X = i1
            show "(internal_iface_name_match i1 p_i  internal_iface_name_match i2 p_i)  internal_iface_name_match X p_i" by auto
          qed
        qed
      } note internal_iface_name_wildcard_longest_correct_Some=this
    
      from internal_iface_name_wildcard_longest_correct_None internal_iface_name_wildcard_longest_correct_Some show ?thesis
        by(simp split:option.split)
    qed
  
    fun iface_conjunct :: "iface  iface  iface option" where
      "iface_conjunct (Iface i1) (Iface i2) = (case (iface_name_is_wildcard i1, iface_name_is_wildcard i2) of
        (True,  True)  map_option Iface  (internal_iface_name_wildcard_longest i1 i2) |
        (True,  False)  (if match_iface (Iface i1) i2 then Some (Iface i2) else None) |
        (False, True)  (if match_iface (Iface i2) i1 then Some (Iface i1) else None) |
        (False, False)  (if i1 = i2 then Some (Iface i1) else None))"

    
    lemma iface_conjunct_Some: "iface_conjunct i1 i2 = Some x  
          match_iface x p_i  match_iface i1 p_i  match_iface i2 p_i"
      apply(cases i1, cases i2, rename_tac i1name i2name)
      apply(simp)
      apply(case_tac "iface_name_is_wildcard i1name")
       apply(case_tac [!] "iface_name_is_wildcard i2name")
         apply(simp_all)
         using internal_iface_name_wildcard_longest_correct apply auto[1]
        apply (metis match_iface.simps match_iface_case_nowildcard option.distinct(1) option.sel)
       apply (metis match_iface.simps match_iface_case_nowildcard option.distinct(1) option.sel)
      by (metis match_iface.simps option.distinct(1) option.inject)
    lemma iface_conjunct_None: "iface_conjunct i1 i2 = None  ¬ (match_iface i1 p_i  match_iface i2 p_i)"
      apply(cases i1, cases i2, rename_tac i1name i2name)
      apply(simp split: bool.split_asm if_split_asm)
         using internal_iface_name_wildcard_longest_correct apply fastforce
        apply (metis match_iface.simps match_iface_case_nowildcard)+
      done
    lemma iface_conjunct: "match_iface i1 p_i  match_iface i2 p_i 
           (case iface_conjunct i1 i2 of None  False | Some x  match_iface x p_i)"
    apply(simp split: option.split)
    by(blast dest: iface_conjunct_Some iface_conjunct_None)

    lemma match_iface_refl: "match_iface (Iface x) x" by (simp add: internal_iface_name_match_refl)
    lemma match_iface_eqI: assumes "x = Iface y" shows "match_iface x y"
      unfolding assms using match_iface_refl .


    lemma iface_conjunct_ifaceAny: "iface_conjunct ifaceAny i = Some i"
      apply(simp add: ifaceAny_def)
      apply(case_tac i, rename_tac iname)
      apply(simp)
      apply(case_tac "iface_name_is_wildcard iname")
       apply(simp add: internal_iface_name_wildcard_longest_def iface_name_is_wildcard_alt Suc_leI; fail)
      apply(simp)
      using internal_iface_name_match.elims(3) by fastforce
       
    lemma iface_conjunct_commute: "iface_conjunct i1 i2 = iface_conjunct i2 i1"
    apply(induction i1 i2 rule: iface_conjunct.induct)
    apply(rename_tac i1 i2, simp)
    apply(case_tac "iface_name_is_wildcard i1")
     apply(case_tac [!] "iface_name_is_wildcard i2")
       apply(simp_all)
    by (simp add: internal_iface_name_wildcard_longest_commute)


    private definition internal_iface_name_subset :: "string  string  bool" where
      "internal_iface_name_subset i1 i2 = (case (iface_name_is_wildcard i1, iface_name_is_wildcard i2) of
        (True,  True)  length i1  length i2  take ((length i2) - 1) i1 = butlast i2 |
        (True,  False)  False |
        (False, True)  take (length i2 - 1) i1 = butlast i2 |
        (False, False)  i1 = i2
        )"

    private lemma butlast_take_length_helper:
      fixes x ::"char list"
      assumes a1: "length i2  length i1"
      assumes a2: "take (length i2 - Suc 0) i1 = butlast i2"
      assumes a3: "butlast i1 = take (length i1 - Suc 0) x"
      shows "butlast i2 = take (length i2 - Suc 0) x"
    proof - (*sledgehammer spass Isar proof*)
      have f4: "List.gen_length 0 i2  List.gen_length 0 i1"
        using a1 by (simp add: length_code)
      have f5: "cs. List.gen_length 0 (cs::char list) - Suc 0 = List.gen_length 0 (tl cs)"
        by (metis (no_types) One_nat_def length_code length_tl)
      obtain nn :: "(nat  nat)  nat" where
        "f. ¬ f (nn f)  f (Suc (nn f))  f (List.gen_length 0 i2)  f (List.gen_length 0 i1)"
        using f4 by (meson lift_Suc_mono_le)
      hence "¬ nn (λn. n - Suc 0) - Suc 0  nn (λn. n - Suc 0)  List.gen_length 0 (tl i2)  List.gen_length 0 (tl i1)"
        using f5 by (metis (lifting) diff_Suc_Suc diff_zero)
      hence f6: "min (List.gen_length 0 (tl i2)) (List.gen_length 0 (tl i1)) = List.gen_length 0 (tl i2)"
        using diff_le_self min.absorb1 by blast
      { assume "take (List.gen_length 0 (tl i2)) i1  take (List.gen_length 0 (tl i2)) x"
        have "List.gen_length 0 (tl i2) = 0  take (List.gen_length 0 (tl i2)) i1 = take (List.gen_length 0 (tl i2)) x"
          using f6 f5 a3 by (metis (lifting) One_nat_def butlast_conv_take length_code take_take)
        hence "take (List.gen_length 0 (tl i2)) i1 = take (List.gen_length 0 (tl i2)) x"
          by force }
      thus "butlast i2 = take (length i2 - Suc 0) x"
        using f5 a2 by (metis (full_types) length_code)
    qed

    private lemma internal_iface_name_subset: "internal_iface_name_subset i1 i2  
        {i. internal_iface_name_match i1 i}  {i. internal_iface_name_match i2 i}"
      unfolding internal_iface_name_subset_def
      proof(cases "iface_name_is_wildcard i1", case_tac [!] "iface_name_is_wildcard i2", simp_all)
        assume a1: "iface_name_is_wildcard i1"
        assume a2: "iface_name_is_wildcard i2"
        show "(length i2  length i1  take (length i2 - Suc 0) i1 = butlast i2) 
            ({i. internal_iface_name_match i1 i}  {i. internal_iface_name_match i2 i})" (is "?l  ?r")
          proof(rule iffI)
            assume ?l with a1 a2 show ?r
             apply(clarify, rename_tac x)
             apply(drule_tac p_i=x in match_iface_case_wildcard_prefix)+
             apply(simp)
             using butlast_take_length_helper by blast
          next
            assume ?r hence r': "internal_iface_name_to_set i1  internal_iface_name_to_set i2 "
              apply -
              apply(subst(asm) internal_iface_name_to_set2[symmetric])+
              by assumption
            have hlp1: "i1 i2. {x. cs. x = i1 @ cs}  {x. cs. x = i2 @ cs}  length i2  length i1"
              apply(simp add: Set.Collect_mono_iff)
              by force
            have hlp2: "i1 i2. {x. cs. x = i1 @ cs}  {x. cs. x = i2 @ cs}  take (length i2) i1 = i2"
              apply(simp add: Set.Collect_mono_iff)
              by force
            from r' a1 a2 show ?l
              apply(simp add: internal_iface_name_to_set)
              apply(safe)
               apply(drule hlp1)
               apply(simp)
               apply (metis One_nat_def Suc_pred diff_Suc_eq_diff_pred diff_is_0_eq iface_name_is_wildcard.simps(1) length_greater_0_conv)
              apply(drule hlp2)
              apply(simp)
              by (metis One_nat_def butlast_conv_take length_butlast length_take take_take)
          qed
      next
      show "iface_name_is_wildcard i1  ¬ iface_name_is_wildcard i2 
            ¬ Collect (internal_iface_name_match i1)  Collect (internal_iface_name_match i2)"
        using internal_iface_name_match_refl match_iface_case_nowildcard by fastforce
      next
      show "¬ iface_name_is_wildcard i1  iface_name_is_wildcard i2 
            (take (length i2 - Suc 0) i1 = butlast i2)  ({i. internal_iface_name_match i1 i}  {i. internal_iface_name_match i2 i})"
        using match_iface_case_nowildcard match_iface_case_wildcard_prefix by force
      next
      show " ¬ iface_name_is_wildcard i1  ¬ iface_name_is_wildcard i2 
           (i1 = i2)  ({i. internal_iface_name_match i1 i}  {i. internal_iface_name_match i2 i})"
        using match_iface_case_nowildcard  by force
      qed
      
       
    
    definition iface_subset :: "iface  iface  bool" where
      "iface_subset i1 i2  internal_iface_name_subset (iface_sel i1) (iface_sel i2)"
    
    lemma iface_subset: "iface_subset i1 i2  {i. match_iface i1 i}  {i. match_iface i2 i}"
      unfolding iface_subset_def
      apply(cases i1, cases i2)
      by(simp add: internal_iface_name_subset)


    definition iface_is_wildcard :: "iface  bool" where
      "iface_is_wildcard ifce  iface_name_is_wildcard (iface_sel ifce)"
   
    lemma iface_is_wildcard_ifaceAny: "iface_is_wildcard ifaceAny"
      by(simp add: iface_is_wildcard_def ifaceAny_def)




  subsection‹Enumerating Interfaces›
    private definition all_chars :: "char list" where
      "all_chars  Enum.enum"
    private lemma all_chars: "set all_chars = (UNIV::char set)"
       by(simp add: all_chars_def enum_UNIV)
  
    text‹we can compute this, but its horribly inefficient!›
    (*valid chars in an interface are NOT limited to the printable ones!*)
    private lemma strings_of_length_n: "set (List.n_lists n all_chars) = {s::string. length s = n}"
      apply(induction n)
       apply(simp; fail)
      apply(simp add: all_chars)
      apply(safe)
       apply(simp; fail)
      apply(simp)
      apply(rename_tac n x)
      apply(rule_tac x="drop 1 x" in exI)
      apply(simp)
      apply(case_tac x)
       apply(simp_all)
      done
  
    text‹Non-wildacrd interfaces of length @{term n}
    private definition non_wildcard_ifaces :: "nat  string list" where
     "non_wildcard_ifaces n  filter (λi. ¬ iface_name_is_wildcard i) (List.n_lists n all_chars)"

    text‹Example: (any number higher than zero are probably too inefficient)›
    private lemma "non_wildcard_ifaces 0 = ['''']" by eval

    private lemma non_wildcard_ifaces: "set (non_wildcard_ifaces n) = {s::string. length s = n  ¬ iface_name_is_wildcard s}"
      using strings_of_length_n non_wildcard_ifaces_def by auto
  
    private lemma "( i  set (non_wildcard_ifaces n). internal_iface_name_to_set i) = {s::string. length s = n  ¬ iface_name_is_wildcard s}"
     by(simp add: non_wildcard_ifaces)
  
    text‹Non-wildacrd interfaces up to length @{term n}
    private fun non_wildcard_ifaces_upto :: "nat  string list" where
      "non_wildcard_ifaces_upto 0 = [[]]" |
      "non_wildcard_ifaces_upto (Suc n) = (non_wildcard_ifaces (Suc n)) @ non_wildcard_ifaces_upto n"
    private lemma non_wildcard_ifaces_upto: "set (non_wildcard_ifaces_upto n) = {s::string. length s  n  ¬ iface_name_is_wildcard s}"
      apply(induction n)
       apply fastforce
      using non_wildcard_ifaces by fastforce


  subsection‹Negating Interfaces›
    private lemma inv_iface_name_set: "- (internal_iface_name_to_set i) = (
      if iface_name_is_wildcard i
      then
        {c |c. length c < length (butlast i)}  {c @ cs |c cs. length c = length (butlast i)  c  butlast i}
      else
        {c | c. length c < length i}  {c@cs | c cs. length c  length i  c  i}
    )"
    proof -
      { fix i::string
        have inv_i_wildcard: "- {i@cs | cs. True} = {c | c. length c < length i}  {c@cs | c cs. length c = length i  c  i}"
          apply(rule Set.equalityI)
           prefer 2
           apply(safe)[1]
            apply(simp;fail)
           apply(simp;fail)
          apply(simp)
          apply(rule Compl_anti_mono[where B="{i @ cs |cs. True}" and A="- ({c | c. length c < length i}  {c@cs | c cs. length c = length i  c  i})", simplified])
          apply(safe)
          apply(simp)
          apply(case_tac "(length i) = length x")
           apply(erule_tac x=x in allE, simp)
          apply(erule_tac x="take (length i) x" in allE)
          apply(simp add: min_def)
          by (metis append_take_drop_id)
      } note inv_i_wildcard=this
      { fix i::string
        have inv_i_nowildcard: "- {i::string} = {c | c. length c < length i}  {c@cs | c cs. length c  length i  c  i}"
        proof -
          have x: "{c | c. length c = length i  c  i}   {c | c. length c > length i} = {c@cs | c cs. length c  length i  c  i}"
            apply(safe)
              apply force+
            done
          have "- {i::string} = {c |c . c  i}"
           by(safe, simp)
          also have " = {c | c. length c < length i}  {c | c. length c = length i  c  i}   {c | c. length c > length i}"
            by(auto)
          finally show ?thesis using x by auto
        qed
      } note inv_i_nowildcard=this
    show ?thesis
      proof(cases "iface_name_is_wildcard i")
      case True with inv_i_wildcard show ?thesis by force
      next
      case False with inv_i_nowildcard show ?thesis by force
      qed
    qed

    text‹Negating is really not intuitive.
          The Interface @{term "''et''"} is in the negated set of @{term "''eth+''"}.
          And the Interface @{term "''et+''"} is also in this set! This is because @{term "''+''"}
          is a normal interface character and not a wildcard here!
          In contrast, the set described by @{term "''et+''"} (with @{term "''+''"} a wildcard)
          is not a subset of the previously negated set.›
    lemma "''et''  - (internal_iface_name_to_set ''eth+'')" by(simp)
    lemma "''et+''  - (internal_iface_name_to_set ''eth+'')" by(simp)
    lemma "''+''  - (internal_iface_name_to_set ''eth+'')" by(simp)
    lemma "¬ {i. match_iface (Iface ''et+'') i}  - (internal_iface_name_to_set ''eth+'')" by force

    text‹Because @{term "''+''"} can appear as interface wildcard and normal interface character,
          we cannot take negate an @{term "Iface i"} such that we get back @{typ "iface list"} which
          describe the negated interface.›
    lemma "''+''  - (internal_iface_name_to_set ''eth+'')" by(simp)




  fun compress_pos_interfaces :: "iface list  iface option" where
    "compress_pos_interfaces [] = Some ifaceAny" |
    "compress_pos_interfaces [i] = Some i" |
    "compress_pos_interfaces (i1#i2#is) = (case iface_conjunct i1 i2 of None  None | Some i  compress_pos_interfaces (i#is))"

  lemma compress_pos_interfaces_Some: "compress_pos_interfaces ifces = Some ifce  
          match_iface ifce p_i  ( i set ifces. match_iface i p_i)"
  proof(induction ifces rule: compress_pos_interfaces.induct)
    case 1 thus ?case by (simp add: match_ifaceAny)
    next
    case 2 thus ?case by simp
    next
    case (3 i1 i2) thus ?case
    apply(simp)
    apply(case_tac "iface_conjunct i1 i2")
     apply(simp; fail)
    apply(simp)
    using iface_conjunct_Some by presburger
  qed

  lemma compress_pos_interfaces_None: "compress_pos_interfaces ifces = None  
          ¬ ( i set ifces. match_iface i p_i)"
  proof(induction ifces rule: compress_pos_interfaces.induct)
    case 1 thus ?case by (simp add: match_ifaceAny)
    next
    case 2 thus ?case by simp
    next
    case (3 i1 i2) thus ?case
      apply(cases "iface_conjunct i1 i2", simp_all)
       apply (blast dest: iface_conjunct_None)
      by (blast dest: iface_conjunct_Some)
  qed
end

end

Theory SimpleFw_Syntax

section‹Simple Firewall Syntax›
theory SimpleFw_Syntax
imports IP_Addresses.Hs_Compat
        Firewall_Common_Decision_State
        "Primitives/Iface"
        "Primitives/L4_Protocol"
        Simple_Packet
begin

  text‹For for IP addresses of arbitrary length›

  datatype simple_action = Accept | Drop
  
  text‹Simple match expressions do not allow negated expressions.
        However, Most match expressions can still be transformed into simple match expressions.
        
        A negated IP address range can be represented as a set of non-negated IP ranges.
        For example !8 = {0..7} ∪ {8 .. ipv4max}›.
        Using CIDR notation (i.e. the a.b.c.d/n› notation), we can represent negated IP
        ranges as a set of non-negated IP ranges with only fair blowup.
        Another handy result is that the conjunction of two IP ranges in CIDR notation is 
        either the smaller of the two ranges or the empty set.
        An empty IP range cannot be represented.
        If one wants to represent the empty range, then the complete rule needs to be removed.

        The same holds for layer 4 ports.
        In addition, there exists an empty port range, e.g. (1,0)›.
        The conjunction of two port ranges is again just one port range.
        
        But negation of interfaces is not supported. Since interfaces support a wildcard character,
        transforming a negated interface would either result in an infeasible blowup or requires
        knowledge about the existing interfaces (e.g. there only is eth0, eth1, wlan3, and vbox42)
        An empirical test shows that negated interfaces do not occur in our data sets.
        Negated interfaces can also be considered bad style: What is !eth0? Everything that is
        not eth0, experience shows that interfaces may come up randomly, in particular in combination 
        with virtual machines, so !eth0 might not be the desired match.
        At the moment, if an negated interface occurs which prevents translation to a simple match,
        we recommend to abstract the negated interface to unknown and remove it (upper or lower closure
        rule set) before translating to a simple match.
        The same discussion holds for negated protocols.

        Noteworthy, simple match expressions are both expressive and support conjunction:
        simple-match1 ∧ simple-match2 = simple-match3›
        (*It took very long to design the simple match such that it can represent everything we need
        and that you can calculate with it. Disjunction is easy: just have two consecutive rules with the same action.
        Conjunction was a tough fight! It is needed to translate:
        common_primitive_match_to_simple_match (MatchAny e1 e2) =
          simple_match_and (common_primitive_match_to_simple_match e1) (common_primitive_match_to_simple_match e2)
        This is key to translate common_primitive_match to simple_match

        It may seem a simple enhancement to support iiface :: "iface negation_type", but then you
        can no longer form the conjunction of two simple_matches.
        *)

  record (overloaded) 'i simple_match =
    iiface :: "iface" ― ‹in-interface›
      (*we cannot (and don't want to) express negated interfaces*)
      (*We could also drop interface wildcard support and try negated interfaces again …*)
    oiface :: "iface" ― ‹out-interface›
    src :: "('i::len word × nat) " ― ‹source IP address›
    dst :: "('i::len word × nat) " ― ‹destination›
    proto :: "protocol"
    sports :: "(16 word × 16 word)" ― ‹source-port first:last›
    dports :: "(16 word × 16 word)" ― ‹destination-port first:last›

  
  context
    notes [[typedef_overloaded]]
  begin
    datatype 'i simple_rule = SimpleRule (match_sel: "'i simple_match") (action_sel: simple_action)
  end



text‹Simple rule destructor. Removes the @{typ "'a simple_rule"} type, returns a tuple with the match and action.›
  definition simple_rule_dtor :: "'a simple_rule  'a simple_match × simple_action" where
    "simple_rule_dtor r  (case r of SimpleRule m a  (m,a))"
  
  lemma simple_rule_dtor_ids:
    "uncurry SimpleRule  simple_rule_dtor = id"
    "simple_rule_dtor  uncurry SimpleRule = id" 
    unfolding simple_rule_dtor_def comp_def fun_eq_iff
    by(simp_all split: simple_rule.splits)

end

Theory SimpleFw_Semantics

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 (simp add: match_iface_eqI)
          } 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

Theory List_Product_More

section‹List Product Helpers›
theory List_Product_More
imports Main
begin

(*TODO: this definition could also go to Main*)
lemma List_product_concat_map: "List.product xs ys = concat (map (λx. map (λy. (x,y)) ys) xs)"
  by(induction xs) (simp)+


definition all_pairs :: "'a list  ('a × 'a) list" where
  "all_pairs xs  concat (map (λx. map (λy. (x,y)) xs) xs)"

lemma all_pairs_list_product: "all_pairs xs = List.product xs xs"
  by(simp add: all_pairs_def List_product_concat_map)
  
lemma all_pairs: " (x,y)  (set xs × set xs). (x,y)  set (all_pairs xs)"
  by(simp add: all_pairs_list_product)

lemma all_pairs_set: "set (all_pairs xs) = set xs × set xs"
  by(simp add: all_pairs_list_product)

end

Theory Option_Helpers

section‹Option to List and Option to Set›
theory Option_Helpers
imports Main
begin

text‹Those are just syntactic helpers.›

definition option2set :: "'a option  'a set" where
  "option2set n  (case n of None  {} | Some s  {s})"

definition option2list :: "'a option  'a list" where
  "option2list n  (case n of None  [] | Some s  [s])"

lemma set_option2list[simp]: "set (option2list k) = option2set k"
  unfolding option2list_def option2set_def by (simp split: option.splits)

lemma option2list_simps[simp]: "option2list (Some x) = [x]" "option2list (None) = []"
  unfolding option2list_def option.simps by(fact refl)+

lemma option2set_None: "option2set None = {}"
  by(simp add: option2set_def)

lemma option2list_map: "option2list (map_option f n) = map f (option2list n)"
  by(simp add: option2list_def split: option.split)

lemma option2set_map: "option2set (map_option f n) = f ` option2set n"
  by(simp add: option2set_def split: option.split)

end

Theory Generic_SimpleFw

section‹Generalize Simple Firewall›
theory Generic_SimpleFw
imports SimpleFw_Semantics "Common/List_Product_More" "Common/Option_Helpers"
begin

subsection‹Semantics›
  text‹The semantics of the @{term simple_fw} is quite close to @{const List.find}. 
  The idea of the generalized @{term simple_fw} semantics is that you can have anything as the 
  resulting action, not only a @{type simple_action}.›
  
  definition generalized_sfw
    :: "('i::len simple_match × 'a) list  ('i, 'pkt_ext) simple_packet_scheme  ('i simple_match × 'a) option"
    where
    "generalized_sfw l p  find (λ(m,a). simple_matches m p) l"

subsection‹Lemmas›
  lemma generalized_sfw_simps:
    "generalized_sfw [] p = None"
    "generalized_sfw (a # as) p = (if (case a of (m,_)  simple_matches m p) then Some a else generalized_sfw as p)"
    unfolding generalized_sfw_def by simp_all
  
  lemma generalized_sfw_append:
    "generalized_sfw (a @ b) p = (case generalized_sfw a p of Some x  Some x
                                                           |  None  generalized_sfw b p)"
    by(induction a) (simp_all add: generalized_sfw_simps)
  
  lemma simple_generalized_undecided:
    "simple_fw fw p  Undecided  generalized_sfw (map simple_rule_dtor fw) p  None" 
    by(induction fw)
    (clarsimp simp add: generalized_sfw_def simple_fw_alt simple_rule_dtor_def
              split: prod.splits if_splits simple_action.splits simple_rule.splits)+
  
  lemma generalized_sfwSomeD: "generalized_sfw fw p = Some (r,d)  (r,d)  set fw  simple_matches r p"
    unfolding generalized_sfw_def
    by(induction fw) (simp split: if_split_asm)+
  
  lemma generalized_sfw_NoneD: "generalized_sfw fw p = None  (a,b)  set fw. ¬ simple_matches a p"
    by(induction fw) (clarsimp simp add: generalized_sfw_simps split: if_splits)+
  
  lemma generalized_fw_split: "generalized_sfw fw p = Some r  fw1 fw3. fw = fw1 @ r # fw3  generalized_sfw fw1 p = None"
    apply(induction fw rule: rev_induct)
     apply(simp add: generalized_sfw_simps generalized_sfw_append split: option.splits;fail)
    apply(clarsimp simp add: generalized_sfw_simps generalized_sfw_append split: option.splits if_splits)
      apply blast+
  done

  lemma generalized_sfw_filterD:
    "generalized_sfw (filter f fw) p = Some (r,d)  simple_matches r p  f (r,d)"
  by(induction fw) (simp_all add: generalized_sfw_simps split: if_splits)

  lemma generalized_sfw_mapsnd:
    "generalized_sfw (map (apsnd f) fw) p = map_option (apsnd f) (generalized_sfw fw p)"
    by(induction fw) (simp add: generalized_sfw_simps split: prod.splits)+


subsection‹Equality with the Simple Firewall›

  text‹A matching action of the simple firewall directly corresponds to a filtering decision›
  definition simple_action_to_decision :: "simple_action  state" where
    "simple_action_to_decision a  case a of Accept  Decision FinalAllow
                                          |   Drop  Decision FinalDeny"
  
  text‹The @{const simple_fw} and the @{const generalized_sfw} are equal, if the state is translated appropriately.›
  lemma simple_fw_iff_generalized_fw:
    "simple_fw fw p = simple_action_to_decision a  (r. generalized_sfw (map simple_rule_dtor fw) p = Some (r,a))"
  by(induction fw)
    (clarsimp simp add: generalized_sfw_simps simple_rule_dtor_def simple_fw_alt simple_action_to_decision_def
              split: simple_rule.splits if_splits simple_action.splits)+
  
  lemma simple_fw_iff_generalized_fw_accept:
    "simple_fw fw p = Decision FinalAllow  (r. generalized_sfw (map simple_rule_dtor fw) p = Some (r, Accept))"
    by(fact simple_fw_iff_generalized_fw[where a = simple_action.Accept,
                                         unfolded simple_action_to_decision_def simple_action.simps])
  lemma simple_fw_iff_generalized_fw_drop:
    "simple_fw fw p = Decision FinalDeny  (r. generalized_sfw (map simple_rule_dtor fw) p = Some (r, Drop))"
    by(fact simple_fw_iff_generalized_fw[where a = simple_action.Drop,
                                         unfolded simple_action_to_decision_def simple_action.simps])


subsection‹Joining two firewalls, i.e. a packet is send through both sequentially.›

  definition generalized_fw_join
    :: "('i::len simple_match × 'a) list  ('i simple_match × 'b) list  ('i simple_match × 'a × 'b) list"
    where
    "generalized_fw_join l1 l2  [(u,(a,b)). (m1,a)  l1, (m2,b)  l2, u  option2list (simple_match_and m1 m2)]"
  
  lemma generalized_fw_join_1_Nil[simp]: "generalized_fw_join [] f2 = []"
  unfolding generalized_fw_join_def by(induction f2) simp+
  
  lemma generalized_fw_join_2_Nil[simp]: "generalized_fw_join f1 [] = []"
  unfolding generalized_fw_join_def by(induction f1) simp+
  
  lemma generalized_fw_join_cons_1:
    "generalized_fw_join ((am,ad) # l1) l2 =
      [(u,(ad,b)). (m2,b)  l2, u  option2list (simple_match_and am m2)] @ generalized_fw_join l1 l2"
  unfolding generalized_fw_join_def by(simp)
  
  lemma generalized_fw_join_1_nomatch:
    "¬ simple_matches am p 
      generalized_sfw [(u,(ad,b)). (m2,b)  l2, u  option2list (simple_match_and am m2)] p = None"
    by(induction l2)
    (clarsimp simp add: generalized_sfw_simps generalized_sfw_append option2list_def simple_match_and_SomeD
              split: prod.splits option.splits)+
    
  lemma generalized_fw_join_2_nomatch:
    "¬ simple_matches bm p 
      generalized_sfw (generalized_fw_join as ((bm, bd) # bs)) p = generalized_sfw (generalized_fw_join as bs) p"
  proof(induction as)
    case (Cons a as)
    note mIH = Cons.IH[OF Cons.prems]
    obtain am ad where a[simp]: "a = (am, ad)" by(cases a)
    have *: "generalized_sfw (concat (map (λ(m2, b). map (λu. (u, ad, b)) (option2list (simple_match_and am m2))) ((bm, bd) # bs))) p = 
      generalized_sfw (concat (map (λ(m2, b). map (λu. (u, ad, b)) (option2list (simple_match_and am m2))) bs)) p" 
      unfolding list.map prod.simps
      apply(cases "simple_match_and am bm")
       apply(simp add: option2list_def; fail)
      apply(frule simple_match_and_SomeD[of _ _ _ p])
      apply(subst option2list_def)
      apply(unfold concat.simps)
      apply(simp add: generalized_sfw_simps Cons.prems)
    done
    show ?case 
      unfolding a
      unfolding generalized_fw_join_cons_1
      unfolding generalized_sfw_append
      unfolding mIH
      unfolding *
      ..
  qed(simp add: generalized_fw_join_def)
  
  lemma generalized_fw_joinI:
    "generalized_sfw f1 p = Some (r1,d1); generalized_sfw f2 p = Some (r2,d2) 
       generalized_sfw (generalized_fw_join f1 f2) p = Some (the (simple_match_and r1 r2), d1,d2)"
  proof(induction f1)
    case (Cons a as)
    obtain am ad where a[simp]: "a = Pair am ad" by(cases a)
    show ?case proof(cases "simple_matches am p")
      case True
      hence dra: "d1 = ad" "r1 = am" using Cons.prems by(simp_all add: generalized_sfw_simps)
      from Cons.prems(2) show ?thesis unfolding a dra
      proof(induction f2)
        case (Cons b bs)
        obtain bm bd where b[simp]: "b = Pair bm bd" by(cases b)
        thus ?case
        proof(cases "simple_matches bm p")
          case True
          hence drb: "d2 = bd" "r2 = bm" using Cons.prems by(simp_all add: generalized_sfw_simps)
          from True ‹simple_matches am p obtain ruc where sma[simp]:
            "simple_match_and am bm = Some ruc" "simple_matches ruc p"
            using simple_match_and_correct[of am p bm]
            by(simp split: option.splits)
          show ?thesis unfolding b
            by(simp add: generalized_fw_join_def option2list_def generalized_sfw_simps drb)
        next
          case False
          with Cons.prems have bd:
            "generalized_sfw (b # bs) p = generalized_sfw bs p"
            "generalized_sfw (b # bs) p = Some (r2, d2)"
          by(simp_all add: generalized_sfw_simps)
          note mIH = Cons.IH[OF bd(2)[unfolded bd(1)]]
          show ?thesis 
            unfolding mIH[symmetric] b
            using generalized_fw_join_2_nomatch[OF False, of "(am, ad) # as" bd bs]
            .
        qed
      qed(simp add: generalized_sfw_simps generalized_fw_join_def)
        (*and empty_concat: "concat (map (λx. []) ms) = []" by simp*)
    next
      case False 
      with Cons.prems have "generalized_sfw (a # as) p = generalized_sfw as p"
        by(simp add: generalized_sfw_simps)
      with Cons.prems have "generalized_sfw as p = Some (r1, d1)" by simp
      note mIH = Cons.IH[OF this Cons.prems(2)]
      show ?thesis
        unfolding mIH[symmetric] a
        unfolding generalized_fw_join_cons_1
        unfolding generalized_sfw_append
        unfolding generalized_fw_join_1_nomatch[OF False, of ad f2]
        by simp
    qed
  qed(simp add: generalized_fw_join_def generalized_sfw_simps;fail)
  
  
  
  (* The structure is nearly the same as with generalized_fw_joinI, so it should be possible to show 
     it in one proof. But I felt like this is the better way *)
  lemma generalized_fw_joinD:
    "generalized_sfw (generalized_fw_join f1 f2) p = Some (u, d1,d2) 
      r1 r2. generalized_sfw f1 p = Some (r1,d1)  generalized_sfw f2 p = Some (r2,d2)  Some u = simple_match_and r1 r2"
  proof(induction f1)
    case (Cons a as)
    obtain am ad where a[simp]: "a = Pair am ad" by(cases a)
    show ?case proof(cases "simple_matches am p", rule exI)
      case True
      show "r2. generalized_sfw (a # as) p = Some (am, d1)  generalized_sfw f2 p = Some (r2, d2)  Some u = simple_match_and am r2"
      using Cons.prems
      proof(induction f2)
        case (Cons b bs)
        obtain bm bd where b[simp]: "b = Pair bm bd" by(cases b)
        show ?case
        proof(cases "simple_matches bm p", rule exI)
          case True
          with ‹simple_matches am p obtain u' (* u' = u, but I don't need that yet. *) 
            where sma: "simple_match_and am bm = Some u'  simple_matches u' p" 
            using simple_match_and_correct[of am p bm] by(simp split: option.splits)
          show "generalized_sfw (a # as) p = Some (am, d1)  generalized_sfw (b # bs) p = Some (bm, d2)  Some u = simple_match_and am bm"
          using Cons.prems True ‹simple_matches am p
          by(simp add: generalized_fw_join_def generalized_sfw_append sma generalized_sfw_simps)
        next
          case False
          have "generalized_sfw (generalized_fw_join (a # as) bs) p = Some (u, d1, d2)" 
            using Cons.prems unfolding b unfolding generalized_fw_join_2_nomatch[OF False] .
          note Cons.IH[OF this]
          moreover have "generalized_sfw (b # bs) p = generalized_sfw bs p" using False by(simp add: generalized_sfw_simps)
          ultimately show ?thesis by presburger
        qed
      qed(simp add: generalized_sfw_simps)
    next
      case False
      with Cons.prems have "generalized_sfw (generalized_fw_join as f2) p = Some (u, d1, d2)" by(simp add: generalized_fw_join_cons_1 generalized_sfw_append generalized_fw_join_1_nomatch)
      note Cons.IH[OF this]
      moreover have "generalized_sfw (a # as) p = generalized_sfw as p" using False by(simp add: generalized_sfw_simps)
      ultimately show ?thesis by presburger
    qed
  qed(simp add: generalized_fw_join_def generalized_sfw_simps)
  
  
  text‹We imagine two firewalls are positioned directly after each other.
        The first one has ruleset rs1 installed, the second one has ruleset rs2 installed.
        A packet needs to pass both firewalls.›
  
  theorem simple_fw_join:
    defines "rule_translate 
      map (λ(u,a,b). SimpleRule u (if a = Accept  b = Accept then Accept else Drop))"
    shows
    "simple_fw rs1 p = Decision FinalAllow  simple_fw rs2 p = Decision FinalAllow 
      simple_fw (rule_translate (generalized_fw_join (map simple_rule_dtor rs1) (map simple_rule_dtor rs2))) p = Decision FinalAllow"
  proof -
    have hlp1:
      "simple_rule_dtor  (λ(u, a, b). SimpleRule u (if a = Accept  b = Accept then Accept else Drop)) =
        apsnd (λ(a, b). if a = Accept  b = Accept then Accept else Drop)"
    unfolding fun_eq_iff comp_def by(simp add: simple_rule_dtor_def)
    show ?thesis
    unfolding simple_fw_iff_generalized_fw_accept
      apply(rule)
       apply(clarify)
       apply(drule (1) generalized_fw_joinI)
       apply(simp add: hlp1 rule_translate_def generalized_sfw_mapsnd ;fail)
      apply(clarsimp simp add: hlp1 generalized_sfw_mapsnd rule_translate_def)
      apply(drule generalized_fw_joinD)
      apply(clarsimp split: if_splits)
    done
  qed
  
  
  
  theorem simple_fw_join2:
    ― ‹translates a @{text "(match, action1, action2)"} tuple of the joined generalized
       firewall to a @{typ "'i::len simple_rule list"}. The two actions are translated such
       that you only get @{const Accept} if both actions are @{const Accept}
    defines "to_simple_rule_list  map (apsnd (λ(a,b)  (case a of Accept  b
                                                                 |  Drop  Drop)))"
    shows "simple_fw rs1 p = Decision FinalAllow  simple_fw rs2 p = Decision FinalAllow 
           (m. (generalized_sfw (to_simple_rule_list
            (generalized_fw_join (map simple_rule_dtor rs1) (map simple_rule_dtor rs2))) p) = Some (m, Accept))"
  unfolding simple_fw_iff_generalized_fw_accept
    apply(rule)
     apply(clarify)
     apply(drule (1) generalized_fw_joinI)
     apply(clarsimp simp add: to_simple_rule_list_def generalized_sfw_mapsnd; fail)
    apply(clarsimp simp add: to_simple_rule_list_def generalized_sfw_mapsnd)
    apply(drule generalized_fw_joinD)
    apply(clarsimp split: if_splits simple_action.splits)
  done
  
  lemma generalized_fw_join_1_1:
    "generalized_fw_join [(m1,d1)] fw2 = foldr (λ(m2,d2). (@) (case simple_match_and m1 m2 of None  [] | Some mu  [(mu,d1,d2)])) fw2 []"
  proof -
    have concat_map_foldr: "concat (map (λx. f x) l) = foldr (λx. (@) (f x)) l []" for f :: "'x  'y list" and l
      by(induction l) simp_all
    show ?thesis
    apply(simp add: generalized_fw_join_cons_1 option2list_def)
    apply(simp add: concat_map_foldr)
    apply(unfold list.map  prod.case_distrib option.case_distrib)
    by simp
  qed
  
  lemma generalized_sfw_2_join_None:
    "generalized_sfw fw2 p = None  generalized_sfw (generalized_fw_join fw1 fw2) p = None"
    by(induction fw2) (simp_all add: generalized_sfw_simps generalized_sfw_append generalized_fw_join_2_nomatch split: if_splits option.splits prod.splits)
  
  lemma generalized_sfw_1_join_None:
    "generalized_sfw fw1 p = None  generalized_sfw (generalized_fw_join fw1 fw2) p = None"
    by(induction fw1) (simp_all add: generalized_sfw_simps generalized_fw_join_cons_1 generalized_sfw_append generalized_fw_join_1_nomatch split: if_splits option.splits prod.splits)


  lemma generalized_sfw_join_set: "(a, b1, b2)  set (generalized_fw_join f1 f2) 
    (a1 a2. (a1, b1)  set f1  (a2, b2)  set f2  simple_match_and a1 a2 = Some a)"
   unfolding generalized_fw_join_def
   apply(rule iffI)
    subgoal unfolding generalized_fw_join_def by(clarsimp simp: option2set_def split: option.splits) blast
   by(clarsimp simp: option2set_def split: option.splits) fastforce

subsection‹Validity›
  text‹There's validity of matches on @{const generalized_sfw}, too, even on the join.›
  
  definition gsfw_valid :: "('i::len simple_match × 'c) list  bool" where
    "gsfw_valid  list_all (simple_match_valid  fst)"
  
  lemma gsfw_join_valid: "gsfw_valid f1  gsfw_valid f2  gsfw_valid (generalized_fw_join f1 f2)"
    unfolding gsfw_valid_def
    apply(induction f1)
     apply(simp;fail)
    apply(simp)
    apply(rename_tac a f1)
    apply(case_tac a)
    apply(simp add: generalized_fw_join_cons_1)
    apply(clarify)
    apply(thin_tac "list_all _ f1")
    apply(thin_tac "list_all _ (generalized_fw_join _ _)")
    apply(induction f2)
     apply(simp;fail)
    apply(simp)
    apply(clarsimp simp add: option2list_def list_all_iff)
    using simple_match_and_valid apply metis
    done
  
  lemma gsfw_validI: "simple_fw_valid fw  gsfw_valid (map simple_rule_dtor fw)"
    unfolding gsfw_valid_def simple_fw_valid_def 
    by(clarsimp simp add: simple_rule_dtor_def list_all_iff split: simple_rule.splits) fastforce


end

Theory Shadowed

section‹Shadowed Rules›
theory Shadowed
imports SimpleFw_Semantics
begin


subsection‹Removing Shadowed Rules›
text‹Testing, not executable›

text‹Assumes: @{term "simple_ruleset"}
fun rmshadow :: "'i::len simple_rule list  'i simple_packet set  'i simple_rule list" where
  "rmshadow [] _ = []" |
  "rmshadow ((SimpleRule m a)#rs) P = (if (pP. ¬ simple_matches m p)
    then 
      rmshadow rs P
    else
      (SimpleRule m a) # (rmshadow rs {p  P. ¬ simple_matches m p}))"


subsubsection‹Soundness›
  lemma rmshadow_sound: 
    "p  P  simple_fw (rmshadow rs P) p = simple_fw rs p"
  proof(induction rs arbitrary: P)
  case Nil thus ?case by simp
  next
  case (Cons r rs)
    from Cons.IH Cons.prems have IH1: "simple_fw (rmshadow rs P) p = simple_fw rs p" by (simp)
    let ?P'="{p  P. ¬ simple_matches (match_sel r) p}"
    from Cons.IH Cons.prems have IH2: "m. p  ?P'  simple_fw (rmshadow rs ?P') p = simple_fw rs p" by simp
    from Cons.prems show ?case
      apply(cases r, rename_tac m a)
      apply(simp)
      apply(case_tac "pP. ¬ simple_matches m p")
       apply(simp add: IH1 nomatch)
      apply(case_tac "p  ?P'")
       apply(frule IH2)
       apply(simp add: nomatch IH1)
      apply(simp)
      apply(case_tac a)
       apply(simp_all)
      by fast+
  qed

  corollary rmshadow:
    fixes p :: "'i::len simple_packet"
    shows "simple_fw (rmshadow rs UNIV) p = simple_fw rs p"
    using rmshadow_sound[of p] by simp

text‹A different approach where we start with the empty set of packets and collect packets which are already ``matched-away''.›
fun rmshadow' :: "'i::len simple_rule list  'i simple_packet set  'i simple_rule list" where
  "rmshadow' [] _ = []" |
  "rmshadow' ((SimpleRule m a)#rs) P = (if {p. simple_matches m p}  P
    then 
      rmshadow' rs P
    else
      (SimpleRule m a) # (rmshadow' rs (P  {p. simple_matches m p})))"

  lemma rmshadow'_sound: 
    "p  P  simple_fw (rmshadow' rs P) p = simple_fw rs p"
  proof(induction rs arbitrary: P)
  case Nil thus ?case by simp
  next
  case (Cons r rs)
    from Cons.IH Cons.prems have IH1: "simple_fw (rmshadow' rs P) p = simple_fw rs p" by (simp)
    let ?P'="{p. simple_matches (match_sel r) p}"
    from Cons.IH Cons.prems have IH2: "m. p  (Collect (simple_matches m))  simple_fw (rmshadow' rs (P  Collect (simple_matches m))) p = simple_fw rs p" by simp
    have nomatch_m: "m. p  P  {p. simple_matches m p}  P  ¬ simple_matches m p" by blast
    from Cons.prems show ?case
      apply(cases r, rename_tac m a)
      apply(simp)
      apply(case_tac "{p. simple_matches m p}  P")
       apply(simp add: IH1)
       apply(drule nomatch_m)
        apply(assumption)
       apply(simp add: nomatch)
      apply(simp)
      apply(case_tac a)
       apply(simp_all)
       apply(simp_all add: IH2)
      done
  qed

corollary 
  fixes p :: "'i::len simple_packet"
  shows "simple_fw (rmshadow rs UNIV) p = simple_fw (rmshadow' rs {}) p"
  using rmshadow'_sound[of p] rmshadow_sound[of p] by simp


text‹Previous algorithm is not executable because we have no code for @{typ "'i::len simple_packet set"}.
      To get some code, some efficient set operations would be necessary.
        We either need union and subset or intersection and negation.
        Both subset and negation are complicated.
      Probably the BDDs which related work uses is really necessary.
›

(*Drafting set operations which might be necessary for an executable implementation. But BDDs might just be the thing here.*)
context
begin
  private type_synonym 'i simple_packet_set = "'i simple_match list"

  private definition simple_packet_set_toSet :: "'i::len simple_packet_set  'i simple_packet set" where
    "simple_packet_set_toSet ms = {p. m  set ms. simple_matches m p}"

  private lemma simple_packet_set_toSet_alt: "simple_packet_set_toSet ms = ( m  set ms. {p. simple_matches m p})"
    unfolding simple_packet_set_toSet_def by blast

  private definition simple_packet_set_union :: "'i::len simple_packet_set 'i  simple_match  'i simple_packet_set" where
    "simple_packet_set_union ps m = m # ps"

  private lemma "simple_packet_set_toSet (simple_packet_set_union ps m) = simple_packet_set_toSet ps  {p. simple_matches m p}"
    unfolding simple_packet_set_toSet_def simple_packet_set_union_def by simp blast

   (*either a sound but not complete executable implementation or a better idea to implement subset*)
   private lemma "(m'  set ms.
        {i. match_iface iif i}  {i. match_iface (iiface m') i} 
        {i. match_iface oif i}  {i. match_iface (oiface m') i} 
        {ip. simple_match_ip sip ip}  {ip. simple_match_ip (src m') ip} 
        {ip. simple_match_ip dip ip}  {ip. simple_match_ip (dst m') ip} 
        {p. match_proto protocol p}  {p. match_proto (proto m') p} 
        {p. simple_match_port sps p}  {p. simple_match_port (sports m') p} 
        {p. simple_match_port dps p}  {p. simple_match_port (dports m') p}
      )
     {p. simple_matches iiface=iif, oiface=oif, src=sip, dst=dip, proto=protocol, sports=sps, dports=dps  p}  (simple_packet_set_toSet ms)"
      unfolding simple_packet_set_toSet_def simple_packet_set_union_def
      apply(simp add: simple_matches.simps)
      apply(simp add: Set.Collect_mono_iff)
      apply clarify
      apply meson
      done

    text‹subset or negation ... One efficient implementation would suffice.›
    private lemma "{p:: 'i::len simple_packet. simple_matches m p}  (simple_packet_set_toSet ms) 
      {p:: 'i::len simple_packet. simple_matches m p}  ( m  set ms. {p. ¬ simple_matches m p}) = {}" (is "?l  ?r")
    proof - 
      have "?l  {p. simple_matches m p} - (simple_packet_set_toSet ms) = {}" by blast
      also have "  {p. simple_matches m p} - ( m  set ms. {p:: 'i::len simple_packet. simple_matches m p}) = {}"
      using simple_packet_set_toSet_alt by blast
      also have "  ?r" by blast
      finally show ?thesis .
    qed

end
end

Theory IP_Partition_Preliminaries

(*  Title:      IP_Partition_Preliminaries
    Authors:    Cornelius Diekmann, Max Haslbeck
*)
(*SetPartitioning.thy
  Original Author: Max Haslbeck, 2015*)
section‹Partition a Set by a Specific Constraint›
theory IP_Partition_Preliminaries
imports Main
begin

text‹Will be used for the IP address space partition of a firewall.
    However, this file is completely generic in terms of sets, it only imports Main.

    It will be used in @{file ‹../Service_Matrix.thy›}.
    Core idea: This file partitions @{typ "'a set set"} by some magic condition.
    Later, we will show that this magic condition implies that all IPs that have been grouped
    by the magic condition show the same behaviour for a simple firewall.›

(* disjoint, ipPartition definitions *)

definition disjoint :: "'a set set  bool" where
  "disjoint ts  A  ts. B  ts. A  B  A  B = {}"

text_raw‹We will call two partitioned sets \emph{complete} iff @{term " ss =  ts"}.›

text‹The condition we use to partition a set. If this holds and 
      @{term A} is the set of IP addresses in each rule in a firewall,
      then @{term B} is a partition of @{term " A"} where each member has the same behavior
      w.r.t the firewall ruleset.›
text@{term A} is the carrier set and @{term B}* should be a partition of @{term " A"} 
     which fulfills the following condition:›
definition ipPartition :: "'a set set  'a set set  bool" where
  "ipPartition A B  a  A. b  B. a  b = {}  b  a"

definition disjoint_list :: "'a set list  bool" where
  "disjoint_list ls  distinct ls  disjoint (set ls)"

context begin
  (*internal*)
  private fun disjoint_list_rec :: "'a set list  bool" where
    "disjoint_list_rec [] = True" |
    "disjoint_list_rec (x#xs) = (x  (set xs) = {}  disjoint_list_rec xs)"
  
  private lemma disjoint_equi: "disjoint_list_rec ts  disjoint (set ts)"
    apply(induction ts)
     apply(simp_all add: disjoint_def)
    by fast
  
  private lemma disjoint_list_disjoint_list_rec: "disjoint_list ts  disjoint_list_rec ts"
    apply(induction ts)
     apply(simp_all add: disjoint_list_def disjoint_def)
    by fast
  
  private definition addSubsetSet :: "'a set  'a set set  'a set set" where
    "addSubsetSet s ts = insert (s - ts) (((∩) s) ` ts)  ((λx. x - s) ` ts)"
  
  private fun partitioning :: "'a set list  'a set set  'a set set" where
    "partitioning [] ts = ts" |
    "partitioning (s#ss) ts = partitioning ss (addSubsetSet s ts)"
  
  
  text‹simple examples›
  lemma "partitioning [{1::nat,2},{3,4},{5,6,7},{6},{10}] {} = {{10}, {6}, {5, 7}, {}, {3, 4}, {1, 2}}" by eval
  lemma " {{1::nat,2},{3,4},{5,6,7},{6},{10}} =  (partitioning [{1,2},{3,4},{5,6,7},{6},{10}] {})" by eval
  lemma "disjoint (partitioning [{1::nat,2},{3,4},{5,6,7},{6},{10}] {})" by eval
  lemma "ipPartition {{1::nat,2},{3,4},{5,6,7},{6},{10}} (partitioning [{1::nat,2},{3,4},{5,6,7},{6},{10}] {})" by eval
  
  lemma "ipPartition A {}" by(simp add: ipPartition_def)
  
  lemma ipPartitionUnion: "ipPartition As Cs  ipPartition Bs Cs  ipPartition (As  Bs) Cs"
    unfolding ipPartition_def by fast
  
  private lemma disjointAddSubset: "disjoint ts  disjoint (addSubsetSet a ts)" 
    by (auto simp add: disjoint_def addSubsetSet_def)
  
  private lemma coversallAddSubset:" (insert a ts) =  (addSubsetSet a ts)" 
    by (auto simp add: addSubsetSet_def)
  
  private lemma ipPartioningAddSubset0: "disjoint ts  ipPartition ts (addSubsetSet a ts)"
    apply(simp add: addSubsetSet_def ipPartition_def)
    apply(safe)
      apply blast
     apply(simp_all add: disjoint_def)
     apply blast+
    done
  
  private lemma ipPartitioningAddSubset1: "disjoint ts  ipPartition (insert a ts) (addSubsetSet a ts)"
    apply(simp add: addSubsetSet_def ipPartition_def)
    apply(safe)
      apply blast
     apply(simp_all add: disjoint_def)
     apply blast+
  done
  
  private lemma addSubsetSetI:
    "s - ts  addSubsetSet s ts"
    "t  ts  s  t  addSubsetSet s ts"
    "t  ts  t - s  addSubsetSet s ts"
  unfolding addSubsetSet_def by blast+
    
  private lemma addSubsetSetE:
    assumes "A  addSubsetSet s ts"
    obtains "A = s - ts" | T where "T  ts" "A = s  T" | T where "T  ts" "A = T - s"
    using assms unfolding addSubsetSet_def by blast
  
  private lemma Union_addSubsetSet: "(addSubsetSet b As) = b  As"
    unfolding addSubsetSet_def by auto
  
  private lemma addSubsetSetCom: "addSubsetSet a (addSubsetSet b As) = addSubsetSet b (addSubsetSet a As)"
  proof -
    {
      fix A a b assume "A  addSubsetSet a (addSubsetSet b As)"
      hence "A  addSubsetSet b (addSubsetSet a As)"
      apply (rule addSubsetSetE)
      proof(goal_cases)
        case 1
        assume "A = a - (addSubsetSet b As)"
        hence "A = (a - As) - b" by (auto simp add: Union_addSubsetSet)
        thus ?thesis by (auto intro: addSubsetSetI)
      next
        case (2 T)
        have "A = b  (a - As)  (SAs. A = b  (a  S))  (SAs. A = (a  S) - b)"
          by (rule addSubsetSetE[OF 2(1)]) (auto simp: 2(2))
        thus ?thesis by (blast intro: addSubsetSetI)
      next
        case (3 T)
        have "A = b - (addSubsetSet a As)  (SAs. A = b  (S - a))  (SAs. A = (S - a) - b)"
          by (rule addSubsetSetE[OF 3(1)]) (auto simp: 3(2) Union_addSubsetSet)
        thus ?thesis by (blast intro: addSubsetSetI)
      qed
    }
    thus ?thesis by blast
  qed
  
  private lemma ipPartitioningAddSubset2: "ipPartition {a} (addSubsetSet a ts)"
    apply(simp add: addSubsetSet_def ipPartition_def) 
    by blast
  
  private lemma disjointPartitioning_helper :"disjoint As  disjoint (partitioning ss As)"
    proof(induction ss arbitrary: As)
    case Nil thus ?case by(simp)
    next
    case (Cons s ss)
      from Cons.prems disjointAddSubset have d: "disjoint (addSubsetSet s As)" by fast
      from Cons.IH d have "disjoint (partitioning ss (addSubsetSet s As))" .
      thus ?case by simp
    qed
  
  private lemma disjointPartitioning: "disjoint (partitioning ss {})"
    proof -
      have "disjoint {}" by(simp add: disjoint_def)
      from this disjointPartitioning_helper show ?thesis by fast
    qed
  
  private lemma coversallPartitioning:" (set ts) =  (partitioning ts {})"
  proof -
    have " (set ts  As) =  (partitioning ts As)" for As
    apply(induction ts arbitrary: As)
     apply(simp_all)
    by (metis Union_addSubsetSet sup_left_commute)
    thus ?thesis by (metis sup_bot.right_neutral)
  qed
  
  private lemma " As =  Bs  ipPartition As Bs  ipPartition As (addSubsetSet a Bs)"
    by(auto simp add: ipPartition_def addSubsetSet_def)
  
  private lemma ipPartitionSingleSet: "ipPartition {t} (addSubsetSet t Bs) 
                ipPartition {t} (partitioning ts (addSubsetSet t Bs))"
    apply(induction ts arbitrary: Bs t)
     apply(simp_all)
    by (metis addSubsetSetCom ipPartitioningAddSubset2)
  
  private lemma ipPartitioning_helper: "disjoint As  ipPartition (set ts) (partitioning ts As)"
    proof(induction ts arbitrary: As)
    case Nil thus ?case by(simp add: ipPartition_def)
    next
    case (Cons t ts)
      from Cons.prems ipPartioningAddSubset0 have d: "ipPartition As (addSubsetSet t As)" by blast
      from Cons.prems Cons.IH d disjointAddSubset ipPartitioningAddSubset1
      have e: "ipPartition (set ts) (partitioning ts (addSubsetSet t As))" by blast
      from ipPartitioningAddSubset2 Cons.prems 
      have "ipPartition {t} (addSubsetSet t As)" by blast 
      from this Cons.prems ipPartitionSingleSet
      have f: "ipPartition {t} (partitioning ts (addSubsetSet t As))" by fast
      have "set (t#ts) = insert t (set ts)" by auto
      from ipPartitionUnion have " As Bs Cs. ipPartition As Cs  ipPartition Bs Cs  ipPartition (As  Bs) Cs" by fast
      with this e f 
      have "ipPartition (set (t # ts)) (partitioning ts (addSubsetSet t As))" by fastforce
      thus ?case by simp
   qed
  
  private lemma ipPartitioning: "ipPartition (set ts) (partitioning ts {})"
    proof -
      have "disjoint {}" by(simp add: disjoint_def)
      from this ipPartitioning_helper show ?thesis by fast
    qed
  
  (* OPTIMIZATION PROOFS *)
  
  private lemma inter_dif_help_lemma: "A  B = {}   B - S = B - (S - A)"
    by blast
  
  private lemma disjoint_list_lem: "disjoint_list ls  s  set(ls). t  set(ls). s  t  s  t = {}"
    proof(induction ls)
    qed(simp_all add: disjoint_list_def disjoint_def)
  
  private lemma disjoint_list_empty: "disjoint_list []"
    by (simp add: disjoint_list_def disjoint_def)
  
  private lemma disjoint_sublist: "disjoint_list (t#ts)  disjoint_list ts"
    proof(induction ts arbitrary: t)
    qed(simp_all add: disjoint_list_empty disjoint_list_def disjoint_def)
  
  private fun intersection_list :: "'a set  'a set list  'a set list" where
    "intersection_list _ [] = []" |
    "intersection_list s (t#ts) = (s  t)#(intersection_list s ts)"
  
  private fun intersection_list_opt :: "'a set  'a set list  'a set list" where
    "intersection_list_opt _ [] = []" |
    "intersection_list_opt s (t#ts) = (s  t)#(intersection_list_opt (s - t) ts)"
  
  private lemma disjoint_subset: "disjoint A  a  A  b  a  disjoint ((A - {a})  {b})"
    apply(simp add: disjoint_def)
    by blast
  
  private lemma disjoint_intersection: "disjoint A  a  A  disjoint ({a  b}  (A - {a}))"
    apply(simp add: disjoint_def)
    by(blast)
  
  private lemma intList_equi: "disjoint_list_rec ts  intersection_list s ts = intersection_list_opt s ts"
    proof(induction ts)
    case Nil thus ?case by simp
    next
    case (Cons t ts)
    from Cons.prems have "intersection_list_opt s ts = intersection_list_opt (s - t) ts"
      proof(induction ts arbitrary: s t)
      case Nil thus ?case by simp
      next
      case Cons
      have "t  set ts. u  t = {}  intersection_list_opt s ts = intersection_list_opt (s - u) ts"
        for u
        apply(induction ts arbitrary: s u)
         apply(simp_all)
        by (metis Diff_Int_distrib2 Diff_empty Diff_eq Un_Diff_Int sup_bot.right_neutral)
      with Cons show ?case
        apply(simp)
        by (metis Diff_Int_distrib2 Diff_empty Un_empty inf_sup_distrib1)
      qed
    with Cons show ?case by simp
    qed
  
  private fun difference_list :: "'a set  'a set list  'a set list" where
    "difference_list _ [] = []" |
    "difference_list s (t#ts) = (t - s)#(difference_list s ts)"
  
  private fun difference_list_opt :: "'a set  'a set list  'a set list" where
    "difference_list_opt _ [] = []" |
    "difference_list_opt s (t#ts) = (t - s)#(difference_list_opt (s - t) ts)"
  
  
  private lemma difList_equi: "disjoint_list_rec ts  difference_list s ts = difference_list_opt s ts"
    proof(induction ts arbitrary: s)
    case Nil thus ?case by simp
    next
    case (Cons t ts)
      have difference_list_opt_lem0: "t  set(ts). u  t = {} 
                                        difference_list_opt s ts = difference_list_opt (s - u) ts"
      for u proof(induction ts arbitrary: s u)
      case Cons thus ?case
         apply(simp_all add: inter_dif_help_lemma)
         by (metis Diff_Int_distrib2 Diff_eq Un_Diff_Int sup_bot.right_neutral)
      qed(simp)
      have "disjoint_list_rec (t # ts)  difference_list_opt s ts = difference_list_opt (s - t) ts"
      proof(induction ts arbitrary: s t)
      case Cons thus ?case
         apply(simp_all add: difference_list_opt_lem0)
         by (metis Un_empty inf_sup_distrib1 inter_dif_help_lemma)
      qed(simp)
    with Cons show ?case by simp
  qed
   
  private fun partList0 :: "'a set  'a set list  'a set list" where
    "partList0 s [] = []" |
    "partList0 s (t#ts) = (s  t)#((t - s)#(partList0 s ts))"
  
  private lemma partList0_set_equi: "set(partList0 s ts) = (((∩) s) ` (set ts))  ((λx. x - s) ` (set ts))"
    by(induction ts arbitrary: s) auto
  
  private lemma partList_sub_equi0: "set(partList0 s ts) =
                             set(difference_list s ts)  set(intersection_list s ts)" 
    by(induction ts arbitrary: s) simp+
  
  private fun partList1 :: "'a set  'a set list  'a set list" where
    "partList1 s [] = []" |
    "partList1 s (t#ts) = (s  t)#((t - s)#(partList1 (s - t) ts))"
  
  private lemma partList_sub_equi: "set(partList1 s ts) = 
                            set(difference_list_opt s ts)  set(intersection_list_opt s ts)" 
    by(induction ts arbitrary: s) (simp_all)
  
  private lemma partList0_partList1_equi: "disjoint_list_rec ts  set (partList0 s ts) = set (partList1 s ts)"
    by (simp add: partList_sub_equi partList_sub_equi0 intList_equi difList_equi)
  
  private fun partList2 :: "'a set  'a set list  'a set list" where
    "partList2 s [] = []" |
    "partList2 s (t#ts) = (if s  t = {} then  (t#(partList2 (s - t) ts))
                                         else (s  t)#((t - s)#(partList2 (s - t) ts)))"
  
  private lemma partList2_empty: "partList2 {} ts = ts"
    by(induction ts) (simp_all)
   
  private lemma partList1_partList2_equi: "set(partList1 s ts) - {{}} = set(partList2 s ts) - {{}}"
    by(induction ts arbitrary: s) (auto)
  
  private fun partList3 :: "'a set  'a set list  'a set list" where
    "partList3 s [] = []" |
    "partList3 s (t#ts) = (if s = {} then (t#ts) else
                            (if s  t = {} then (t#(partList3 (s - t) ts))
                                           else 
                              (if t - s = {} then (t#(partList3 (s - t) ts))
                                             else (t  s)#((t - s)#(partList3 (s - t) ts)))))"
  
  private lemma partList2_partList3_equi: "set(partList2 s ts) - {{}} = set(partList3 s ts) - {{}}"
    apply(induction ts arbitrary: s)
     apply(simp; fail)
    apply(simp add: partList2_empty)
    by blast
  
  fun partList4 :: "'a set  'a set list  'a set list" where
    "partList4 s [] = []" |
    "partList4 s (t#ts) = (if s = {} then (t#ts) else
                            (if s  t = {} then (t#(partList4 s ts))
                                           else 
                              (if t - s = {} then (t#(partList4 (s - t) ts))
                                             else (t  s)#((t - s)#(partList4 (s - t) ts)))))"
  
  private lemma partList4: "partList4 s ts = partList3 s ts"
    apply(induction ts arbitrary: s)
     apply(simp; fail)
    apply (simp add: Diff_triv)
    done
  
  private lemma partList0_addSubsetSet_equi: "s  (set ts)  
                                      addSubsetSet s (set ts) - {{}} = set(partList0 s ts) - {{}}"
    by(simp add: addSubsetSet_def partList0_set_equi)
  
  private fun partitioning_nontail :: "'a set list  'a set set  'a set set" where
    "partitioning_nontail [] ts = ts" |
    "partitioning_nontail (s#ss) ts = addSubsetSet s (partitioning_nontail ss ts)"
  
  private lemma partitioningCom: "addSubsetSet a (partitioning ss ts) = partitioning ss (addSubsetSet a ts)"
    apply(induction ss arbitrary: a ts)
     apply(simp; fail)
    apply(simp add: addSubsetSetCom)
  done
  
  private lemma partitioning_nottail_equi: "partitioning_nontail ss ts = partitioning ss ts"
    apply(induction ss arbitrary: ts)
     apply(simp; fail)
    apply(simp add: addSubsetSetCom partitioningCom)
  done
  
  fun partitioning1 :: "'a set list  'a set list  'a set list" where
    "partitioning1 [] ts = ts" |
    "partitioning1 (s#ss) ts = partList4 s (partitioning1 ss ts)"
  
  lemma partList4_empty: "{}  set ts  {}  set (partList4 s ts)"
    apply(induction ts arbitrary: s)
     apply(simp; fail)
    by auto
  
  lemma partitioning1_empty0: "{}  set ts  {}  set (partitioning1 ss ts)"
    apply(induction ss arbitrary: ts)
     apply(simp; fail)
    apply(simp add: partList4_empty)
    done
  
  lemma partitioning1_empty1: "{}  set ts  
                                set(partitioning1 ss ts) - {{}} = set(partitioning1 ss ts)"
    by(simp add: partitioning1_empty0)
  
  lemma partList4_subset: "a  (set ts)  a  (set (partList4 b ts))"
    apply(simp add: partList4)
    apply(induction ts arbitrary: a b)
     apply(simp; fail)
    apply(simp)
    by fast
  
  private lemma "a  {}  disjoint_list_rec (a # ts)  disjoint_list_rec ts  a   (set ts) = {}" by auto
  
  lemma partList4_complete0: "s  (set ts)  (set (partList4 s ts)) = (set ts)"
  unfolding partList4
  proof(induction ts arbitrary: s)
    case Nil thus ?case by(simp)
    next
    case Cons thus ?case by (simp add: Diff_subset_conv Un_Diff_Int inf_sup_aci(7) sup.commute)
  qed
  
  private lemma partList4_disjoint: "s  (set ts)  disjoint_list_rec ts  
                             disjoint_list_rec (partList4 s ts)"
    apply(induction ts arbitrary: s)
     apply(simp; fail)
    apply(simp add: Diff_subset_conv)
    apply(rule conjI)
     apply (metis Diff_subset_conv Int_absorb1 Int_lower2 Un_absorb1 partList4_complete0)
    apply(safe)
       using partList4_complete0 apply (metis Diff_subset_conv Diff_triv IntI UnionI)
      apply (metis Diff_subset_conv Diff_triv)
     using partList4_complete0 by (metis Diff_subset_conv IntI UnionI)+
  
  lemma union_set_partList4: "(set (partList4 s ts)) = (set ts)"
    by (induction ts arbitrary: s, auto)
  
  
  private lemma partList4_distinct_hlp: assumes "a  {}" "a  set ts" "disjoint (insert a (set ts))"
    shows "a  set (partList4 s ts)"
  proof -
    from assms have "¬ a  (set ts)" unfolding disjoint_def by fastforce
    hence "¬ a  (set (partList4 s ts))" using union_set_partList4 by metis
    thus ?thesis by blast
  qed
  
  private lemma partList4_distinct: "{}  set ts  disjoint_list ts  distinct (partList4 s ts)"
    proof(induction ts arbitrary: s)
    case Nil thus ?case by simp
    next
    case(Cons t ts)
      have x1: "x xa xb xc.
         t  set ts 
         disjoint (insert t (set ts)) 
         xa  t 
         xb  s  
         xb  t  
         xb  {}  
         xc  s  
         xc  {}  
         t  s  set (partList4 (s - t) ts)  
         ¬ t  s  (set (partList4 (s - t) ts))"
        by(simp add: union_set_partList4 disjoint_def, force) (*1s*)
      have x2: "x xa xb xc.
         t  set ts 
         disjoint (insert t (set ts)) 
         x  t 
         xa  t 
         xa  s 
         xb  s  
         xc  s  
         ¬ t - s  (set (partList4 (s - t) ts))"
        by(simp add: union_set_partList4 disjoint_def, force) (*1s*)
      from Cons have IH: "distinct (partList4 s ts)" for s
        using disjoint_sublist list.set_intros(2) by auto 
      from Cons.prems(1,2) IH show ?case
      unfolding disjoint_list_def
       apply(simp)
       apply(safe)
            apply(metis partList4_distinct_hlp)
           apply(metis partList4_distinct_hlp)
          apply(metis partList4_distinct_hlp)
         apply blast
        using x1 apply blast
       using x2 by blast
    qed
  
  lemma partList4_disjoint_list: assumes "s  (set ts)" "disjoint_list ts" "{}  set ts"
    shows "disjoint_list (partList4 s ts)"
    unfolding disjoint_list_def
    proof
      from assms(2,3) show "distinct (partList4 s ts)" 
        using partList4_distinct disjoint_list_def by auto
      show "disjoint (set (partList4 s ts))"
      proof -
        have disjoint_list_disjoint_list_rec: "disjoint_list ts  disjoint_list_rec ts"
        proof(induction ts)
        case Cons thus ?case by(auto simp add: disjoint_list_def disjoint_def)
        qed(simp)
        with partList4_disjoint disjoint_equi assms(1,2) show ?thesis by blast
      qed
    qed
  
  lemma partitioning1_subset: "a   (set ts)  a   (set (partitioning1 ss ts))"
    apply(induction ss arbitrary: ts a)
     apply(simp)
    apply(simp add: partList4_subset)
    done
  
  lemma partitioning1_disjoint_list: "{}  (set ts)   (set ss)   (set ts) 
                                 disjoint_list ts  disjoint_list (partitioning1 ss ts)"
  proof(induction ss)
  case Nil thus ?case by simp
  next
  case(Cons t ts) thus ?case
    apply(clarsimp)
    apply(rule partList4_disjoint_list)
      using partitioning1_subset apply(metis)
     apply(blast)
    using partitioning1_empty0 apply(metis)
    done
  qed
  
  private lemma partitioning1_disjoint: " (set ss)   (set ts) 
                                 disjoint_list_rec ts  disjoint_list_rec (partitioning1 ss ts)"
    proof(induction ss arbitrary: ts)
    qed(simp_all add: partList4_disjoint partitioning1_subset)

  private lemma partitioning_equi: "{}  set ts  disjoint_list_rec ts   (set ss)   (set ts) 
           set(partitioning1 ss ts) = partitioning_nontail ss (set ts) - {{}}"
    proof(induction ss)
    case Nil thus ?case by simp
    next
    case (Cons s ss)
      have addSubsetSet_empty: "addSubsetSet s (ts - {{}}) - {{}} = addSubsetSet s ts - {{}}"
        for s and ts::"'a set set"
        unfolding addSubsetSet_def by blast
      have r: "disjoint_list_rec ts  s  (set ts) 
                                        addSubsetSet s (set ts) - {{}} = set (partList4 s ts) - {{}}"
        for ts::"'a set list"
        unfolding partList4
        by(simp add: partList0_addSubsetSet_equi partList0_partList1_equi partList1_partList2_equi
                   partList2_partList3_equi)
      have 1: "disjoint_list_rec (partitioning1 ss ts)"
        using partitioning1_disjoint Cons.prems by auto
      from Cons.prems have 2: "s  (set (partitioning1 ss ts))"
        by (meson Sup_upper dual_order.trans list.set_intros(1) partitioning1_subset)
      from Cons have IH: "set (partitioning1 ss ts) = partitioning_nontail ss (set ts) - {{}}" by auto
      with r[OF 1 2] show ?case by (simp add: partList4_empty addSubsetSet_empty)
    qed
  
  lemma ipPartitioning_helper_opt: "{}  set ts  disjoint_list ts   (set ss)   (set ts) 
                                     ipPartition (set ss) (set (partitioning1 ss ts))"
    apply(drule disjoint_list_disjoint_list_rec)
    apply(simp add: partitioning_equi partitioning_nottail_equi)
    by (meson Diff_subset disjoint_equi ipPartition_def ipPartitioning_helper subsetCE)
  
  lemma complete_helper: "{}  set ts   (set ss)   (set ts)
         (set ts) =  (set (partitioning1 ss ts))"
    apply(induction ss arbitrary: ts)
     apply(simp_all)
    by (metis partList4_complete0)

  lemma "partitioning1  [{1::nat},{2},{}] [{1},{},{2},{3}] = [{1}, {}, {2}, {3}]" by eval

  lemma partitioning_foldr: "partitioning X B = foldr addSubsetSet X B"
    apply(induction X)
     apply(simp; fail)
    apply(simp)
    by (metis partitioningCom)
  
  lemma "ipPartition (set X) (foldr addSubsetSet X {})"
    apply(subst partitioning_foldr[symmetric])
    using ipPartitioning by auto
  
  lemma " (set X) =  (foldr addSubsetSet X {})"
    apply(subst partitioning_foldr[symmetric])
    by (simp add: coversallPartitioning)
  
  lemma "partitioning1 X B = foldr partList4 X B"
    by(induction X)(simp_all)
  
  lemma "ipPartition (set X) (set (partitioning1 X [UNIV]))"
    apply(rule ipPartitioning_helper_opt)
      by(simp_all add: disjoint_list_def disjoint_def)
  
  lemma "((set (partitioning1 X [UNIV]))) = UNIV"
    apply(subgoal_tac "UNIV =  (set (partitioning1 X [UNIV]))")
     prefer 2
     apply(rule complete_helper[where ts="[UNIV]", simplified])
    apply(simp)
    done
  
end
end

Theory GroupF

section‹Group by Function›
theory GroupF
imports Main
begin

text‹Grouping elements of a list according to a function.›

fun groupF ::  "('a  'b)  'a list  'a list list"  where
  "groupF f [] = []" |
  "groupF f (x#xs) = (x#(filter (λy. f x = f y) xs))#(groupF f (filter (λy. f x  f y) xs))"

text‹trying a more efficient implementation of @{term groupF}
context
begin
  private fun select_p_tuple :: "('a  bool)  'a  ('a list × 'a list)  ('a list × 'a list)"
  where
    "select_p_tuple p x (ts,fs) = (if p x then (x#ts, fs) else (ts, x#fs))"
  
  private definition partition_tailrec :: "('a  bool)  'a list  ('a list × 'a list)"
  where
    "partition_tailrec p xs = foldr (select_p_tuple p) xs ([],[])"
  
  private lemma partition_tailrec: "partition_tailrec f as =  (filter f as,  filter (λx. ¬f x) as)"
  proof - 
    {fix ts_accu fs_accu
      have "foldr (select_p_tuple f) as (ts_accu, fs_accu) =
              (filter f as @ ts_accu,  filter (λx. ¬f x) as @ fs_accu)"
      by(induction as arbitrary: ts_accu fs_accu) simp_all
    } thus ?thesis unfolding partition_tailrec_def by simp
  qed
  
  private lemma
    "groupF f (x#xs) = (let (ts, fs) = partition_tailrec (λy. f x = f y) xs in (x#ts)#(groupF f fs))"
  by(simp add: partition_tailrec)
  
  (*is this more efficient?*)
  private function groupF_code ::  "('a  'b)  'a list  'a list list"  where
    "groupF_code f [] = []" |
    "groupF_code f (x#xs) = (let
                               (ts, fs) = partition_tailrec (λy. f x = f y) xs
                             in
                               (x#ts)#(groupF_code f fs))"
  by(pat_completeness) auto
  
  private termination groupF_code
    apply(relation "measure (λ(f,as). length (filter (λx. (λy. f x = f y) x) as))")
     apply(simp; fail)
    apply(simp add: partition_tailrec)
    using le_imp_less_Suc length_filter_le by blast
  
  lemma groupF_code[code]: "groupF f as = groupF_code f as"
    by(induction f as rule: groupF_code.induct) (simp_all add: partition_tailrec)
  
  export_code groupF checking SML
end

lemma groupF_concat_set: "set (concat (groupF f xs)) = set xs"
  proof(induction f xs rule: groupF.induct)
  case 2 thus ?case by (simp) blast
  qed(simp)

lemma groupF_Union_set: "(x  set (groupF f xs). set x) = set xs"
  proof(induction f xs rule: groupF.induct)
  case 2 thus ?case by (simp) blast
  qed(simp)

lemma groupF_set: "X  set (groupF f xs). x  set X. x  set xs"
  using groupF_concat_set by fastforce

lemma groupF_equality:
  defines "same f A  a1  set A. a2  set A. f a1 = f a2"
  shows "A  set (groupF f xs). same f A"
  proof(induction f xs rule: groupF.induct)
    case 1 thus ?case by simp
  next
    case (2 f x xs)
      have groupF_fst:
        "groupF f (x # xs) = (x # [yxs . f x = f y]) # groupF f [yxs . f x  f y]" by force
      have step: " Aset [x # [yxs . f x = f y]]. same f A" unfolding same_def by fastforce
      with 2 show ?case unfolding groupF_fst by fastforce
  qed

lemma groupF_nequality: "A  set (groupF f xs)  B  set (groupF f xs)  A  B 
     a  set A. b  set B. f a  f b"
  proof(induction f xs rule: groupF.induct)
  case 1 thus ?case by simp
  next
  case 2 thus ?case
    apply -
    apply(subst (asm) groupF.simps)+
    using groupF_set by fastforce (*1s*)
  qed

lemma groupF_cong: fixes xs::"'a list" and f1::"'a  'b" and f2::"'a  'c"
  assumes "x  set xs. y  set xs. (f1 x = f1 y  f2 x = f2 y)"
  shows "groupF f1 xs = groupF f2 xs"
  using assms proof(induction f1 xs rule: groupF.induct)
    case (2 f x xs) thus ?case using filter_cong[of xs xs "λy. f x = f y" "λy. f2 x = f2 y"]
                                     filter_cong[of xs xs "λy. f x  f y" "λy. f2 x  f2 y"] by auto
  qed (simp)

lemma groupF_empty: "groupF f xs  []  xs  []"
  by(induction f xs rule: groupF.induct) auto
lemma groupF_empty_elem: "x  set (groupF f xs)  x  []"
  by(induction f xs rule: groupF.induct) auto

lemma groupF_distinct: "distinct xs  distinct (concat (groupF f xs))"
  by (induction f xs rule: groupF.induct) (auto simp add: groupF_Union_set)

text‹It is possible to use
    @{term "map (map fst) (groupF snd (map (λx. (x, f x)) P))"}
  instead of
    @{term "groupF f P"}
  for the following reasons:
    @{const groupF} executes its compare function (first parameter) very often;
    it always tests for @{term "(f x = f y)"}.
    The function @{term f} may be really expensive.
    At least polyML does not share the result of @{term f} but (probably) always recomputes (part of) it.
    The optimization pre-computes @{term f} and tells @{const groupF} to use
    a really cheap function (@{const snd}) to compare.
    The following lemma tells that those are equal.›
  (* is this also faster for Haskell?*)

lemma groupF_tuple: "groupF f xs = map (map fst) (groupF snd (map (λx. (x, f x)) xs))"
  proof(induction f xs rule: groupF.induct)
  case (1 f) thus ?case by simp
  next
  case (2 f x xs)
    have g1: "[yxs . f x = f y] = map fst [ymap (λx. (x, f x)) xs . f x = snd y]"
      proof(induction xs arbitrary: f x)
      case Cons thus ?case by fastforce
      qed(simp)
    have g2: "(map (λx. (x, f x)) [yxs . f x  f y]) = [ymap (λx. (x, f x)) xs . f x  snd y]"
      proof(induction xs)
      case Cons thus ?case by fastforce
      qed(simp)
    from 2 g1 g2 show ?case by simp
  qed
end

Theory IP_Addr_WordInterval_toString

section‹Helper: Pretty Printing Word Intervals which correspond to IP address Ranges›
theory IP_Addr_WordInterval_toString
imports IP_Addresses.IP_Address_toString
begin

(*The "u" stands for union. I guess you may want to customize this pretty printing syntax :D*)

fun ipv4addr_wordinterval_toString :: "32 wordinterval  string" where
  "ipv4addr_wordinterval_toString (WordInterval s e) =
    (if s = e then ipv4addr_toString s else ''{''@ipv4addr_toString s@'' .. ''@ipv4addr_toString e@''}'')" |
  "ipv4addr_wordinterval_toString (RangeUnion a b) =
    ipv4addr_wordinterval_toString a @ '' u ''@ipv4addr_wordinterval_toString b"

fun ipv6addr_wordinterval_toString :: "128 wordinterval  string" where
  "ipv6addr_wordinterval_toString (WordInterval s e) =
    (if s = e then ipv6addr_toString s else ''{''@ipv6addr_toString s@'' .. ''@ipv6addr_toString e@''}'')" |
  "ipv6addr_wordinterval_toString (RangeUnion a b) =
    ipv6addr_wordinterval_toString a @ '' u ''@ipv6addr_wordinterval_toString b"

end

Theory Primitives_toString

section‹toString Functions for Primitives›
theory Primitives_toString
imports "../Common/Lib_Enum_toString"
        IP_Addresses.IP_Address_toString
        Iface
        L4_Protocol
begin


definition ipv4_cidr_toString :: "(ipv4addr × nat)  string" where
  "ipv4_cidr_toString ip_n = (case ip_n of (base, n)   (ipv4addr_toString base @''/''@ string_of_nat n))"
lemma "ipv4_cidr_toString (ipv4addr_of_dotdecimal (192,168,0,1), 22) = ''192.168.0.1/22''" by eval

definition ipv6_cidr_toString :: "(ipv6addr × nat)  string" where
  "ipv6_cidr_toString ip_n = (case ip_n of (base, n)   (ipv6addr_toString base @''/''@ string_of_nat n))"
lemma "ipv6_cidr_toString (42540766411282592856906245548098208122, 64) = ''2001:db8::8:800:200c:417a/64''" by eval

definition primitive_protocol_toString :: "primitive_protocol  string" where
  "primitive_protocol_toString protid  ( 
  if protid = TCP then ''tcp'' else
  if protid = UDP then ''udp'' else
  if protid = ICMP then ''icmp'' else
  if protid = L4_Protocol.SCTP then ''sctp'' else
  if protid = L4_Protocol.IGMP then ''igmp'' else
  if protid = L4_Protocol.GRE then ''gre'' else
  if protid = L4_Protocol.ESP then ''esp'' else
  if protid = L4_Protocol.AH then ''ah'' else
  if protid = L4_Protocol.IPv6ICMP then ''ipv6-icmp'' else
  ''protocolid:''@dec_string_of_word0 protid)"

fun protocol_toString :: "protocol  string" where
  "protocol_toString (ProtoAny) = ''all''" |
  "protocol_toString (Proto protid) = primitive_protocol_toString protid"

definition iface_toString :: "string  iface  string" where
  "iface_toString descr iface = (if iface = ifaceAny then '''' else
      (case iface of (Iface name)  descr@name))"
lemma "iface_toString ''in: '' (Iface ''+'') = ''''" by eval
lemma "iface_toString ''in: '' (Iface ''eth0'') = ''in: eth0''" by eval

definition port_toString :: "16 word  string" where
  "port_toString p  dec_string_of_word0 p"

fun ports_toString :: "string  (16 word × 16 word)  string" where
  "ports_toString descr (s,e) = (if s = 0  e = max_word then '''' else descr @ (if s=e then port_toString s else port_toString s@'':''@port_toString e))"
lemma "ports_toString ''spt: '' (0,65535) = ''''" by eval
lemma "ports_toString ''spt: '' (1024,2048) = ''spt: 1024:2048''" by eval
lemma "ports_toString ''spt: '' (1024,1024) = ''spt: 1024''" by eval

definition ipv4_cidr_opt_toString :: "string  ipv4addr × nat  string" where
  "ipv4_cidr_opt_toString descr ip = (if ip = (0,0) then '''' else
      descr@ipv4_cidr_toString ip)"

definition protocol_opt_toString :: "string  protocol  string" where
  "protocol_opt_toString descr prot = (if prot = ProtoAny then '''' else
      descr@protocol_toString prot)"

end

Theory Service_Matrix

(*  Title:      Service_Matrix.thy
    Authors:    Cornelius Diekmann, Max Haslbeck
*)
(*IPPartitioning.thy
  Original Author: Max Haslbeck, 2015*)
section‹Service Matrices›
theory Service_Matrix
imports "Common/List_Product_More"
        "Common/IP_Partition_Preliminaries"
        "Common/GroupF"
        "Common/IP_Addr_WordInterval_toString"
        "Primitives/Primitives_toString"
        SimpleFw_Semantics
        IP_Addresses.WordInterval_Sorted
begin


subsection‹IP Address Space Partition›

(* could be generalized more *)
fun extract_IPSets_generic0
  :: "('i::len simple_match  'i word × nat)  'i simple_rule list  ('i wordinterval) list"
  where
  "extract_IPSets_generic0 _ [] = []" |
  "extract_IPSets_generic0 sel ((SimpleRule m _)#ss) = (ipcidr_tuple_to_wordinterval (sel m)) #
                                                       (extract_IPSets_generic0 sel ss)"

lemma extract_IPSets_generic0_length: "length (extract_IPSets_generic0 sel rs) = length rs"
  by(induction rs rule: extract_IPSets_generic0.induct) (simp_all)


(*
The order in which extract_IPSets returns the collected IP ranges heavily influences the running time
of the subsequent algorithms.
For example:
1) iterating through the ruleset and collecting all source and destination ips:
   10:10:49 elapsed time, 38:41:17 cpu time, factor 3.80
2) iterating through the ruleset and first returning all source ips and iterating again and then return all destination ips:
   3:39:56 elapsed time, 21:08:34 cpu time, factor 5.76

To get a more deterministic runtime, we are sorting the output. As a performance optimization, we also remove duplicate entries.
We use mergesort_remdups, which does a mergesort (i.e sorts!) and removes duplicates and mergesort_by_rel which does a mergesort
(without removing duplicates) and allows to specify the relation we use to sort.
In theory, the largest ip ranges (smallest prefix length) should be put first, the following evaluation shows that this may not
be the fastest solution. The reason might be that access_matrix_pretty_ipv4 picks (almost randomly) one IP from the result and
there are fast and slower choices. The faster choices are the ones where the firewall ruleset has a decision very early. 
Therefore, the running time is still a bit unpredictable.

Here is the data:
map ipcidr_tuple_to_wordinterval (mergesort_by_rel (λ (a1,a2) (b1, b2). (a2, a1) ≤ (b2, b1)) (mergesort_remdups
                        ((map (src ∘ match_sel) rs) @ (map (dst ∘ match_sel) rs))))
 (2:47:04 elapsed time, 17:08:01 cpu time, factor 6.15)


map ipcidr_tuple_to_wordinterval (mergesort_remdups ((map (src ∘ match_sel) rs) @ (map (dst ∘ match_sel) rs)))
 (2:41:03 elapsed time, 16:56:46 cpu time, factor 6.31)


map ipcidr_tuple_to_wordinterval (mergesort_by_rel (λ (a1,a2) (b1, b2). (a2, a1) ≤ (b2, b1)) (
                         ((map (src ∘ match_sel) rs) @ (map (dst ∘ match_sel) rs)))
 (5:52:28 elapsed time, 41:50:10 cpu time, factor 7.12)


map ipcidr_tuple_to_wordinterval (mergesort_by_rel (≤)
                         ((map (src ∘ match_sel) rs) @ (map (dst ∘ match_sel) rs))))
  (3:10:57 elapsed time, 19:12:25 cpu time, factor 6.03)


map ipcidr_tuple_to_wordinterval (mergesort_by_rel (λ (a1,a2) (b1, b2). (a2, a1) ≤ (b2, b1)) (mergesort_remdups
                        (extract_src_dst_ips rs [])))
 (2:49:57 elapsed time, 17:10:49 cpu time, factor 6.06)

map ipcidr_tuple_to_wordinterval ((mergesort_remdups (extract_src_dst_ips rs [])))
 (2:43:44 elapsed time, 16:57:49 cpu time, factor 6.21)

map ipcidr_tuple_to_wordinterval (mergesort_by_rel (λ (a1,a2) (b1, b2). (a2, a1) ≥ (b2, b1)) (mergesort_remdups (extract_src_dst_ips rs [])))
 (2:47:37 elapsed time, 16:54:47 cpu time, factor 6.05)

There is a clear looser: not using mergesort_remdups
There is no clear winner. We will just stick to mergesort_remdups.

*)

(*check the the order of mergesort_remdups did not change*)
lemma "mergesort_remdups [(1::ipv4addr, 2::nat), (8,0), (8,1), (2,2), (2,4), (1,2), (2,2)] =
        [(1, 2), (2, 2), (2, 4), (8, 0), (8, 1)]" by eval


(*a tail-recursive implementation*)
fun extract_src_dst_ips
  :: "'i::len simple_rule list  ('i word × nat) list  ('i word × nat) list" where
  "extract_src_dst_ips [] ts = ts" |
  "extract_src_dst_ips ((SimpleRule m _)#ss) ts = extract_src_dst_ips ss  (src m # dst m # ts)"

lemma extract_src_dst_ips_length: "length (extract_src_dst_ips rs acc) = 2*length rs + length acc"
proof(induction rs arbitrary: acc)
case (Cons r rs) thus ?case by(cases r, simp)
qed(simp)

definition extract_IPSets
  :: "'i::len simple_rule list  ('i wordinterval) list" where
  "extract_IPSets rs  map ipcidr_tuple_to_wordinterval (mergesort_remdups (extract_src_dst_ips rs []))"
lemma extract_IPSets:
  "set (extract_IPSets rs) = set (extract_IPSets_generic0 src rs)  set (extract_IPSets_generic0 dst rs)"
proof -
  { fix acc
    have "ipcidr_tuple_to_wordinterval ` set (extract_src_dst_ips rs acc) =
            ipcidr_tuple_to_wordinterval ` set acc  set (extract_IPSets_generic0 src rs) 
            set (extract_IPSets_generic0 dst rs)"
    proof(induction rs arbitrary: acc)
    case (Cons r rs ) thus ?case
      apply(cases r)
      apply(simp)
      by fast
    qed(simp)
  } thus ?thesis unfolding extract_IPSets_def by(simp_all add: extract_IPSets_def mergesort_remdups_correct)
qed

lemma "(a::nat) div 2 + a mod 2  a" by fastforce

lemma merge_length: "length (merge l1 l2)  length l1 + length l2"
by(induction l1 l2 rule: merge.induct) auto

lemma merge_list_length: "length (merge_list as ls)  length (concat (as @ ls))"
proof(induction as ls rule: merge_list.induct)
case (5 l1 l2 acc2 ls)
  have "length (merge l2 acc2)  length l2 + length acc2" using merge_length by blast
  with 5 show ?case by simp
qed(simp_all)

lemma mergesort_remdups_length: "length (mergesort_remdups as)  length as"
unfolding mergesort_remdups_def
proof -
  have "concat ([] @ (map (λx. [x]) as)) = as" by simp
  with merge_list_length show "length (merge_list [] (map (λx. [x]) as))  length as" by metis
qed

lemma extract_IPSets_length: "length (extract_IPSets rs)  2 * length rs"
apply(simp add: extract_IPSets_def)
using extract_src_dst_ips_length mergesort_remdups_length by (metis add.right_neutral list.size(3)) 


(*
export_code extract_IPSets in SML
why you no work?
*)


lemma extract_equi0:
  "set (map wordinterval_to_set (extract_IPSets_generic0 sel rs)) =
    (λ(base,len). ipset_from_cidr base len) ` sel ` match_sel ` set rs"
  proof(induction rs)
  case (Cons r rs) thus ?case
    apply(cases r, simp)
    using wordinterval_to_set_ipcidr_tuple_to_wordinterval by fastforce
  qed(simp)

lemma src_ipPart_motivation:
fixes   rs
defines "X  (λ(base,len). ipset_from_cidr base len) ` src ` match_sel ` set rs"
assumes "A  X. B  A  B  A = {}" and "s1  B" and "s2  B"
shows "simple_fw rs (pp_src:=s1) = simple_fw rs (pp_src:=s2)"
proof -
  have "A  (λ(base,len). ipset_from_cidr base len) ` src ` match_sel ` set rs. B  A  B  A = {}  ?thesis"
  proof(induction rs)
    case Nil thus ?case by simp
  next
    case (Cons r rs)
    { fix m
      from s1  B s2  B have 
        "B  (case src m of (x, xa)  ipset_from_cidr x xa)  B  (case src m of (x, xa) 
                       ipset_from_cidr x xa) = {} 
             simple_matches m (pp_src := s1)  simple_matches m (pp_src := s2)"
      apply(cases m)
      apply(rename_tac iiface oiface srca dst proto sports dports)
      apply(case_tac srca)
      apply(simp add: simple_matches.simps)
      by blast
    } note helper=this
    from Cons[simplified] show ?case
     apply(cases r, rename_tac m a)
     apply(simp)
     apply(case_tac a)
      using helper apply force+
     done
  qed
  with assms show ?thesis by blast
qed

    
lemma src_ipPart:
  assumes "ipPartition (set (map wordinterval_to_set (extract_IPSets_generic0 src rs))) A"
          "B  A" "s1  B" "s2  B"
  shows "simple_fw rs (pp_src:=s1) = simple_fw rs (pp_src:=s2)"
proof -
  from src_ipPart_motivation[OF _ assms(3) assms(4)]
  have "A  (λ(base,len). ipset_from_cidr base len) ` src ` match_sel ` set rs. B  A  B  A = {} 
      simple_fw rs (pp_src:=s1) = simple_fw rs (pp_src:=s2)" by fast
  thus ?thesis using assms(1) assms(2)
    unfolding ipPartition_def
    by (metis (full_types) Int_commute extract_equi0)
qed
  
(*basically a copy of src_ipPart*)
lemma dst_ipPart:
  assumes "ipPartition (set (map wordinterval_to_set (extract_IPSets_generic0 dst rs))) A"
          "B  A" "s1  B" "s2  B"
  shows "simple_fw rs (pp_dst:=s1) = simple_fw rs (pp_dst:=s2)"
proof -
  have "A  (λ(base,len). ipset_from_cidr base len) ` dst ` match_sel ` set rs. B  A  B  A = {} 
      simple_fw rs (pp_dst:=s1) = simple_fw rs (pp_dst:=s2)"
  proof(induction rs)
    case Nil thus ?case by simp
  next
    case (Cons r rs)
    { fix m
      from s1  B s2  B have
        "B  (case dst m of (x, xa)  ipset_from_cidr x xa)  B  (case dst m of (x, xa) 
                   ipset_from_cidr x xa) = {} 
         simple_matches m (pp_dst := s1)  simple_matches m (pp_dst := s2)"
          apply(cases m)
          apply(rename_tac iiface oiface src dsta proto sports dports)
          apply(case_tac dsta)
          apply(simp add: simple_matches.simps)
          by blast
    } note helper=this
    from Cons show ?case
     apply(simp)
     apply(case_tac r, rename_tac m a)
     apply(simp)
     apply(case_tac a)
      using helper apply force+
     done
  qed
  thus ?thesis using assms(1) assms(2)
    unfolding ipPartition_def
    by (metis (full_types) Int_commute extract_equi0)
qed



(* OPTIMIZED PARTITIONING *)

definition wordinterval_list_to_set :: "'a::len wordinterval list  'a::len word set" where
  "wordinterval_list_to_set ws = (set (map wordinterval_to_set ws))"

lemma wordinterval_list_to_set_compressed:
  "wordinterval_to_set (wordinterval_compress (foldr wordinterval_union xs Empty_WordInterval)) =
          wordinterval_list_to_set xs"
  proof(induction xs)
  qed(simp_all add: wordinterval_compress wordinterval_list_to_set_def)

fun partIps :: "'a::len wordinterval  'a::len wordinterval list 
                 'a::len wordinterval list" where
  "partIps _ [] = []" |
  "partIps s (t#ts) = (if wordinterval_empty s then (t#ts) else
                        (if wordinterval_empty (wordinterval_intersection s t)
                          then (t#(partIps s ts))
                          else
                            (if wordinterval_empty (wordinterval_setminus t s)
                              then (t#(partIps (wordinterval_setminus s t) ts))
                              else (wordinterval_intersection t s)#((wordinterval_setminus t s)#
                                   (partIps (wordinterval_setminus s t) ts)))))"


lemma "partIps (WordInterval (1::ipv4addr) 1) [WordInterval 0 1] = [WordInterval 1 1, WordInterval 0 0]" by eval

lemma partIps_length: "length (partIps s ts)  (length ts) * 2"
proof(induction ts arbitrary: s)
case Cons thus ?case 
  apply(simp)
  using le_Suc_eq by blast
qed(simp)

fun partitioningIps :: "'a::len wordinterval list  'a::len wordinterval list 
                        'a::len wordinterval list" where
  "partitioningIps [] ts = ts" |
  "partitioningIps (s#ss) ts = partIps s (partitioningIps ss ts)"


lemma partitioningIps_length: "length (partitioningIps ss ts)  (2^length ss) * length ts"
proof(induction ss)
case Nil thus ?case by simp
next
case (Cons s ss)
  have "length (partIps s (partitioningIps ss ts))  length (partitioningIps ss ts) * 2"
    using partIps_length by fast
  with Cons show  ?case by force
qed

lemma partIps_equi: "map wordinterval_to_set (partIps s ts) = 
    partList4 (wordinterval_to_set s) (map wordinterval_to_set ts)"
  proof(induction ts arbitrary: s)
  qed(simp_all)

lemma partitioningIps_equi: "map wordinterval_to_set (partitioningIps ss ts)
       = (partitioning1 (map wordinterval_to_set ss) (map wordinterval_to_set ts))"
  apply(induction ss arbitrary: ts)
   apply(simp; fail)
  apply(simp add: partIps_equi)
  done

           
definition getParts :: "'i::len simple_rule list  'i wordinterval list" where
   "getParts rs = partitioningIps (extract_IPSets rs) [wordinterval_UNIV]"

lemma partitioningIps_foldr: "partitioningIps ss ts = foldr partIps ss ts"
  by(induction ss) (simp_all)

lemma getParts_foldr: "getParts rs = foldr partIps (extract_IPSets rs) [wordinterval_UNIV]"
  by(simp add: getParts_def partitioningIps_foldr)

lemma getParts_length: "length (getParts rs)  2^(2 * length rs)"
proof -
  from partitioningIps_length[where ss="extract_IPSets rs" and ts="[wordinterval_UNIV]"] have
    1: "length (partitioningIps (extract_IPSets rs) [wordinterval_UNIV])  2 ^ length (extract_IPSets rs)" by simp
  from extract_IPSets_length have "(2::nat) ^ length (extract_IPSets rs)  2 ^ (2 * length rs)" by simp
  with 1 have "length (partitioningIps (extract_IPSets rs) [wordinterval_UNIV])  2 ^ (2 * length rs)" by linarith
  thus ?thesis by(simp add: getParts_def) 
qed

lemma getParts_ipPartition: "ipPartition (set (map wordinterval_to_set (extract_IPSets rs)))
                                         (set (map wordinterval_to_set (getParts rs)))"
proof -
  have hlp_rule: "{}  set (map wordinterval_to_set ts)  disjoint_list (map wordinterval_to_set ts)  
     (wordinterval_list_to_set ss)  (wordinterval_list_to_set ts)  
     ipPartition (set (map wordinterval_to_set ss)) 
                 (set (map wordinterval_to_set (partitioningIps ss ts)))" for ts ss::"'a wordinterval list"
  by (metis ipPartitioning_helper_opt partitioningIps_equi wordinterval_list_to_set_def)
  have "disjoint_list [UNIV]" by(simp add: disjoint_list_def disjoint_def)
  have "ipPartition (set (map wordinterval_to_set ss)) 
                   (set (map wordinterval_to_set (partitioningIps ss [wordinterval_UNIV])))"
     for ss::"'a wordinterval list"
  apply(rule hlp_rule)
    apply(simp_all add: wordinterval_list_to_set_def ‹disjoint_list [UNIV])
  done
  thus ?thesis
  unfolding getParts_def by blast
qed


lemma getParts_complete: "wordinterval_list_to_set (getParts rs) = UNIV"
  proof -
  have "{}  set (map wordinterval_to_set ts) 
     (wordinterval_list_to_set ss)  (wordinterval_list_to_set ts)  
     wordinterval_list_to_set (partitioningIps ss ts) = (wordinterval_list_to_set ts)"
     for ss ts::"'a wordinterval list"
    using complete_helper by (metis partitioningIps_equi wordinterval_list_to_set_def)
  hence "wordinterval_list_to_set (getParts rs) = wordinterval_list_to_set [wordinterval_UNIV]"
    unfolding getParts_def by(simp add: wordinterval_list_to_set_def)
  also have " = UNIV" by (simp add: wordinterval_list_to_set_def)
  finally show ?thesis .
qed

theorem getParts_samefw: 
  assumes "A  set (map wordinterval_to_set (getParts rs))" "s1  A" "s2  A" 
  shows "simple_fw rs (pp_src:=s1) = simple_fw rs (pp_src:=s2) 
         simple_fw rs (pp_dst:=s1) = simple_fw rs (pp_dst:=s2)"
proof -
  let ?X="(set (map wordinterval_to_set (getParts rs)))"
  from getParts_ipPartition have "ipPartition (set (map wordinterval_to_set (extract_IPSets rs))) ?X" .
  hence "ipPartition (set (map wordinterval_to_set (extract_IPSets_generic0 src rs))) ?X 
         ipPartition (set (map wordinterval_to_set (extract_IPSets_generic0 dst rs))) ?X"
    by(simp add: extract_IPSets ipPartitionUnion image_Un)
  thus ?thesis using assms dst_ipPart src_ipPart by blast
qed


lemma partIps_nonempty: "ts  []  partIps s ts  []"
  by(induction ts arbitrary: s) simp_all
lemma partitioningIps_nonempty: "ts  []  partitioningIps ss ts  []"
proof(induction ss arbitrary: ts)
  case Nil thus ?case by simp
  next
  case (Cons s ss) thus ?case
    apply(cases ts)
     apply(simp; fail)
    apply(simp)
    using partIps_nonempty by blast
qed

(*
lemma partIps_nonempty: "∀t ∈ set ts. ¬ wordinterval_empty t 
       ⟹ {} ∉ set (map wordinterval_to_set (partIps s ts))"
  apply(induction ts arbitrary: s)
   apply(simp; fail)
  apply(simp)
  by blast
*)

lemma getParts_nonempty: "getParts rs  []" by(simp add: getParts_def partitioningIps_nonempty)
lemma getParts_nonempty_elems: "wset (getParts rs). ¬ wordinterval_empty w"
  unfolding getParts_def
  proof -
    have partitioning_nonempty: "t  set ts. ¬ wordinterval_empty t 
      {}  set (map wordinterval_to_set (partitioningIps ss ts))"
      for ts ss::"'a wordinterval list"
      proof(induction ss arbitrary: ts)
        case Nil thus ?case by auto
        case Cons thus ?case by (simp add: partIps_equi partList4_empty)
      qed
    have "t  set [wordinterval_UNIV].¬ wordinterval_empty t" by(simp)
    with partitioning_nonempty have
      "{}  set (map wordinterval_to_set (partitioningIps (extract_IPSets rs) [wordinterval_UNIV]))" 
      by blast
    thus "wset (partitioningIps (extract_IPSets rs) [wordinterval_UNIV]). ¬ wordinterval_empty w" by auto
  qed

(* HELPER FUNCTIONS UNIFICATION *)

fun getOneIp :: "'a::len wordinterval  'a::len word" where
  "getOneIp (WordInterval b _) = b" |
  "getOneIp (RangeUnion r1 r2) = (if wordinterval_empty r1 then getOneIp r2
                                                           else getOneIp r1)"

lemma getOneIp_elem: "¬ wordinterval_empty W  wordinterval_element (getOneIp W) W"
  by (induction W) simp_all

record parts_connection = pc_iiface :: string
                          pc_oiface :: string
                          pc_proto :: primitive_protocol
                          pc_sport :: "16 word"
                          pc_dport :: "16 word"



(* SAME FW DEFINITIONS AND PROOFS *)



definition same_fw_behaviour :: "⌦‹'pkt_ext itself ⇒› 'i::len word  'i word  'i simple_rule list  bool" where
  "same_fw_behaviour ⌦‹TYPE('pkt_ext)› a b rs 
      (p:: 'i::len simple_packet).
                simple_fw rs (pp_src:=a) = simple_fw rs (pp_src:=b) 
                simple_fw rs (pp_dst:=a) = simple_fw rs (pp_dst:=b)"

lemma getParts_same_fw_behaviour:
  "A  set (map wordinterval_to_set (getParts rs))   s1  A  s2  A  
   same_fw_behaviour s1 s2 rs"
  unfolding same_fw_behaviour_def
  using getParts_samefw by blast

definition "runFw s d c rs = simple_fw rs p_iiface=pc_iiface c,p_oiface=pc_oiface c,
                          p_src=s,p_dst=d,
                          p_proto=pc_proto c,
                          p_sport=pc_sport c,p_dport=pc_dport c,
                          p_tcp_flags={TCP_SYN},
                          p_payload=''''"

text‹We use @{const runFw} for executable code, but in general, everything applies to generic packets›
definition runFw_scheme :: "'i::len word  'i word  'b parts_connection_scheme 
                              ('i, 'a) simple_packet_scheme  'i simple_rule list  state"
  where
"runFw_scheme s d c p rs = simple_fw rs
                        (pp_iiface:=pc_iiface c,
                          p_oiface:=pc_oiface c,
                          p_src:=s,
                          p_dst:=d,
                          p_proto:=pc_proto c,
                          p_sport:=pc_sport c,
                          p_dport:=pc_dport c)"

lemma runFw_scheme: "runFw s d c rs = runFw_scheme s d c p rs"
  apply(simp add: runFw_def runFw_scheme_def)
  apply(case_tac p)
  apply(simp)
  apply(thin_tac _, simp)
proof(induction rs)
  case Nil thus ?case by(simp; fail)
next
  case(Cons r rs)
  obtain m a where r: "r = SimpleRule m a" by(cases r) simp
  from simple_matches_extended_packet[symmetric, of _ "pc_iiface c" "pc_oiface c"
                                      s d "pc_proto c" "pc_sport c" "pc_dport c" _ _ _ "{TCP_SYN}" "[]"]
  have pext: "simple_matches m
   p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c,
      p_tcp_flags = tcp_flags2, p_payload = payload2,  = aux =
  simple_matches m
   p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst = d, p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c,
      p_tcp_flags = {TCP_SYN}, p_payload = []" for tcp_flags2 payload2 and aux::'c by fast
  show ?case
   apply(simp add: r, cases a, simp)
    using Cons.IH by(simp add: pext)+
qed 


lemma has_default_policy_runFw: "has_default_policy rs  runFw s d c rs = Decision FinalAllow  runFw s d c rs = Decision FinalDeny"
  by(simp add: runFw_def has_default_policy)

definition same_fw_behaviour_one :: "'i::len word  'i word  'a parts_connection_scheme  'i simple_rule list  bool" where
  "same_fw_behaviour_one ip1 ip2 c rs 
            d s. runFw ip1 d c rs = runFw ip2 d c rs  runFw s ip1 c rs = runFw s ip2 c rs"

lemma same_fw_spec: "same_fw_behaviour ip1 ip2 rs  same_fw_behaviour_one ip1 ip2 c rs"
  apply(simp add: same_fw_behaviour_def same_fw_behaviour_one_def runFw_def)
  apply(rule conjI)
   apply(clarify)
   apply(erule_tac x="p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = ip1, p_dst= d,
                       p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c,
                       p_tcp_flags = {TCP_SYN},
                       p_payload=''''" in allE)
   apply(simp;fail)
  apply(clarify)
  apply(erule_tac x="p_iiface = pc_iiface c, p_oiface = pc_oiface c, p_src = s, p_dst= ip1,
                       p_proto = pc_proto c, p_sport = pc_sport c, p_dport = pc_dport c,
                       p_tcp_flags = {TCP_SYN},
                       p_payload=''''" in allE)
  apply(simp)
  done

text‹Is an equivalence relation›
lemma same_fw_behaviour_one_equi:
  "same_fw_behaviour_one x x c rs"
  "same_fw_behaviour_one x y c rs = same_fw_behaviour_one y x c rs"
  "same_fw_behaviour_one x y c rs  same_fw_behaviour_one y z c rs  same_fw_behaviour_one x z c rs"
  unfolding same_fw_behaviour_one_def by metis+

lemma same_fw_behaviour_equi:
  "same_fw_behaviour x x rs"
  "same_fw_behaviour x y rs = same_fw_behaviour y x rs"
  "same_fw_behaviour x y rs  same_fw_behaviour y z rs  same_fw_behaviour x z rs"
  unfolding same_fw_behaviour_def by auto

lemma runFw_sameFw_behave: 
       fixes W :: "'i::len word set set"
       shows
       "A  W. a1  A. a2  A. same_fw_behaviour_one a1 a2 c rs   W = UNIV 
       B  W. b  B. runFw ip1 b c rs = runFw ip2 b c rs 
       B  W. b  B. runFw b ip1 c rs = runFw b ip2 c rs 
       same_fw_behaviour_one ip1 ip2 c rs"
proof -
  assume a1: "A  W. a1  A. a2  A. same_fw_behaviour_one a1 a2 c rs"
   and a2: " W = UNIV "
   and a3: "B  W. b  B. runFw ip1 b c rs = runFw ip2 b c rs"
   and a4: "B  W. b  B. runFw b ip1 c rs = runFw b ip2 c rs"

   
  have relation_lem: "D  W. d1  D. d2  D. s. f s d1 = f s d2   W = UNIV 
                     B  W. b  B. f s1 b = f s2 b 
                     f s1 d = f s2 d" for W and f::"'c  'b  'd" and s1 d s2
    by (metis UNIV_I Union_iff)

  from a1 have a1':"AW. a1A. a2A. s. runFw s a1 c rs = runFw s a2 c rs"
    unfolding same_fw_behaviour_one_def by fast
  from relation_lem[OF a1' a2 a3] have s1: " d. runFw ip1 d c rs = runFw ip2 d c rs" by simp

  from a1 have a1'':"AW. a1A. a2A. d. runFw a1 d c rs = runFw a2 d c rs"
    unfolding same_fw_behaviour_one_def by fast
  from relation_lem[OF a1'' a2 a4] have s2: " s. runFw s ip1 c rs = runFw s ip2 c rs" by simp
  from s1 s2 show "same_fw_behaviour_one ip1 ip2 c rs"
    unfolding same_fw_behaviour_one_def by fast
qed

lemma sameFw_behave_sets:
  "wset A. a1  w. a2  w. same_fw_behaviour_one a1 a2 c rs 
   w1set A. w2set A. a1w1. a2w2. same_fw_behaviour_one a1 a2 c rs 
   w1set A. w2set A.
     a1w1. a2w2. same_fw_behaviour_one a1 a2 c rs"
proof -
  assume a1: "wset A. a1  w. a2  w. same_fw_behaviour_one a1 a2 c rs" and
         "w1set A. w2set A. a1w1. a2w2.  same_fw_behaviour_one a1 a2 c rs"
  from this have "w1set A. w2set A. a1w1. a2w2.  same_fw_behaviour_one a1 a2 c rs"
    using same_fw_behaviour_one_equi(3) by metis
  from a1 this show "w1set A. w2set A. a1w1. a2w2. same_fw_behaviour_one a1 a2 c rs"
    using same_fw_behaviour_one_equi(3) by metis
qed
  



definition groupWIs :: "parts_connection  'i::len simple_rule list  'i wordinterval list list" where
  "groupWIs c rs = (let W = getParts rs in 
                       (let f = (λwi. (map (λd. runFw (getOneIp wi) d c rs) (map getOneIp W),
                                      map (λs. runFw s (getOneIp wi) c rs) (map getOneIp W))) in
                       groupF f W))"



lemma groupWIs_not_empty: "groupWIs c rs  []"
  proof -
    have "getParts rs  []" by(simp add: getParts_def partitioningIps_nonempty)
    with groupF_empty have "f. groupF f (getParts rs)  []" by blast
    thus ?thesis by(simp add: groupWIs_def Let_def) blast
  qed
lemma groupWIs_not_empty_elem: "V  set (groupWIs c rs)  V  []"
  by(simp add: groupWIs_def Let_def groupF_empty_elem)
lemma groupWIs_not_empty_elems: 
  assumes V: "V  set (groupWIs c rs)" and w: "w  set V"
  shows "¬ wordinterval_empty w"
  proof -
    have "wset (concat (groupWIs c rs)). ¬ wordinterval_empty w"
      apply(subst groupWIs_def)
      apply(subst Let_def)+
      apply(subst groupF_concat_set)
      using getParts_nonempty_elems by blast
    from this V w show ?thesis by auto
  qed

lemma groupParts_same_fw_wi0:
    assumes "V  set (groupWIs c rs)"
    shows "w  set (map wordinterval_to_set V). a1  w. a2  w. same_fw_behaviour_one a1 a2 c rs"
proof -
  have "Aset (map wordinterval_to_set (concat (groupWIs c rs))). 
        a1A. a2A. same_fw_behaviour_one a1 a2 c rs"
    apply(subst groupWIs_def)
    apply(subst Let_def)+
    apply(subst set_map)
    apply(subst groupF_concat_set)
    using getParts_same_fw_behaviour same_fw_spec by fastforce
  from this assms show ?thesis by force
qed

lemma groupWIs_same_fw_not: "A  set (groupWIs c rs)  B  set (groupWIs c rs)  
                            A  B 
                             aw  set (map wordinterval_to_set A).
                             bw  set (map wordinterval_to_set B).
                             a  aw. b  bw. ¬ same_fw_behaviour_one a b c rs"
proof -
  assume asm: "A  set (groupWIs c rs)" "B  set (groupWIs c rs)" "A  B"
  from this have b1: "aw  set A. bw  set B.
                  (map (λd. runFw (getOneIp aw) d c rs) (map getOneIp (getParts rs)),
                   map (λs. runFw s (getOneIp aw) c rs) (map getOneIp (getParts rs))) 
                  (map (λd. runFw (getOneIp bw) d c rs) (map getOneIp (getParts rs)),
                   map (λs. runFw s (getOneIp bw) c rs) (map getOneIp (getParts rs)))"
    apply(simp add: groupWIs_def Let_def)
    using groupF_nequality by fastforce
  have same_behave_runFw_not:
        "(map (λd. runFw x1 d c rs) W, map (λs. runFw s x1 c rs) W) 
         (map (λd. runFw x2 d c rs) W, map (λs. runFw s x2 c rs) W) 
         ¬ same_fw_behaviour_one x1 x2 c rs" for x1 x2 W
  by (simp add: same_fw_behaviour_one_def) (blast)
  have "C  set (groupWIs c rs). c  set C. getOneIp c  wordinterval_to_set c"
    apply(simp add: groupWIs_def Let_def)
    using getParts_nonempty_elems groupF_set getOneIp_elem by fastforce
  from this b1 asm have
  "aw  set (map wordinterval_to_set A). bw  set (map wordinterval_to_set B).
   a  aw. b  bw. (map (λd. runFw a d c rs) (map getOneIp (getParts rs)), map (λs. runFw s a c rs) (map getOneIp (getParts rs))) 
    (map (λd. runFw b d c rs) (map getOneIp (getParts rs)), map (λs. runFw s b c rs) (map getOneIp (getParts rs)))"
   by (simp) (blast)
  from this same_behave_runFw_not asm
  have " aw  set (map wordinterval_to_set A). bw  set (map wordinterval_to_set B).
         a  aw. b  bw. ¬ same_fw_behaviour_one a b c rs" by fast
  from this groupParts_same_fw_wi0[of A c rs]  groupParts_same_fw_wi0[of B c rs] asm
  have "aw  set (map wordinterval_to_set A).
        bw  set (map wordinterval_to_set B).
        a  aw. b  bw. ¬ same_fw_behaviour_one a b c rs"
    apply(simp) using same_fw_behaviour_one_equi(3) by blast
  from this groupParts_same_fw_wi0[of A c rs]  groupParts_same_fw_wi0[of B c rs] asm
  show "aw  set (map wordinterval_to_set A).
        bw  set (map wordinterval_to_set B).
        a  aw. b  bw. ¬ same_fw_behaviour_one a b c rs"
    apply(simp) using same_fw_behaviour_one_equi(3) by fast
qed





(*beginning is copy&paste of previous proof*)
lemma groupParts_same_fw_wi1:
  "V  set (groupWIs c rs)  w1  set V. w2  set V.
     a1  wordinterval_to_set w1. a2  wordinterval_to_set w2. same_fw_behaviour_one a1 a2 c rs"
proof -
  assume asm: "V  set (groupWIs c rs)"
  from getParts_same_fw_behaviour same_fw_spec
    have b1: "A  set (map wordinterval_to_set (getParts rs)) . a1  A. a2  A.
              same_fw_behaviour_one a1 a2 c rs" by fast
  from getParts_complete have complete: "(set (map wordinterval_to_set (getParts rs))) = UNIV"
    by(simp add: wordinterval_list_to_set_def)
  from getParts_nonempty_elems have nonempty: "wset (getParts rs). ¬ wordinterval_empty w" by simp

  { fix W x1 x2
    assume a1: "A  set (map wordinterval_to_set W). a1  A. a2  A. same_fw_behaviour_one a1 a2 c rs"
    and a2: "wordinterval_list_to_set W = UNIV"
    and a3: "w  set W. ¬ wordinterval_empty w"
    and a4: "(map (λd. runFw x1 d c rs) (map getOneIp W), map (λs. runFw s x1 c rs) (map getOneIp W)) =
             (map (λd. runFw x2 d c rs) (map getOneIp W), map (λs. runFw s x2 c rs) (map getOneIp W))"
      from a3 a4 getOneIp_elem
        have b1: "B  set (map wordinterval_to_set W). b  B. runFw x1 b c rs = runFw x2 b c rs"
        by fastforce
      from a3 a4 getOneIp_elem
        have b2: "B  set (map wordinterval_to_set W). b  B. runFw b x1 c rs = runFw b x2 c rs"
        by fastforce
      from runFw_sameFw_behave[OF a1 _ b1 b2] a2[unfolded wordinterval_list_to_set_def] have
        "same_fw_behaviour_one x1 x2 c rs" by simp
  } note same_behave_runFw=this

  from same_behave_runFw[OF b1 getParts_complete nonempty]
       groupF_equality[of "(λwi. (map (λd. runFw (getOneIp wi) d c rs) (map getOneIp (getParts rs)),
                             map (λs. runFw s (getOneIp wi) c rs) (map getOneIp (getParts rs))))"
                     "(getParts rs)"] asm
  have b2: "a1set V. a2set V. same_fw_behaviour_one (getOneIp a1) (getOneIp a2) c rs"
    apply(subst (asm) groupWIs_def)
    apply(subst (asm) Let_def)+
    by fast
  from groupWIs_not_empty_elems asm have "w  set V. ¬ wordinterval_empty w" by blast
  from this b2 getOneIp_elem
    have b3: "w1set (map wordinterval_to_set V). w2set (map wordinterval_to_set V). 
           ip1 w1. ip2w2.
           same_fw_behaviour_one ip1 ip2 c rs" by (simp) (blast)
  from groupParts_same_fw_wi0 asm 
    have "Aset (map wordinterval_to_set V). a1 A. a2 A. same_fw_behaviour_one a1 a2 c rs" 
    by metis
  from sameFw_behave_sets[OF this b3]
  show "w1  set V. w2  set V.
   a1  wordinterval_to_set w1. a2  wordinterval_to_set w2. same_fw_behaviour_one a1 a2 c rs"
  by force
qed

lemma groupParts_same_fw_wi2: "V  set (groupWIs c rs) 
                               ip1  wordinterval_list_to_set V.
                               ip2  wordinterval_list_to_set V.
                               same_fw_behaviour_one ip1 ip2 c rs"
  using groupParts_same_fw_wi0 groupParts_same_fw_wi1
  apply (simp add: wordinterval_list_to_set_def)
  by fast

lemma groupWIs_same_fw_not2: "A  set (groupWIs c rs)  B  set (groupWIs c rs)  
                                A  B 
                                ip1  wordinterval_list_to_set A.
                                ip2  wordinterval_list_to_set B.
                                ¬ same_fw_behaviour_one ip1 ip2 c rs"
  apply(simp add: wordinterval_list_to_set_def)
  using groupWIs_same_fw_not by fastforce

(*I like this version -- corny*)
lemma "A  set (groupWIs c rs)  B  set (groupWIs c rs)  
                ip1  wordinterval_list_to_set A.
                ip2  wordinterval_list_to_set B. same_fw_behaviour_one ip1 ip2 c rs
                 A = B"
using groupWIs_same_fw_not2 by blast


lemma groupWIs_complete: "(x set (groupWIs c rs). wordinterval_list_to_set x) = (UNIV::'i::len word set)"
  proof -
  have "( y  (x set (groupWIs c rs). set x). wordinterval_to_set y) = (UNIV::'i word set)"
    apply(simp add: groupWIs_def Let_def groupF_Union_set)
    using getParts_complete wordinterval_list_to_set_def by fastforce
  thus ?thesis by(simp add: wordinterval_list_to_set_def)
qed


(*begin groupWIs1 and groupWIs2 optimization*)
  definition groupWIs1 :: "'a parts_connection_scheme  'i::len simple_rule list  'i wordinterval list list" where
    "groupWIs1 c rs = (let P = getParts rs in
                        (let W = map getOneIp P in 
                         (let f = (λwi. (map (λd. runFw (getOneIp wi) d c rs) W,
                                         map (λs. runFw s (getOneIp wi) c rs) W)) in
                        map (map fst) (groupF snd (map (λx. (x, f x)) P)))))"
  
  lemma groupWIs_groupWIs1_equi: "groupWIs1 c rs = groupWIs c rs"
    apply(subst groupWIs1_def)
    apply(subst groupWIs_def)
  using groupF_tuple by metis
  
  definition simple_conn_matches :: "'i::len simple_match  parts_connection  bool" where
      "simple_conn_matches m c 
        (match_iface (iiface m) (pc_iiface c)) 
        (match_iface (oiface m) (pc_oiface c)) 
        (match_proto (proto m) (pc_proto c)) 
        (simple_match_port (sports m) (pc_sport c)) 
        (simple_match_port (dports m) (pc_dport c))"
  
  lemma simple_conn_matches_simple_match_any: "simple_conn_matches simple_match_any c"
    apply (simp add: simple_conn_matches_def simple_match_any_def match_ifaceAny)
    apply (subgoal_tac "(65535::16 word) = max_word")
     apply (simp only:)
     apply simp_all
    done
  
  lemma has_default_policy_simple_conn_matches:
    "has_default_policy rs  has_default_policy [rrs . simple_conn_matches (match_sel r) c]"
    apply(induction rs rule: has_default_policy.induct)
      apply(simp; fail)
     apply(simp add: simple_conn_matches_simple_match_any; fail)
    apply(simp)
    apply(intro conjI)
     apply(simp split: if_split_asm; fail)
    apply(simp add: has_default_policy_fst split: if_split_asm)
    done
  
  
  lemma filter_conn_fw_lem: 
    "runFw s d c (filter (λr. simple_conn_matches (match_sel r) c) rs) = runFw s d c rs"
    apply(simp add: runFw_def simple_conn_matches_def match_sel_def)
    apply(induction rs "p_iiface = pc_iiface c, p_oiface = pc_oiface c,
                         p_src = s, p_dst = d, p_proto = pc_proto c, 
                         p_sport = pc_sport c, p_dport = pc_dport c,
                         p_tcp_flags = {TCP_SYN},p_payload=''''"
          rule: simple_fw.induct)
    apply(simp add: simple_matches.simps)+
  done
  
  
  (*performance: despite optimization, this function takes quite long and can be optimized*)
  definition groupWIs2 :: "parts_connection  'i::len simple_rule list  'i wordinterval list list" where
    "groupWIs2 c rs =  (let P = getParts rs in
                         (let W = map getOneIp P in 
                         (let filterW = (filter (λr. simple_conn_matches (match_sel r) c) rs) in
                           (let f = (λwi. (map (λd. runFw (getOneIp wi) d c filterW) W,
                                           map (λs. runFw s (getOneIp wi) c filterW) W)) in
                        map (map fst) (groupF snd (map (λx. (x, f x)) P))))))"
  
  lemma groupWIs1_groupWIs2_equi: "groupWIs2 c rs = groupWIs1 c rs"
    by(simp add: groupWIs2_def groupWIs1_def filter_conn_fw_lem)
  
  
  lemma groupWIs_code[code]: "groupWIs c rs = groupWIs2 c rs"
    using groupWIs1_groupWIs2_equi groupWIs_groupWIs1_equi by metis
(*end groupWIs1 and groupWIs2 optimization*)


(*begin groupWIs3 optimization*)
  fun matching_dsts :: "'i::len word  'i simple_rule list  'i wordinterval  'i wordinterval" where
    "matching_dsts _ [] _ = Empty_WordInterval" |
    "matching_dsts s ((SimpleRule m Accept)#rs) acc_dropped =
        (if simple_match_ip (src m) s then
           wordinterval_union (wordinterval_setminus (ipcidr_tuple_to_wordinterval (dst m)) acc_dropped) (matching_dsts s rs acc_dropped)
         else
           matching_dsts s rs acc_dropped)" |
    "matching_dsts s ((SimpleRule m Drop)#rs) acc_dropped =
        (if simple_match_ip (src m) s then
           matching_dsts s rs (wordinterval_union (ipcidr_tuple_to_wordinterval (dst m)) acc_dropped)
         else
           matching_dsts s rs acc_dropped)"
  
  lemma matching_dsts_pull_out_accu:
    "wordinterval_to_set (matching_dsts s rs (wordinterval_union a1 a2)) = wordinterval_to_set (matching_dsts s rs a2) - wordinterval_to_set a1"
    apply(induction s rs a2 arbitrary: a1 a2 rule: matching_dsts.induct)
       apply(simp_all)
    by blast+
  
  (*a copy of matching_dsts*)
  fun matching_srcs :: "'i::len word  'i simple_rule list  'i wordinterval  'i wordinterval" where
    "matching_srcs _ [] _ = Empty_WordInterval" |
    "matching_srcs d ((SimpleRule m Accept)#rs) acc_dropped =
        (if simple_match_ip (dst m) d then
           wordinterval_union (wordinterval_setminus (ipcidr_tuple_to_wordinterval (src m)) acc_dropped) (matching_srcs d rs acc_dropped)
         else
           matching_srcs d rs acc_dropped)" |
    "matching_srcs d ((SimpleRule m Drop)#rs) acc_dropped =
        (if simple_match_ip (dst m) d then
           matching_srcs d rs (wordinterval_union (ipcidr_tuple_to_wordinterval (src m)) acc_dropped)
         else
           matching_srcs d rs acc_dropped)"
  
  lemma matching_srcs_pull_out_accu:
    "wordinterval_to_set (matching_srcs d rs (wordinterval_union a1 a2)) = wordinterval_to_set (matching_srcs d rs a2) - wordinterval_to_set a1"
    apply(induction d rs a2 arbitrary: a1 a2 rule: matching_srcs.induct)
       apply(simp_all)
    by blast+
  
  
  lemma matching_dsts: "r  set rs. simple_conn_matches (match_sel r) c 
          wordinterval_to_set (matching_dsts s rs Empty_WordInterval) = {d. runFw s d c rs = Decision FinalAllow}"
    proof(induction rs)
    case Nil thus ?case by (simp add: runFw_def)
    next
    case (Cons r rs)
      obtain m a where r: "r = SimpleRule m a" by(cases r, blast)
      
      from Cons.prems r have simple_match_ip_Accept: "d. simple_match_ip (src m) s 
        runFw s d c (SimpleRule m Accept # rs) = Decision FinalAllow  simple_match_ip (dst m) d  runFw s d c rs = Decision FinalAllow"
        by(simp add: simple_conn_matches_def runFw_def simple_matches.simps)
  
      { fix d a
        have "¬ simple_match_ip (src m) s 
         runFw s d c (SimpleRule m a # rs) = Decision FinalAllow  runFw s d c rs = Decision FinalAllow"
        apply(cases a)
         by(simp add: simple_conn_matches_def runFw_def simple_matches.simps)+
       } note not_simple_match_ip=this
  
      from Cons.prems r have simple_match_ip_Drop: "d. simple_match_ip (src m) s 
             runFw s d c (SimpleRule m Drop # rs) = Decision FinalAllow  ¬ simple_match_ip (dst m) d  runFw s d c rs = Decision FinalAllow"
        by(simp add: simple_conn_matches_def runFw_def simple_matches.simps)
  
      show ?case
        proof(cases a)
        case Accept with r Cons show ?thesis
         apply(simp, intro conjI impI)
          apply(simp add: simple_match_ip_Accept wordinterval_to_set_ipcidr_tuple_to_wordinterval_simple_match_ip_set)
          apply blast
         apply(simp add: not_simple_match_ip; fail)
         done
        next
        case Drop with r Cons show ?thesis
          apply(simp,intro conjI impI)
           apply(simp add: simple_match_ip_Drop matching_dsts_pull_out_accu wordinterval_to_set_ipcidr_tuple_to_wordinterval_simple_match_ip_set)
           apply blast
          apply(simp add: not_simple_match_ip; fail)
         done
        qed
    qed
  lemma matching_srcs: "r  set rs. simple_conn_matches (match_sel r) c 
          wordinterval_to_set (matching_srcs d rs Empty_WordInterval) = {s. runFw s d c rs = Decision FinalAllow}"
    proof(induction rs)
    case Nil thus ?case by (simp add: runFw_def)
    next
    case (Cons r rs)
      obtain m a where r: "r = SimpleRule m a" by(cases r, blast)
      
      from Cons.prems r have simple_match_ip_Accept: "s. simple_match_ip (dst m) d 
         runFw s d c (SimpleRule m Accept # rs) = Decision FinalAllow 
          simple_match_ip (src m) s  runFw s d c rs = Decision FinalAllow"
        by(simp add: simple_conn_matches_def runFw_def simple_matches.simps)
  
      { fix s a
        have "¬ simple_match_ip (dst m) d 
         runFw s d c (SimpleRule m a # rs) = Decision FinalAllow  runFw s d c rs = Decision FinalAllow"
        apply(cases a)
         by(simp add: simple_conn_matches_def runFw_def simple_matches.simps)+
       } note not_simple_match_ip=this
  
      from Cons.prems r have simple_match_ip_Drop: "s. simple_match_ip (dst m) d 
         runFw s d c (SimpleRule m Drop # rs) = Decision FinalAllow 
          ¬ simple_match_ip (src m) s  runFw s d c rs = Decision FinalAllow"
        by(simp add: simple_conn_matches_def runFw_def simple_matches.simps)
  
      show ?case
        proof(cases a)
        case Accept with r Cons show ?thesis
         apply(simp, intro conjI impI)
          apply(simp add: simple_match_ip_Accept wordinterval_to_set_ipcidr_tuple_to_wordinterval_simple_match_ip_set)
          apply blast
         apply(simp add: not_simple_match_ip; fail)
         done
        next
        case Drop with r Cons show ?thesis
          apply(simp,intro conjI impI)
           apply(simp add: simple_match_ip_Drop matching_srcs_pull_out_accu wordinterval_to_set_ipcidr_tuple_to_wordinterval_simple_match_ip_set)
           apply blast
          apply(simp add: not_simple_match_ip; fail)
         done
        qed
    qed
  
  
  
  (*TODO: if we can get wordinterval_element to log runtime ...*)
  definition groupWIs3_default_policy :: "parts_connection  'i::len simple_rule list  'i wordinterval list list" where
    "groupWIs3_default_policy c rs =  (let P = getParts rs in
                         (let W = map getOneIp P in 
                         (let filterW = (filter (λr. simple_conn_matches (match_sel r) c) rs) in
                           (let f = (λwi. let mtch_dsts = (matching_dsts (getOneIp wi) filterW Empty_WordInterval);
                                              mtch_srcs = (matching_srcs (getOneIp wi) filterW Empty_WordInterval) in 
                                          (map (λd. wordinterval_element d mtch_dsts) W,
                                           map (λs. wordinterval_element s mtch_srcs) W)) in
                        map (map fst) (groupF snd (map (λx. (x, f x)) P))))))"
  
  
  lemma groupWIs3_default_policy_groupWIs2:
  fixes rs :: "'i::len simple_rule list"
  assumes "has_default_policy rs"
  shows "groupWIs2 c rs = groupWIs3_default_policy c rs"
  proof -
    { fix filterW s d
      from matching_dsts[where c=c] have "filterW = filter (λr. simple_conn_matches (match_sel r) c) rs 
           wordinterval_element d (matching_dsts s filterW Empty_WordInterval)  runFw s d c filterW = Decision FinalAllow"
      by force
    } note matching_dsts_filterW=this[simplified]
  
    { fix filterW s d
      from matching_srcs[where c=c] have "filterW = filter (λr. simple_conn_matches (match_sel r) c) rs 
            wordinterval_element s (matching_srcs d filterW Empty_WordInterval)  runFw s d c filterW = Decision FinalAllow"
      by force
    } note matching_srcs_filterW=this[simplified]
  
    { fix W and rs<