# Theory Word

(*  Author:     Sebastian Skalberg, TU Muenchen
*)

section ‹Binary Words›

theory Word
imports Main
begin

subsection ‹Auxilary Lemmas›

lemma max_le [intro!]: "[| x ≤ z; y ≤ z |] ==> max x y ≤ z"

lemma max_mono:
fixes x :: "'a::linorder"
assumes mf: "mono f"
shows       "max (f x) (f y) ≤ f (max x y)"
proof -
from mf and max.cobounded1 [of x y]
have fx: "f x ≤ f (max x y)" by (rule monoD)
from mf and max.cobounded2 [of y x]
have fy: "f y ≤ f (max x y)" by (rule monoD)
from fx and fy
show "max (f x) (f y) ≤ f (max x y)" by auto
qed

declare zero_le_power [intro]
and zero_less_power [intro]

lemma int_nat_two_exp: "2 ^ k = int (2 ^ k)"
by simp

subsection ‹Bits›

datatype bit =
Zero ("𝟬")
| One ("𝟭")

primrec bitval :: "bit => nat" where
"bitval 𝟬 = 0"
| "bitval 𝟭 = 1"

primrec bitnot :: "bit => bit"  ("¬⇩b _"  40) where
bitnot_zero: "(¬⇩b 𝟬) = 𝟭"
| bitnot_one : "(¬⇩b 𝟭) = 𝟬"

primrec bitand :: "bit => bit => bit"  (infixr "∧⇩b" 35) where
bitand_zero: "(𝟬 ∧⇩b y) = 𝟬"
| bitand_one:  "(𝟭 ∧⇩b y) = y"

primrec bitor :: "bit => bit => bit"  (infixr "∨⇩b" 30) where
bitor_zero: "(𝟬 ∨⇩b y) = y"
| bitor_one:  "(𝟭 ∨⇩b y) = 𝟭"

primrec bitxor :: "bit => bit => bit"  (infixr "⊕⇩b" 30) where
bitxor_zero: "(𝟬 ⊕⇩b y) = y"
| bitxor_one:  "(𝟭 ⊕⇩b y) = (bitnot y)"

lemma bitnot_bitnot [simp]: "(bitnot (bitnot b)) = b"
by (cases b) simp_all

lemma bitand_cancel [simp]: "(b ∧⇩b b) = b"
by (cases b) simp_all

lemma bitor_cancel [simp]: "(b ∨⇩b b) = b"
by (cases b) simp_all

lemma bitxor_cancel [simp]: "(b ⊕⇩b b) = 𝟬"
by (cases b) simp_all

subsection ‹Bit Vectors›

text ‹First, a couple of theorems expressing case analysis and
induction principles for bit vectors.›

lemma bit_list_cases:
assumes empty: "w = [] ==> P w"
and     zero:  "!!bs. w = 𝟬 # bs ==> P w"
and     one:   "!!bs. w = 𝟭 # bs ==> P w"
shows   "P w"
proof (cases w)
assume "w = []"
thus ?thesis by (rule empty)
next
fix b bs
assume [simp]: "w = b # bs"
show "P w"
proof (cases b)
assume "b = 𝟬"
hence "w = 𝟬 # bs" by simp
thus ?thesis by (rule zero)
next
assume "b = 𝟭"
hence "w = 𝟭 # bs" by simp
thus ?thesis by (rule one)
qed
qed

lemma bit_list_induct:
assumes empty: "P []"
and     zero:  "!!bs. P bs ==> P (𝟬#bs)"
and     one:   "!!bs. P bs ==> P (𝟭#bs)"
shows   "P w"
proof (induct w, simp_all add: empty)
fix b bs
assume "P bs"
then show "P (b#bs)"
by (cases b) (auto intro!: zero one)
qed

definition
bv_msb :: "bit list => bit" where
"bv_msb w = (if w = [] then 𝟬 else hd w)"

definition
bv_extend :: "[nat,bit,bit list]=>bit list" where
"bv_extend i b w = (replicate (i - length w) b) @ w"

definition
bv_not :: "bit list => bit list" where
"bv_not w = map bitnot w"

lemma bv_length_extend [simp]: "length w ≤ i ==> length (bv_extend i b w) = i"

lemma bv_not_Nil [simp]: "bv_not [] = []"

lemma bv_not_Cons [simp]: "bv_not (b#bs) = (bitnot b) # bv_not bs"

lemma bv_not_bv_not [simp]: "bv_not (bv_not w) = w"
by (rule bit_list_induct [of _ w]) simp_all

lemma bv_msb_Nil [simp]: "bv_msb [] = 𝟬"

lemma bv_msb_Cons [simp]: "bv_msb (b#bs) = b"

lemma bv_msb_bv_not [simp]: "0 < length w ==> bv_msb (bv_not w) = (bitnot (bv_msb w))"
by (cases w) simp_all

lemma bv_msb_one_length [simp,intro]: "bv_msb w = 𝟭 ==> 0 < length w"
by (cases w) simp_all

lemma length_bv_not [simp]: "length (bv_not w) = length w"
by (induct w) simp_all

definition
bv_to_nat :: "bit list => nat" where
"bv_to_nat = foldl (%bn b. 2 * bn + bitval b) 0"

lemma bv_to_nat_Nil [simp]: "bv_to_nat [] = 0"

lemma bv_to_nat_helper [simp]: "bv_to_nat (b # bs) = bitval b * 2 ^ length bs + bv_to_nat bs"
proof -
let ?bv_to_nat' = "foldl (λbn b. 2 * bn + bitval b)"
have helper: "⋀base. ?bv_to_nat' base bs = base * 2 ^ length bs + ?bv_to_nat' 0 bs"
proof (induct bs)
case Nil
show ?case by simp
next
case (Cons x xs base)
show ?case
apply (simp only: foldl_Cons)
apply (subst Cons [of "2 * base + bitval x"])
apply simp
apply (subst Cons [of "bitval x"])
done
qed
show ?thesis by (simp add: bv_to_nat_def) (rule helper)
qed

lemma bv_to_nat0 [simp]: "bv_to_nat (𝟬#bs) = bv_to_nat bs"
by simp

lemma bv_to_nat1 [simp]: "bv_to_nat (𝟭#bs) = 2 ^ length bs + bv_to_nat bs"
by simp

lemma bv_to_nat_upper_range: "bv_to_nat w < 2 ^ length w"
proof (induct w, simp_all)
fix b bs
assume "bv_to_nat bs < 2 ^ length bs"
show "bitval b * 2 ^ length bs + bv_to_nat bs < 2 * 2 ^ length bs"
proof (cases b, simp_all)
have "bv_to_nat bs < 2 ^ length bs" by fact
also have "... < 2 * 2 ^ length bs" by auto
finally show "bv_to_nat bs < 2 * 2 ^ length bs" by simp
next
have "bv_to_nat bs < 2 ^ length bs" by fact
hence "2 ^ length bs + bv_to_nat bs < 2 ^ length bs + 2 ^ length bs" by arith
also have "... = 2 * (2 ^ length bs)" by simp
finally show "bv_to_nat bs < 2 ^ length bs" by simp
qed
qed

lemma bv_extend_longer [simp]:
assumes wn: "n ≤ length w"
shows       "bv_extend n b w = w"

lemma bv_extend_shorter [simp]:
assumes wn: "length w < n"
shows       "bv_extend n b w = bv_extend n b (b#w)"
proof -
from wn
have s: "n - Suc (length w) + 1 = n - length w"
by arith
have "bv_extend n b w = replicate (n - length w) b @ w"
also have "... = replicate (n - Suc (length w) + 1) b @ w"
by (subst s) rule
also have "... = (replicate (n - Suc (length w)) b @ replicate 1 b) @ w"
also have "... = replicate (n - Suc (length w)) b @ b # w"
by simp
also have "... = bv_extend n b (b#w)"
finally show "bv_extend n b w = bv_extend n b (b#w)" .
qed

primrec rem_initial :: "bit => bit list => bit list" where
"rem_initial b [] = []"
| "rem_initial b (x#xs) = (if b = x then rem_initial b xs else x#xs)"

lemma rem_initial_length: "length (rem_initial b w) ≤ length w"
by (rule bit_list_induct [of _ w],simp_all (no_asm),safe,simp_all)

lemma rem_initial_equal:
assumes p: "length (rem_initial b w) = length w"
shows      "rem_initial b w = w"
proof -
have "length (rem_initial b w) = length w --> rem_initial b w = w"
proof (induct w, simp_all, clarify)
fix xs
assume "length (rem_initial b xs) = length xs --> rem_initial b xs = xs"
assume f: "length (rem_initial b xs) = Suc (length xs)"
with rem_initial_length [of b xs]
show "rem_initial b xs = b#xs"
by auto
qed
from this and p show ?thesis ..
qed

lemma bv_extend_rem_initial: "bv_extend (length w) b (rem_initial b w) = w"
proof (induct w, simp_all, safe)
fix xs
assume ind: "bv_extend (length xs) b (rem_initial b xs) = xs"
from rem_initial_length [of b xs]
have [simp]: "Suc (length xs) - length (rem_initial b xs) =
1 + (length xs - length (rem_initial b xs))"
by arith
have "bv_extend (Suc (length xs)) b (rem_initial b xs) =
replicate (Suc (length xs) - length (rem_initial b xs)) b @ (rem_initial b xs)"
also have "... =
replicate (1 + (length xs - length (rem_initial b xs))) b @ rem_initial b xs"
by simp
also have "... =
(replicate 1 b @ replicate (length xs - length (rem_initial b xs)) b) @ rem_initial b xs"
also have "... = b # bv_extend (length xs) b (rem_initial b xs)"
by (auto simp add: bv_extend_def [symmetric])
also have "... = b # xs"
finally show "bv_extend (Suc (length xs)) b (rem_initial b xs) = b # xs" .
qed

lemma rem_initial_append1:
assumes "rem_initial b xs ~= []"
shows   "rem_initial b (xs @ ys) = rem_initial b xs @ ys"
using assms by (induct xs) auto

lemma rem_initial_append2:
assumes "rem_initial b xs = []"
shows   "rem_initial b (xs @ ys) = rem_initial b ys"
using assms by (induct xs) auto

definition
norm_unsigned :: "bit list => bit list" where
"norm_unsigned = rem_initial 𝟬"

lemma norm_unsigned_Nil [simp]: "norm_unsigned [] = []"

lemma norm_unsigned_Cons0 [simp]: "norm_unsigned (𝟬#bs) = norm_unsigned bs"

lemma norm_unsigned_Cons1 [simp]: "norm_unsigned (𝟭#bs) = 𝟭#bs"

lemma norm_unsigned_idem [simp]: "norm_unsigned (norm_unsigned w) = norm_unsigned w"
by (rule bit_list_induct [of _ w],simp_all)

