Theory IPv6

(*  Title:      IPv6.thy
    Authors:    Cornelius Diekmann
*)
theory IPv6
  imports
    IP_Address
    NumberWang_IPv6
    (* include "HOL-Library.Code_Target_Nat" if you need to work with actual numbers.*)
begin

section ‹IPv6 Addresses›
  text‹An IPv6 address is basically a 128 bit unsigned integer. RFC 4291, Section 2.›
  type_synonym ipv6addr = "128 word"
 
  text‹Conversion between natural numbers and IPv6 adresses›
  definition nat_of_ipv6addr :: "ipv6addr ⇒ nat" where
    "nat_of_ipv6addr a = unat a"
  definition ipv6addr_of_nat :: "nat ⇒ ipv6addr" where
    "ipv6addr_of_nat n =  of_nat n"

  lemma "ipv6addr_of_nat n = word_of_int (int n)"
    by(simp add: ipv6addr_of_nat_def)

  text‹The maximum IPv6 address›
  definition max_ipv6_addr :: "ipv6addr" where 
    "max_ipv6_addr ≡ ipv6addr_of_nat ((2^128) - 1)"

  lemma max_ipv6_addr_number: "max_ipv6_addr = 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF"
    unfolding max_ipv6_addr_def ipv6addr_of_nat_def by(simp)
  lemma "max_ipv6_addr = 340282366920938463463374607431768211455"
    by(fact max_ipv6_addr_number)
  lemma max_ipv6_addr_max_word: "max_ipv6_addr = - 1"
    by(simp add: max_ipv6_addr_number)
  lemma max_ipv6_addr_max: "∀a. a ≤ max_ipv6_addr"
    by(simp add: max_ipv6_addr_max_word)
  lemma UNIV_ipv6addrset: "UNIV = {0 .. max_ipv6_addr}" (*not in the simp set, for a reason*)
    by(simp add: max_ipv6_addr_max_word) fastforce

  text‹identity functions›
  lemma nat_of_ipv6addr_ipv6addr_of_nat_mod: "nat_of_ipv6addr (ipv6addr_of_nat n) = n mod 2^128"
    by (simp add: ipv6addr_of_nat_def nat_of_ipv6addr_def unat_of_nat take_bit_eq_mod)
  lemma nat_of_ipv6addr_ipv6addr_of_nat:
    "n ≤ nat_of_ipv6addr max_ipv6_addr ⟹ nat_of_ipv6addr (ipv6addr_of_nat n) = n"
    by (simp add: nat_of_ipv6addr_ipv6addr_of_nat_mod max_ipv6_addr_def)
  lemma ipv6addr_of_nat_nat_of_ipv6addr: "ipv6addr_of_nat (nat_of_ipv6addr addr) = addr"
    by(simp add: ipv6addr_of_nat_def nat_of_ipv6addr_def)

  subsection‹Syntax of IPv6 Adresses›
  text‹RFC 4291, Section 2.2.: Text Representation of Addresses›

  text‹Quoting the RFC (note: errata exists):›
  text_raw‹
  \begin{verbatim}
   1. The preferred form is x:x:x:x:x:x:x:x, where the 'x's are one to
      four hexadecimal digits of the eight 16-bit pieces of the address.
      Examples:
         ABCD:EF01:2345:6789:ABCD:EF01:2345:6789
         2001:DB8:0:0:8:800:200C:417A
  \end{verbatim}
›
  datatype ipv6addr_syntax = 
    IPv6AddrPreferred "16 word" "16 word" "16 word" "16 word" "16 word" "16 word" "16 word" "16 word"

  text_raw‹
  \begin{verbatim}
   2. [...] In order to make writing addresses containing zero
      bits easier, a special syntax is available to compress the zeros.
      The use of "::" indicates one or more groups of 16 bits of zeros.
      The "::" can only appear once in an address.  The "::" can also be
      used to compress leading or trailing zeros in an address.

      For example, the following addresses
         2001:DB8:0:0:8:800:200C:417A   a unicast address
         FF01:0:0:0:0:0:0:101           a multicast address
         0:0:0:0:0:0:0:1                the loopback address
         0:0:0:0:0:0:0:0                the unspecified address

      may be represented as
         2001:DB8::8:800:200C:417A      a unicast address
         FF01::101                      a multicast address
         ::1                            the loopback address
         ::                             the unspecified address
  \end{verbatim}
