Theory IpAddresses

theory IpAddresses
imports IP_Addresses.IP_Address_toString
  IP_Addresses.CIDR_Split
  "../Common/WordInterval_Lists"
begin




― ‹Misc›
(*we dont't have an empty ip space, but a space which only contains the 0 address. We will use the option type to denote the empty space in some functions.*)
lemma "ipset_from_cidr (ipv4addr_of_dotdecimal (0, 0, 0, 0)) 33 = {0}"
  by(simp add: ipv4addr_of_dotdecimal.simps ipv4addr_of_nat_def ipset_from_cidr_large_pfxlen)
  

  (*helper we use for spoofing protection specification*)
  definition all_but_those_ips :: "('i::len word × nat) list ⇒ ('i word × nat) list" where
    "all_but_those_ips cidrips = cidr_split (wordinterval_invert (l2wi (map ipcidr_to_interval cidrips)))"
  
  lemma all_but_those_ips:
    "ipcidr_union_set (set (all_but_those_ips cidrips)) =
      UNIV - (⋃ (ip,n) ∈ set cidrips. ipset_from_cidr ip n)"
    apply(simp add: )
    unfolding ipcidr_union_set_uncurry all_but_those_ips_def
    apply(simp add: cidr_split_prefix)
    apply(simp add: l2wi)
    apply(simp add: ipcidr_to_interval_def)
    using ipset_from_cidr_ipcidr_to_interval by blast
  

section‹IPv4 Addresses›



subsection‹IPv4 Addresses in IPTables Notation (how we parse it)›
  context
    notes [[typedef_overloaded]]
  begin
    datatype 'i ipt_iprange =
                          ― ‹Singleton IP Address›
                          IpAddr "'i::len word"
  
                          ― ‹CIDR notation: addr/xx›
                          | IpAddrNetmask "'i word" nat
  
                          ― ‹-m iprange --src-range a.b.c.d-e.f.g.h›
                          | IpAddrRange  "'i word" "'i word"
                              (*the range is inclusive*)
  end  
  
  fun ipt_iprange_to_set :: "'i::len ipt_iprange ⇒ 'i word set" where
    "ipt_iprange_to_set (IpAddrNetmask base m) = ipset_from_cidr base m" |
    "ipt_iprange_to_set (IpAddr ip) = { ip }" |
    "ipt_iprange_to_set (IpAddrRange ip1 ip2) = { ip1 .. ip2 }"
  
  text‹@{term ipt_iprange_to_set} can only represent an empty set if it is an empty range.›
  lemma ipt_iprange_to_set_nonempty: "ipt_iprange_to_set ip = {} ⟷ 
    (∃ip1 ip2. ip = IpAddrRange ip1 ip2 ∧ ip1 > ip2)"
    apply(cases ip)
      apply(simp; fail)
     apply(simp add: ipset_from_cidr_alt bitmagic_zeroLast_leq_or1Last; fail)
    apply(simp add:linorder_not_le; fail)
    done
  
  text‹maybe this is necessary as code equation?›
  lemma element_ipt_iprange_to_set[code_unfold]: "(addr::'i::len word) ∈ ipt_iprange_to_set X = (
    case X of (IpAddrNetmask pre len) ⇒
                  (pre AND ((mask len) << (len_of (TYPE('i)) - len))) ≤ addr ∧
                  addr ≤ pre OR (mask (len_of (TYPE('i)) - len))
    | IpAddr ip ⇒ (addr = ip)
    | IpAddrRange ip1 ip2 ⇒ ip1 ≤ addr ∧ ip2 ≥ addr)"
  apply(cases X)
    apply(simp; fail)
   apply(simp add: ipset_from_cidr_alt; fail)
  apply(simp; fail)
  done

  
  lemma ipt_iprange_to_set_uncurry_IpAddrNetmask:
    "ipt_iprange_to_set (uncurry IpAddrNetmask a) = uncurry ipset_from_cidr a"
    by(simp split: uncurry_splits)
  

  text‹IP address ranges to ‹(start, end)› notation›
  fun ipt_iprange_to_interval :: "'i::len ipt_iprange ⇒ ('i word × 'i word)" where
    "ipt_iprange_to_interval (IpAddr addr) = (addr, addr)" |
    "ipt_iprange_to_interval (IpAddrNetmask pre len) = ipcidr_to_interval (pre, len)" |
    "ipt_iprange_to_interval (IpAddrRange ip1 ip2) = (ip1, ip2)"
  
  lemma ipt_iprange_to_interval: "ipt_iprange_to_interval ip = (s,e) ⟹ {s .. e} = ipt_iprange_to_set ip"
    apply(cases ip)
      apply(auto simp add: ipcidr_to_interval)
    done


  text‹A list of IP address ranges to a @{typ "'i::len wordinterval"}.
        The nice thing is: the usual set operations are defined on this type.
        We can use the existing function @{const l2wi_intersect} if we want the intersection of the supplied list›
  lemma "wordinterval_to_set (l2wi_intersect (map ipt_iprange_to_interval ips)) =
            (⋂ ip ∈ set ips. ipt_iprange_to_set ip)"
    apply(simp add: l2wi_intersect)
    using ipt_iprange_to_interval by blast
  
  text‹We can use @{const l2wi} if we want the union of the supplied list›
  lemma "wordinterval_to_set (l2wi (map ipt_iprange_to_interval ips)) = (⋃ ip ∈ set ips. ipt_iprange_to_set ip)"
    apply(simp add: l2wi)
    using ipt_iprange_to_interval by blast

  text‹A list of (negated) IP address to a @{typ "'i::len wordinterval"}.›
  definition ipt_iprange_negation_type_to_br_intersect ::
    "'i::len ipt_iprange negation_type list ⇒ 'i wordinterval" where
    "ipt_iprange_negation_type_to_br_intersect l = l2wi_negation_type_intersect (NegPos_map ipt_iprange_to_interval l)" 

  lemma ipt_iprange_negation_type_to_br_intersect: "wordinterval_to_set (ipt_iprange_negation_type_to_br_intersect l) =
      (⋂ ip ∈ set (getPos l). ipt_iprange_to_set ip) - (⋃ ip ∈ set (getNeg l). ipt_iprange_to_set ip)"
    apply(simp add: ipt_iprange_negation_type_to_br_intersect_def l2wi_negation_type_intersect NegPos_map_simps)
    using ipt_iprange_to_interval by blast

  text‹The @{typ "'i::len wordinterval"} can be translated back into a list of IP ranges.
        If a list of intervals is enough, we can use @{const wi2l}.
        If we need it in @{typ "'i::len ipt_iprange"}, we can use this function.›
  definition wi_2_cidr_ipt_iprange_list :: "'i::len wordinterval ⇒ 'i ipt_iprange list" where
    "wi_2_cidr_ipt_iprange_list r = map (uncurry IpAddrNetmask) (cidr_split r)"

  lemma wi_2_cidr_ipt_iprange_list:
    "(⋃ ip ∈ set (wi_2_cidr_ipt_iprange_list r). ipt_iprange_to_set ip) = wordinterval_to_set r"
    proof -
    have "(⋃ ip ∈ set (wi_2_cidr_ipt_iprange_list r). ipt_iprange_to_set ip) =
           (⋃x∈set (cidr_split r). uncurry ipset_from_cidr x)"
      unfolding wi_2_cidr_ipt_iprange_list_def by force
    thus ?thesis using cidr_split_prefix by metis
  qed

  text‹For example, this allows the following transformation›
  definition ipt_iprange_compress :: "'i::len ipt_iprange negation_type list ⇒ 'i ipt_iprange list" where
    "ipt_iprange_compress = wi_2_cidr_ipt_iprange_list ∘ ipt_iprange_negation_type_to_br_intersect"

  lemma ipt_iprange_compress: "(⋃ ip ∈ set (ipt_iprange_compress l). ipt_iprange_to_set ip) =
      (⋂ ip ∈ set (getPos l). ipt_iprange_to_set ip) - (⋃ ip ∈ set (getNeg l). ipt_iprange_to_set ip)"
    by (metis wi_2_cidr_ipt_iprange_list comp_apply ipt_iprange_compress_def ipt_iprange_negation_type_to_br_intersect)
  
  definition normalized_cidr_ip :: "'i::len ipt_iprange ⇒ bool" where
    "normalized_cidr_ip ip ≡ case ip of IpAddrNetmask _ _ ⇒ True | _ ⇒ False"

  lemma wi_2_cidr_ipt_iprange_list_normalized_IpAddrNetmask: 
    "∀a'∈set (wi_2_cidr_ipt_iprange_list as). normalized_cidr_ip a'"
    apply(clarify)
    apply(simp add: wi_2_cidr_ipt_iprange_list_def normalized_cidr_ip_def)
    by force

  lemma ipt_iprange_compress_normalized_IpAddrNetmask:
    "∀a'∈set (ipt_iprange_compress as). normalized_cidr_ip a'"
    by(simp add: ipt_iprange_compress_def wi_2_cidr_ipt_iprange_list_normalized_IpAddrNetmask)


  
  definition ipt_iprange_to_cidr :: "'i::len ipt_iprange ⇒ ('i word × nat) list" where
    "ipt_iprange_to_cidr ips = cidr_split (iprange_interval (ipt_iprange_to_interval ips))"

  lemma ipt_ipvange_to_cidr: "ipcidr_union_set (set (ipt_iprange_to_cidr ips)) = (ipt_iprange_to_set ips)"
    apply(simp add: ipt_iprange_to_cidr_def)
    apply(simp add: ipcidr_union_set_uncurry)
    apply(case_tac "(ipt_iprange_to_interval ips)")
    apply(simp add: ipt_iprange_to_interval cidr_split_prefix_single)
    done
    



(* actually, these are toString pretty printing helpers*)
definition interval_to_wi_to_ipt_iprange :: "'i::len word ⇒ 'i word ⇒ 'i ipt_iprange" where
  "interval_to_wi_to_ipt_iprange s e ≡
    if s = e
    then IpAddr s
    else case cidr_split (WordInterval s e) of [(ip,nmask)] ⇒ IpAddrNetmask ip nmask
                                            |   _ ⇒ IpAddrRange s e"

lemma interval_to_wi_to_ipt_ipv4range: "ipt_iprange_to_set (interval_to_wi_to_ipt_iprange s e) = {s..e}"
  proof -
    from cidr_split_prefix_single[of s e] have
      "cidr_split (WordInterval s e) = [(a, b)] ⟹ ipset_from_cidr a b = {s..e}" for a b
        by(simp add: iprange_interval.simps)
    thus ?thesis 
      by(simp add: interval_to_wi_to_ipt_iprange_def split: list.split)
  qed

fun wi_to_ipt_iprange :: "'i::len wordinterval ⇒ 'i ipt_iprange list" where
  "wi_to_ipt_iprange (WordInterval s e) = (if s > e then [] else 
      [interval_to_wi_to_ipt_iprange s e])" |
  "wi_to_ipt_iprange (RangeUnion a b) = wi_to_ipt_iprange a @ wi_to_ipt_iprange b"

lemma wi_to_ipt_ipv4range: "⋃(set (map ipt_iprange_to_set (wi_to_ipt_iprange wi))) = wordinterval_to_set wi"
  apply(induction wi)
   apply(simp add: interval_to_wi_to_ipt_ipv4range)
  apply(simp)
  done

end