# Theory IPv6

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

text‹An IPv6 address is basically a 128 bit unsigned integer. RFC 4291, Section 2.›

text‹Conversion between natural numbers and IPv6 adresses›

lemma

lemma UNIV_ipv6addrset:  (*not in the simp set, for a reason*)

text‹identity functions›

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
Examples:
ABCD:EF01:2345:6789:ABCD:EF01:2345:6789
2001:DB8:0:0:8:800:200C:417A
\end{verbatim}
›
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

may be represented as
\end{verbatim}
›
(*datatype may take some minutes to load*)
― ‹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_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_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):
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', '']
*)
"parse_ipv6_address_compressed as = (case as of
| [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.›
)"

where
[None]"
[None, Some a]"
[None, Some a, Some b]"
[None, Some a, Some b, Some c]"
[None, Some a, Some b, Some c, Some d]"
[None, Some a, Some b, Some c, Some d, Some e]"
[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]"

[Some a, None]"
[Some a, None, Some b]"
[Some a, None, Some b, Some c]"
[Some a, None, Some b, Some c, Some d]"
[Some a, None, Some b, Some c, Some d, Some e]"
[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]"
[Some a, Some b, None, Some c]"
[Some a, Some b, None, Some c, Some d]"
[Some a, Some b, None, Some c, Some d, Some e]"
[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]"

[Some a, Some b, Some c, None]"
[Some a, Some b, Some c, None, Some d]"
[Some a, Some b, Some c, None, Some d, Some e]"
[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]"

[Some a, Some b, Some c, Some d, None]"
[Some a, Some b, Some c, Some d, None, Some e]"
[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]"

[Some a, Some b, Some c, Some d, Some e, None]"
[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]"

[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*)
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"
qed

assumes
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
by (auto split: list.split_asm option.split_asm) (* takes a minute *)

(is "?lhs = ?rhs")
proof
assume ?rhs
thus ?lhs
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
›
length (filter (λp. p = None) as) = 1  length (filter (λp. p  None) as)  7"
(is "?lhs = ?rhs")
proof
assume ?lhs
by blast
thus ?rhs
next
assume ?rhs
thus ?lhs
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

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 ::  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 ::  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

text‹Correctness: round trip property one›

lemma ipv6preferred_to_int_int_to_ipv6preferred:

proof -
have and_mask_shift_helper: "w AND (mask m << n) >> n << n = w AND (mask m << n)"
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"
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)"
apply(subst ucast_ipv6_piece_rule)
apply(simp; fail)
apply simp
done

"(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 auto
done

"(ucast ((ucast::ipv6addr  16 word) (ip AND 0xFFFF))) = ip AND 0xFFFF"
done

"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"
apply(subst word_ao_dist2[symmetric])+
apply simp
done

show ?thesis
apply (simp add: ipv6preferred_to_int.simps int_to_ipv6preferred_def shiftl_def shiftr_def)
done
qed

text‹Correctness: round trip property two›
lemma int_to_ipv6preferred_ipv6preferred_to_int:
proof -
show ?thesis
apply (cases ip, rename_tac a b c d e f g h)
apply (simp add: word_ao_dist ucast_shift_simps ucast_simps)
done
qed

text‹compressed to preferred format›