›
  (*datatype may take some minutes to load*)
  datatype ipv6addr_syntax_compressed =
  ― ‹using @{typ unit} for the omission @{text "::"}. 

     Naming convention of the datatype: 
      The first number is the position where the omission occurs.
      The second number is the length of the specified address pieces.
        I.e. `8 minus the second number' pieces are omitted.›
    IPv6AddrCompressed1_0 unit
  | IPv6AddrCompressed1_1 unit "16 word"
  | IPv6AddrCompressed1_2 unit "16 word" "16 word"
  | IPv6AddrCompressed1_3 unit "16 word" "16 word" "16 word"
  | IPv6AddrCompressed1_4 unit "16 word" "16 word" "16 word" "16 word" 
  | IPv6AddrCompressed1_5 unit "16 word" "16 word" "16 word" "16 word" "16 word"
  | IPv6AddrCompressed1_6 unit "16 word" "16 word" "16 word" "16 word" "16 word" "16 word"
  | IPv6AddrCompressed1_7 unit "16 word" "16 word" "16 word" "16 word" "16 word" "16 word" "16 word"

  | IPv6AddrCompressed2_1 "16 word" unit
  | IPv6AddrCompressed2_2 "16 word" unit "16 word"
  | IPv6AddrCompressed2_3 "16 word" unit "16 word" "16 word"
  | IPv6AddrCompressed2_4 "16 word" unit "16 word" "16 word" "16 word"
  | IPv6AddrCompressed2_5 "16 word" unit "16 word" "16 word" "16 word" "16 word"
  | IPv6AddrCompressed2_6 "16 word" unit "16 word" "16 word" "16 word" "16 word" "16 word"
  | IPv6AddrCompressed2_7 "16 word" unit "16 word" "16 word" "16 word" "16 word" "16 word" "16 word"

  | IPv6AddrCompressed3_2 "16 word" "16 word" unit
  | IPv6AddrCompressed3_3 "16 word" "16 word" unit "16 word"
  | IPv6AddrCompressed3_4 "16 word" "16 word" unit "16 word" "16 word"
  | IPv6AddrCompressed3_5 "16 word" "16 word" unit "16 word" "16 word" "16 word"
  | IPv6AddrCompressed3_6 "16 word" "16 word" unit "16 word" "16 word" "16 word" "16 word"
  | IPv6AddrCompressed3_7 "16 word" "16 word" unit "16 word" "16 word" "16 word" "16 word" "16 word"

  | IPv6AddrCompressed4_3 "16 word" "16 word" "16 word" unit
  | IPv6AddrCompressed4_4 "16 word" "16 word" "16 word" unit "16 word"
  | IPv6AddrCompressed4_5 "16 word" "16 word" "16 word" unit "16 word" "16 word"
  | IPv6AddrCompressed4_6 "16 word" "16 word" "16 word" unit "16 word" "16 word" "16 word"
  | IPv6AddrCompressed4_7 "16 word" "16 word" "16 word" unit "16 word" "16 word" "16 word" "16 word"

  | IPv6AddrCompressed5_4 "16 word" "16 word" "16 word" "16 word" unit
  | IPv6AddrCompressed5_5 "16 word" "16 word" "16 word" "16 word" unit "16 word"
  | IPv6AddrCompressed5_6 "16 word" "16 word" "16 word" "16 word" unit "16 word" "16 word"
  | IPv6AddrCompressed5_7 "16 word" "16 word" "16 word" "16 word" unit "16 word" "16 word" "16 word"

  | IPv6AddrCompressed6_5 "16 word" "16 word" "16 word" "16 word" "16 word" unit
  | IPv6AddrCompressed6_6 "16 word" "16 word" "16 word" "16 word" "16 word" unit "16 word"
  | IPv6AddrCompressed6_7 "16 word" "16 word" "16 word" "16 word" "16 word" unit "16 word" "16 word"

  | IPv6AddrCompressed7_6 "16 word" "16 word" "16 word" "16 word" "16 word" "16 word" unit
  | IPv6AddrCompressed7_7 "16 word" "16 word" "16 word" "16 word" "16 word" "16 word" unit "16 word"

  | IPv6AddrCompressed8_7 "16 word" "16 word" "16 word" "16 word" "16 word" "16 word" "16 word" unit

  (*RFC 5952:
    """
    4.  A Recommendation for IPv6 Text Representation
    4.2.2.  Handling One 16-Bit 0 Field
       The symbol "::" MUST NOT be used to shorten just one 16-bit 0 field.
       For example, the representation 2001:db8:0:1:1:1:1:1 is correct, but
       2001:db8::1:1:1:1:1 is not correct.
    """

    So we could remove all IPv6AddrCompressed*_7 constructors.
    But these are `recommendations', we might still see these non-recommended definitions.
    "[...] all implementations must accept and be able to handle any legitimate RFC 4291 format."
  *)

  (*More convenient parser helper function for compressed IPv6 addresses:
    Input list (from parser):
      Some 16word ⟶ address piece
      None ⟶ omission '::'
    
  
   Basically, the parser must only do the following (python syntax):
     split the string which is an ipv6 address at ':'
     map empty string to None
     map everything else to Some (string_to_16word str)
     sanitize empty strings at the start and the end (see toString and parser theories)
   Example:
     "1:2:3".split(":")  = ['1', '2', '3']
     ":2:3:4".split(":") = ['', '2', '3', '4']
     ":2::3".split(":")  = ['', '2', '', '3']
     "1:2:3:".split(":") = ['1', '2', '3', '']
  *)
  definition parse_ipv6_address_compressed :: "((16 word) option) list ⇒ ipv6addr_syntax_compressed option" where
    "parse_ipv6_address_compressed as = (case as of 
      [None] ⇒ Some (IPv6AddrCompressed1_0 ())
    | [None, Some a] ⇒ Some (IPv6AddrCompressed1_1 () a)
    | [None, Some a, Some b] ⇒ Some (IPv6AddrCompressed1_2 () a b)
    | [None, Some a, Some b, Some c] ⇒ Some (IPv6AddrCompressed1_3 () a b c)
    | [None, Some a, Some b, Some c, Some d] ⇒ Some (IPv6AddrCompressed1_4 () a b c d)
    | [None, Some a, Some b, Some c, Some d, Some e] ⇒ Some (IPv6AddrCompressed1_5 () a b c d e)
    | [None, Some a, Some b, Some c, Some d, Some e, Some f] ⇒ Some (IPv6AddrCompressed1_6 () a b c d e f)
    | [None, Some a, Some b, Some c, Some d, Some e, Some f, Some g] ⇒ Some (IPv6AddrCompressed1_7 () a b c d e f g)
  
    | [Some a, None] ⇒ Some (IPv6AddrCompressed2_1 a ())
    | [Some a, None, Some b] ⇒ Some (IPv6AddrCompressed2_2 a () b)
    | [Some a, None, Some b, Some c] ⇒ Some (IPv6AddrCompressed2_3 a () b c)
    | [Some a, None, Some b, Some c, Some d] ⇒ Some (IPv6AddrCompressed2_4 a () b c d)
    | [Some a, None, Some b, Some c, Some d, Some e] ⇒ Some (IPv6AddrCompressed2_5 a () b c d e)
    | [Some a, None, Some b, Some c, Some d, Some e, Some f] ⇒ Some (IPv6AddrCompressed2_6 a () b c d e f)
    | [Some a, None, Some b, Some c, Some d, Some e, Some f, Some g] ⇒ Some (IPv6AddrCompressed2_7 a () b c d e f g)
  
    | [Some a, Some b, None] ⇒ Some (IPv6AddrCompressed3_2 a b ())
    | [Some a, Some b, None, Some c] ⇒ Some (IPv6AddrCompressed3_3 a b () c)
    | [Some a, Some b, None, Some c, Some d] ⇒ Some (IPv6AddrCompressed3_4 a b () c d)
    | [Some a, Some b, None, Some c, Some d, Some e] ⇒ Some (IPv6AddrCompressed3_5 a b () c d e)
    | [Some a, Some b, None, Some c, Some d, Some e, Some f] ⇒ Some (IPv6AddrCompressed3_6 a b () c d e f)
    | [Some a, Some b, None, Some c, Some d, Some e, Some f, Some g] ⇒ Some (IPv6AddrCompressed3_7 a b () c d e f g)
  
    | [Some a, Some b, Some c, None] ⇒ Some (IPv6AddrCompressed4_3 a b c ())
    | [Some a, Some b, Some c, None, Some d] ⇒ Some (IPv6AddrCompressed4_4 a b c () d)
    | [Some a, Some b, Some c, None, Some d, Some e] ⇒ Some (IPv6AddrCompressed4_5 a b c () d e)
    | [Some a, Some b, Some c, None, Some d, Some e, Some f] ⇒ Some (IPv6AddrCompressed4_6 a b c () d e f)
    | [Some a, Some b, Some c, None, Some d, Some e, Some f, Some g] ⇒ Some (IPv6AddrCompressed4_7 a b c () d e f g)
  
    | [Some a, Some b, Some c, Some d, None] ⇒ Some (IPv6AddrCompressed5_4 a b c d ())
    | [Some a, Some b, Some c, Some d, None, Some e] ⇒ Some (IPv6AddrCompressed5_5 a b c d () e)
    | [Some a, Some b, Some c, Some d, None, Some e, Some f] ⇒ Some (IPv6AddrCompressed5_6 a b c d () e f)
    | [Some a, Some b, Some c, Some d, None, Some e, Some f, Some g] ⇒ Some (IPv6AddrCompressed5_7 a b c d () e f g)
  
    | [Some a, Some b, Some c, Some d, Some e, None] ⇒ Some (IPv6AddrCompressed6_5 a b c d e ())
    | [Some a, Some b, Some c, Some d, Some e, None, Some f] ⇒ Some (IPv6AddrCompressed6_6 a b c d e () f)
    | [Some a, Some b, Some c, Some d, Some e, None, Some f, Some g] ⇒ Some (IPv6AddrCompressed6_7 a b c d e () f g)
  
    | [Some a, Some b, Some c, Some d, Some e, Some f, None] ⇒ Some (IPv6AddrCompressed7_6 a b c d e f ())
    | [Some a, Some b, Some c, Some d, Some e, Some f, None, Some g] ⇒ Some (IPv6AddrCompressed7_7 a b c d e f () g)

    | [Some a, Some b, Some c, Some d, Some e, Some f, Some g, None] ⇒ Some (IPv6AddrCompressed8_7 a b c d e f g ())
    | _ ⇒ None ― ‹invalid ipv6 copressed address.›
)"

  fun ipv6addr_syntax_compressed_to_list :: "ipv6addr_syntax_compressed ⇒ ((16 word) option) list"
    where 
      "ipv6addr_syntax_compressed_to_list (IPv6AddrCompressed1_0 _) =
                                     [None]"
    | "ipv6addr_syntax_compressed_to_list (IPv6AddrCompressed1_1 () a) =
                                     [None, Some a]"
    | "ipv6addr_syntax_compressed_to_list (IPv6AddrCompressed1_2 () a b) =
                                     [None, Some a, Some b]"
    | "ipv6addr_syntax_compressed_to_list (IPv6AddrCompressed1_3 () a b c) =
                                     [None, Some a, Some b, Some c]"
    | "ipv6addr_syntax_compressed_to_list (IPv6AddrCompressed1_4 () a b c d) =
                                     [None, Some a, Some b, Some c, Some d]"
    | "ipv6addr_syntax_compressed_to_list (IPv6AddrCompressed1_5 () a b c d e) =
                                     [None, Some a, Some b, Some c, Some d, Some e]"
    | "ipv6addr_syntax_compressed_to_list (IPv6AddrCompressed1_6 () a b c d e f) =
                                     [None, Some a, Some b, Some c, Some d, Some e, Some f]"
    | "ipv6addr_syntax_compressed_to_list (IPv6AddrCompressed1_7 () a b c d e f g) =
                                     [None, Some a, Some b, Some c, Some d, Some e, Some f, Some g]"
  
    | "ipv6addr_syntax_compressed_to_list (IPv6AddrCompressed2_1 a ()) =
                                     [Some a, None]"
    | "ipv6addr_syntax_compressed_to_list (IPv6AddrCompressed2_2 a () b) =
                                     [Some a, None, Some b]"
    | "ipv6addr_syntax_compressed_to_list (IPv6AddrCompressed2_3 a () b c) =
                                     [Some a, None, Some b, Some c]"
    | "ipv6addr_syntax_compressed_to_list (IPv6AddrCompressed2_4 a () b c d) =
                                     [Some a, None, Some b, Some c, Some d]"
    | "ipv6addr_syntax_compressed_to_list (IPv6AddrCompressed2_5 a () b c d e) =
                                     [Some a, None, Some b, Some c, Some d, Some e]"
    | "ipv6addr_syntax_compressed_to_list (IPv6AddrCompressed2_6 a () b c d e f) =
                                     [Some a, None, Some b, Some c, Some d, Some e, Some f]"
    | "ipv6addr_syntax_compressed_to_list (IPv6AddrCompressed2_7 a () b c d e f g) =
                                     [Some a, None, Some b, Some c, Some d, Some e, Some f, Some g]"
  
    | "ipv6addr_syntax_compressed_to_list (IPv6AddrCompressed3_2 a b ()) = [Some a, Some b, None]"
    | "ipv6addr_syntax_compressed_to_list (IPv6AddrCompressed3_3 a b () c) =
                                     [Some a, Some b, None, Some c]"
    | "ipv6addr_syntax_compressed_to_list (IPv6AddrCompressed3_4 a b () c d) =
                                     [Some a, Some b, None, Some c, Some d]"
    | "ipv6addr_syntax_compressed_to_list (IPv6AddrCompressed3_5 a b () c d e) =
                                     [Some a, Some b, None, Some c, Some d, Some e]"
    | "ipv6addr_syntax_compressed_to_list (IPv6AddrCompressed3_6 a b () c d e f) =
                                     [Some a, Some b, None, Some c, Some d, Some e, Some f]"
    | "ipv6addr_syntax_compressed_to_list (IPv6AddrCompressed3_7 a b () c d e f g) =
                                     [Some a, Some b, None, Some c, Some d, Some e, Some f, Some g]"
  
    | "ipv6addr_syntax_compressed_to_list (IPv6AddrCompressed4_3 a b c ()) =
                                     [Some a, Some b, Some c, None]"
    | "ipv6addr_syntax_compressed_to_list (IPv6AddrCompressed4_4 a b c () d) =
                                     [Some a, Some b, Some c, None, Some d]"
    | "ipv6addr_syntax_compressed_to_list (IPv6AddrCompressed4_5 a b c () d e) =
                                     [Some a, Some b, Some c, None, Some d, Some e]"
    | "ipv6addr_syntax_compressed_to_list (IPv6AddrCompressed4_6 a b c () d e f) =
                                     [Some a, Some b, Some c, None, Some d, Some e, Some f]"
    | "ipv6addr_syntax_compressed_to_list (IPv6AddrCompressed4_7 a b c () d e f g) =
                                     [Some a, Some b, Some c, None, Some d, Some e, Some f, Some g]"
  
    | "ipv6addr_syntax_compressed_to_list (IPv6AddrCompressed5_4 a b c d ()) =
                                     [Some a, Some b, Some c, Some d, None]"
    | "ipv6addr_syntax_compressed_to_list (IPv6AddrCompressed5_5 a b c d () e) =
                                     [Some a, Some b, Some c, Some d, None, Some e]"
    | "ipv6addr_syntax_compressed_to_list (IPv6AddrCompressed5_6 a b c d () e f) =
                                     [Some a, Some b, Some c, Some d, None, Some e, Some f]"
    | "ipv6addr_syntax_compressed_to_list (IPv6AddrCompressed5_7 a b c d () e f g) =
                                     [Some a, Some b, Some c, Some d, None, Some e, Some f, Some g]"
  
    | "ipv6addr_syntax_compressed_to_list (IPv6AddrCompressed6_5 a b c d e ()) =
                                     [Some a, Some b, Some c, Some d, Some e, None]"
    | "ipv6addr_syntax_compressed_to_list (IPv6AddrCompressed6_6 a b c d e () f) =
                                     [Some a, Some b, Some c, Some d, Some e, None, Some f]"
    | "ipv6addr_syntax_compressed_to_list (IPv6AddrCompressed6_7 a b c d e () f g) =
                                     [Some a, Some b, Some c, Some d, Some e, None, Some f, Some g]"
  
    | "ipv6addr_syntax_compressed_to_list (IPv6AddrCompressed7_6 a b c d e f ()) =
                                     [Some a, Some b, Some c, Some d, Some e, Some f, None]"
    | "ipv6addr_syntax_compressed_to_list (IPv6AddrCompressed7_7 a b c d e f () g) =
                                     [Some a, Some b, Some c, Some d, Some e, Some f, None, Some g]"

    | "ipv6addr_syntax_compressed_to_list (IPv6AddrCompressed8_7 a b c d e f g ()) =
                                     [Some a, Some b, Some c, Some d, Some e, Some f, Some g, None]"