fun
nat_to_bv_helper :: "nat => bit list => bit list"
where
"nat_to_bv_helper n bs = (if n = 0 then bs
else nat_to_bv_helper (n div 2) ((if n mod 2 = 0 then 𝟬 else 𝟭)#bs))"

definition
nat_to_bv :: "nat => bit list" where
"nat_to_bv n = nat_to_bv_helper n []"

lemma nat_to_bv0 [simp]: "nat_to_bv 0 = []"

lemmas [simp del] = nat_to_bv_helper.simps

lemma n_div_2_cases:
assumes zero: "(n::nat) = 0 ==> R"
and     div : "[| n div 2 < n ; 0 < n |] ==> R"
shows         "R"
proof (cases "n = 0")
assume "n = 0"
thus R by (rule zero)
next
assume "n ~= 0"
hence "0 < n" by simp
hence "n div 2 < n" by arith
from this and ‹0 < n› show R by (rule div)
qed

lemma int_wf_ge_induct:
assumes ind :  "!!i::int. (!!j. [| k ≤ j ; j < i |] ==> P j) ==> P i"
shows          "P i"
proof (rule wf_induct_rule [OF wf_int_ge_less_than])
fix x
assume ih: "(⋀y::int. (y, x) ∈ int_ge_less_than k ⟹ P y)"
thus "P x"
by (rule ind) (simp add: int_ge_less_than_def)
qed

lemma unfold_nat_to_bv_helper:
"nat_to_bv_helper b l = nat_to_bv_helper b [] @ l"
proof -
have "∀l. nat_to_bv_helper b l = nat_to_bv_helper b [] @ l"
proof (induct b rule: less_induct)
fix n
assume ind: "!!j. j < n ⟹ ∀ l. nat_to_bv_helper j l = nat_to_bv_helper j [] @ l"
show "∀l. nat_to_bv_helper n l = nat_to_bv_helper n [] @ l"
proof
fix l
show "nat_to_bv_helper n l = nat_to_bv_helper n [] @ l"
proof (cases "n < 0")
assume "n < 0"
thus ?thesis
next
assume "~n < 0"
show ?thesis
proof (rule n_div_2_cases [of n])
assume [simp]: "n = 0"
show ?thesis
apply (simp only: nat_to_bv_helper.simps [of n])
apply simp
done
next
assume n2n: "n div 2 < n"
assume [simp]: "0 < n"
hence n20: "0 ≤ n div 2"
by arith
from ind [of "n div 2"] and n2n n20
have ind': "∀l. nat_to_bv_helper (n div 2) l = nat_to_bv_helper (n div 2) [] @ l"
by blast
show ?thesis
apply (simp only: nat_to_bv_helper.simps [of n])
apply (cases "n=0")
apply simp
apply (simp only: if_False)
apply simp
apply (subst spec [OF ind',of "𝟬#l"])
apply (subst spec [OF ind',of "𝟭#l"])
apply (subst spec [OF ind',of ""])
apply (subst spec [OF ind',of ""])
apply simp
done
qed
qed
qed
qed
thus ?thesis ..
qed

lemma nat_to_bv_non0 [simp]: "n≠0 ==> nat_to_bv n = nat_to_bv (n div 2) @ [if n mod 2 = 0 then 𝟬 else 𝟭]"
proof -
assume n: "n≠0"
show ?thesis
apply (subst nat_to_bv_def [of n])
apply (simp only: nat_to_bv_helper.simps [of n])
apply (subst unfold_nat_to_bv_helper)
apply (subst nat_to_bv_def [of "n div 2"])
apply auto
done
qed

lemma bv_to_nat_dist_append:
"bv_to_nat (l1 @ l2) = bv_to_nat l1 * 2 ^ length l2 + bv_to_nat l2"
proof -
have "∀l2. bv_to_nat (l1 @ l2) = bv_to_nat l1 * 2 ^ length l2 + bv_to_nat l2"
proof (induct l1, simp_all)
fix x xs
assume ind: "∀l2. bv_to_nat (xs @ l2) = bv_to_nat xs * 2 ^ length l2 + bv_to_nat l2"
show "∀l2::bit list. bitval x * 2 ^ (length xs + length l2) + bv_to_nat xs * 2 ^ length l2 = (bitval x * 2 ^ length xs + bv_to_nat xs) * 2 ^ length l2"
proof
fix l2
show "bitval x * 2 ^ (length xs + length l2) + bv_to_nat xs * 2 ^ length l2 = (bitval x * 2 ^ length xs + bv_to_nat xs) * 2 ^ length l2"
proof -
have "(2::nat) ^ (length xs + length l2) = 2 ^ length xs * 2 ^ length l2"
by (induct ("length xs")) simp_all
hence "bitval x * 2 ^ (length xs + length l2) + bv_to_nat xs * 2 ^ length l2 =
bitval x * 2 ^ length xs * 2 ^ length l2 + bv_to_nat xs * 2 ^ length l2"
by simp
also have "... = (bitval x * 2 ^ length xs + bv_to_nat xs) * 2 ^ length l2"
finally show ?thesis by simp
qed
qed
qed
thus ?thesis ..
qed

lemma bv_nat_bv [simp]: "bv_to_nat (nat_to_bv n) = n"
proof (induct n rule: less_induct)
fix n
assume ind: "!!j. j < n ⟹ bv_to_nat (nat_to_bv j) = j"
show "bv_to_nat (nat_to_bv n) = n"
proof (rule n_div_2_cases [of n])
assume "n = 0" then show ?thesis by simp
next
assume nn: "n div 2 < n"
assume n0: "0 < n"
from ind and nn
have ind': "bv_to_nat (nat_to_bv (n div 2)) = n div 2" by blast
from n0 have n0': "n ≠ 0" by simp
show ?thesis
apply (subst nat_to_bv_def)
apply (simp only: nat_to_bv_helper.simps [of n])
apply (simp only: n0' if_False)
apply (subst unfold_nat_to_bv_helper)
apply (subst bv_to_nat_dist_append)
apply (fold nat_to_bv_def)
apply (simp add: ind' split del: if_split)
apply (cases "n mod 2 = 0")
proof (simp_all)
assume "n mod 2 = 0"
with div_mult_mod_eq [of n 2]
show "n div 2 * 2 = n" by simp
next
assume "n mod 2 = Suc 0"
with div_mult_mod_eq [of n 2]
show "Suc (n div 2 * 2) = n" by arith
qed
qed
qed

lemma bv_to_nat_type [simp]: "bv_to_nat (norm_unsigned w) = bv_to_nat w"
by (rule bit_list_induct) simp_all

lemma length_norm_unsigned_le [simp]: "length (norm_unsigned w) ≤ length w"
by (rule bit_list_induct) simp_all

lemma bv_to_nat_rew_msb: "bv_msb w = 𝟭 ==> bv_to_nat w = 2 ^ (length w - 1) + bv_to_nat (tl w)"
by (rule bit_list_cases [of w]) simp_all

lemma norm_unsigned_result: "norm_unsigned xs = [] ∨ bv_msb (norm_unsigned xs) = 𝟭"
proof (rule length_induct [of _ xs])
fix xs :: "bit list"
assume ind: "∀ys. length ys < length xs --> norm_unsigned ys = [] ∨ bv_msb (norm_unsigned ys) = 𝟭"
show "norm_unsigned xs = [] ∨ bv_msb (norm_unsigned xs) = 𝟭"
proof (rule bit_list_cases [of xs],simp_all)
fix bs
assume [simp]: "xs = 𝟬#bs"
from ind
have "length bs < length xs --> norm_unsigned bs = [] ∨ bv_msb (norm_unsigned bs) = 𝟭" ..
thus "norm_unsigned bs = [] ∨ bv_msb (norm_unsigned bs) = 𝟭" by simp
qed
qed

lemma norm_empty_bv_to_nat_zero:
assumes nw: "norm_unsigned w = []"
shows       "bv_to_nat w = 0"
proof -
have "bv_to_nat w = bv_to_nat (norm_unsigned w)" by simp
also have "... = bv_to_nat []" by (subst nw) (rule refl)
also have "... = 0" by simp
finally show ?thesis .
qed

lemma bv_to_nat_lower_limit:
assumes w0: "0 < bv_to_nat w"
shows "2 ^ (length (norm_unsigned w) - 1) ≤ bv_to_nat w"
proof -
from w0 and norm_unsigned_result [of w]
have msbw: "bv_msb (norm_unsigned w) = 𝟭"
have "2 ^ (length (norm_unsigned w) - 1) ≤ bv_to_nat (norm_unsigned w)"
by (subst bv_to_nat_rew_msb [OF msbw],simp)
thus ?thesis by simp
qed

lemmas [simp del] = nat_to_bv_non0

lemma norm_unsigned_length [intro!]: "length (norm_unsigned w) ≤ length w"
by (subst norm_unsigned_def,rule rem_initial_length)

lemma norm_unsigned_equal:
"length (norm_unsigned w) = length w ==> norm_unsigned w = w"

lemma bv_extend_norm_unsigned: "bv_extend (length w) 𝟬 (norm_unsigned w) = w"

lemma norm_unsigned_append1 [simp]:
"norm_unsigned xs ≠ [] ==> norm_unsigned (xs @ ys) = norm_unsigned xs @ ys"

lemma norm_unsigned_append2 [simp]:
"norm_unsigned xs = [] ==> norm_unsigned (xs @ ys) = norm_unsigned ys"

lemma bv_to_nat_zero_imp_empty:
"bv_to_nat w = 0 ⟹ norm_unsigned w = []"
by (atomize (full), induct w rule: bit_list_induct) simp_all

lemma bv_to_nat_nzero_imp_nempty:
"bv_to_nat w ≠ 0 ⟹ norm_unsigned w ≠ []"
by (induct w rule: bit_list_induct) simp_all

lemma nat_helper1:
assumes ass: "nat_to_bv (bv_to_nat w) = norm_unsigned w"
shows        "nat_to_bv (2 * bv_to_nat w + bitval x) = norm_unsigned (w @ [x])"
proof (cases x)
assume [simp]: "x = 𝟭"
have "nat_to_bv (Suc (2 * bv_to_nat w) div 2) @  =
nat_to_bv ((1 + 2 * bv_to_nat w) div 2) @ "
also have "... = nat_to_bv (bv_to_nat w) @ "
also have "... = norm_unsigned w @ "
by (subst ass) (rule refl)
also have "... = norm_unsigned (w @ )"
by (cases "norm_unsigned w") simp_all
finally have "nat_to_bv (Suc (2 * bv_to_nat w) div 2) @  = norm_unsigned (w @ )" .
then show ?thesis by (simp add: nat_to_bv_non0)
next
assume [simp]: "x = 𝟬"
show ?thesis
proof (cases "bv_to_nat w = 0")
assume "bv_to_nat w = 0"
thus ?thesis
next
assume "bv_to_nat w ≠ 0"
thus ?thesis
apply simp
apply (subst nat_to_bv_non0)
apply simp
apply auto
apply (subst ass)
apply (cases "norm_unsigned w")
done
qed
qed

lemma nat_helper2: "nat_to_bv (2 ^ length xs + bv_to_nat xs) = 𝟭 # xs"
proof -
have "∀xs. nat_to_bv (2 ^ length (rev xs) + bv_to_nat (rev xs)) = 𝟭 # (rev xs)" (is "∀xs. ?P xs")
proof
fix xs
show "?P xs"
proof (rule length_induct [of _ xs])
fix xs :: "bit list"
assume ind: "∀ys. length ys < length xs --> ?P ys"
show "?P xs"
proof (cases xs)
assume "xs = []"
then show ?thesis by (simp add: nat_to_bv_non0)
next
fix y ys
assume [simp]: "xs = y # ys"
show ?thesis
apply simp
apply (subst bv_to_nat_dist_append)
apply simp
proof -
have "nat_to_bv (2 * 2 ^ length ys + (bv_to_nat (rev ys) * 2 + bitval y)) =
nat_to_bv (2 * (2 ^ length ys + bv_to_nat (rev ys)) + bitval y)"
also have "... = nat_to_bv (2 * (bv_to_nat (𝟭#rev ys)) + bitval y)"
by simp
also have "... = norm_unsigned (𝟭#rev ys) @ [y]"
proof -
from ind
have "nat_to_bv (2 ^ length (rev ys) + bv_to_nat (rev ys)) = 𝟭 # rev ys"
by auto
hence [simp]: "nat_to_bv (2 ^ length ys + bv_to_nat (rev ys)) = 𝟭 # rev ys"
by simp
show ?thesis
apply (subst nat_helper1)
apply simp_all
done
qed
also have "... = (𝟭#rev ys) @ [y]"
by simp
also have "... = 𝟭 # rev ys @ [y]"
by simp
finally show "nat_to_bv (2 * 2 ^ length ys + (bv_to_nat (rev ys) * 2 + bitval y)) =
𝟭 # rev ys @ [y]" .
qed
qed
qed
qed
hence "nat_to_bv (2 ^ length (rev (rev xs)) + bv_to_nat (rev (rev xs))) =
𝟭 # rev (rev xs)" ..
thus ?thesis by simp
qed

lemma nat_bv_nat [simp]: "nat_to_bv (bv_to_nat w) = norm_unsigned w"
proof (rule bit_list_induct [of _ w],simp_all)
fix xs
assume "nat_to_bv (bv_to_nat xs) = norm_unsigned xs"
have "bv_to_nat xs = bv_to_nat (norm_unsigned xs)" by simp
have "bv_to_nat xs < 2 ^ length xs"
by (rule bv_to_nat_upper_range)
show "nat_to_bv (2 ^ length xs + bv_to_nat xs) = 𝟭 # xs"
by (rule nat_helper2)
qed

lemma bv_to_nat_qinj:
assumes one: "bv_to_nat xs = bv_to_nat ys"
and     len: "length xs = length ys"
shows        "xs = ys"
proof -
from one
have "nat_to_bv (bv_to_nat xs) = nat_to_bv (bv_to_nat ys)"
by simp
hence xsys: "norm_unsigned xs = norm_unsigned ys"
by simp
have "xs = bv_extend (length xs) 𝟬 (norm_unsigned xs)"
also have "... = bv_extend (length ys) 𝟬 (norm_unsigned ys)"
also have "... = ys"
finally show ?thesis .
qed

lemma norm_unsigned_nat_to_bv [simp]:
"norm_unsigned (nat_to_bv n) = nat_to_bv n"
proof -
have "norm_unsigned (nat_to_bv n) = nat_to_bv (bv_to_nat (norm_unsigned (nat_to_bv n)))"
by (subst nat_bv_nat) simp
also have "... = nat_to_bv n" by simp
finally show ?thesis .
qed

lemma length_nat_to_bv_upper_limit:
assumes nk: "n ≤ 2 ^ k - 1"
shows       "length (nat_to_bv n) ≤ k"
proof (cases "n = 0")
case True
thus ?thesis
next
case False
hence n0: "0 < n" by simp
show ?thesis
proof (rule ccontr)
assume "~ length (nat_to_bv n) ≤ k"
hence "k < length (nat_to_bv n)" by simp
hence "k ≤ length (nat_to_bv n) - 1" by arith
hence "(2::nat) ^ k ≤ 2 ^ (length (nat_to_bv n) - 1)" by simp
also have "... = 2 ^ (length (norm_unsigned (nat_to_bv n)) - 1)" by simp
also have "... ≤ bv_to_nat (nat_to_bv n)"
by (rule bv_to_nat_lower_limit) (simp add: n0)
also have "... = n" by simp
finally have "2 ^ k ≤ n" .
with n0 have "2 ^ k - 1 < n" by arith
with nk show False by simp
qed
qed

lemma length_nat_to_bv_lower_limit:
assumes nk: "2 ^ k ≤ n"
shows       "k < length (nat_to_bv n)"
proof (rule ccontr)
assume "~ k < length (nat_to_bv n)"
hence lnk: "length (nat_to_bv n) ≤ k" by simp
have "n = bv_to_nat (nat_to_bv n)" by simp
also have "... < 2 ^ length (nat_to_bv n)"
by (rule bv_to_nat_upper_range)
also from lnk have "... ≤ 2 ^ k" by simp
finally have "n < 2 ^ k" .
with nk show False by simp
qed

subsection ‹Unsigned Arithmetic Operations›

definition
bv_add :: "[bit list, bit list ] => bit list" where
"bv_add w1 w2 = nat_to_bv (bv_to_nat w1 + bv_to_nat w2)"

lemma bv_add_length: "length (bv_add w1 w2) ≤ Suc (max (length w1) (length w2))"
from bv_to_nat_upper_range [of w1] and bv_to_nat_upper_range [of w2]
have "bv_to_nat w1 + bv_to_nat w2 ≤ (2 ^ length w1 - 1) + (2 ^ length w2 - 1)"
by arith
also have "... ≤
max (2 ^ length w1 - 1) (2 ^ length w2 - 1) + max (2 ^ length w1 - 1) (2 ^ length w2 - 1)"
by (rule add_mono,safe intro!: max.cobounded1 max.cobounded2)
also have "... = 2 * max (2 ^ length w1 - 1) (2 ^ length w2 - 1)" by simp
also have "... ≤ 2 ^ Suc (max (length w1) (length w2)) - 2"
proof (cases "length w1 ≤ length w2")
assume w1w2: "length w1 ≤ length w2"
hence "(2::nat) ^ length w1 ≤ 2 ^ length w2" by simp
hence "(2::nat) ^ length w1 - 1 ≤ 2 ^ length w2 - 1" by arith
with w1w2 show ?thesis
by (simp add: diff_mult_distrib2 split: split_max)
next
assume [simp]: "~ (length w1 ≤ length w2)"
have "~ ((2::nat) ^ length w1 - 1 ≤ 2 ^ length w2 - 1)"
proof
assume "(2::nat) ^ length w1 - 1 ≤ 2 ^ length w2 - 1"
hence "((2::nat) ^ length w1 - 1) + 1 ≤ (2 ^ length w2 - 1) + 1"
hence "(2::nat) ^ length w1 ≤ 2 ^ length w2" by simp
hence "length w1 ≤ length w2" by simp
thus False by simp
qed
thus ?thesis
by (simp add: diff_mult_distrib2 split: split_max)
qed
finally show "bv_to_nat w1 + bv_to_nat w2 ≤ 2 ^ Suc (max (length w1) (length w2)) - 1"
by arith
qed

definition
bv_mult :: "[bit list, bit list ] => bit list" where
"bv_mult w1 w2 = nat_to_bv (bv_to_nat w1 * bv_to_nat w2)"

lemma bv_mult_type1 [simp]: "bv_mult (norm_unsigned w1) w2 = bv_mult w1 w2"

lemma bv_mult_type2 [simp]: "bv_mult w1 (norm_unsigned w2) = bv_mult w1 w2"

lemma bv_mult_returntype [simp]: "norm_unsigned (bv_mult w1 w2) = bv_mult w1 w2"

lemma bv_mult_length: "length (bv_mult w1 w2) ≤ length w1 + length w2"
proof (unfold bv_mult_def,rule length_nat_to_bv_upper_limit)
from bv_to_nat_upper_range [of w1] and bv_to_nat_upper_range [of w2]
have h: "bv_to_nat w1 ≤ 2 ^ length w1 - 1 ∧ bv_to_nat w2 ≤ 2 ^ length w2 - 1"
by arith
have "bv_to_nat w1 * bv_to_nat w2 ≤ (2 ^ length w1 - 1) * (2 ^ length w2 - 1)"
apply (cut_tac h)
apply (rule mult_mono)
apply auto
done
also have "... < 2 ^ length w1 * 2 ^ length w2"
by (rule mult_strict_mono,auto)
also have "... = 2 ^ (length w1 + length w2)"
finally show "bv_to_nat w1 * bv_to_nat w2 ≤ 2 ^ (length w1 + length w2) - 1"
by arith
qed

subsection ‹Signed Vectors›

primrec norm_signed :: "bit list => bit list" where
norm_signed_Nil: "norm_signed [] = []"
| norm_signed_Cons: "norm_signed (b#bs) =
(case b of
𝟬 => if norm_unsigned bs = [] then [] else b#norm_unsigned bs
| 𝟭 => b#rem_initial b bs)"

lemma norm_signed0 [simp]: "norm_signed  = []"
by simp

lemma norm_signed1 [simp]: "norm_signed  = "
by simp

lemma norm_signed01 [simp]: "norm_signed (𝟬#𝟭#xs) = 𝟬#𝟭#xs"
by simp

lemma norm_signed00 [simp]: "norm_signed (𝟬#𝟬#xs) = norm_signed (𝟬#xs)"
by simp

lemma norm_signed10 [simp]: "norm_signed (𝟭#𝟬#xs) = 𝟭#𝟬#xs"
by simp

lemma norm_signed11 [simp]: "norm_signed (𝟭#𝟭#xs) = norm_signed (𝟭#xs)"
by simp

lemmas [simp del] = norm_signed_Cons

definition
int_to_bv :: "int => bit list" where
"int_to_bv n = (if 0 ≤ n
then norm_signed (𝟬#nat_to_bv (nat n))
else norm_signed (bv_not (𝟬#nat_to_bv (nat (-n- 1)))))"

lemma int_to_bv_ge0 [simp]: "0 ≤ n ==> int_to_bv n = norm_signed (𝟬 # nat_to_bv (nat n))"

lemma int_to_bv_lt0 [simp]:
"n < 0 ==> int_to_bv n = norm_signed (bv_not (𝟬#nat_to_bv (nat (-n- 1))))"

lemma norm_signed_idem [simp]: "norm_signed (norm_signed w) = norm_signed w"
proof (rule bit_list_induct [of _ w], simp_all)
fix xs
assume eq: "norm_signed (norm_signed xs) = norm_signed xs"
show "norm_signed (norm_signed (𝟬#xs)) = norm_signed (𝟬#xs)"
proof (rule bit_list_cases [of xs],simp_all)
fix ys
assume "xs = 𝟬#ys"
from this [symmetric] and eq
show "norm_signed (norm_signed (𝟬#ys)) = norm_signed (𝟬#ys)"
by simp
qed
next
fix xs
assume eq: "norm_signed (norm_signed xs) = norm_signed xs"
show "norm_signed (norm_signed (𝟭#xs)) = norm_signed (𝟭#xs)"
proof (rule bit_list_cases [of xs],simp_all)
fix ys
assume "xs = 𝟭#ys"
from this [symmetric] and eq
show "norm_signed (norm_signed (𝟭#ys)) = norm_signed (𝟭#ys)"
by simp
qed
qed

definition
bv_to_int :: "bit list => int" where
"bv_to_int w =
(case bv_msb w of 𝟬 => int (bv_to_nat w)
| 𝟭 => - int (bv_to_nat (bv_not w) + 1))"

lemma bv_to_int_Nil [simp]: "bv_to_int [] = 0"

lemma bv_to_int_Cons0 [simp]: "bv_to_int (𝟬#bs) = int (bv_to_nat bs)"

lemma bv_to_int_Cons1 [simp]: "bv_to_int (𝟭#bs) = - int (bv_to_nat (bv_not bs) + 1)"

lemma bv_to_int_type [simp]: "bv_to_int (norm_signed w) = bv_to_int w"
proof (rule bit_list_induct [of _ w], simp_all)
fix xs
assume ind: "bv_to_int (norm_signed xs) = bv_to_int xs"
show "bv_to_int (norm_signed (𝟬#xs)) = int (bv_to_nat xs)"
proof (rule bit_list_cases [of xs], simp_all)
fix ys
assume [simp]: "xs = 𝟬#ys"
from ind
show "bv_to_int (norm_signed (𝟬#ys)) = int (bv_to_nat ys)"
by simp
qed
next
fix xs
assume ind: "bv_to_int (norm_signed xs) = bv_to_int xs"
show "bv_to_int (norm_signed (𝟭#xs)) = -1 - int (bv_to_nat (bv_not xs))"
proof (rule bit_list_cases [of xs], simp_all)
fix ys
assume [simp]: "xs = 𝟭#ys"
from ind
show "bv_to_int (norm_signed (𝟭#ys)) = -1 - int (bv_to_nat (bv_not ys))"
by simp
qed
qed

lemma bv_to_int_upper_range: "bv_to_int w < 2 ^ (length w - 1)"
proof (rule bit_list_cases [of w],simp_all add: bv_to_nat_upper_range)
fix bs
have "-1 - int (bv_to_nat (bv_not bs)) ≤ 0" by simp
also have "... < 2 ^ length bs" by (induct bs) simp_all
finally show "-1 - int (bv_to_nat (bv_not bs)) < 2 ^ length bs" .
qed

lemma bv_to_int_lower_range: "- (2 ^ (length w - 1)) ≤ bv_to_int w"
proof (rule bit_list_cases [of w],simp_all)
fix bs :: "bit list"
have "- (2 ^ length bs) ≤ (0::int)" by (induct bs) simp_all
also have "... ≤ int (bv_to_nat bs)" by simp
finally show "- (2 ^ length bs) ≤ int (bv_to_nat bs)" .
next
fix bs
from bv_to_nat_upper_range [of "bv_not bs"]
show "- (2 ^ length bs) ≤ -1 - int (bv_to_nat (bv_not bs))"
qed

lemma int_bv_int [simp]: "int_to_bv (bv_to_int w) = norm_signed w"
proof (rule bit_list_cases [of w],simp)
fix xs
assume [simp]: "w = 𝟬#xs"
show ?thesis
apply simp
apply (subst norm_signed_Cons [of "𝟬" "xs"])
apply simp
using norm_unsigned_result [of xs]
apply safe
apply (rule bit_list_cases [of "norm_unsigned xs"])
apply simp_all
done
next
fix xs
assume [simp]: "w = 𝟭#xs"
show ?thesis
apply (simp del: int_to_bv_lt0)
apply (rule bit_list_induct [of _ xs], simp)
apply (subst int_to_bv_lt0)
apply linarith
apply simp
apply (metis add.commute bitnot_zero bv_not_Cons bv_not_bv_not int_nat_two_exp length_bv_not nat_helper2 nat_int norm_signed10 of_nat_add)
apply simp
done
qed

lemma bv_int_bv [simp]: "bv_to_int (int_to_bv i) = i"
by (cases "0 ≤ i") simp_all

lemma bv_msb_norm [simp]: "bv_msb (norm_signed w) = bv_msb w"
by (rule bit_list_cases [of w]) (simp_all add: norm_signed_Cons)

lemma norm_signed_length: "length (norm_signed w) ≤ length w"
apply (cases w, simp_all)
apply (subst norm_signed_Cons)
apply (case_tac a, simp_all)
apply (rule rem_initial_length)
done

lemma norm_signed_equal: "length (norm_signed w) = length w ==> norm_signed w = w"
proof (rule bit_list_cases [of w], simp_all)
fix xs
assume "length (norm_signed (𝟬#xs)) = Suc (length xs)"
thus "norm_signed (𝟬#xs) = 𝟬#xs"
by (simp add: norm_signed_Cons norm_unsigned_equal [THEN eqTrueI]
split: if_split_asm)
next
fix xs
assume "length (norm_signed (𝟭#xs)) = Suc (length xs)"
thus "norm_signed (𝟭#xs) = 𝟭#xs"
apply (rule rem_initial_equal)
apply assumption
done
qed

lemma bv_extend_norm_signed: "bv_msb w = b ==> bv_extend (length w) b (norm_signed w) = w"
proof (rule bit_list_cases [of w],simp_all)
fix xs
show "bv_extend (Suc (length xs)) 𝟬 (norm_signed (𝟬#xs)) = 𝟬#xs"
assume "norm_unsigned xs = []"
hence xx: "rem_initial 𝟬 xs = []"
have "bv_extend (Suc (length xs)) 𝟬 (𝟬#rem_initial 𝟬 xs) = 𝟬#xs"
apply (fold bv_extend_def)
apply (rule bv_extend_rem_initial)
done
thus "bv_extend (Suc (length xs)) 𝟬  = 𝟬#xs"
next
show "bv_extend (Suc (length xs)) 𝟬 (𝟬#norm_unsigned xs) = 𝟬#xs"
apply (fold bv_extend_def)
apply (rule bv_extend_rem_initial)
done
qed
next
fix xs
show "bv_extend (Suc (length xs)) 𝟭 (norm_signed (𝟭#xs)) = 𝟭#xs"
apply (fold bv_extend_def)
apply (rule bv_extend_rem_initial)
done
qed

lemma bv_to_int_qinj:
assumes one: "bv_to_int xs = bv_to_int ys"
and     len: "length xs = length ys"
shows        "xs = ys"
proof -
from one
have "int_to_bv (bv_to_int xs) = int_to_bv (bv_to_int ys)" by simp
hence xsys: "norm_signed xs = norm_signed ys" by simp
hence xsys': "bv_msb xs = bv_msb ys"
proof -
have "bv_msb xs = bv_msb (norm_signed xs)" by simp
also have "... = bv_msb (norm_signed ys)" by (simp add: xsys)
also have "... = bv_msb ys" by simp
finally show ?thesis .
qed
have "xs = bv_extend (length xs) (bv_msb xs) (norm_signed xs)"
also have "... = bv_extend (length ys) (bv_msb ys) (norm_signed ys)"
by (simp add: xsys xsys' len)
also have "... = ys"
finally show ?thesis .
qed

lemma int_to_bv_returntype [simp]: "norm_signed (int_to_bv w) = int_to_bv w"

lemma bv_to_int_msb0: "0 ≤ bv_to_int w1 ==> bv_msb w1 = 𝟬"
by (rule bit_list_cases,simp_all)

lemma bv_to_int_msb1: "bv_to_int w1 < 0 ==> bv_msb w1 = 𝟭"
by (rule bit_list_cases,simp_all)

lemma bv_to_int_lower_limit_gt0:
assumes w0: "0 < bv_to_int w"
shows       "2 ^ (length (norm_signed w) - 2) ≤ bv_to_int w"
proof -
from w0
have "0 ≤ bv_to_int w" by simp
hence [simp]: "bv_msb w = 𝟬" by (rule bv_to_int_msb0)
have "2 ^ (length (norm_signed w) - 2) ≤ bv_to_int (norm_signed w)"
proof (rule bit_list_cases [of w])
assume "w = []"
with w0 show ?thesis by simp
next
fix w'
assume weq: "w = 𝟬 # w'"
thus ?thesis
assume "norm_unsigned w' = []"
with weq and w0 show False
next
assume w'0: "norm_unsigned w' ≠ []"
have "0 < bv_to_nat w'"
proof (rule ccontr)
assume "~ (0 < bv_to_nat w')"
hence "bv_to_nat w' = 0"
by arith
hence "norm_unsigned w' = []"
with w'0
show False by simp
qed
with bv_to_nat_lower_limit [of w']
show "2 ^ (length (norm_unsigned w') - Suc 0) ≤ bv_to_nat w'"
using One_nat_def int_nat_two_exp by presburger
qed
next
fix w'
assume weq: "w = 𝟭 # w'"
from w0 have "bv_msb w = 𝟬" by simp
with weq show ?thesis by simp
qed
also have "...  = bv_to_int w" by simp
finally show ?thesis .
qed

lemma norm_signed_result: "norm_signed w = [] ∨ norm_signed w =  ∨ bv_msb (norm_signed w) ≠ bv_msb (tl (norm_signed w))"
apply (rule bit_list_cases [of w],simp_all)
apply (case_tac "bs",simp_all)
apply (case_tac "a",simp_all)
apply safe
apply simp
proof -
fix l
assume msb: "𝟬 = bv_msb (norm_unsigned l)"
assume "norm_unsigned l ≠ []"
with norm_unsigned_result [of l]
have "bv_msb (norm_unsigned l) = 𝟭" by simp
with msb show False by simp
next
fix xs
assume p: "𝟭 = bv_msb (tl (norm_signed (𝟭 # xs)))"
have "𝟭 ≠ bv_msb (tl (norm_signed (𝟭 # xs)))"
by (rule bit_list_induct [of _ xs],simp_all)
with p show False by simp
qed

lemma bv_to_int_upper_limit_lem1:
assumes w0: "bv_to_int w < -1"
shows       "bv_to_int w < - (2 ^ (length (norm_signed w) - 2))"
proof -
from w0
have "bv_to_int w < 0" by simp
hence msbw [simp]: "bv_msb w = 𝟭"
by (rule bv_to_int_msb1)
have "bv_to_int w = bv_to_int (norm_signed w)" by simp
also from norm_signed_result [of w]
have "... < - (2 ^ (length (norm_signed w) - 2))"
proof safe
assume "norm_signed w = []"
hence "bv_to_int (norm_signed w) = 0" by simp
with w0 show ?thesis by simp
next
assume "norm_signed w = "
hence "bv_to_int (norm_signed w) = -1" by simp
with w0 show ?thesis by simp
next
assume "bv_msb (norm_signed w) ≠ bv_msb (tl (norm_signed w))"
hence msb_tl: "𝟭 ≠ bv_msb (tl (norm_signed w))" by simp
show "bv_to_int (norm_signed w) < - (2 ^ (length (norm_signed w) - 2))"
proof (rule bit_list_cases [of "norm_signed w"])
assume "norm_signed w = []"
hence "bv_to_int (norm_signed w) = 0" by simp
with w0 show ?thesis by simp
next
fix w'
assume nw: "norm_signed w = 𝟬 # w'"
from msbw have "bv_msb (norm_signed w) = 𝟭" by simp
with nw show ?thesis by simp
next
fix w'
assume weq: "norm_signed w = 𝟭 # w'"
show ?thesis
proof (rule bit_list_cases [of w'])
assume w'eq: "w' = []"
from w0 have "bv_to_int (norm_signed w) < -1" by simp
with w'eq and weq show ?thesis by simp
next
fix w''
assume w'eq: "w' = 𝟬 # w''"
show ?thesis
next
fix w''
assume w'eq: "w' = 𝟭 # w''"
with weq and msb_tl show ?thesis by simp
qed
qed
qed
finally show ?thesis .
qed

lemma length_int_to_bv_upper_limit_gt0:
assumes w0: "0 < i"
and     wk: "i ≤ 2 ^ (k - 1) - 1"
shows       "length (int_to_bv i) ≤ k"
proof (rule ccontr)
from w0 wk
have k1: "1 < k"
by (cases "k - 1",simp_all)
assume "~ length (int_to_bv i) ≤ k"
hence "k < length (int_to_bv i)" by simp
hence "k ≤ length (int_to_bv i) - 1" by arith
hence a: "k - 1 ≤ length (int_to_bv i) - 2" by arith
hence "(2::int) ^ (k - 1) ≤ 2 ^ (length (int_to_bv i) - 2)" by simp
also have "... ≤ i"
proof -
have "2 ^ (length (norm_signed (int_to_bv i)) - 2) ≤ bv_to_int (int_to_bv i)"
proof (rule bv_to_int_lower_limit_gt0)
from w0 show "0 < bv_to_int (int_to_bv i)" by simp
qed
thus ?thesis by simp
qed
finally have "2 ^ (k - 1) ≤ i" .
with wk show False by simp
qed

lemma pos_length_pos:
assumes i0: "0 < bv_to_int w"
shows       "0 < length w"
proof -
from norm_signed_result [of w]
have "0 < length (norm_signed w)"
proof (auto)
assume ii: "norm_signed w = []"
have "bv_to_int (norm_signed w) = 0" by (subst ii) simp
hence "bv_to_int w = 0" by simp
with i0 show False by simp
next
assume ii: "norm_signed w = []"
assume jj: "bv_msb w ≠ 𝟬"
have "𝟬 = bv_msb (norm_signed w)"
by (subst ii) simp
also have "... ≠ 𝟬"
finally show False by simp
qed
also have "... ≤ length w"
by (rule norm_signed_length)
finally show ?thesis .
qed

lemma neg_length_pos:
assumes i0: "bv_to_int w < -1"
shows       "0 < length w"
proof -
from norm_signed_result [of w]
have "0 < length (norm_signed w)"
proof (auto)
assume ii: "norm_signed w = []"
have "bv_to_int (norm_signed w) = 0"
by (subst ii) simp
hence "bv_to_int w = 0" by simp
with i0 show False by simp
next
assume ii: "norm_signed w = []"
assume jj: "bv_msb w ≠ 𝟬"
have "𝟬 = bv_msb (norm_signed w)" by (subst ii) simp
also have "... ≠ 𝟬" by (simp add: jj)
finally show False by simp
qed
also have "... ≤ length w"
by (rule norm_signed_length)
finally show ?thesis .
qed

lemma length_int_to_bv_lower_limit_gt0:
assumes wk: "2 ^ (k - 1) ≤ i"
shows       "k < length (int_to_bv i)"
proof (rule ccontr)
have "0 < (2::int) ^ (k - 1)"
by (rule zero_less_power) simp
also have "... ≤ i" by (rule wk)
finally have i0: "0 < i" .
have lii0: "0 < length (int_to_bv i)"
apply (rule pos_length_pos)
apply (simp,rule i0)
done
assume "~ k < length (int_to_bv i)"
hence "length (int_to_bv i) ≤ k" by simp
with lii0
have a: "length (int_to_bv i) - 1 ≤ k - 1"
by arith
have "i < 2 ^ (length (int_to_bv i) - 1)"
proof -
have "i = bv_to_int (int_to_bv i)"
by simp
also have "... < 2 ^ (length (int_to_bv i) - 1)"
by (rule bv_to_int_upper_range)
finally show ?thesis .
qed
also have "(2::int) ^ (length (int_to_bv i) - 1) ≤ 2 ^ (k - 1)" using a
by simp
finally have "i < 2 ^ (k - 1)" .
with wk show False by simp
qed

lemma length_int_to_bv_upper_limit_lem1:
assumes w1: "i < -1"
and     wk: "- (2 ^ (k - 1)) ≤ i"
shows       "length (int_to_bv i) ≤ k"
proof (rule ccontr)
from w1 wk
have k1: "1 < k" by (cases "k - 1") simp_all
assume "~ length (int_to_bv i) ≤ k"
hence "k < length (int_to_bv i)" by simp
hence "k ≤ length (int_to_bv i) - 1" by arith
hence a: "k - 1 ≤ length (int_to_bv i) - 2" by arith
have "i < - (2 ^ (length (int_to_bv i) - 2))"
proof -
have "i = bv_to_int (int_to_bv i)"
by simp
also have "... < - (2 ^ (length (norm_signed (int_to_bv i)) - 2))"
by (rule bv_to_int_upper_limit_lem1,simp,rule w1)
finally show ?thesis by simp
qed
also have "... ≤ -(2 ^ (k - 1))"
proof -
have "(2::int) ^ (k - 1) ≤ 2 ^ (length (int_to_bv i) - 2)" using a by simp
thus ?thesis by simp
qed
finally have "i < -(2 ^ (k - 1))" .
with wk show False by simp
qed

lemma length_int_to_bv_lower_limit_lem1:
assumes wk: "i < -(2 ^ (k - 1))"
shows       "k < length (int_to_bv i)"
proof (rule ccontr)
from wk have "i ≤ -(2 ^ (k - 1)) - 1" by simp
also have "... < -1"
proof -
have "0 < (2::int) ^ (k - 1)"
by (rule zero_less_power) simp
hence "-((2::int) ^ (k - 1)) < 0" by simp
thus ?thesis by simp
qed
finally have i1: "i < -1" .
have lii0: "0 < length (int_to_bv i)"
apply (rule neg_length_pos)
apply (simp, rule i1)
done
assume "~ k < length (int_to_bv i)"
hence "length (int_to_bv i) ≤ k"
by simp
with lii0 have a: "length (int_to_bv i) - 1 ≤ k - 1" by arith
hence "(2::int) ^ (length (int_to_bv i) - 1) ≤ 2 ^ (k - 1)" by simp
hence "-((2::int) ^ (k - 1)) ≤ - (2 ^ (length (int_to_bv i) - 1))" by simp
also have "... ≤ i"
proof -
have "- (2 ^ (length (int_to_bv i) - 1)) ≤ bv_to_int (int_to_bv i)"
by (rule bv_to_int_lower_range)
also have "... = i"
by simp
finally show ?thesis .
qed
finally have "-(2 ^ (k - 1)) ≤ i" .
with wk show False by simp
qed

subsection ‹Signed Arithmetic Operations›

subsubsection ‹Conversion from unsigned to signed›

definition
utos :: "bit list => bit list" where
"utos w = norm_signed (𝟬 # w)"

lemma utos_type [simp]: "utos (norm_unsigned w) = utos w"

lemma utos_returntype [simp]: "norm_signed (utos w) = utos w"

lemma utos_length: "length (utos w) ≤ Suc (length w)"

lemma bv_to_int_utos: "bv_to_int (utos w) = int (bv_to_nat w)"
proof (simp add: utos_def norm_signed_Cons, safe)
assume "norm_unsigned w = []"
hence "bv_to_nat (norm_unsigned w) = 0" by simp
thus "bv_to_nat w = 0" by simp
qed

subsubsection ‹Unary minus›

definition
bv_uminus :: "bit list => bit list" where
"bv_uminus w = int_to_bv (- bv_to_int w)"

lemma bv_uminus_type [simp]: "bv_uminus (norm_signed w) = bv_uminus w"

lemma bv_uminus_returntype [simp]: "norm_signed (bv_uminus w) = bv_uminus w"

lemma bv_uminus_length: "length (bv_uminus w) ≤ Suc (length w)"
proof -
have "1 < -bv_to_int w ∨ -bv_to_int w = 1 ∨ -bv_to_int w = 0 ∨ -bv_to_int w = -1 ∨ -bv_to_int w < -1"
by arith
thus ?thesis
proof safe
assume p: "1 < - bv_to_int w"
have lw: "0 < length w"
apply (rule neg_length_pos)
using p
apply simp
done
show ?thesis
from p show "bv_to_int w < 0" by simp
next
have "-(2^(length w - 1)) ≤ bv_to_int w"
by (rule bv_to_int_lower_range)
hence "- bv_to_int w ≤ 2^(length w - 1)" by simp
also from lw have "... < 2 ^ length w" by simp
finally show "- bv_to_int w < 2 ^ length w" by simp
qed
next
assume p: "- bv_to_int w = 1"
hence lw: "0 < length w" by (cases w) simp_all
from p
show ?thesis
using lw
done
next
assume "- bv_to_int w = 0"
thus ?thesis by (simp add: bv_uminus_def)
next
assume p: "- bv_to_int w = -1"
thus ?thesis by (simp add: bv_uminus_def)
next
assume p: "- bv_to_int w < -1"
show ?thesis
apply (rule length_int_to_bv_upper_limit_lem1)
apply (rule p)
apply simp
proof -
have "bv_to_int w < 2 ^ (length w - 1)"
by (rule bv_to_int_upper_range)
also have "... ≤ 2 ^ length w" by simp
finally show "bv_to_int w ≤ 2 ^ length w" by simp
qed
qed
qed

lemma bv_uminus_length_utos: "length (bv_uminus (utos w)) ≤ Suc (length w)"
proof -
have "-bv_to_int (utos w) = 0 ∨ -bv_to_int (utos w) = -1 ∨ -bv_to_int (utos w) < -1"
thus ?thesis
proof safe
assume "-bv_to_int (utos w) = 0"
thus ?thesis by (simp add: bv_uminus_def)
next
assume "-bv_to_int (utos w) = -1"
thus ?thesis by (simp add: bv_uminus_def)
next
assume p: "-bv_to_int (utos w) < -1"
show ?thesis
apply (rule length_int_to_bv_upper_limit_lem1)
apply (rule p)
using bv_to_nat_upper_range [of w] int_nat_two_exp apply presburger
done
qed
qed

definition
bv_sadd :: "[bit list, bit list ] => bit list" where
"bv_sadd w1 w2 = int_to_bv (bv_to_int w1 + bv_to_int w2)"

assumes lw: "0 < max (length w1) (length w2)"
shows   "((2::int) ^ (length w1 - 1)) + (2 ^ (length w2 - 1)) ≤ 2 ^ max (length w1) (length w2)"
proof -
have "((2::int) ^ (length w1 - 1)) + (2 ^ (length w2 - 1)) ≤
2 ^ (max (length w1) (length w2) - 1) + 2 ^ (max (length w1) (length w2) - 1)"
by (auto simp:max_def)
also have "... = 2 ^ max (length w1) (length w2)"
proof -
from lw
show ?thesis
apply simp
apply (subst power_Suc [symmetric])
apply simp
done
qed
finally show ?thesis .
qed

lemma bv_sadd_length: "length (bv_sadd w1 w2) ≤ Suc (max (length w1) (length w2))"
proof -
let ?Q = "bv_to_int w1 + bv_to_int w2"

have helper: "?Q ≠ 0 ==> 0 < max (length w1) (length w2)"
proof -
assume p: "?Q ≠ 0"
show "0 < max (length w1) (length w2)"
assume [simp]: "w1 = []"
show "w2 ≠ []"
proof (rule ccontr,simp)
assume [simp]: "w2 = []"
from p show False by simp
qed
qed
qed

have "0 < ?Q ∨ ?Q = 0 ∨ ?Q = -1 ∨ ?Q < -1" by arith
thus ?thesis
proof safe
assume "?Q = 0"
thus ?thesis
next
assume "?Q = -1"
thus ?thesis
next
assume p: "0 < ?Q"
show ?thesis
apply (rule length_int_to_bv_upper_limit_gt0)
apply (rule p)
proof simp
from bv_to_int_upper_range [of w2]
have "bv_to_int w2 ≤ 2 ^ (length w2 - 1)"
by simp
with bv_to_int_upper_range [of w1]
have "bv_to_int w1 + bv_to_int w2 < (2 ^ (length w1 - 1)) + (2 ^ (length w2 - 1))"
also have "... ≤ 2 ^ max (length w1) (length w2)"
apply (rule helper)
using p
apply simp
done
finally show "?Q < 2 ^ max (length w1) (length w2)" .
qed
next
assume p: "?Q < -1"
show ?thesis
apply (rule length_int_to_bv_upper_limit_lem1,simp_all)
apply (rule p)
proof -
have "(2 ^ (length w1 - 1)) + 2 ^ (length w2 - 1) ≤ (2::int) ^ max (length w1) (length w2)"
apply (rule helper)
using p
apply simp
done
hence "-((2::int) ^ max (length w1) (length w2)) ≤ - (2 ^ (length w1 - 1)) + -(2 ^ (length w2 - 1))"
by simp
also have "- (2 ^ (length w1 - 1)) + -(2 ^ (length w2 - 1)) ≤ ?Q"
apply (rule bv_to_int_lower_range [of w1])
apply (rule bv_to_int_lower_range [of w2])
done
finally show "- (2^max (length w1) (length w2)) ≤ ?Q" .
qed
qed
qed

definition
bv_sub :: "[bit list, bit list] => bit list" where
"bv_sub w1 w2 = bv_sadd w1 (bv_uminus w2)"

lemma bv_sub_type1 [simp]: "bv_sub (norm_signed w1) w2 = bv_sub w1 w2"

lemma bv_sub_type2 [simp]: "bv_sub w1 (norm_signed w2) = bv_sub w1 w2"

lemma bv_sub_returntype [simp]: "norm_signed (bv_sub w1 w2) = bv_sub w1 w2"

lemma bv_sub_length: "length (bv_sub w1 w2) ≤ Suc (max (length w1) (length w2))"
proof (cases "bv_to_int w2 = 0")
assume p: "bv_to_int w2 = 0"
show ?thesis
have "length (norm_signed w1) ≤ length w1"
by (rule norm_signed_length)
also have "... ≤ max (length w1) (length w2)"
by (rule max.cobounded1)
also have "... ≤ Suc (max (length w1) (length w2))"
by arith
finally show "length (norm_signed w1) ≤ Suc (max (length w1) (length w2))" .
qed
next
assume "bv_to_int w2 ≠ 0"
hence "0 < length w2" by (cases w2,simp_all)
hence lmw: "0 < max (length w1) (length w2)" by arith

let ?Q = "bv_to_int w1 - bv_to_int w2"

have "0 < ?Q ∨ ?Q = 0 ∨ ?Q = -1 ∨ ?Q < -1" by arith
thus ?thesis
proof safe
assume "?Q = 0"
thus ?thesis
next
assume "?Q = -1"
thus ?thesis
next
assume p: "0 < ?Q"
show ?thesis
apply (rule length_int_to_bv_upper_limit_gt0)
apply (rule p)
proof simp
from bv_to_int_lower_range [of w2]
have v2: "- bv_to_int w2 ≤ 2 ^ (length w2 - 1)" by simp
have "bv_to_int w1 + - bv_to_int w2 < (2 ^ (length w1 - 1)) + (2 ^ (length w2 - 1))"
apply (rule bv_to_int_upper_range [of w1])
apply (rule v2)
done
also have "... ≤ 2 ^ max (length w1) (length w2)"
apply (rule lmw)
done
finally show "?Q < 2 ^ max (length w1) (length w2)" by simp
qed
next
assume p: "?Q < -1"
show ?thesis
apply (rule length_int_to_bv_upper_limit_lem1)
apply (rule p)
proof simp
have "(2 ^ (length w1 - 1)) + 2 ^ (length w2 - 1) ≤ (2::int) ^ max (length w1) (length w2)"
apply (rule lmw)
done
hence "-((2::int) ^ max (length w1) (length w2)) ≤ - (2 ^ (length w1 - 1)) + -(2 ^ (length w2 - 1))"
by simp
also have "- (2 ^ (length w1 - 1)) + -(2 ^ (length w2 - 1)) ≤ bv_to_int w1 + -bv_to_int w2"
apply (rule bv_to_int_lower_range [of w1])
using bv_to_int_upper_range [of w2]
apply simp
done
finally show "- (2^max (length w1) (length w2)) ≤ ?Q" by simp
qed
qed
qed

definition
bv_smult :: "[bit list, bit list] => bit list" where
"bv_smult w1 w2 = int_to_bv (bv_to_int w1 * bv_to_int w2)"

lemma bv_smult_type1 [simp]: "bv_smult (norm_signed w1) w2 = bv_smult w1 w2"

lemma bv_smult_type2 [simp]: "bv_smult w1 (norm_signed w2) = bv_smult w1 w2"

lemma bv_smult_returntype [simp]: "norm_signed (bv_smult w1 w2) = bv_smult w1 w2"

lemma bv_smult_length: "length (bv_smult w1 w2) ≤ length w1 + length w2"
proof -
let ?Q = "bv_to_int w1 * bv_to_int w2"

have lmw: "?Q ≠ 0 ==> 0 < length w1 ∧ 0 < length w2" by auto

have "0 < ?Q ∨ ?Q = 0 ∨ ?Q = -1 ∨ ?Q < -1" by arith
thus ?thesis
proof (safe dest!: iffD1 [OF mult_eq_0_iff])
assume "bv_to_int w1 = 0"
thus ?thesis by (simp add: bv_smult_def)
next
assume "bv_to_int w2 = 0"
thus ?thesis by (simp add: bv_smult_def)
next
assume p: "?Q = -1"
show ?thesis
apply (cut_tac lmw)
apply arith
using p
apply simp
done
next
assume p: "0 < ?Q"
thus ?thesis
assume bi1: "0 < bv_to_int w1"
assume bi2: "0 < bv_to_int w2"
show ?thesis
apply (rule length_int_to_bv_upper_limit_gt0)
apply (rule p)
proof simp
have "?Q < 2 ^ (length w1 - 1) * 2 ^ (length w2 - 1)"
apply (rule mult_strict_mono)
apply (rule bv_to_int_upper_range)
apply (rule bv_to_int_upper_range)
apply (rule zero_less_power)
apply simp
using bi2
apply simp
done
also have "... ≤ 2 ^ (length w1 + length w2 - Suc 0)"
apply simp
apply simp
done
finally show "?Q < 2 ^ (length w1 + length w2 - Suc 0)" .
qed
next
assume bi1: "bv_to_int w1 < 0"
assume bi2: "bv_to_int w2 < 0"
show ?thesis
apply (rule length_int_to_bv_upper_limit_gt0)
apply (rule p)
proof simp
have "-bv_to_int w1 * -bv_to_int w2 ≤ 2 ^ (length w1 - 1) * 2 ^(length w2 - 1)"
apply (rule mult_mono)
using bv_to_int_lower_range [of w1]
apply simp
using bv_to_int_lower_range [of w2]
apply simp
apply (rule zero_le_power,simp)
using bi2
apply simp
done
hence "?Q ≤ 2 ^ (length w1 - 1) * 2 ^(length w2 - 1)"
by simp
also have "... < 2 ^ (length w1 + length w2 - Suc 0)"
apply simp
apply simp
apply (cut_tac lmw)
apply arith
apply (cut_tac p)
apply arith
done
finally show "?Q < 2 ^ (length w1 + length w2 - Suc 0)" .
qed
qed
next
assume p: "?Q < -1"
show ?thesis
apply (subst bv_smult_def)
apply (rule length_int_to_bv_upper_limit_lem1)
apply (rule p)
proof simp
have "(2::int) ^ (length w1 - 1) * 2 ^(length w2 - 1) ≤ 2 ^ (length w1 + length w2 - Suc 0)"
apply simp
apply simp
done
hence "-((2::int) ^ (length w1 + length w2 - Suc 0)) ≤ -(2^(length w1 - 1) * 2 ^ (length w2 - 1))"
by simp
also have "... ≤ ?Q"
proof -
from p
have q: "bv_to_int w1 * bv_to_int w2 < 0"
by simp
thus ?thesis
assume bi1: "0 < bv_to_int w1"
assume bi2: "bv_to_int w2 < 0"
have "-bv_to_int w2 * bv_to_int w1 ≤ ((2::int)^(length w2 - 1)) * (2 ^ (length w1 - 1))"
apply (rule mult_mono)
using bv_to_int_lower_range [of w2]
apply simp
using bv_to_int_upper_range [of w1]
apply simp
apply (rule zero_le_power,simp)
using bi1
apply simp
done
hence "-?Q ≤ ((2::int)^(length w1 - 1)) * (2 ^ (length w2 - 1))"
thus "-(((2::int)^(length w1 - Suc 0)) * (2 ^ (length w2 - Suc 0))) ≤ ?Q"
by simp
next
assume bi1: "bv_to_int w1 < 0"
assume bi2: "0 < bv_to_int w2"
have "-bv_to_int w1 * bv_to_int w2 ≤ ((2::int)^(length w1 - 1)) * (2 ^ (length w2 - 1))"
apply (rule mult_mono)
using bv_to_int_lower_range [of w1]
apply simp
using bv_to_int_upper_range [of w2]
apply simp
apply (rule zero_le_power,simp)
using bi2
apply simp
done
hence "-?Q ≤ ((2::int)^(length w1 - 1)) * (2 ^ (length w2 - 1))"
thus "-(((2::int)^(length w1 - Suc 0)) * (2 ^ (length w2 - Suc 0))) ≤ ?Q"
by simp
qed
qed
finally show "-(2 ^ (length w1 + length w2 - Suc 0)) ≤ ?Q" .
qed
qed
qed

lemma bv_msb_one: "bv_msb w = 𝟭 ==> bv_to_nat w ≠ 0"
by (cases w) simp_all

lemma bv_smult_length_utos: "length (bv_smult (utos w1) w2) ≤ length w1 + length w2"
proof -
let ?Q = "bv_to_int (utos w1) * bv_to_int w2"

have lmw: "?Q ≠ 0 ==> 0 < length (utos w1) ∧ 0 < length w2" by auto

have "0 < ?Q ∨ ?Q = 0 ∨ ?Q = -1 ∨ ?Q < -1" by arith
thus ?thesis
proof (safe dest!: iffD1 [OF mult_eq_0_iff])
assume "bv_to_int (utos w1) = 0"
thus ?thesis by (simp add: bv_smult_def)
next
assume "bv_to_int w2 = 0"
thus ?thesis by (simp add: bv_smult_def)
next
assume p: "0 < ?Q"
thus ?thesis
assume biw2: "0 < bv_to_int w2"
show ?thesis
apply (rule length_int_to_bv_upper_limit_gt0)
apply (rule p)
proof simp
have "?Q < 2 ^ length w1 * 2 ^ (length w2 - 1)"
apply (rule mult_strict_mono)
apply (simp add: bv_to_int_utos bv_to_nat_upper_range int_nat_two_exp del: of_nat_power)
apply (rule bv_to_int_upper_range)
apply (rule zero_less_power,simp)
using biw2
apply simp
done
also have "... ≤ 2 ^ (length w1 + length w2 - Suc 0)"
apply simp
apply simp
apply (cut_tac lmw)
apply arith
using p
apply auto
done
finally show "?Q < 2 ^ (length w1 + length w2 - Suc 0)" .
qed
next
assume "bv_to_int (utos w1) < 0"
thus ?thesis by (simp add: bv_to_int_utos)
qed
next
assume p: "?Q = -1"
thus ?thesis
apply (cut_tac lmw)
apply arith
apply simp
done
next
assume p: "?Q < -1"
show ?thesis
apply (subst bv_smult_def)
apply (rule length_int_to_bv_upper_limit_lem1)
apply (rule p)
proof simp
have "(2::int) ^ length w1 * 2 ^(length w2 - 1) ≤ 2 ^ (length w1 + length w2 - Suc 0)"
apply simp
apply simp
apply (cut_tac lmw)
apply arith
apply (cut_tac p)
apply arith
done
hence "-((2::int) ^ (length w1 + length w2 - Suc 0)) ≤ -(2^ length w1 * 2 ^ (length w2 - 1))"
by simp
also have "... ≤ ?Q"
proof -
from p
have q: "bv_to_int (utos w1) * bv_to_int w2 < 0"
by simp
thus ?thesis
assume bi1: "0 < bv_to_int (utos w1)"
assume bi2: "bv_to_int w2 < 0"
have "-bv_to_int w2 * bv_to_int (utos w1) ≤ ((2::int)^(length w2 - 1)) * (2 ^ length w1)"
apply (rule mult_mono)
using bv_to_int_lower_range [of w2]
apply simp
using bv_to_nat_upper_range [of w1]
apply (simp add: int_nat_two_exp del: of_nat_power)
apply (rule zero_le_power,simp)
using bi1
apply simp
done
hence "-?Q ≤ ((2::int)^length w1) * (2 ^ (length w2 - 1))"
thus "-(((2::int)^length w1) * (2 ^ (length w2 - Suc 0))) ≤ ?Q"
by simp
next
assume bi1: "bv_to_int (utos w1) < 0"
thus "-(((2::int)^length w1) * (2 ^ (length w2 - Suc 0))) ≤ ?Q"
qed
qed
finally show "-(2 ^ (length w1 + length w2 - Suc 0)) ≤ ?Q" .
qed
qed
qed

lemma bv_smult_sym: "bv_smult w1 w2 = bv_smult w2 w1"

subsection ‹Structural operations›

definition
bv_select :: "[bit list,nat] => bit" where
"bv_select w i = w ! (length w - 1 - i)"

definition
bv_chop :: "[bit list,nat] => bit list * bit list" where
"bv_chop w i = (let len = length w in (take (len - i) w,drop (len - i) w))"

definition
bv_slice :: "[bit list,nat*nat] => bit list" where
"bv_slice w = (λ(b,e). fst (bv_chop (snd (bv_chop w (b+1))) e))"

lemma bv_select_rev:
assumes notnull: "n < length w"
shows            "bv_select w n = rev w ! n"
proof -
have "∀n. n < length w --> bv_select w n = rev w ! n"
proof (rule length_induct [of _ w],auto simp add: bv_select_def)
fix xs :: "bit list"
fix n
assume ind: "∀ys::bit list. length ys < length xs --> (∀n. n < length ys --> ys ! (length ys - Suc n) = rev ys ! n)"
assume notx: "n < length xs"
show "xs ! (length xs - Suc n) = rev xs ! n"
proof (cases xs)
assume "xs = []"
with notx show ?thesis by simp
next
fix y ys
assume [simp]: "xs = y # ys"
show ?thesis
assume noty: "n < length ys"
from spec [OF ind,of ys]
have "∀n. n < length ys --> ys ! (length ys - Suc n) = rev ys ! n"
by simp
hence "n < length ys --> ys ! (length ys - Suc n) = rev ys ! n" ..
from this and noty
show "ys ! (length ys - Suc n) = rev ys ! n" ..
next
assume "~ n < length ys"
hence x: "length ys ≤ n" by simp
from notx have "n < Suc (length ys)" by simp
hence "n ≤ length ys" by simp
with x have "length ys = n" by simp
thus "y = [y] ! (n - length ys)" by simp
qed
qed
qed
then have "n < length w --> bv_select w n = rev w ! n" ..
from this and notnull show ?thesis ..
qed

lemma bv_chop_append: "bv_chop (w1 @ w2) (length w2) = (w1,w2)"

lemma append_bv_chop_id: "fst (bv_chop w l) @ snd (bv_chop w l) = w"

lemma bv_chop_length_fst [simp]: "length (fst (bv_chop w i)) = length w - i"

lemma bv_chop_length_snd [simp]: "length (snd (bv_chop w i)) = min i (length w)"

lemma bv_slice_length [simp]: "[| j ≤ i; i < length w |] ==> length (bv_slice w (i,j)) = i - j + 1"

definition
length_nat :: "nat => nat" where
[code del]: "length_nat x = (LEAST n. x < 2 ^ n)"

lemma length_nat: "length (nat_to_bv n) = length_nat n"
apply (rule Least_equality [symmetric])
prefer 2
apply (rule length_nat_to_bv_upper_limit)
apply arith
apply (rule ccontr)
proof -
assume "~ n < 2 ^ length (nat_to_bv n)"
hence "2 ^ length (nat_to_bv n) ≤ n" by simp
hence "length (nat_to_bv n) < length (nat_to_bv n)"
by (rule length_nat_to_bv_lower_limit)
thus False by simp
qed

lemma length_nat_0 [simp]: "length_nat 0 = 0"

lemma length_nat_non0:
assumes n0: "n ≠ 0"
shows       "length_nat n = Suc (length_nat (n div 2))"
apply (subst nat_to_bv_non0 [of n])
done

definition
length_int :: "int => nat" where
"length_int x =
(if 0 < x then Suc (length_nat (nat x))
else if x = 0 then 0
else Suc (length_nat (nat (-x - 1))))"

lemma length_int: "length (int_to_bv i) = length_int i"
proof (cases "0 < i")
assume i0: "0 < i"
hence "length (int_to_bv i) =
length (norm_signed (𝟬 # norm_unsigned (nat_to_bv (nat i))))" by simp
also from norm_unsigned_result [of "nat_to_bv (nat i)"]
have "... = Suc (length_nat (nat i))"
apply safe
apply (simp del: norm_unsigned_nat_to_bv)
apply (drule norm_empty_bv_to_nat_zero)
using i0 apply simp
apply (cases "norm_unsigned (nat_to_bv (nat i))")
apply (drule norm_empty_bv_to_nat_zero [of "nat_to_bv (nat i)"])
using i0 apply simp
using i0 apply (simp add: length_nat [symmetric])
done
finally show ?thesis
using i0
next
assume "~ 0 < i"
hence i0: "i ≤ 0" by simp
show ?thesis
proof (cases "i = 0")
assume "i = 0"
thus ?thesis by (simp add: length_int_def)
next
assume "i ≠ 0"
with i0 have i0: "i < 0" by simp
hence "length (int_to_bv i) =
length (norm_signed (𝟭 # bv_not (norm_unsigned (nat_to_bv (nat (- i) - 1)))))"
also from norm_unsigned_result [of "nat_to_bv (nat (- i) - 1)"]
have "... = Suc (length_nat (nat (- i) - 1))"
apply safe
apply (simp del: norm_unsigned_nat_to_bv)
apply (drule norm_empty_bv_to_nat_zero [of "nat_to_bv (nat (-i) - Suc 0)"])
using i0 apply simp
apply (cases "- i - 1 = 0")
apply simp
apply (cases "norm_unsigned (nat_to_bv (nat (- i) - 1))")
apply simp
apply simp
done
finally
show ?thesis
using i0 by (simp add: length_int_def nat_diff_distrib del: int_to_bv_lt0)
qed
qed

lemma length_int_0 [simp]: "length_int 0 = 0"

lemma length_int_gt0: "0 < i ==> length_int i = Suc (length_nat (nat i))"

lemma length_int_lt0: "i < 0 ==> length_int i = Suc (length_nat (nat (- i) - 1))"

lemma bv_chopI: "[| w = w1 @ w2 ; i = length w2 |] ==> bv_chop w i = (w1,w2)"

lemma bv_sliceI: "[| j ≤ i ; i < length w ; w = w1 @ w2 @ w3 ; Suc i = length w2 + j ; j = length w3  |] ==> bv_slice w (i,j) = w2"
apply (subst bv_chopI [of "w1 @ w2 @ w3" w1 "w2 @ w3"])
apply simp
apply simp
apply simp
apply (subst bv_chopI [of "w2 @ w3" w2 w3],simp_all)
done

lemma bv_slice_bv_slice:
assumes ki: "k ≤ i"
and     ij: "i ≤ j"
and     jl: "j ≤ l"
and     lw: "l < length w"
shows       "bv_slice w (j,i) = bv_slice (bv_slice w (l,k)) (j-k,i-k)"
proof -
define w1 w2 w3 w4 w5
where w_defs:
"w1 = fst (bv_chop w (Suc l))"
"w2 = fst (bv_chop (snd (bv_chop w (Suc l))) (Suc j))"
"w3 = fst (bv_chop (snd (bv_chop (snd (bv_chop w (Suc l))) (Suc j))) i)"
"w4 = fst (bv_chop (snd (bv_chop (snd (bv_chop (snd (bv_chop w (Suc l))) (Suc j))) i)) k)"
"w5 = snd (bv_chop (snd (bv_chop (snd (bv_chop (snd (bv_chop w (Suc l))) (Suc j))) i)) k)"

have w_def: "w = w1 @ w2 @ w3 @ w4 @ w5"

from ki ij jl lw
show ?thesis
apply (subst bv_sliceI [where ?j = i and ?i = j and ?w = w and ?w1.0 = "w1 @ w2" and ?w2.0 = w3 and ?w3.0 = "w4 @ w5"])
apply simp_all
apply (rule w_def)
apply (subst bv_sliceI [where ?j = k and ?i = l and ?w = w and ?w1.0 = w1 and ?w2.0 = "w2 @ w3 @ w4" and ?w3.0 = w5])
apply simp_all
apply (rule w_def)
apply (subst bv_sliceI [where ?j = "i-k" and ?i = "j-k" and ?w = "w2 @ w3 @ w4" and ?w1.0 = w2 and ?w2.0 = w3 and ?w3.0 = w4])
apply simp_all
done
qed

lemma bv_to_nat_extend [simp]: "bv_to_nat (bv_extend n 𝟬 w) = bv_to_nat w"
apply (subst bv_to_nat_dist_append)
apply simp
apply (induct ("n - length w"))
apply simp_all
done

lemma bv_msb_extend_same [simp]: "bv_msb w = b ==> bv_msb (bv_extend n b w) = b"
apply (cases "n - length w")
apply simp_all
done

lemma bv_to_int_extend [simp]:
assumes a: "bv_msb w = b"
shows      "bv_to_int (bv_extend n b w) = bv_to_int w"
proof (cases "bv_msb w")
assume [simp]: "bv_msb w = 𝟬"
with a have [simp]: "b = 𝟬" by simp
show ?thesis by (simp add: bv_to_int_def)
next
assume [simp]: "bv_msb w = 𝟭"
with a have [simp]: "b = 𝟭" by simp
show ?thesis
apply (induct ("n - length w"), simp_all)
done
qed

lemma length_nat_mono [simp]: "x ≤ y ==> length_nat x ≤ length_nat y"
proof (rule ccontr)
assume xy: "x ≤ y"
assume "~ length_nat x ≤ length_nat y"
hence lxly: "length_nat y < length_nat x"
by simp
hence "length_nat y < (LEAST n. x < 2 ^ n)"
hence "~ x < 2 ^ length_nat y"
by (rule not_less_Least)
hence xx: "2 ^ length_nat y ≤ x"
by simp
have yy: "y < 2 ^ length_nat y"
apply (rule LeastI)
apply (subgoal_tac "y < 2 ^ y",assumption)
apply (cases "0 ≤ y")
apply (induct y,simp_all)
done
with xx have "y < x" by simp
with xy show False by simp
qed

lemma length_nat_mono_int: "x ≤ y ==> length_nat x ≤ length_nat y"
by (rule length_nat_mono) arith

lemma length_nat_pos [simp,intro!]: "0 < x ==> 0 < length_nat x"

lemma length_int_mono_gt0: "[| 0 ≤ x ; x ≤ y |] ==> length_int x ≤ length_int y"
by (cases "x = 0") (simp_all add: length_int_gt0 nat_le_eq_zle)

lemma length_int_mono_lt0: "[| x ≤ y ; y ≤ 0 |] ==> length_int y ≤ length_int x"
by (cases "y = 0") (simp_all add: length_int_lt0)

lemmas [simp] = length_nat_non0

primrec fast_bv_to_nat_helper :: "[bit list, num] => num" where
fast_bv_to_nat_Nil: "fast_bv_to_nat_helper [] k = k"
| fast_bv_to_nat_Cons: "fast_bv_to_nat_helper (b#bs) k =
fast_bv_to_nat_helper bs ((case_bit Num.Bit0 Num.Bit1 b) k)"

declare fast_bv_to_nat_helper.simps [code del]

lemma fast_bv_to_nat_Cons0: "fast_bv_to_nat_helper (𝟬#bs) bin =
fast_bv_to_nat_helper bs (Num.Bit0 bin)"
by simp

lemma fast_bv_to_nat_Cons1: "fast_bv_to_nat_helper (𝟭#bs) bin =
fast_bv_to_nat_helper bs (Num.Bit1 bin)"
by simp

lemma mult_Bit0_left: "Num.Bit0 m * n = Num.Bit0 (m * n)"
by (simp add: num_eq_iff nat_of_num_mult distrib_right)

lemma fast_bv_to_nat_def:
"bv_to_nat (𝟭 # bs) == numeral (fast_bv_to_nat_helper bs Num.One)"
proof -
have "⋀k. foldl (λbn b. 2 * bn + bitval b) (numeral k) bs = numeral (fast_bv_to_nat_helper bs k)"
apply (induct bs, simp)
apply (case_tac a, simp_all add: mult_Bit0_left)
done
thus "PROP ?thesis"
del: numeral_One One_nat_def)
qed

declare fast_bv_to_nat_Cons [simp del]
declare fast_bv_to_nat_Cons0 [simp]
declare fast_bv_to_nat_Cons1 [simp]

simproc_setup bv_to_nat ("bv_to_nat (x # xs)") = ‹
fn _ => fn ctxt => fn ct =>
let
fun is_const_bool (Const(@{const_name True},_)) = true
| is_const_bool (Const(@{const_name False},_)) = true
| is_const_bool _ = false
fun is_const_bit (Const(@{const_name Zero},_)) = true
| is_const_bit (Const(@{const_name One},_)) = true
| is_const_bit _ = false
fun vec_is_usable (Const(@{const_name Nil},_)) = true
| vec_is_usable (Const(@{const_name Cons},_) $b$ bs) =
vec_is_usable bs andalso is_const_bit b
| vec_is_usable _ = false
fun proc (Const(@{const_name bv_to_nat},_) $(Const(@{const_name Cons},_)$ Const(@{const_name One},_) \$ t)) =
if vec_is_usable t then
SOME
(infer_instantiate ctxt
[(("bs", 0), Thm.cterm_of ctxt t)] @{thm fast_bv_to_nat_def})
else NONE
| proc _ = NONE
in proc (Thm.term_of ct) end
›

declare bv_to_nat1 [simp del]
declare bv_to_nat_helper [simp del]

definition
bv_mapzip :: "[bit => bit => bit,bit list, bit list] => bit list" where
"bv_mapzip f w1 w2 =
(let g = bv_extend (max (length w1) (length w2)) 𝟬
in map (case_prod f) (zip (g w1) (g w2)))"

lemma bv_length_bv_mapzip [simp]:
"length (bv_mapzip f w1 w2) = max (length w1) (length w2)"
by (simp add: bv_mapzip_def Let_def split: split_max)

lemma bv_mapzip_Nil [simp]: "bv_mapzip f [] [] = []"

lemma bv_mapzip_Cons [simp]: "length w1 = length w2 ==>
bv_mapzip f (x#w1) (y#w2) = f x y # bv_mapzip f w1 w2"

end


# Theory WordOperations

(*  Title:      RSAPSS/Wordoperations.thy
Author:     Christina Lindenberg, Kai Wirt, Technische Universität Darmstadt
*)

section  ‹Extensions to the Word theory required for SHA1›

theory WordOperations
imports Word
begin

type_synonym bv = "bit list"

datatype HEX = x0 | x1 | x2 | x3 | x4 | x5 | x6 | x7 | x8 | x9 | xA | xB | xC | xD | xE | xF

definition
bvxor: "bvxor a b = bv_mapzip (⊕⇩b) a b"

definition
bvand: "bvand a b = bv_mapzip (∧⇩b) a b"

definition
bvor: "bvor a b = bv_mapzip (∨⇩b) a b"

primrec last where
"last [] = Zero"
| "last (x#r) = (if (r=[]) then x else (last r))"

primrec dellast where
"dellast [] = []"
| "dellast (x#r) = (if (r = []) then [] else (x#dellast r))"

fun bvrol where
"bvrol a 0 = a"
| "bvrol [] x = []"
| "bvrol (x#r) (Suc n) = bvrol (r@[x]) n"

fun bvror where
"bvror a 0 = a"
| "bvror [] x = []"
| "bvror x (Suc n) = bvror (last x # dellast x) n"

fun selecthelp where
"selecthelp [] n = (if (n <= 0) then [Zero] else (Zero # selecthelp [] (n-(1::nat))))"
| "selecthelp (x#l) n = (if (n <= 0) then [x] else (x # selecthelp l (n-(1::nat))))"

fun select where
"select [] i n = (if (i <= 0) then (selecthelp [] n) else select [] (i-(1::nat)) (n-(1::nat)))"
| "select (x#l) i n = (if (i <= 0) then (selecthelp (x#l) n) else select l (i-(1::nat)) (n-(1::nat)))"

definition
rev (select (rev (nat_to_bv ((bv_to_nat a) + (bv_to_nat b)))) 0 31)"

definition
bv_prepend: "bv_prepend x b bv = replicate x b @ bv"

primrec zerolist where
"zerolist 0 = []"
| "zerolist (Suc n) = zerolist n  @ [Zero]"

primrec hextobv where
"hextobv x0 = [Zero,Zero,Zero,Zero]"
| "hextobv x1 = [Zero,Zero,Zero,One]"
| "hextobv x2 = [Zero,Zero,One,Zero]"
| "hextobv x3 = [Zero,Zero,One,One]"
| "hextobv x4 = [Zero,One,Zero,Zero]"
| "hextobv x5 = [Zero,One,Zero,One]"
| "hextobv x6 = [Zero,One,One,Zero]"
| "hextobv x7 = [Zero,One,One,One]"
| "hextobv x8 = [One,Zero,Zero,Zero]"
| "hextobv x9 = [One,Zero,Zero,One]"
| "hextobv xA = [One,Zero,One,Zero]"
| "hextobv xB = [One,Zero,One,One]"
| "hextobv xC = [One,One,Zero,Zero]"
| "hextobv xD = [One,One,Zero,One]"
| "hextobv xE = [One,One,One,Zero]"
| "hextobv xF = [One,One,One,One]"

primrec hexvtobv where
"hexvtobv [] = []"
| "hexvtobv (x#r) = hextobv x @ hexvtobv r"

lemma selectlenhelp: "length (selecthelp l i) = (i + 1)"
proof (induct i arbitrary: l)
case 0
show "length (selecthelp l 0) = 0 + 1"
proof (cases l)
case Nil
then have "selecthelp l 0 = [Zero]" by simp
then show ?thesis by simp
next
case (Cons a as)
then have "selecthelp l 0 = [a]" by simp
then show ?thesis by simp
qed
next
case (Suc x)
show "length (selecthelp l (Suc x)) = (Suc x) + 1"
proof (cases l)
case Nil
then have "selecthelp l (Suc x) = Zero # selecthelp l x" by simp
then show "length (selecthelp l (Suc x)) = Suc x + 1" using Suc by simp
next
case (Cons a b)
then have "selecthelp l (Suc x) = a # selecthelp b x" by simp
then have "length (selecthelp l (Suc x)) = 1 + length (selecthelp b x)" by simp
then show "length (selecthelp l (Suc x)) = Suc x + 1" using Suc by simp
qed
qed

lemma selectlenhelp2:  "⋀i. ∀l j. ∃k. select l i j = select k 0 (j - i)"
proof (auto)
fix i
show "⋀l j. ∃k. select l i j = select k 0 (j - i)"
proof (induct i)
fix l and j
have "select l 0 j = select l 0 (j-(0::nat))" by simp
then show "∃k. select l 0 j = select k 0 (j - (0::nat))" by auto
next
case (Suc x)
have b: "select l (Suc x) j = select (tl l) x (j-(1::nat))"
proof (cases l)
case Nil
then have "select l (Suc x) j = select l x (j-(1::nat))" by simp
moreover have "tl l = l" using Nil by simp
ultimately show ?thesis by (simp)
next
then have "select l (Suc x) j = select tail x (j-(1::nat))" by simp
moreover have "tail = tl l" using Cons by simp
ultimately show ?thesis by simp
qed
have "∃k. select l x j = select k 0 (j - (x::nat))" using Suc by simp
moreover have  "∃k. select (tl l) x (j-(1::nat)) = select k 0 (j-(1::nat)-(x::nat))" using Suc[of "tl l" "j-(1::nat)"] by auto
ultimately have "∃k. select l (Suc x) j = select k 0 (j-(1::nat) - (x::nat))" using b by auto
then show "∃k. select l (Suc x) j = select k 0 (j - Suc x)" by simp
qed
qed

lemma selectlenhelp3: "∀j. select l 0 j = selecthelp l j"
proof
fix j
show "select l 0 j = selecthelp l j"
proof (cases l)
case Nil
assume "l=[]"
then show "select l 0 j = selecthelp l j" by simp
next
case (Cons a b)
then show "select l 0 j = selecthelp l j" by simp
qed
qed

lemma selectlen: "length (select l i j) = j - i + 1"
proof -
from selectlenhelp2 have "∃k. select l i j = select k 0 (j-i)" by simp
then have "∃k. length (select l i j) = length (select k 0 (j-i))" by auto
then have c: "∃k. length (select l i j) = length (selecthelp k (j-i))"
using selectlenhelp3 by simp
from c obtain k where d: "length (select l i j) = length (selecthelp k (j-i))" by auto
have "0<=j-i" by arith
then have "length (selecthelp k (j-i)) = j-i+1" using selectlenhelp by simp
then show "length (select l i j) = j-i+1" using d by simp
qed

using selectlen [of _ 0 31] addmod32 by simp

end


(*  Title:      RSAPSS/SHA1Padding.thy
Author:     Christina Lindenberg, Kai Wirt, Technische Universität Darmstadt
*)

imports WordOperations
begin

definition zerocount :: "nat ⇒ nat" where
zerocount: "zerocount n = ((((n + 64) div 512) + 1) * 512) - n - (65::nat)"

definition helppadd :: "bv ⇒ bv ⇒ nat ⇒ bv" where
"helppadd x y n = x @ [One] @ zerolist (zerocount n) @ zerolist (64 - length y) @y"

definition sha1padd :: "bv ⇒ bv" where

end


# Theory SHA1

(*  Title:      RSAPSS/SHA1.thy
Author:     Christina Lindenberg, Kai Wirt, Technische Universität Darmstadt
*)

section  "Formal definition of the secure hash algorithm"

theory SHA1
begin

text ‹We define the secure hash algorithm SHA-1 and give a proof for the
length of the message digest›

definition fif where
fif: "fif x y z = bvor (bvand x y) (bvand (bv_not x) z)"

definition fxor where
fxor: "fxor x y z = bvxor (bvxor x y) z"

definition fmaj where
fmaj: "fmaj x y z = bvor (bvor (bvand x y) (bvand x z)) (bvand y z)"

definition fselect :: "nat ⇒ bit list ⇒ bit list ⇒ bit list ⇒ bit list" where
fselect: "fselect r x y z = (if (r < 20) then (fif x y z) else
(if (r < 40) then (fxor x y z) else
(if (r < 60) then (fmaj x y z) else
(fxor x y z))))"

definition K1 where
K1: "K1 = hexvtobv [x5,xA,x8,x2,x7,x9,x9,x9]"

definition K2 where
K2: "K2 = hexvtobv [x6,xE,xD,x9,xE,xB,xA,x1]"

definition K3 where
K3: "K3 = hexvtobv [x8,xF,x1,xB,xB,xC,xD,xC]"

definition K4 where
K4: "K4 = hexvtobv [xC,xA,x6,x2,xC,x1,xD,x6]"

definition kselect :: "nat ⇒ bit list" where
kselect: "kselect r = (if (r < 20) then K1 else
(if (r < 40) then K2 else
(if (r < 60) then K3 else
K4)))"

definition getblock where
getblock: "getblock x = select x 0 511"

fun delblockhelp where
"delblockhelp [] n = []"
| "delblockhelp (x#r) n = (if n <= 0 then x#r else delblockhelp r (n-(1::nat)))"

definition delblock where
delblock: "delblock x = delblockhelp x 512"

primrec sha1compress where
"sha1compress 0 b A B C D E = (let j = (79::nat) in
(let W = select b (32*j) ((32*j)+31) in
BB = A;
CC = bvrol B 30;
DD = C;
EE = D in
AA@BB@CC@DD@EE)))"
| "sha1compress (Suc n) b A B C D E = (let j = (79 - (Suc n)) in
(let W = select b (32*j) ((32*j)+31) in
BB = A;
CC = bvrol B 30;
DD = C;
EE = D in
sha1compress n b AA BB CC DD EE)))"

definition sha1expandhelp where
"sha1expandhelp x i = (let j = (79+16-i) in (bvrol (bvxor(bvxor(
select x (32*(j-(3::nat))) (31+(32*(j-(3::nat))))) (select x (32*(j-(8::nat))) (31+(32*(j-(8::nat)))))) (bvxor(select x (32*(j-(14::nat))) (31+(32*(j-(14::nat))))) (select x (32*(j-(16::nat))) (31+(32*(j-(16::nat))))))) 1))"

fun sha1expand where
"sha1expand x i = (if (i < 16) then x else
let y = sha1expandhelp x i in
sha1expand (x @ y) (i - 1))"

definition sha1compressstart where
sha1compressstart: "sha1compressstart r b A B C D E = sha1compress r (sha1expand b 79) A B C D E"

function (sequential) sha1block where
"sha1block b [] A B C D E = (let H = sha1compressstart 79 b A B C D E;
AA = addmod32 A (select H 0 31);
BB = addmod32 B (select H 32 63);
CC = addmod32 C (select H 64 95);
DD = addmod32 D (select H 96 127);
EE = addmod32 E (select H 128 159)
in AA@BB@CC@DD@EE)"
| "sha1block b x A B C D E =  (let H = sha1compressstart 79 b A B C D E;
AA = addmod32 A (select H 0 31);
BB = addmod32 B (select H 32 63);
CC = addmod32 C (select H 64 95);
DD = addmod32 D (select H 96 127);
EE = addmod32 E (select H 128 159)
in sha1block (getblock x) (delblock x) AA BB CC DD E)"
by pat_completeness auto

termination proof -
have aux: "⋀n xs :: bit list. length (delblockhelp xs n) <= length xs"
proof -
fix n and xs :: "bit list"
show "length (delblockhelp xs n) ≤ length xs"
by (induct n rule: delblockhelp.induct) auto
qed
have "⋀x xs :: bit list. length (delblock (x#xs)) < Suc (length xs)"
proof -
fix x and xs :: "bit list"
from aux have "length (delblockhelp xs 511) < Suc (length xs)"
using le_less_trans [of "length (delblockhelp xs 511)" "length xs"] by auto
then show "length (delblock (x#xs)) < Suc (length xs)" by (simp add: delblock)
qed
then show ?thesis
by (relation "measure (λ(b, x, A, B, C, D, E). length x)") auto
qed

definition IV1 where
IV1: "IV1 = hexvtobv [x6,x7,x4,x5,x2,x3,x0,x1]"

definition IV2 where
IV2: "IV2 = hexvtobv [xE,xF,xC,xD,xA,xB,x8,x9]"

definition IV3 where
IV3: "IV3 = hexvtobv [x9,x8,xB,xA,xD,xC,xF,xE]"

definition IV4 where
IV4: "IV4 = hexvtobv [x1,x0,x3,x2,x5,x4,x7,x6]"

definition IV5 where
IV5: "IV5 = hexvtobv [xC,x3,xD,x2,xE,x1,xF,x0]"

definition sha1 where
sha1: "sha1 x = (let y = sha1padd x in
sha1block (getblock y) (delblock y) IV1 IV2 IV3 IV4 IV5)"

lemma sha1blocklen: "length (sha1block b x A B C D E) = 160"
proof (induct b x A B C D E rule: sha1block.induct)
next
case 2 then show ?case by (simp add: Let_def)
qed

lemma sha1len: "length (sha1 m) = 160"
unfolding sha1 Let_def sha1blocklen ..

end


# Theory Wordarith

(*  Title:      RSAPSS/Wordarith.thy
Author:     Christina Lindenberg, Kai Wirt, Technische Universität Darmstadt
*)

section "Extensions to the Word theory required for PSS"

theory Wordarith
imports WordOperations "HOL-Computational_Algebra.Primes"
begin

definition
nat_to_bv_length :: "nat ⇒ nat ⇒  bv" where
(* nat_to_bv_length converts nat (if 0 ≤ nat ∧ nat < 2^nat) nato a bit string of length l *)
nat_to_bv_length:
"nat_to_bv_length n l = (if length(nat_to_bv n) ≤ l then bv_extend l 𝟬 (nat_to_bv n) else [])"

lemma length_nat_to_bv_length:
"nat_to_bv_length x y ≠ [] ⟹ length (nat_to_bv_length x y) = y"
unfolding nat_to_bv_length by auto

lemma bv_to_nat_nat_to_bv_length:
"nat_to_bv_length x y ≠ [] ⟹ bv_to_nat (nat_to_bv_length x y) = x"
unfolding nat_to_bv_length by auto

definition
roundup :: "nat ⇒ nat ⇒ nat" where
roundup: "roundup x y = (if (x mod y = 0) then (x div y) else (x div y) + 1)"

lemma rnddvd: "b dvd a ⟹ roundup a b * b = a"
by (auto simp add: roundup dvd_eq_mod_eq_0)

lemma bv_to_nat_zero_prepend: "bv_to_nat a = bv_to_nat (𝟬#a)"
by auto

primrec remzero:: "bv ⇒ bv" where
"remzero [] = []"
| "remzero (a#b) = (if a = 𝟭 then (a#b) else remzero b)"

lemma remzeroeq: "bv_to_nat a = bv_to_nat (remzero a)"
proof (induct a)
show "bv_to_nat [] = bv_to_nat (remzero [])"
by simp
next
case (Cons a1 a2)
show "bv_to_nat a2 = bv_to_nat (remzero a2) ⟹
bv_to_nat (a1 # a2) = bv_to_nat (remzero (a1 # a2))"
proof (cases a1)
assume a: "a1=𝟬" then have "bv_to_nat (a1#a2) = bv_to_nat a2"
using bv_to_nat_zero_prepend by simp
moreover have "remzero (a1 # a2) = remzero a2" using a by simp
ultimately show ?thesis using Cons by simp
next
assume "a1=𝟭" then show ?thesis by simp
qed
qed

lemma len_nat_to_bv_pos: assumes x: "1 < a" shows "0< length (nat_to_bv a)"
proof (auto)
assume b: "nat_to_bv a = []"
have a: "bv_to_nat [] = 0" by simp
have c: "bv_to_nat (nat_to_bv a) = 0" using a and b by simp
from x have d: "bv_to_nat (nat_to_bv a) = a" by simp
from d and c have "a=0" by simp
then show False using x by simp
qed

lemma remzero_replicate: "remzero ((replicate n 𝟬)@l) = remzero l"
by (induct n, auto)

lemma length_bvxor_bound: "a <= length l ⟹ a <= length (bvxor l l2)"
proof (induct a)
case 0
then show ?case by simp
next
case (Suc a)
have a: "Suc a ≤ length l" by fact
with Suc.hyps have b: "a ≤ length (bvxor l l2)" by simp
show "Suc a ≤ length (bvxor l l2)"
proof cases
assume c: "a = length (bvxor l l2)"
show "Suc a ≤ length (bvxor l l2)"
have "length l <= max (length l) (length l2)" by simp
then show "Suc a ≤ max (length l) (length l2)" using a by simp
qed
next
assume "a ≠ length (bvxor l l2)"
then have "a < length (bvxor l l2)" using b by simp
then show ?thesis by simp
qed
qed

lemma nat_to_bv_helper_legacy_induct:
"(⋀n. n ≠ (0::nat) ⟶ P (n div 2) ⟹ P n) ⟹ P x"
unfolding atomize_imp[symmetric]
by (induction_schema, simp, lexicographic_order)

lemma len_lower_bound:
assumes "0 < n"
shows "2^(length (nat_to_bv n) - Suc 0) ≤ n"
proof (cases "1<n")
assume l1: "1<n"
then show ?thesis
proof (simp add: nat_to_bv_def, induct n rule: nat_to_bv_helper_legacy_induct, auto)
fix n
assume a: "Suc 0 < (n::nat)" and b: "~Suc 0<n div 2"
then have "n=2 ∨ n=3"
proof (cases "n<=3")
assume "n<=3" and "Suc 0<n"
then show "n=2 ∨ n=3" by auto
next
assume "~n<=3" then have "3<n" by simp
then have "1 < n div 2" by arith
then show "n=2 ∨ n=3" using b by simp
qed
then show "2 ^ (length (nat_to_bv_helper n []) - Suc 0) ≤ n"
proof (cases "n=2")
assume a: "n=2" then have "nat_to_bv_helper n [] = [𝟭, 𝟬]"
proof -
have "nat_to_bv_helper n [] = nat_to_bv n" using b by (simp add: nat_to_bv_def)
then show ?thesis using a by (simp add: nat_to_bv_non0)
qed
then show "2 ^ (length (nat_to_bv_helper n []) - Suc 0) ≤ n" using a by simp
next
assume "n=2 ∨ n=3" and "n~=2"
then have a: "n=3" by simp
then have "nat_to_bv_helper n [] = [𝟭, 𝟭]"
proof -
have "nat_to_bv_helper n [] = nat_to_bv n" using a by (simp add: nat_to_bv_def)
then show ?thesis using a by (simp add: nat_to_bv_non0)
qed
then show "2^(length (nat_to_bv_helper n []) - Suc 0) <=n" using a by simp
qed
next
fix n
assume a: "Suc 0<n" and
b: "2 ^ (length (nat_to_bv_helper (n div 2) []) - Suc 0) ≤ n div 2"
have "(2::nat) ^ (length (nat_to_bv_helper n []) - Suc 0) =
2^(length (nat_to_bv_helper (n div 2) []) + 1 - Suc 0)"
proof -
have "length (nat_to_bv n) = length (nat_to_bv (n div 2)) + 1"
using a by (simp add: nat_to_bv_non0)
then show ?thesis by (simp add: nat_to_bv_def)
qed
moreover have "(2::nat)^(length (nat_to_bv_helper (n div 2) []) + 1 - Suc 0) =
2^(length (nat_to_bv_helper (n div 2) []) - Suc 0) * 2"
proof auto
have "(2::nat)^(length (nat_to_bv_helper (n div 2) []) -Suc 0)*2 =
2^(length (nat_to_bv_helper (n div 2) []) - Suc 0 + 1)" by simp
moreover have "(2::nat)^(length (nat_to_bv_helper (n div 2) []) - Suc 0 + 1) =
2^(length (nat_to_bv_helper (n div 2) []))"
proof -
have "0<n div 2" using a by arith
then have "0<length (nat_to_bv (n div 2))" by (simp add: nat_to_bv_non0)
then have "0< length (nat_to_bv_helper (n div 2) [])" using a by (simp add: nat_to_bv_def)
then show ?thesis by simp
qed
ultimately show "(2::nat) ^ length (nat_to_bv_helper (n div 2) []) =
2 ^ (length (nat_to_bv_helper (n div 2) []) - Suc 0) * 2" by simp
qed
ultimately show  "2 ^ (length (nat_to_bv_helper n []) - Suc 0) <= n"
using b by (simp add: nat_to_bv_def) arith
qed
next
assume c: "~1<n"
show ?thesis
proof (cases "n=1")
assume a: "n=1" then have "nat_to_bv n = " by (simp add: nat_to_bv_non0)
then show "2^(length (nat_to_bv n) - Suc 0) <= n" using a by simp
next
assume "n~=1"
with ‹0 < n› show "2^(length (nat_to_bv n) - Suc 0) <= n" using c by simp
qed
qed

lemma length_lower: assumes a: "length a < length b" and b: "(hd b) ~= 𝟬" shows "bv_to_nat a < bv_to_nat b"
proof -
have ha: "bv_to_nat a < 2^length a" by (simp add: bv_to_nat_upper_range)
have "b ~= []" using a by auto
then have "b=(hd b)#(tl b)" by simp
then have "bv_to_nat b = bitval (hd b) * 2^(length (tl b)) + bv_to_nat (tl b)" using bv_to_nat_helper[of "hd b" "tl b"] by simp
moreover have "bitval (hd b) = 1"
proof (cases "hd b")
assume "hd b = 𝟬 "
then show  "bitval (hd b) = 1" using b by simp
next
assume "hd b = 𝟭"
then show "bitval (hd b) = 1" by simp
qed
ultimately have hb: "2^length (tl b) <= bv_to_nat b" by simp
have "2^(length a) <= (2::nat)^length (tl b)" using a by auto
then show ?thesis using hb and ha by arith
qed

lemma nat_to_bv_non_empty: assumes a: "0<n" shows "nat_to_bv n ~= []"
proof -
from nat_to_bv_non0[of n] have "∃x. nat_to_bv n = x@[if n mod 2 = 0 then 𝟬 else 𝟭]" using a by simp
then show ?thesis by auto
qed

lemma hd_append: "x ~= [] ⟹ hd (x @ xs) = hd x"
by (induct x) auto

lemma hd_one: "0<n ⟹ hd (nat_to_bv_helper n []) = 𝟭"
proof (induct n rule: nat_to_bv_helper_legacy_induct)
fix n
assume *: "n ≠ 0 ⟶ 0 < n div 2 ⟶ hd (nat_to_bv_helper (n div 2) []) = 𝟭"
and "0 < n"
show "hd (nat_to_bv_helper n []) = 𝟭"
proof (cases "1<n")
assume a: "1<n"
with * have b: "0 < n div 2 ⟶ hd (nat_to_bv_helper (n div 2) []) = 𝟭" by simp
from a have c: "0<n div 2" by arith
then have d: "hd (nat_to_bv_helper (n div 2) []) = 𝟭" using b by simp
also from a have "0<n" by simp
then have "hd (nat_to_bv_helper n []) =
hd (nat_to_bv (n div 2) @ [if n mod 2 = 0 then 𝟬 else 𝟭])"
using nat_to_bv_def and nat_to_bv_non0[of n] by auto
then have "hd (nat_to_bv_helper n []) =
hd (nat_to_bv (n div 2))"
using nat_to_bv_non0[of "n div 2"] and c and
nat_to_bv_non_empty[of "n div 2"] and hd_append[of " nat_to_bv (n div 2)"] by auto
then have "hd (nat_to_bv_helper n []) = hd (nat_to_bv_helper (n div 2) [])"
using nat_to_bv_def by simp
then show "hd (nat_to_bv_helper n []) = 𝟭" using b and c by simp
next
assume "~1 < n" with ‹0<n› have c: "n=1" by simp
have "nat_to_bv_helper 1 [] = " by (simp add: nat_to_bv_helper.simps)
then show "hd (nat_to_bv_helper n []) = 𝟭" using c by simp
qed
qed

lemma prime_hd_non_zero:
fixes p::nat assumes a: "prime p" and b: "prime q" shows "hd (nat_to_bv (p*q)) ~= 𝟬"
proof -
have "0 < p*q"
by (metis a b mult_is_0 neq0_conv not_prime_0)
then show ?thesis using hd_one[of "p*q"] and nat_to_bv_def by auto
qed

lemma primerew: fixes p::nat shows  "⟦m dvd p; m~=1; m~=p⟧ ⟹ ~ prime p"

lemma two_dvd_exp: "0<x ⟹ (2::nat) dvd 2^x"
by (induct x) auto

lemma exp_prod1: "⟦1<b;2^x=2*(b::nat)⟧ ⟹ 2 dvd b"
proof -
assume a: "1<b" and b: "2^x=2*(b::nat)"
have s1: "1<x"
proof (cases "1<x")
assume "1<x" then show ?thesis by simp
next
assume x: "~1 < x" then have "2^x <= (2::nat)" using b
proof (cases "x=0")
assume "x=0" then show "2^x <= (2::nat)" by simp
next
assume "x~=0" then have "x=1" using x by simp
then show "2^x <= (2::nat)" by simp
qed
then have "b<=1" using b by simp
then show ?thesis using a by simp
qed
have s2: "2^(x-(1::nat)) = b"
proof -
from s1 b have "2^((x-Suc 0)+1) = 2*b" by simp
then have "2*2^(x-Suc 0) = 2*b" by simp
then show "2^(x-(1::nat)) = b" by simp
qed
from s1 and s2 show ?thesis using two_dvd_exp[of "x-(1::nat)"] by simp
qed

lemma exp_prod2: "⟦1<a; 2^x=a*2⟧ ⟹ (2::nat) dvd a"
proof -
assume "2^x=a*2"
then have "2^x=2*a" by simp
moreover assume "1<a"
ultimately show "2 dvd a" using exp_prod1 by simp
qed

lemma odd_mul_odd: "⟦~(2::nat) dvd p; ~2 dvd q⟧ ⟹ ~2 dvd p*q"
by simp

lemma prime_equal: fixes p::nat shows "⟦prime p; prime q; 2^x=p*q⟧ ⟹ (p=q)"
proof -
assume a: "prime p" and b: "prime q" and c: "2^x=p*q"
from a have d: "1 < p" by (simp add: prime_nat_iff)
moreover from b have e: "1<q" by (simp add: prime_nat_iff)
show "p=q"
proof (cases "p=2")
assume p: "p=2" then have "2 dvd q" using c and exp_prod1[of q x] and e by simp
then have "2=q" using primerew[of 2 q] and b by auto
then show ?thesis using p by simp
next
assume p: "p~=2" show "p=q"
proof (cases "q=2")
assume q: "q=2" then have "2 dvd p" using c and exp_prod1[of p x] and d by simp
then have "2=p" using primerew[of 2 p] and a by auto
then show ?thesis using p by simp
next
assume q: "q~=2" show "p=q"
proof -
from p have "~ 2 dvd p" using primerew and a by auto
moreover from q have "~2 dvd q" using primerew and b by auto
ultimately have "~2 dvd p*q" by (simp add: odd_mul_odd)
then have "odd ((2 :: nat) ^ x)" by (simp only: c) simp
moreover have "(2::nat) dvd 2^x"
proof (cases "x=0")
assume "x=0" then have "(2::nat)^x=1" by simp
then show ?thesis using c and d and e by simp
next
assume "x~=0" then have "0<x" by simp
then show ?thesis using two_dvd_exp by simp
qed
ultimately show ?thesis by simp
qed
qed
qed
qed

lemma nat_to_bv_length_bv_to_nat:
"length xs = n ⟹ xs ≠ [] ⟹ nat_to_bv_length (bv_to_nat xs) n = xs"
apply (simp only: nat_to_bv_length)
apply (auto)
done

end


# Theory EMSAPSS

(*  Title:      RSAPSS/EMSAPSS.thy
Author:     Christina Lindenberg, Kai Wirt, Technische Universität Darmstadt
*)

section "EMSA-PSS encoding and decoding operation"

theory EMSAPSS
imports SHA1 Wordarith
begin

text ‹We define the encoding and decoding operations for the probabilistic
signature scheme. Finally we show, that encoded messages always can be
verified›

definition show_rightmost_bits:: "bv ⇒ nat ⇒ bv" (* extract n rightmost bits of a bit string*)
where "show_rightmost_bits bvec n = rev (take n (rev bvec))"

definition BC:: "bv" (* 0xbc *)
where "BC = [One, Zero, One, One, One, One, Zero, Zero]"

definition salt:: "bv"
where "salt = []"

definition sLen:: "nat" (* length of salt *)
where "sLen = length salt"

definition generate_M':: "bv ⇒ bv ⇒ bv" (* generate_M' outputs "M'" a bit string of length "64 + length(sha1 _ ) + sLen" with 64 initial zero bits *)
where "generate_M' mHash salt_new = bv_prepend 64 𝟬 [] @ mHash @ salt_new"

definition generate_PS:: "nat ⇒ nat ⇒ bv" (* generate_PS outputs "PS" a bit string consisting of "nat (roundup emBits 8) * 8 - sLen - length (sha1 _ ) - 16" zero bits *)
where "generate_PS emBits hLen = bv_prepend ((roundup emBits 8)*8 - sLen - hLen - 16) 𝟬 []"

definition generate_DB:: "bv ⇒ bv" (* generate_DB outputs the bit string DB="PS#(0x01)#salt" of length "nat (roundup emBits 8) * 8 - length (sha1 _ ) - 8" *)
where "generate_DB PS = PS @ [Zero, Zero, Zero, Zero, Zero, Zero, Zero, One] @ salt"

definition maskedDB_zero:: "bv ⇒ nat ⇒ bv" (* sets "roundup emBits 8 * 8 - emBits" bits of maskedDB to zero *)
where "maskedDB_zero maskedDB emBits = bv_prepend ((roundup emBits 8) * 8 - emBits)  𝟬 (drop ((roundup emBits 8)*8 - emBits) maskedDB)"

definition generate_H:: "bv ⇒ nat ⇒ nat ⇒ bv" (* generate_H returns a bit string of length (sha1 _) *)
where "generate_H EM emBits hLen = take hLen (drop ((roundup emBits 8)*8 - hLen - 8) EM)"

definition generate_maskedDB:: "bv ⇒ nat ⇒ nat ⇒ bv " (* outputs a bit string of length "nat (roundup emBits 8) * 8 - length (sha1 _) - 8" *)
where "generate_maskedDB EM emBits hLen = take ((roundup emBits 8)*8 - hLen - 8) EM"

definition generate_salt:: "bv ⇒ bv" (* outputs a bit string of length sLen *)
where "generate_salt DB_zero = show_rightmost_bits DB_zero sLen"

primrec MGF2:: "bv ⇒ nat ⇒ bv" (* help function for MGF1 *)
where
"MGF2 Z 0 = sha1 (Z@(nat_to_bv_length 0 32))"
| "MGF2 Z (Suc n) = (MGF2 Z n)@(sha1 (Z@(nat_to_bv_length (Suc n) 32)))"

definition MGF1:: "bv ⇒ nat ⇒ nat ⇒ bv" (* help function for MGF *)
where "MGF1 Z n l = take l (MGF2 Z n)"

definition MGF:: "bv ⇒ nat ⇒ bv" (* mask generation function *)
where
"MGF Z l = (if l = 0 ∨ 2^32*(length (sha1 Z)) < l
then []
else MGF1 Z ( roundup l (length (sha1 Z))  - 1 ) l)"

definition emsapss_encode_help8:: "bv ⇒ bv ⇒ bv"
where "emsapss_encode_help8 DBzero H = DBzero @ H @ BC"

definition emsapss_encode_help7:: "bv ⇒ bv ⇒ nat ⇒ bv"
where "emsapss_encode_help7 maskedDB H emBits =

definition emsapss_encode_help6:: "bv ⇒ bv ⇒ bv ⇒ nat ⇒ bv"
where "emsapss_encode_help6 DB dbMask H emBits =
then []
else emsapss_encode_help7 (bvxor DB dbMask) H emBits)"

definition emsapss_encode_help5:: "bv ⇒ bv ⇒ nat ⇒ bv"
where "emsapss_encode_help5 DB H emBits =
emsapss_encode_help6 DB (MGF H (length DB)) H emBits"

definition emsapss_encode_help4:: "bv ⇒ bv ⇒ nat ⇒ bv"
where "emsapss_encode_help4 PS H emBits =
emsapss_encode_help5 (generate_DB PS) H emBits"

definition emsapss_encode_help3:: "bv ⇒ nat ⇒ bv"
where "emsapss_encode_help3 H emBits =
emsapss_encode_help4 (generate_PS emBits (length H)) H emBits"

definition emsapss_encode_help2:: "bv ⇒ nat ⇒ bv"
where "emsapss_encode_help2 M' emBits = emsapss_encode_help3 (sha1 M') emBits"

definition emsapss_encode_help1:: "bv ⇒ nat ⇒ bv"
where "emsapss_encode_help1 mHash emBits =
(if emBits  < length (mHash) + sLen + 16
then []
else emsapss_encode_help2 (generate_M' mHash salt) emBits)"

definition emsapss_encode:: "bv ⇒ nat ⇒ bv" (* outputs the encoded message of length emBits *)
where "emsapss_encode M emBits =
(if (2^64 ≤ length M ∨ 2^32 * 160 < emBits)
then []
else emsapss_encode_help1 (sha1 M) emBits)"

definition emsapss_decode_help11:: "bv ⇒ bv ⇒ bool"
where "emsapss_decode_help11 H' H = (if H' ≠ H then False else True)"

definition emsapss_decode_help10:: "bv ⇒ bv ⇒ bool"
where "emsapss_decode_help10 M' H = emsapss_decode_help11 (sha1 M') H"

definition emsapss_decode_help9:: "bv ⇒ bv ⇒ bv ⇒ bool"
where "emsapss_decode_help9 mHash salt_new H =
emsapss_decode_help10 (generate_M' mHash salt_new) H"

definition emsapss_decode_help8:: "bv ⇒ bv ⇒ bv ⇒ bool"
where "emsapss_decode_help8 mHash DB_zero H =
emsapss_decode_help9 mHash (generate_salt DB_zero) H"

definition emsapss_decode_help7:: "bv ⇒ bv ⇒ bv ⇒ nat ⇒ bool"
where "emsapss_decode_help7 mHash DB_zero H emBits =
(if (take ( (roundup emBits 8)*8 - (length mHash) - sLen - 16) DB_zero ≠ bv_prepend ( (roundup emBits 8)*8 - (length mHash) - sLen - 16) 𝟬 []) ∨ (take 8 ( drop ((roundup emBits 8)*8 - (length mHash) - sLen - 16 ) DB_zero ) ≠ [Zero, Zero, Zero, Zero, Zero, Zero, Zero, One])
then False
else emsapss_decode_help8 mHash DB_zero H)"

definition emsapss_decode_help6:: "bv ⇒ bv ⇒ bv ⇒ nat ⇒ bool"
where "emsapss_decode_help6 mHash DB H emBits =
emsapss_decode_help7 mHash (maskedDB_zero DB emBits) H emBits"

definition emsapss_decode_help5:: "bv ⇒ bv ⇒ bv ⇒ bv ⇒ nat ⇒ bool"

definition emsapss_decode_help4:: "bv ⇒ bv ⇒ bv ⇒ nat ⇒ bool"
where "emsapss_decode_help4 mHash maskedDB H emBits =
(if take ((roundup emBits 8)*8 - emBits) maskedDB ≠ bv_prepend ((roundup emBits 8)*8 - emBits) 𝟬 []
then False
else emsapss_decode_help5 mHash maskedDB (MGF H ((roundup emBits 8)*8 - (length mHash) - 8)) H emBits)"

definition emsapss_decode_help3:: "bv ⇒ bv ⇒ nat ⇒ bool"
where "emsapss_decode_help3 mHash EM emBits =
emsapss_decode_help4 mHash (generate_maskedDB EM emBits (length mHash)) (generate_H EM emBits (length mHash)) emBits"

definition emsapss_decode_help2:: "bv ⇒ bv ⇒ nat ⇒ bool"
where "emsapss_decode_help2 mHash EM emBits =
(if show_rightmost_bits EM 8 ≠ BC
then False
else emsapss_decode_help3 mHash EM emBits)"

definition emsapss_decode_help1:: "bv ⇒ bv ⇒ nat ⇒ bool"
where "emsapss_decode_help1 mHash EM emBits =
(if emBits < length (mHash) + sLen + 16
then False
else emsapss_decode_help2 mHash EM emBits)"

definition emsapss_decode:: "bv ⇒ bv ⇒ nat ⇒ bool" (* outputs "true" if EM is encoding of M *)
where "emsapss_decode M EM emBits =
(if (2^64 ≤ length M ∨ 2^32*160<emBits)
then False
else emsapss_decode_help1 (sha1 M) EM emBits)"

lemma roundup_positiv: "0 < emBits ⟹ 0 < roundup emBits 160"

lemma roundup_ge_emBits:" 0 < emBits ⟹ 0 < x ⟹ emBits ≤ (roundup emBits x) * x"
apply (safe)
apply (simp)
apply (insert mult_div_mod_eq [of x emBits])
apply (subgoal_tac "emBits mod x < x")
apply (arith)
apply (simp only: mod_less_divisor)
done

lemma roundup_ge_0: "0 < emBits ⟹ 0 < x ⟹ 0 ≤ roundup emBits x * x - emBits"

lemma roundup_le_7: "0 < emBits ⟹ roundup emBits 8 * 8 - emBits ≤  7"
by (auto simp add: roundup) arith

lemma roundup_nat_ge_8_help:
"length (sha1 M) + sLen + 16 ≤ emBits ⟹ 8 ≤ roundup emBits 8 * 8 - (length (sha1 M) + 8)"
apply (insert roundup_ge_emBits [of emBits 8])
apply (simp add: roundup sha1len sLen_def)
done

lemma roundup_nat_ge_8:
"length (sha1 M) + sLen + 16 ≤ emBits ⟹ 8 ≤ roundup emBits 8 * 8 - (length (sha1 M) + 8)"
apply (insert roundup_nat_ge_8_help [of M emBits])
apply arith
done

lemma roundup_le_ub:
"⟦ 176 + sLen ≤ emBits; emBits ≤ 2^32 * 160⟧ ⟹ (roundup emBits 8) * 8 - 168 ≤ 2^32 * 160"
apply (safe)
apply (simp)
apply (arith)+
done

lemma modify_roundup_ge1: "⟦8 ≤ roundup emBits 8 * 8 - 168⟧ ⟹ 176 ≤  roundup emBits 8 * 8"
by arith

lemma modify_roundup_ge2: "⟦ 176 ≤ roundup emBits 8 * 8⟧ ⟹ 21 < roundup emBits 8"
by simp

lemma roundup_help1: "⟦ 0 < roundup l 160⟧ ⟹ (roundup l 160 - 1) + 1 = (roundup l 160)"
by arith

lemma roundup_help1_new: "⟦ 0 < l⟧ ⟹ (roundup l 160 - 1) + 1 = (roundup l 160)"
apply (drule roundup_positiv [of l])
apply arith
done

lemma roundup_help2: "⟦176 + sLen ≤ emBits⟧ ⟹ roundup emBits 8 * 8 - emBits <=  roundup emBits 8 * 8 - 160 - sLen - 16"

lemma bv_prepend_equal: "bv_prepend (Suc n) b l = b#bv_prepend n b l"

lemma length_bv_prepend: "length (bv_prepend n b l) = n+length l"
by (induct n) (simp_all add: bv_prepend)

lemma length_bv_prepend_drop: "a <= length xs ⟶ length (bv_prepend a b (drop a xs)) = length xs"

lemma take_bv_prepend: "take n (bv_prepend n b x) = bv_prepend n b []"
by (induct n) (simp add: bv_prepend)+

lemma take_bv_prepend2: "take n (bv_prepend n b xs@ys@zs) = bv_prepend n b []"
by (induct n) (simp add: bv_prepend)+

lemma bv_prepend_append: "bv_prepend a b x = bv_prepend a b [] @ x"

lemma bv_prepend_append2:
"x < y ⟹ bv_prepend y b xs = (bv_prepend x b [])@(bv_prepend (y-x) b [])@xs"

lemma drop_bv_prepend_help2: "⟦x < y⟧ ⟹ drop x (bv_prepend y b []) = bv_prepend (y-x) b []"
apply (insert bv_prepend_append2 [of "x" "y" b "[]"])

lemma drop_bv_prepend_help3: "⟦x = y⟧ ⟹ drop x (bv_prepend y b []) = bv_prepend (y-x) b []"
apply (insert length_bv_prepend [of y b "[]"])

lemma drop_bv_prepend_help4: "⟦x ≤ y⟧ ⟹ drop x (bv_prepend y b []) = bv_prepend (y-x) b []"
apply (insert drop_bv_prepend_help2 [of x y b] drop_bv_prepend_help3 [of x y b])
by (arith)

lemma bv_prepend_add: "bv_prepend x b [] @ bv_prepend y b [] = bv_prepend (x + y) b []"
by (induct x) (simp add: bv_prepend)+

lemma bv_prepend_drop: "x ≤ y ⟶ bv_prepend x b (drop x (bv_prepend y b [])) = bv_prepend y b []"
apply (simp add: drop_bv_prepend_help4 [of x y b])
by (simp add: bv_prepend_append [of "x" b "(bv_prepend (y - x) b [])"] bv_prepend_add)

lemma bv_prepend_split: "bv_prepend x b (left @ right) = bv_prepend x b left @ right"
by (induct x) (simp add: bv_prepend)+

lemma length_generate_DB: "length (generate_DB PS) = length PS + 8 + sLen"

lemma length_generate_PS: "length (generate_PS emBits 160) = (roundup emBits 8)*8 - sLen - 160 - 16"

lemma length_bvxor: "length a = length b ⟹ length (bvxor a b) = length a"

lemma length_MGF2: "length (MGF2 Z m) = Suc m * length (sha1 (Z @ nat_to_bv_length m 32))"
by (induct m) (simp+, simp add: sha1len)

lemma length_MGF1: "l ≤ (Suc n) * 160 ⟹ length (MGF1 Z n l) = l"
by (simp add: MGF1_def length_MGF2 sha1len)

lemma length_MGF: "0 < l ⟹ l ≤  2^32 * length (sha1 x) ⟹ length (MGF x l) = l"
apply (insert roundup_help1_new [of l])
apply (rule length_MGF1)
apply (simp)
apply (insert roundup_ge_emBits [of l 160])
apply (arith)
done

lemma solve_length_generate_DB:
"⟦ 0 < emBits; length (sha1 M) + sLen + 16 ≤ emBits⟧
⟹ length (generate_DB (generate_PS emBits (length (sha1 x)) )) = (roundup emBits 8) * 8 - 168"
apply (insert roundup_ge_emBits [of emBits 8])
apply (simp add: length_generate_DB length_generate_PS sha1len)
done

"⟦ roundup emBits 8 * 8 - emBits ≤ length maskedDB⟧

lemma take_equal_bv_prepend:
"⟦ 176 + sLen ≤ emBits; roundup emBits 8 * 8 - emBits ≤ 7⟧
⟹ take (roundup emBits 8 * 8 - length (sha1 M) - sLen - 16) (maskedDB_zero (generate_DB (generate_PS emBits 160)) emBits) =
bv_prepend (roundup emBits 8 * 8 - length (sha1 M) - sLen - 16) 𝟬 []"
apply (insert roundup_help2 [of emBits] length_generate_PS [of emBits])
bv_prepend_split bv_prepend_drop)
done

lemma lastbits_BC: "BC = show_rightmost_bits (xs @ ys @ BC) 8"

lemma equal_zero:
"176 + sLen ≤ emBits ⟹ roundup emBits 8 * 8 - emBits ≤ roundup emBits 8 * 8 - (176 + sLen)
⟹ 0 = roundup emBits 8 * 8 - emBits - (roundup emBits 8 * 8 - (176 + sLen))"
by arith

lemma get_salt: "⟦ 176 + sLen ≤ emBits; roundup emBits 8 * 8 - emBits ≤ 7⟧ ⟹ (generate_salt (maskedDB_zero (generate_DB (generate_PS emBits 160)) emBits)) = salt"
apply (insert roundup_help2 [of emBits] length_generate_PS [of emBits] equal_zero [of emBits])
apply (simp add: bv_prepend_split bv_prepend_drop generate_salt_def
show_rightmost_bits_def sLen_def)
done

lemma generate_maskedDB_elim: "⟦roundup emBits 8 * 8 - emBits ≤ length x; ( roundup emBits 8) * 8 - (length (sha1 M)) - 8 = length (maskedDB_zero x emBits)⟧ ⟹ generate_maskedDB (maskedDB_zero x emBits @ y @ z) emBits (length(sha1 M)) = maskedDB_zero x emBits"
apply (insert length_bv_prepend_drop [of "(roundup emBits 8 * 8 - emBits)" "x"])
done

lemma generate_H_elim: "⟦ roundup emBits 8 * 8 - emBits ≤ length x; length (maskedDB_zero x emBits) =  (roundup emBits 8) * 8 - 168; length y = 160⟧ ⟹ generate_H (maskedDB_zero x emBits @ y @ z) emBits 160 = y"
apply (insert length_bv_prepend_drop [of "roundup emBits 8 * 8 - emBits" "x"])
done

lemma length_bv_prepend_drop_special: "[|roundup emBits 8 * 8 - emBits <= roundup emBits 8 * 8 - (176 + sLen); length (generate_PS emBits 160) = roundup emBits 8 * 8 - (176 + sLen)|] ==> length ( bv_prepend (roundup emBits 8 * 8 - emBits) 𝟬 (drop (roundup emBits 8 * 8 - emBits) (generate_PS emBits 160))) = length (generate_PS emBits 160)"

lemma x01_elim: "⟦176 + sLen ≤ emBits; roundup emBits 8 * 8 - emBits ≤ 7⟧ ⟹ take 8 (drop (roundup emBits 8 * 8 - (length (sha1 M) + sLen + 16))(maskedDB_zero (generate_DB (generate_PS emBits 160)) emBits)) = [𝟬, 𝟬, 𝟬, 𝟬, 𝟬, 𝟬, 𝟬, 𝟭]"
apply (insert roundup_help2 [of emBits] length_generate_PS [of emBits] equal_zero [of emBits])
bv_prepend_split bv_prepend_drop)
done

lemma drop_bv_mapzip:
assumes "n <= length x" "length x = length y"
shows "drop n (bv_mapzip f x y) = bv_mapzip f (drop n x) (drop n y)"
proof -
have "⋀x y. n <= length x ⟹ length x = length y ⟹
drop n (bv_mapzip f x y) = bv_mapzip f (drop n x) (drop n y)"
apply (induct n)
apply simp
apply (case_tac x, case_tac[!] y, auto)
done
with assms show ?thesis by simp
qed

lemma [simp]:
assumes "length a = length b"
shows "bvxor (bvxor a b) b = a"
proof -
have "⋀b. length a = length b ⟹ bvxor (bvxor a b) b = a"
apply (induct a)
apply (case_tac b)
apply (simp)+
apply (case_tac a1)
apply (case_tac a)
apply (safe)
apply (simp)+
apply (case_tac a)
apply (simp)+
done
with assms show ?thesis by simp
qed

lemma bvxorxor_elim_help:
assumes "x <= length a" and "length a = length b"
shows "bv_prepend x 𝟬 (drop x (bvxor (bv_prepend x 𝟬 (drop x (bvxor a b))) b)) =
bv_prepend x 𝟬 (drop x a)"
proof -
have "drop x (bvxor (bv_prepend x 𝟬 (drop x (bvxor a b))) b) = drop x a"
apply (unfold bvxor bv_prepend)
apply (cut_tac assms)
apply (insert length_replicate [of x 𝟬 ])
apply (insert length_drop [of x a])
apply (insert length_drop [of x b])
apply (insert length_bvxor [of "drop x a" "drop x b"])
apply (subgoal_tac "length (replicate x 𝟬 @ drop x (bv_mapzip (⊕⇩b) a b)) = length b")
apply (subgoal_tac "b = (take x b)@(drop x b)")
apply (insert drop_bv_mapzip [of x "(replicate x 𝟬 @ drop x (bv_mapzip (⊕⇩b) a b))" b "(⊕⇩b)"])
apply (simp)
apply (insert drop_bv_mapzip [of x a b "(⊕⇩b)"])
apply (simp)
apply (fold bvxor)
apply (simp_all)
done
with assms show ?thesis by simp
qed

lemma bvxorxor_elim: "⟦ roundup emBits 8 * 8 - emBits ≤ length a; length a = length b⟧ ⟹ (maskedDB_zero (bvxor (maskedDB_zero (bvxor a b) emBits)b) emBits) = bv_prepend (roundup emBits 8 * 8 - emBits) 𝟬 (drop (roundup emBits 8 * 8 - emBits) a)"

lemma verify: "⟦(emsapss_encode M emBits) ≠ []; EM=(emsapss_encode M emBits)⟧ ⟹ emsapss_decode M EM emBits = True"
apply (safe, simp+)
apply (safe, simp+)
apply (safe)
emsapss_encode_help5_def emsapss_encode_help6_def)
apply (safe)
apply (simp add: emsapss_encode_help7_def emsapss_encode_help8_def lastbits_BC [symmetric])+
emsapss_decode_help4_def emsapss_encode_help4_def)
apply (safe)
apply (insert roundup_le_7 [of emBits] roundup_ge_0 [of emBits 8] roundup_nat_ge_8 [of M emBits])
apply (safe)
apply (simp)
apply (simp only: emsapss_encode_help8_def)
apply (simp only: take_bv_prepend2 min.absorb1)
apply (simp)
apply (safe)
apply (simp)+
apply (insert solve_length_generate_DB [of emBits M "generate_M' (sha1 M) salt"] roundup_le_ub [of emBits])
apply (insert length_MGF [of "(roundup emBits 8) * 8 - 168" "(sha1 (generate_M' (sha1 M) salt))"])
apply (insert modify_roundup_ge1 [of emBits] modify_roundup_ge2 [of emBits])
apply (simp add: sha1len emsapss_encode_help7_def emsapss_encode_help8_def)
apply (insert length_bvxor [of "(generate_DB (generate_PS emBits 160))" "(MGF (sha1 (generate_M' (sha1 M) salt)) ((roundup emBits 8) * 8 - 168))"])
apply (insert generate_maskedDB_elim [of emBits "(bvxor (generate_DB (generate_PS emBits 160))(MGF (sha1 (generate_M' (sha1 M) salt)) ((roundup emBits 8) * 8 - 168)))" M "sha1 (generate_M' (sha1 M) salt)" BC])
apply (insert length_maskedDB_zero [of emBits "(bvxor (generate_DB (generate_PS emBits 160))(MGF (sha1 (generate_M' (sha1 M) salt)) ((roundup emBits 8) * 8 - 168)))"])
apply (insert generate_H_elim [of emBits "(bvxor (generate_DB (generate_PS emBits 160))(MGF (sha1 (generate_M' (sha1 M) salt)) (roundup emBits 8 * 8 - 168)))" "sha1 (generate_M' (sha1 M) salt)" BC])
apply (simp only: emsapss_decode_help6_def emsapss_decode_help7_def)
apply (insert bvxorxor_elim [of emBits "(generate_DB (generate_PS emBits 160))" "(MGF (sha1 (generate_M' (sha1 M) salt)) ((roundup emBits 8) * 8 - 168))"])
apply (insert take_equal_bv_prepend [of emBits M] x01_elim [of emBits M] get_salt [of emBits])
apply (simp add: emsapss_decode_help8_def emsapss_decode_help9_def emsapss_decode_help10_def emsapss_decode_help11_def)
done

end


# Theory Mod

(*  Title:      RSAPSS/Mod.thy

Author:     Christina Lindenberg, Kai Wirt, Technische Universität Darmstadt
*)

section "Leammata for modular arithmetic"

theory Mod
imports Main
begin

lemma divmultassoc: "a div (b*c) * (b*c) = ((a div (b * c)) * b)*(c::nat)"
by (rule mult.assoc [symmetric])

lemma delmod: "(a::nat) mod (b*c) mod c = a mod c"
by (rule mod_mod_cancel [OF dvd_triv_right])

lemma timesmod1: "((x::nat)*((y::nat) mod n)) mod (n::nat) = ((x*y) mod n)"
by (rule mod_mult_right_eq)

lemma timesmod3: "((a mod (n::nat)) * b) mod n = (a*b) mod n"
by (rule mod_mult_left_eq)

lemma remainderexplemma: "(y mod (a::nat) = z mod a) ⟹ (x*y) mod a = (x*z) mod a"
by (rule mod_mult_cong [OF refl])

lemma remainderexp: "((a mod (n::nat))^i) mod n = (a^i) mod n"
by (rule power_mod)

end


# Theory Crypt

(*  Title:      RSAPSS/Crypt.thy

Author:     Christina Lindenberg, Kai Wirt, Technische Universität Darmstadt
*)

section "Definition of rsacrypt"

theory Crypt
imports Main Mod
begin

text ‹
This theory defines the rsacrypt function which implements RSA using fast
exponentiation. An proof, that this function calculates RSA is also given
›

definition rsa_crypt :: "nat ⇒ nat ⇒ nat ⇒ nat"
where
cryptcorrect: "rsa_crypt M e n = M ^ e mod n"

lemma rsa_crypt_code [code]:
"rsa_crypt M e n = (if e = 0 then 1 mod n
else if even e then rsa_crypt M (e div 2) n ^ 2 mod n
else (M * rsa_crypt M (e div 2) n ^ 2 mod n) mod n)"
proof -
{ fix m
have "(M ^ m mod n)⇧2 mod n = (M ^ m)⇧2 mod n"
then have "(M mod n) * ((M ^ m mod n)⇧2 mod n) = (M mod n) * ((M ^ m)⇧2 mod n)"
by simp
have "M * (M ^ m mod n)⇧2 mod n = M * (M ^ m)⇧2 mod n"
by (metis mod_mult_right_eq power_mod)
}
then show ?thesis
by (auto simp add: cryptcorrect power_even_eq remainderexp elim!: evenE oddE)
qed

end



# Theory Pdifference

(*  Title:      RSAPSS/Pdifference.thy

Author:     Christina Lindenberg, Kai Wirt, Technische Universität Darmstadt
*)
section "Positive differences"

theory Pdifference
imports "HOL-Computational_Algebra.Primes" Mod
begin

definition
pdifference :: "nat ⇒ nat ⇒ nat" where
[simp]: "pdifference a b = (if a < b then (b-a) else (a-b))"

lemma timesdistributesoverpdifference:
"m*(pdifference a b) = pdifference (m*(a::nat)) (m* (b::nat))"

lemma addconst: "a = (b::nat) ⟹ c+a = c+b"
by auto

lemma invers: "a ≤ x ⟹ (x::nat) = x - a + a"
by auto

lemma invers2: "⟦a ≤ b; (b-a) = p*q⟧ ⟹ (b::nat) = a+p*q"
apply (assumption)
apply (subst add.commute, rule invers, simp)
done

lemma modadd: "⟦b = a+p*q⟧ ⟹ (a::nat) mod p = b mod p"
by auto

lemma equalmodstrick1: "pdifference a b mod p = 0 ⟹ a mod p = b mod p"
using mod_eq_dvd_iff_nat [of a b p] mod_eq_dvd_iff_nat [of b a p]
by (cases "a < b") auto

lemma diff_add_assoc: "b ≤ c ⟹ c - (c - b) = c - c + (b::nat)"
by auto

lemma diff_add_assoc2: "a ≤ c ⟹ c - (c - a + b) = (c - c + (a::nat) - b)"
apply (subst diff_diff_left [symmetric])
apply auto
done

lemma diff_add_diff: "x ≤ b ⟹ (b::nat) - x + y - b = y - x"
by (induct b) auto

lemma equalmodstrick2:
assumes "a mod p = b mod p"
shows "pdifference a b mod p = 0"
proof -
{ fix a b
assume *: "a mod p = b mod p"
have "a - b = a div p * p + a mod p - b div p * p - b mod p"
by simp
also have "… = a div p * p - b div p * p"
using * by (simp only:)
also have "… = (a div p - b div p) * p"
finally have "(a - b) mod p = 0"
by simp
}
from this [OF assms] this [OF assms [symmetric]]
show ?thesis by simp
qed

lemma primekeyrewrite:
fixes p::nat shows "⟦prime p; p dvd (a*b);~(p dvd a)⟧ ⟹ p dvd b"
apply (subst (asm) prime_dvd_mult_nat)
apply auto
done

lemma multzero: "⟦0 < m mod p; m*a = 0⟧ ⟹ (a::nat) = 0"
by auto

lemma primekeytrick:
fixes A B :: nat
assumes "(M * A) mod P = (M * B) mod P"
assumes "M mod P ≠ 0" and "prime P"
shows "A mod P = B mod P"
proof -
from assms have "M > 0"
by (auto intro: ccontr)
from assms have *: "⋀q. P dvd M * q ⟹ P dvd q"
using primekeyrewrite [of P M] unfolding dvd_eq_mod_eq_0 [symmetric] by blast
from equalmodstrick2 [OF assms(1)] ‹M > 0› show ?thesis
apply -
apply (rule equalmodstrick1)
apply (auto intro: * dvdI simp add: dvd_eq_mod_eq_0 [symmetric] diff_mult_distrib2 [symmetric])
done
qed

end



# Theory Productdivides

(*  Title:      RSAPSS/Productdivides.thy
Author:     Christina Lindenberg, Kai Wirt, Technische Universität Darmstadt
*)

section "Lemmata for modular arithmetic with primes"

theory Productdivides
imports Pdifference
begin

lemma productdivides: "⟦x mod a = (0::nat); x mod b = 0; prime a; prime b; a ≠ b⟧ ⟹ x mod (a*b) = 0"
by (simp add: mod_eq_0_iff_dvd primes_coprime divides_mult)

lemma specializedtoprimes1:
fixes p::nat
shows "⟦prime p; prime q; p ≠ q; a mod p = b mod p ; a mod q = b mod q⟧
⟹ a mod (p*q) = b mod (p*q)"
by (metis equalmodstrick1 equalmodstrick2 productdivides)

lemma specializedtoprimes1a:
fixes p::nat
shows "⟦prime p; prime q; p ≠ q; a mod p = b mod p; a mod q = b mod q; b < p*q ⟧
⟹ a mod (p*q) = b"

end


# Theory Cryptinverts

(*  Title:      RSAPSS/Cryptinverts.thy
Author:     Christina Lindenberg, Kai Wirt, Technische Universität Darmstadt
*)

section "Correctness proof for RSA"

theory Cryptinverts
imports  Crypt Productdivides  "HOL-Number_Theory.Residues"
begin

text ‹
In this theory we show, that a RSA encrypted message can be decrypted
›

primrec pred:: "nat ⇒ nat"
where
"pred 0 = 0"
| "pred (Suc a) = a"

lemma pred_unfold:
"pred n = n - 1"
by (induct n) simp_all

lemma fermat:
assumes "prime p" "m mod p ≠ 0"
shows "m^(p-(1::nat)) mod p = 1"
proof -
from assms have "[m ^ (p - 1) = 1] (mod p)"
using fermat_theorem [of p m] by (simp add: mod_eq_0_iff_dvd)
then show ?thesis
using ‹prime p› prime_gt_1_nat [of p] by (simp add: cong_def)
qed

lemma cryptinverts_hilf1: "prime p ⟹ (m * m ^(k * pred p)) mod p = m mod p"
apply (cases "m mod p = 0")
apply (simp only: mult.commute [of k "pred p"]
power_mult mod_mult_right_eq [of "m" "(m^pred p)^k" "p"]
remainderexp [of "m^pred p" "p" "k", symmetric])
apply (insert fermat [of p m], auto)
apply (simp add: mult.commute [of k] power_mult pred_unfold)
by (metis One_nat_def mod_mult_right_eq mult.right_neutral power_Suc_0 power_mod)

lemma cryptinverts_hilf2: "prime p ⟹ m*(m^(k * (pred p) * (pred q))) mod p = m mod p"
apply (simp add: mult.commute [of "k * pred p" "pred q"] mult.assoc [symmetric])
apply (rule cryptinverts_hilf1 [of "p" "m" "(pred q) * k"])
apply simp
done

lemma cryptinverts_hilf3: "prime q ⟹ m*(m^(k * (pred p) * (pred q))) mod q = m mod q"
by (fact cryptinverts_hilf1)

lemma cryptinverts_hilf4:
"m ^ x mod (p * q) = m" if "prime p" "prime q" "p ≠ q"
"m < p * q" "x mod (pred p * pred q) = 1"
proof (cases x)
case 0
with that show ?thesis
by simp
next
case (Suc x)
with that(5) have "Suc x mod (pred p * pred q) = Suc 0"
by simp
then have "pred p * pred q dvd x"
using dvd_minus_mod [of "(pred p * pred q)" "Suc x"]
by simp
then obtain y where "x = pred p * pred q * y" ..
then have "m ^ Suc x mod p = m mod p" and "m ^ Suc x mod q = m mod q"
using cryptinverts_hilf2 [of p m y q, OF ‹prime p›]
cryptinverts_hilf3 [of q m y p, OF ‹prime q›]
with that Suc show ?thesis
by (auto intro: specializedtoprimes1a)
qed

lemma primmultgreater: fixes p::nat shows "⟦ prime p; prime q; p ≠ 2; q ≠ 2⟧ ⟹ 2 < p*q"
apply (insert mult_le_mono [of 2 p 2 q])
apply auto
done

lemma primmultgreater2: fixes p::nat shows "⟦prime p; prime q; p ≠ q⟧ ⟹  2 < p*q"
apply (cases "p = 2")
apply simp+
apply (cases "q = 2")
apply (erule primmultgreater)
apply auto
done

lemma cryptinverts: "⟦ prime p; prime q; p ≠ q; n = p*q; m < n;
e*d mod ((pred p)*(pred q)) = 1⟧ ⟹ rsa_crypt (rsa_crypt m e n) d n = m"
apply (insert cryptinverts_hilf4 [of p q m "e*d"])
apply (insert cryptcorrect [of "p*q" "rsa_crypt m e (p * q)" d])
apply (insert cryptcorrect [of "p*q" m e])
apply (insert primmultgreater2 [of p q])
apply (simp add: cryptcorrect remainderexp [of "m^e" "p*q" d] power_mult [symmetric])
done

end


# Theory RSAPSS

(*  Title:      RSAPSS/RSAPSS.thy
Author:     Christina Lindenberg, Kai Wirt, Technische Universität Darmstadt
*)

section "RSS-PSS encoding and decoding operation"

theory RSAPSS
imports EMSAPSS Cryptinverts
begin

text ‹We define the RSA-PSS signature and verification operations. Moreover we
show, that messages signed with RSA-PSS can always be verified
›

definition rsapss_sign_help1:: "nat ⇒ nat ⇒ nat ⇒ bv"
where "rsapss_sign_help1 em_nat e n =
nat_to_bv_length (rsa_crypt em_nat e n) (length (nat_to_bv n))"

definition rsapss_sign:: "bv ⇒ nat ⇒ nat ⇒ bv" (* Input: message (an bv), private key, RSA modulus; Output: signature (an bv)*)
where "rsapss_sign m e n =
(if (emsapss_encode m (length (nat_to_bv n) - 1)) = []
then []
else (rsapss_sign_help1 (bv_to_nat (emsapss_encode m (length (nat_to_bv n) - 1)) ) e n))"

definition rsapss_verify:: "bv ⇒ bv ⇒ nat ⇒ nat ⇒ bool" (* Input:  Message, Signature to be verified (an bv), public key, RSA modulus; Output: valid or invalid signature *)
where "rsapss_verify m s d n =
(if (length s) ≠ length(nat_to_bv n)
then False
else let em = nat_to_bv_length (rsa_crypt (bv_to_nat s) d n) ((roundup (length(nat_to_bv n) - 1) 8) * 8) in emsapss_decode m em (length(nat_to_bv n) - 1))"

lemma length_emsapss_encode:
"emsapss_encode m x ≠ [] ⟹ length (emsapss_encode m x) = roundup x 8 * 8"
apply (atomize (full))