Theory NumberWang_IPv6
theory NumberWang_IPv6
imports
Word_Lib.Word_Lemmas
Word_Lib.Word_Syntax
Word_Lib.Reversed_Bit_Lists
begin
section‹Helper Lemmas for Low-Level Operations on Machine Words›
text‹Needed for IPv6 Syntax›
lemma length_drop_bl: "length (dropWhile Not (to_bl (of_bl bs))) ≤ length bs"
proof -
have length_takeWhile_Not_replicate_False:
"length (takeWhile Not (replicate n False @ ls)) = n + length (takeWhile Not ls)"
for n ls by(subst takeWhile_append2) simp+
show ?thesis by(simp add: word_rep_drop dropWhile_eq_drop length_takeWhile_Not_replicate_False)
qed
lemma bl_drop_leading_zeros:
"(of_bl:: bool list ⇒ 'a::len word) (dropWhile Not bs) =
(of_bl:: bool list ⇒ 'a::len word) bs"
by(induction bs) simp_all
lemma bl_length_drop_bound: assumes "length (dropWhile Not bs) ≤ n"
shows "length (dropWhile Not (to_bl ((of_bl:: bool list ⇒ 'a::len word) bs))) ≤ n"
proof -
have bl_length_drop_twice:
"length (dropWhile Not (to_bl ((of_bl:: bool list ⇒ 'a::len word) (dropWhile Not bs)))) =
length (dropWhile Not (to_bl ((of_bl:: bool list ⇒ 'a::len word) bs)))"
by(simp add: bl_drop_leading_zeros)
from length_drop_bl
have *: "length (dropWhile Not (to_bl ((of_bl:: bool list ⇒ 'a::len word) bs))) ≤ length (dropWhile Not bs)"
apply(rule dual_order.trans)
apply(subst bl_length_drop_twice)
..
show ?thesis
apply(rule order.trans, rule *)
using assms by(simp)
qed
context
includes bit_operations_syntax
begin
lemma length_drop_mask_outer: fixes ip::"'a::len word"
shows "LENGTH('a) - n' = len ⟹ length (dropWhile Not (to_bl (ip AND (mask n << n') >> n'))) ≤ len"
apply(subst word_and_mask_shiftl)
apply(subst shiftl_shiftr1)
apply(simp; fail)
apply(simp)
apply(subst and_mask)
apply(simp add: word_size)
apply(simp add: length_drop_mask)
done
lemma length_drop_mask_inner: fixes ip::"'a::len word"
shows "n ≤ LENGTH('a) - n' ⟹ length (dropWhile Not (to_bl (ip AND (mask n << n') >> n'))) ≤ n"
apply(subst word_and_mask_shiftl)
apply(subst shiftl_shiftr3)
apply(simp; fail)
apply(simp)
apply(simp add: word_size)
apply(simp add: mask_twice)
apply(simp add: length_drop_mask)
done
end
lemma mask128: "0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF = (mask 128 :: 'a::len word)"
by (simp add: mask_numeral)
lemma helper_masked_ucast_generic:
fixes b::"16 word"
assumes "n + 16 ≤ m" and "m < 128"
shows "((ucast:: 16 word ⇒ 128 word) b << n) && (mask 16 << m) = 0"
proof -
have "x < 2 ^ (m - n)" if mnh2: "x < 0x10000"
for x::"128 word"
proof -
from assms(1) have mnh3: "16 ≤ m - n" by fastforce
have power_2_16_nat: "(16::nat) ≤ n ⟹ (65535::nat) < 2 ^ n" if a:"16 ≤ n"for n
proof -
have power2_rule: "a ≤ b ⟹ (2::nat)^a ≤ 2 ^ b" for a b by fastforce
show ?thesis
apply(subgoal_tac "65536 ≤ 2 ^ n")
apply(subst Nat.less_eq_Suc_le)
apply(simp; fail)
apply(subgoal_tac "(65536::nat) = 2^16")
subgoal using power2_rule ‹16 ≤ n› by presburger
by(simp)
qed
have "65536 = unat (65536::128 word)" by auto
moreover from mnh2 have "unat x < unat (65536::128 word)" by(rule Word.unat_mono)
ultimately have x: "unat x < 65536" by simp
with mnh3 have "unat x < 2 ^ (m - n)"
using power_2_16_nat [of ‹m - n›] by simp
with assms(2) show ?thesis by(subst word_less_nat_alt) simp
qed
hence mnhelper2: "(of_bl::bool list ⇒ 128 word) (to_bl b) < 2 ^ (m - n)"
apply(subgoal_tac "(of_bl::bool list ⇒ 128 word) (to_bl b) < 2^(LENGTH(16))")
apply(simp; fail)
by(rule of_bl_length_less) simp+
have mnhelper3: "(of_bl::bool list ⇒ 128 word) (to_bl b) * 2 ^ n < 2 ^ m"
apply(rule div_lt_mult)
apply(rule word_less_two_pow_divI)
using assms by(simp_all add: mnhelper2 p2_gt_0)
show ?thesis
apply (rule bit_word_eqI)
apply (simp only: bit_simps)
using assms(1)
apply auto
apply (transfer fixing: m n)
apply auto
done
qed
lemma unat_of_bl_128_16_less_helper:
fixes b::"16 word"
shows "unat ((of_bl::bool list ⇒ 128 word) (to_bl b)) < 2^16"
proof -
from word_bl_Rep' have 1: "length (to_bl b) = 16" by simp
have "unat ((of_bl::bool list ⇒ 128 word) (to_bl b)) < 2^(length (to_bl b))"
by(fact unat_of_bl_length)
with 1 show ?thesis by auto
qed
lemma unat_of_bl_128_16_le_helper: "unat ((of_bl:: bool list ⇒ 128 word) (to_bl (b::16 word))) ≤ 65535"
proof -
from unat_of_bl_128_16_less_helper[of b] have
"unat ((of_bl:: bool list ⇒ 128 word) (to_bl b)) < 65536" by simp
from Suc_leI[OF this] show ?thesis by simp
qed
lemma helper_masked_ucast_reverse_generic:
fixes b::"16 word"
assumes "m + 16 ≤ n" and "n ≤ 128 - 16"
shows "((ucast:: 16 word ⇒ 128 word) b << n) && (mask 16 << m) = 0"
proof -
have power_less_128_helper: "2 ^ n * unat ((of_bl::bool list ⇒ 128 word) (to_bl b)) < 2 ^ LENGTH(128)"
if n: "n ≤ 128 - 16" for n
proof -
have help_mult: "n ≤ l ⟹ 2 ^ n * x < 2 ^ l ⟷ x < 2 ^ (l - n)" for x::nat and l
by (simp add: nat_mult_power_less_eq semiring_normalization_rules(7))
from n show ?thesis
apply(subst help_mult)
subgoal by (simp)
apply(rule order_less_le_trans)
apply(rule unat_of_bl_128_16_less_helper)
apply(rule Power.power_increasing)
apply(simp_all)
done
qed
have *: "2 ^ m * (2 ^ (n - m) * unat ((of_bl::bool list ⇒ 128 word) (to_bl b))) =
2 ^ n * unat ((of_bl::bool list ⇒ 128 word) (to_bl b))"
proof(cases "unat ((of_bl::bool list ⇒ 128 word) (to_bl b)) = 0")
case True thus ?thesis by simp
next
case False
have help_mult: "x ≠ 0 ⟹ b * (c * x) = a * (x::nat) ⟷ b * c = a" for x a b c by simp
from assms show ?thesis
apply(subst help_mult[OF False])
apply(subst Power.monoid_mult_class.power_add[symmetric])
apply(simp)
done
qed
from assms have "unat ((2 ^ n)::128 word) * unat ((of_bl::bool list ⇒ 128 word) (to_bl b)) mod 2 ^ LENGTH(128) =
2 ^ m * (2 ^ (n - m) * unat ((of_bl::bool list ⇒ 128 word) (to_bl b)) mod 2 ^ LENGTH(128))"
apply(subst nat_mod_eq')
subgoal apply(subst unat_power_lower)
subgoal by(simp; fail)
subgoal by (rule power_less_128_helper) simp
done
apply(subst nat_mod_eq')
subgoal by(rule power_less_128_helper) simp
apply(subst unat_power_lower)
apply(simp; fail)
apply(simp only: *)
done
hence ex_k: "∃k. unat ((2 ^ n)::128 word) * unat ((of_bl::bool list ⇒ 128 word) (to_bl b)) mod 2 ^ LENGTH(128) = 2 ^ m * k"
by blast
hence aligned: "is_aligned ((of_bl::bool list ⇒ 128 word) (to_bl b) << n) m"
unfolding is_aligned_iff_dvd_nat
unfolding dvd_def
unfolding shiftl_t2n
unfolding Word.unat_word_ariths(2)
by assumption
from assms have of_bl_to_bl_shift_mask: "((of_bl::bool list ⇒ 128 word) (to_bl b) << n) && mask (16 + m) = 0"
using is_aligned_mask is_aligned_shiftl by force
show ?thesis
apply(subst ucast_bl)+
apply(subst word_and_mask_shiftl)
apply(subst aligned_shiftr_mask_shiftl)
subgoal by (fact aligned)
subgoal by (fact of_bl_to_bl_shift_mask)
done
qed
lemma helper_masked_ucast_equal_generic:
fixes b::"16 word"
assumes "n ≤ 128 - 16"
shows "ucast (((ucast:: 16 word ⇒ 128 word) b << n) && (mask 16 << n) >> n) = b"
proof -
have ucast_mask: "(ucast:: 16 word ⇒ 128 word) b && mask 16 = ucast b"
by (simp only: flip: take_bit_eq_mask unsigned_take_bit_eq) (simp add: take_bit_word_eq_self)
from assms have "ucast (((ucast:: 16 word ⇒ 128 word) b && mask (128 - n) && mask 16) && mask (128 - n)) = b"
by (simp only: take_bit_of_mask flip: take_bit_eq_mask unsigned_take_bit_eq)
(simp add: unsigned_ucast_eq take_bit_word_eq_self)
thus ?thesis
apply(subst word_and_mask_shiftl)
apply(subst shiftl_shiftr3)
apply(simp; fail)
apply(simp)
apply(subst shiftl_shiftr3)
apply(simp_all add: word_size and.assoc)
done
qed
end