(*for all ipv6_syntax, there is a corresponding list representation*)
lemma parse_ipv6_address_compressed_exists:
  obtains ss where "parse_ipv6_address_compressed ss = Some ipv6_syntax"
proof
  define ss where "ss = ipv6addr_syntax_compressed_to_list ipv6_syntax"
  thus "parse_ipv6_address_compressed ss = Some ipv6_syntax"
    by (cases ipv6_syntax; simp add: parse_ipv6_address_compressed_def)
qed

lemma parse_ipv6_address_compressed_identity:
      "parse_ipv6_address_compressed (ipv6addr_syntax_compressed_to_list (ipv6_syntax)) = Some ipv6_syntax"
  by(cases ipv6_syntax; simp add: parse_ipv6_address_compressed_def)


lemma parse_ipv6_address_compressed_someE:
  assumes "parse_ipv6_address_compressed as = Some ipv6"
  obtains
    "as = [None]" "ipv6 = (IPv6AddrCompressed1_0 ())"  |
    a where "as = [None, Some a]" "ipv6 = (IPv6AddrCompressed1_1 () a)"  |
    a b where "as = [None, Some a, Some b]" "ipv6 = (IPv6AddrCompressed1_2 () a b)"  |
    a b c where "as = [None, Some a, Some b, Some c]" "ipv6 = (IPv6AddrCompressed1_3 () a b c)" |
    a b c d where "as = [None, Some a, Some b, Some c, Some d]" "ipv6 = (IPv6AddrCompressed1_4 () a b c d)" |
    a b c d e where "as = [None, Some a, Some b, Some c, Some d, Some e]" "ipv6 = (IPv6AddrCompressed1_5 () a b c d e)" |
    a b c d e f where "as = [None, Some a, Some b, Some c, Some d, Some e, Some f]" "ipv6 = (IPv6AddrCompressed1_6 () a b c d e f)" |
    a b c d e f g where "as = [None, Some a, Some b, Some c, Some d, Some e, Some f, Some g]" "ipv6 = (IPv6AddrCompressed1_7 () a b c d e f g)" |
  
    a where "as = [Some a, None]" "ipv6 = (IPv6AddrCompressed2_1 a ())" |
    a b where "as = [Some a, None, Some b]" "ipv6 = (IPv6AddrCompressed2_2 a () b)" |
    a b c where "as = [Some a, None, Some b, Some c]" "ipv6 = (IPv6AddrCompressed2_3 a () b c)" |
    a b c d where "as = [Some a, None, Some b, Some c, Some d]" "ipv6 = (IPv6AddrCompressed2_4 a () b c d)" |
    a b c d e where "as = [Some a, None, Some b, Some c, Some d, Some e]" "ipv6 = (IPv6AddrCompressed2_5 a () b c d e)" |
    a b c d e f where "as = [Some a, None, Some b, Some c, Some d, Some e, Some f]" "ipv6 = (IPv6AddrCompressed2_6 a () b c d e f)" |
    a b c d e f g where "as = [Some a, None, Some b, Some c, Some d, Some e, Some f, Some g]" "ipv6 = (IPv6AddrCompressed2_7 a () b c d e f g)" |
  
    a b where "as = [Some a, Some b, None]" "ipv6 = (IPv6AddrCompressed3_2 a b ())" |
    a b c where "as = [Some a, Some b, None, Some c]" "ipv6 = (IPv6AddrCompressed3_3 a b () c)" |
    a b c d where "as = [Some a, Some b, None, Some c, Some d]" "ipv6 = (IPv6AddrCompressed3_4 a b () c d)" |
    a b c d e where "as = [Some a, Some b, None, Some c, Some d, Some e]" "ipv6 = (IPv6AddrCompressed3_5 a b () c d e)" |
    a b c d e f where "as = [Some a, Some b, None, Some c, Some d, Some e, Some f]" "ipv6 = (IPv6AddrCompressed3_6 a b () c d e f)" |
    a b c d e f g where "as = [Some a, Some b, None, Some c, Some d, Some e, Some f, Some g]" "ipv6 = (IPv6AddrCompressed3_7 a b () c d e f g)" |
  
    a b c where "as = [Some a, Some b, Some c, None]" "ipv6 = (IPv6AddrCompressed4_3 a b c ())" |
    a b c d where "as = [Some a, Some b, Some c, None, Some d]" "ipv6 = (IPv6AddrCompressed4_4 a b c () d)" |
    a b c d e where "as = [Some a, Some b, Some c, None, Some d, Some e]" "ipv6 = (IPv6AddrCompressed4_5 a b c () d e)" |
    a b c d e f where "as = [Some a, Some b, Some c, None, Some d, Some e, Some f]" "ipv6 = (IPv6AddrCompressed4_6 a b c () d e f)" |
    a b c d e f g where "as = [Some a, Some b, Some c, None, Some d, Some e, Some f, Some g]" "ipv6 = (IPv6AddrCompressed4_7 a b c () d e f g)" |
  
    a b c d where "as = [Some a, Some b, Some c, Some d, None]" "ipv6 = (IPv6AddrCompressed5_4 a b c d ())" |
    a b c d e where "as = [Some a, Some b, Some c, Some d, None, Some e]" "ipv6 = (IPv6AddrCompressed5_5 a b c d () e)" |
    a b c d e f where "as = [Some a, Some b, Some c, Some d, None, Some e, Some f]" "ipv6 = (IPv6AddrCompressed5_6 a b c d () e f)" |
    a b c d e f g where "as = [Some a, Some b, Some c, Some d, None, Some e, Some f, Some g]" "ipv6 = (IPv6AddrCompressed5_7 a b c d () e f g)" |
  
    a b c d e where "as = [Some a, Some b, Some c, Some d, Some e, None]" "ipv6 = (IPv6AddrCompressed6_5 a b c d e ())" |
    a b c d e f where "as = [Some a, Some b, Some c, Some d, Some e, None, Some f]" "ipv6 = (IPv6AddrCompressed6_6 a b c d e () f)" |
    a b c d e f g where "as = [Some a, Some b, Some c, Some d, Some e, None, Some f, Some g]" "ipv6 = (IPv6AddrCompressed6_7 a b c d e () f g)" |
  
    a b c d e f where "as = [Some a, Some b, Some c, Some d, Some e, Some f, None]" "ipv6 = (IPv6AddrCompressed7_6 a b c d e f ())" |
    a b c d e f g where "as = [Some a, Some b, Some c, Some d, Some e, Some f, None, Some g]" "ipv6 = (IPv6AddrCompressed7_7 a b c d e f () g)" |

    a b c d e f g where "as = [Some a, Some b, Some c, Some d, Some e, Some f, Some g, None]" "ipv6 = (IPv6AddrCompressed8_7 a b c d e f g ())"
using assms
unfolding parse_ipv6_address_compressed_def
by (auto split: list.split_asm option.split_asm) (* takes a minute *)

lemma parse_ipv6_address_compressed_identity2:
      "ipv6addr_syntax_compressed_to_list ipv6_syntax = ls ⟷
        (parse_ipv6_address_compressed ls) = Some ipv6_syntax"
      (is "?lhs = ?rhs")
proof
  assume ?rhs
  thus ?lhs
    by (auto elim: parse_ipv6_address_compressed_someE)
next
  assume ?lhs
  thus ?rhs
    by (cases ipv6_syntax) (auto simp: parse_ipv6_address_compressed_def)
qed

text‹Valid IPv6 compressed notation:
  ▪ at most one omission
  ▪ at most 7 pieces
›
lemma RFC_4291_format: "parse_ipv6_address_compressed as ≠ None ⟷
       length (filter (λp. p = None) as) = 1 ∧ length (filter (λp. p ≠ None) as) ≤ 7"
       (is "?lhs = ?rhs")
proof
  assume ?lhs
  then obtain addr where "parse_ipv6_address_compressed as = Some addr"
    by blast
  thus ?rhs
    by (elim parse_ipv6_address_compressed_someE; simp)
next
  assume ?rhs
  thus ?lhs
    unfolding parse_ipv6_address_compressed_def
    by (auto split: option.split list.split if_split_asm)
qed

  text_raw‹
  \begin{verbatim}
  3. An alternative form that is sometimes more convenient when dealing
      with a mixed environment of IPv4 and IPv6 nodes is
      x:x:x:x:x:x:d.d.d.d, where the 'x's are the hexadecimal values of
      the six high-order 16-bit pieces of the address, and the 'd's are
      the decimal values of the four low-order 8-bit pieces of the
      address (standard IPv4 representation).  Examples:

         0:0:0:0:0:0:13.1.68.3
         0:0:0:0:0:FFFF:129.144.52.38

      or in compressed form:

         ::13.1.68.3
         ::FFFF:129.144.52.38
  \end{verbatim}

  This is currently not supported by our library!
›
  (*TODO*)
  (*TODO: oh boy, they can also be compressed*)

  subsection‹Semantics›

  context
    includes bit_operations_syntax
  begin

  fun ipv6preferred_to_int :: "ipv6addr_syntax ⇒ ipv6addr" where
    "ipv6preferred_to_int (IPv6AddrPreferred a b c d e f g h) = (ucast a << (16 * 7)) OR
                                                                (ucast b << (16 * 6)) OR
                                                                (ucast c << (16 * 5)) OR
                                                                (ucast d << (16 * 4)) OR
                                                                (ucast e << (16 * 3)) OR
                                                                (ucast f << (16 * 2)) OR
                                                                (ucast g << (16 * 1)) OR
                                                                (ucast h << (16 * 0))"

  lemma "ipv6preferred_to_int (IPv6AddrPreferred 0x2001 0xDB8 0x0 0x0 0x8 0x800 0x200C 0x417A) = 
          42540766411282592856906245548098208122" by eval

  lemma "ipv6preferred_to_int (IPv6AddrPreferred 0xFF01 0x0 0x0 0x0 0x0 0x0 0x0 0x101) = 
          338958331222012082418099330867817087233" by eval

  declare ipv6preferred_to_int.simps[simp del]

  definition int_to_ipv6preferred :: "ipv6addr ⇒ ipv6addr_syntax" where
    "int_to_ipv6preferred i = IPv6AddrPreferred (ucast ((i AND 0xFFFF0000000000000000000000000000) >> 16*7))
                                                (ucast ((i AND 0xFFFF000000000000000000000000) >> 16*6))
                                                (ucast ((i AND 0xFFFF00000000000000000000) >> 16*5))
                                                (ucast ((i AND 0xFFFF0000000000000000) >> 16*4))
                                                (ucast ((i AND 0xFFFF000000000000) >> 16*3))
                                                (ucast ((i AND 0xFFFF00000000) >> 16*2))
                                                (ucast ((i AND 0xFFFF0000) >> 16*1))
                                                (ucast ((i AND 0xFFFF)))"

  lemma "int_to_ipv6preferred 42540766411282592856906245548098208122 =
         IPv6AddrPreferred 0x2001 0xDB8 0x0 0x0 0x8 0x800 0x200C 0x417A" by eval

  lemma word128_masks_ipv6pieces:
    "(0xFFFF0000000000000000000000000000::ipv6addr) = (mask 16) << 112"
    "(0xFFFF000000000000000000000000::ipv6addr) = (mask 16) << 96"
    "(0xFFFF00000000000000000000::ipv6addr) = (mask 16) << 80"
    "(0xFFFF0000000000000000::ipv6addr) = (mask 16) << 64"
    "(0xFFFF000000000000::ipv6addr) = (mask 16) << 48"
    "(0xFFFF00000000::ipv6addr) = (mask 16) << 32"
    "(0xFFFF0000::ipv6addr) = (mask 16) << 16"
    "(0xFFFF::ipv6addr) = (mask 16)"
    by (simp_all add: mask_eq)


  text‹Correctness: round trip property one›

  lemma ipv6preferred_to_int_int_to_ipv6preferred:
    "ipv6preferred_to_int (int_to_ipv6preferred ip) = ip"
  proof -
    have and_mask_shift_helper: "w AND (mask m << n) >> n << n = w AND (mask m << n)"
      for m n::nat and w::ipv6addr
      by (metis is_aligned_shift is_aligned_shiftr_shiftl shiftr_and_eq_shiftl)
    have ucast_ipv6_piece_rule:
      "length (dropWhile Not (to_bl w)) ≤ 16 ⟹ (ucast::16 word ⇒ 128 word) ((ucast::128 word ⇒ 16 word) w) = w"
      for w::ipv6addr 
      by(rule ucast_short_ucast_long_ingoreLeadingZero) (simp_all)
    have ucast_ipv6_piece: "16 ≤ 128 - n ⟹ 
      (ucast::16 word ⇒ 128 word) ((ucast::128 word ⇒ 16 word) (w AND (mask 16 << n) >> n)) << n = w AND (mask 16 << n)"
      for w::ipv6addr and n::nat
      apply(subst ucast_ipv6_piece_rule)
       apply(rule length_drop_mask_inner)
       apply(simp; fail)
      apply(subst and_mask_shift_helper)
      apply simp
      done

    have ucast16_ucast128_masks_highest_bits:
      "(ucast ((ucast::ipv6addr ⇒ 16 word) (ip AND 0xFFFF0000000000000000000000000000 >> 112)) << 112) = 
             (ip AND 0xFFFF0000000000000000000000000000)"
      "(ucast ((ucast::ipv6addr ⇒ 16 word) (ip AND 0xFFFF000000000000000000000000 >> 96)) << 96) =
           ip AND 0xFFFF000000000000000000000000"
      "(ucast ((ucast::ipv6addr ⇒ 16 word) (ip AND 0xFFFF00000000000000000000 >> 80)) << 80) =
           ip AND 0xFFFF00000000000000000000" 
      "(ucast ((ucast::ipv6addr ⇒ 16 word) (ip AND 0xFFFF0000000000000000 >> 64)) << 64) =
           ip AND 0xFFFF0000000000000000"
      "(ucast ((ucast::ipv6addr ⇒ 16 word) (ip AND 0xFFFF000000000000 >> 48)) << 48) =
           ip AND 0xFFFF000000000000"
      "(ucast ((ucast::ipv6addr ⇒ 16 word) (ip AND 0xFFFF00000000 >> 32)) << 32) =
           ip AND 0xFFFF00000000"
      "(ucast ((ucast::ipv6addr ⇒ 16 word) (ip AND 0xFFFF0000 >> 16)) << 16) =
           ip AND 0xFFFF0000"
            apply (simp_all only: word128_masks_ipv6pieces ucast_ipv6_piece and_mask2 word_size bit_eq_iff bit_simps comp_def)
      apply auto
      done

    have ucast16_ucast128_masks_highest_bits0: 
      "(ucast ((ucast::ipv6addr ⇒ 16 word) (ip AND 0xFFFF))) = ip AND 0xFFFF"
      apply (simp only: word128_masks_ipv6pieces flip: take_bit_eq_mask)
      apply (simp add: unsigned_ucast_eq)
      done

    have mask_len_word:"n = (LENGTH('a)) ⟹ w AND mask n = w"
      for n and w::"'a::len word" by (simp add: mask_eq_iff) 

    have ipv6addr_16word_pieces_compose_or:
            "ip && (mask 16 << 112) ||
             ip && (mask 16 << 96) ||
             ip && (mask 16 << 80) ||
             ip && (mask 16 << 64) ||
             ip && (mask 16 << 48) ||
             ip && (mask 16 << 32) ||
             ip && (mask 16 << 16) ||
             ip && mask 16 =
             ip"
      apply(subst word_ao_dist2[symmetric])+
      apply(simp add: mask_numeral)
      apply(subst mask128)
      apply(rule mask_len_word)
      apply simp
      done

    show ?thesis
      apply (simp add: ipv6preferred_to_int.simps int_to_ipv6preferred_def shiftl_def shiftr_def)
      apply (simp only: word128_masks_ipv6pieces flip: take_bit_eq_mask)
      apply (simp add: unsigned_ucast_eq push_bit_take_bit)
      using ipv6addr_16word_pieces_compose_or
      apply (simp add: take_bit_push_bit slice_eq_mask)
      apply (simp add: take_bit_eq_mask shiftl_def push_bit_mask_eq)
      done
  qed

  text‹Correctness: round trip property two›
  lemma int_to_ipv6preferred_ipv6preferred_to_int: "int_to_ipv6preferred (ipv6preferred_to_int ip) = ip"
  proof -
    note ucast_shift_simps=helper_masked_ucast_generic helper_masked_ucast_reverse_generic
                           helper_masked_ucast_generic[where n=0, simplified]
                           helper_masked_ucast_equal_generic 
    note ucast_simps=helper_masked_ucast_reverse_generic[where m=0, simplified]
                     helper_masked_ucast_equal_generic[where n=0, simplified]
    show ?thesis
    apply (cases ip, rename_tac a b c d e f g h)
    apply (simp add: ipv6preferred_to_int.simps int_to_ipv6preferred_def)
    apply (simp add: word128_masks_ipv6pieces)
      apply (simp add: word_ao_dist ucast_shift_simps ucast_simps)
      done
  qed


text‹compressed to preferred format›
fun ipv6addr_c2p :: "ipv6addr_syntax_compressed ⇒ ipv6addr_syntax" where
    "ipv6addr_c2p (IPv6AddrCompressed1_0 ()) = IPv6AddrPreferred 0 0 0 0 0 0 0 0"
  | "ipv6addr_c2p (IPv6AddrCompressed1_1 () h) = IPv6AddrPreferred 0 0 0 0 0 0 0 h"
  | "ipv6addr_c2p (IPv6AddrCompressed1_2 () g h) = IPv6AddrPreferred 0 0 0 0 0 0 g h"
  | "ipv6addr_c2p (IPv6AddrCompressed1_3 () f g h) = IPv6AddrPreferred 0 0 0 0 0 f g h"
  | "ipv6addr_c2p (IPv6AddrCompressed1_4 () e f g h) = IPv6AddrPreferred 0 0 0 0 e f g h"
  | "ipv6addr_c2p (IPv6AddrCompressed1_5 () d e f g h) = IPv6AddrPreferred 0 0 0 d e f g h"
  | "ipv6addr_c2p (IPv6AddrCompressed1_6 () c d e f g h) = IPv6AddrPreferred 0 0 c d e f g h"
  | "ipv6addr_c2p (IPv6AddrCompressed1_7 () b c d e f g h) = IPv6AddrPreferred 0 b c d e f g h"

  | "ipv6addr_c2p (IPv6AddrCompressed2_1 a ()) = IPv6AddrPreferred a 0 0 0 0 0 0 0"
  | "ipv6addr_c2p (IPv6AddrCompressed2_2 a () h) = IPv6AddrPreferred a 0 0 0 0 0 0 h"
  | "ipv6addr_c2p (IPv6AddrCompressed2_3 a () g h) = IPv6AddrPreferred a 0 0 0 0 0 g h"
  | "ipv6addr_c2p (IPv6AddrCompressed2_4 a () f g h) = IPv6AddrPreferred a 0 0 0 0 f g h"
  | "ipv6addr_c2p (IPv6AddrCompressed2_5 a () e f g h) = IPv6AddrPreferred a 0 0 0 e f g h"
  | "ipv6addr_c2p (IPv6AddrCompressed2_6 a () d e f g h) = IPv6AddrPreferred a 0 0 d e f g h"
  | "ipv6addr_c2p (