Session RSAPSS

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"
  by (simp add: max_def)

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] 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"
  by (simp add: bv_extend_def)

lemma bv_not_Nil [simp]: "bv_not [] = []"
  by (simp add: bv_not_def)

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

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 [] = 𝟬"
  by (simp add: bv_msb_def)

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

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"
  by (simp add: bv_to_nat_def)

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"])
      apply (simp add: add_mult_distrib)
      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"
  by (simp add: bv_extend_def wn)

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"
    by (simp add: bv_extend_def)
  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"
    by (subst replicate_add) rule
  also have "... = replicate (n - Suc (length w)) b @ b # w"
    by simp
  also have "... = bv_extend n b (b#w)"
    by (simp add: bv_extend_def)
  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)"
    by (simp add: bv_extend_def)
  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"
    by (subst replicate_add) (rule refl)
  also have "... = b # bv_extend (length xs) b (rem_initial b xs)"
    by (auto simp add: bv_extend_def [symmetric])
  also have "... = b # xs"
    by (simp add: ind)
  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 [] = []"
  by (simp add: norm_unsigned_def)

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

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

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 = []"
  by (simp add: nat_to_bv_def)

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
          by (simp add: nat_to_bv_helper.simps)
      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]: "n0 ==> nat_to_bv n = nat_to_bv (n div 2) @ [if n mod 2 = 0 then 𝟬 else 𝟭]"
proof -
  assume n: "n0"
  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 (simp add: n)
    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"
          by (simp add: ring_distribs)
        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) = 𝟭"
    by (auto simp add: norm_empty_bv_to_nat_zero)
  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"
by (simp add: norm_unsigned_def,rule rem_initial_equal)

lemma bv_extend_norm_unsigned: "bv_extend (length w) 𝟬 (norm_unsigned w) = w"
by (simp add: norm_unsigned_def,rule bv_extend_rem_initial)

lemma norm_unsigned_append1 [simp]:
  "norm_unsigned xs  [] ==> norm_unsigned (xs @ ys) = norm_unsigned xs @ ys"
by (simp add: norm_unsigned_def,rule rem_initial_append1)

lemma norm_unsigned_append2 [simp]:
  "norm_unsigned xs = [] ==> norm_unsigned (xs @ ys) = norm_unsigned ys"
by (simp add: norm_unsigned_def,rule rem_initial_append2)

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) @ [𝟭]"
    by (simp add: add.commute)
  also have "... = nat_to_bv (bv_to_nat w) @ [𝟭]"
    by (subst div_add1_eq) simp
  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
      by (simp add: bv_to_nat_zero_imp_empty)
  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")
      apply (simp_all add: norm_empty_bv_to_nat_zero)
      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)"
            by (simp add: ac_simps ac_simps)
          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)"
    by (simp add: bv_extend_norm_unsigned)
  also have "... = bv_extend (length ys) 𝟬 (norm_unsigned ys)"
    by (simp add: xsys len)
  also have "... = ys"
    by (simp add: bv_extend_norm_unsigned)
  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
    by (simp add: nat_to_bv_def nat_to_bv_helper.simps)
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_type1 [simp]: "bv_add (norm_unsigned w1) w2 = bv_add w1 w2"
  by (simp add: bv_add_def)

lemma bv_add_type2 [simp]: "bv_add w1 (norm_unsigned w2) = bv_add w1 w2"
  by (simp add: bv_add_def)

lemma bv_add_returntype [simp]: "norm_unsigned (bv_add w1 w2) = bv_add w1 w2"
  by (simp add: bv_add_def)

lemma bv_add_length: "length (bv_add w1 w2)  Suc (max (length w1) (length w2))"
proof (unfold bv_add_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 "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"
        by (rule add_right_mono)
      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"
  by (simp add: bv_mult_def)

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

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

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)"
    by (simp add: power_add)
  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))"
  by (simp add: int_to_bv_def)

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

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"
  by (simp add: bv_to_int_def)

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

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

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))"
    apply (simp add: algebra_simps) 
    by (metis of_nat_power add.commute not_less of_nat_numeral zle_add1_eq_le of_nat_le_iff)
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 (simp add: norm_signed_Cons)
    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"
  proof (simp add: norm_signed_def,auto)
    assume "norm_unsigned xs = []"
    hence xx: "rem_initial 𝟬 xs = []"
      by (simp add: norm_unsigned_def)
    have "bv_extend (Suc (length xs)) 𝟬 (𝟬#rem_initial 𝟬 xs) = 𝟬#xs"
      apply (simp add: bv_extend_def replicate_app_Cons_same)
      apply (fold bv_extend_def)
      apply (rule bv_extend_rem_initial)
      done
    thus "bv_extend (Suc (length xs)) 𝟬 [𝟬] = 𝟬#xs"
      by (simp add: xx)
  next
    show "bv_extend (Suc (length xs)) 𝟬 (𝟬#norm_unsigned xs) = 𝟬#xs"
      apply (simp add: norm_unsigned_def)
      apply (simp add: bv_extend_def replicate_app_Cons_same)
      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 (simp add: norm_signed_Cons)
    apply (simp add: bv_extend_def replicate_app_Cons_same)
    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)"
    by (simp add: bv_extend_norm_signed)
  also have "... = bv_extend (length ys) (bv_msb ys) (norm_signed ys)"
    by (simp add: xsys xsys' len)
  also have "... = ys"
    by (simp add: bv_extend_norm_signed)
  finally show ?thesis .
qed

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

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
    proof (simp add: norm_signed_Cons,safe)
      assume "norm_unsigned w' = []"
      with weq and w0 show False
        by (simp add: norm_empty_bv_to_nat_zero)
    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' = []"
          by (simp add: bv_to_nat_zero_imp_empty)
        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 (simp add: norm_signed_Cons)
  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
          by (simp add: weq w'eq)
      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 "...  𝟬"
      by (simp add: jj)
    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"
  by (simp add: utos_def norm_signed_Cons)

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

lemma utos_length: "length (utos w)  Suc (length w)"
  by (simp add: utos_def norm_signed_Cons)

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"
  by (simp add: bv_uminus_def)

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

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
    proof (simp add: bv_uminus_def,rule length_int_to_bv_upper_limit_gt0,simp_all)
      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
      apply (simp add: bv_uminus_def)
      using lw
      apply (simp (no_asm) add: nat_to_bv_non0)
      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 (simp add: bv_uminus_def)
      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"
    by (simp add: bv_to_int_utos, arith)
  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 (simp add: bv_uminus_def)
      apply (rule length_int_to_bv_upper_limit_lem1)
      apply (rule p)
      apply (simp add: bv_to_int_utos)
      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)"

lemma bv_sadd_type1 [simp]: "bv_sadd (norm_signed w1) w2 = bv_sadd w1 w2"
  by (simp add: bv_sadd_def)

lemma bv_sadd_type2 [simp]: "bv_sadd w1 (norm_signed w2) = bv_sadd w1 w2"
  by (simp add: bv_sadd_def)

lemma bv_sadd_returntype [simp]: "norm_signed (bv_sadd w1 w2) = bv_sadd w1 w2"
  by (simp add: bv_sadd_def)

lemma adder_helper:
  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)"
    proof (simp add: less_max_iff_disj,rule)
      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
      by (simp add: bv_sadd_def)
  next
    assume "?Q = -1"
    thus ?thesis
      by (simp add: bv_sadd_def)
  next
    assume p: "0 < ?Q"
    show ?thesis
      apply (simp add: bv_sadd_def)
      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))"
        by (rule add_less_le_mono)
      also have "...  2 ^ max (length w1) (length w2)"
        apply (rule adder_helper)
        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 (simp add: bv_sadd_def)
      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 adder_helper)
        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 add_mono)
        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"
  by (simp add: bv_sub_def)

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

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

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
  proof (simp add: bv_sub_def bv_sadd_def bv_uminus_def p)
    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
      by (simp add: bv_sub_def bv_sadd_def bv_uminus_def)
  next
    assume "?Q = -1"
    thus ?thesis
      by (simp add: bv_sub_def bv_sadd_def bv_uminus_def)
  next
    assume p: "0 < ?Q"
    show ?thesis
      apply (simp add: bv_sub_def bv_sadd_def bv_uminus_def)
      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 add_less_le_mono)
        apply (rule bv_to_int_upper_range [of w1])
        apply (rule v2)
        done
      also have "...  2 ^ max (length w1) (length w2)"
        apply (rule adder_helper)
        apply (rule lmw)
        done
      finally show "?Q < 2 ^ max (length w1) (length w2)" by simp
    qed
  next
    assume p: "?Q < -1"
    show ?thesis
      apply (simp add: bv_sub_def bv_sadd_def bv_uminus_def)
      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 adder_helper)
        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 add_mono)
        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"
  by (simp add: bv_smult_def)

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

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

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 (simp add: bv_smult_def p)
      apply (cut_tac lmw)
      apply arith
      using p
      apply simp
      done
  next
    assume p: "0 < ?Q"
    thus ?thesis
    proof (simp add: zero_less_mult_iff,safe)
      assume bi1: "0 < bv_to_int w1"
      assume bi2: "0 < bv_to_int w2"
      show ?thesis
        apply (simp add: bv_smult_def)
        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 (subst power_add [symmetric])
          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 (simp add: bv_smult_def)
        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 (subst power_add [symmetric])
          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 (subst power_add [symmetric])
        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
        proof (simp add: mult_less_0_iff,safe)
          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))"
            by (simp add: ac_simps)
          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))"
            by (simp add: ac_simps)
          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
    proof (simp add: zero_less_mult_iff,safe)
      assume biw2: "0 < bv_to_int w2"
      show ?thesis
        apply (simp add: bv_smult_def)
        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 (subst power_add [symmetric])
          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 (simp add: bv_smult_def)
      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 (subst power_add [symmetric])
        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
        proof (simp add: mult_less_0_iff,safe)
          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
            apply (simp add: bv_to_int_utos)
            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))"
            by (simp add: ac_simps)
          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"
            by (simp add: bv_to_int_utos)
        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"
  by (simp add: bv_smult_def ac_simps)

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
      proof (auto simp add: nth_append)
        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)"
  by (simp add: bv_chop_def Let_def)

lemma append_bv_chop_id: "fst (bv_chop w l) @ snd (bv_chop w l) = w"
  by (simp add: bv_chop_def Let_def)

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

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

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

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 (simp add: length_nat_def)
  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"
  by (simp add: length_nat_def Least_equality)

lemma length_nat_non0:
  assumes n0: "n  0"
  shows       "length_nat n = Suc (length_nat (n div 2))"
  apply (simp add: length_nat [symmetric])
  apply (subst nat_to_bv_non0 [of n])
  apply (simp_all add: n0)
  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
    apply (simp add: i0)
    using i0 apply (simp add: length_nat [symmetric])
    done
  finally show ?thesis
    using i0
    by (simp add: length_int_def)
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)))))"
      by (simp add: int_to_bv_def nat_diff_distrib)
    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 (simp add: length_nat [symmetric])
      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"
  by (simp add: length_int_def)

lemma length_int_gt0: "0 < i ==> length_int i = Suc (length_nat (nat i))"
  by (simp add: length_int_def)

lemma length_int_lt0: "i < 0 ==> length_int i = Suc (length_nat (nat (- i) - 1))"
  by (simp add: length_int_def nat_diff_distrib)

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

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 (simp add: bv_slice_def)
  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"
    by (simp add: w_defs append_bv_chop_id)

  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 (simp add: w_defs)
    apply (simp add: w_defs)
    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 (simp add: w_defs)
    apply (simp add: w_defs)
    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
    apply (simp_all add: w_defs)
    done
qed

lemma bv_to_nat_extend [simp]: "bv_to_nat (bv_extend n 𝟬 w) = bv_to_nat w"
  apply (simp add: bv_extend_def)
  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 (simp add: bv_extend_def)
  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 (simp add: bv_to_int_def)
    apply (simp add: bv_extend_def)
    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)"
    by (simp add: length_nat_def)
  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 (simp add: length_nat_def)
    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"
  by (simp add: length_nat_non0)

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"
    by (simp add: bv_to_nat_def add: numeral_One [symmetric]
      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 [] [] = []"
  by (simp add: bv_mapzip_def Let_def)

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

end

Theory WordOperations

(*  Title:      RSAPSS/Wordoperations.thy
    Author:     Christina Lindenberg, Kai Wirt, Technische Universität Darmstadt
    Copyright:  2005 - 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
  addmod32: "addmod32 a b =
    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
      case (Cons head tail)
      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

lemma addmod32len: " a b. length (addmod32 a b) = 32"
  using selectlen [of _ 0 31] addmod32 by simp

end

Theory SHA1Padding

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


section "Message Padding for SHA1"

theory SHA1Padding
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
  sha1padd: "sha1padd x = helppadd x (nat_to_bv (length x)) (length x)"

end

Theory SHA1

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

section  "Formal definition of the secure hash algorithm"

theory SHA1
imports SHA1Padding
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 
                                        (let AA = addmod32 (addmod32 (addmod32 W (bvrol A 5)) (fselect j B C D)) (addmod32 E (kselect j));
                                             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 
                                        (let AA = addmod32 (addmod32 (addmod32 W (bvrol A 5)) (fselect j B C D)) (addmod32 E (kselect j));
                                             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)
  case 1 show ?case by (simp add: Let_def addmod32len)
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
    Copyright:  2005 - 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)"
    proof (simp add: bvxor)
      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"
  by (auto simp add: prime_nat_iff)


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)
  apply (simp add: bv_extend_norm_unsigned)
  done

end

Theory EMSAPSS

(*  Title:      RSAPSS/EMSAPSS.thy
    Author:     Christina Lindenberg, Kai Wirt, Technische Universität Darmstadt
    Copyright:  2005 - 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 =
    emsapss_encode_help8 (maskedDB_zero maskedDB emBits) H"

definition emsapss_encode_help6:: "bv  bv  bv  nat  bv"
  where "emsapss_encode_help6 DB dbMask H emBits =
    (if dbMask = []
     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"
  where "emsapss_decode_help5 mHash maskedDB dbMask H emBits =
    emsapss_decode_help6 mHash (bvxor maskedDB dbMask) H emBits"

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"
  by (auto simp add: roundup)

lemma roundup_ge_emBits:" 0 < emBits  0 < x  emBits  (roundup emBits x) * x"
  apply (simp add: roundup mult.commute)
  apply (safe)
  apply (simp)
  apply (simp add: add.commute [of x "x*(emBits div x)" ])
  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"
  by (simp add: roundup)

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 (simp add: roundup)
  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"
  by (simp add: sLen_def)

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

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"
  by (simp add:length_bv_prepend)

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"
  by (induct a) (simp add: bv_prepend, simp add: bv_prepend_equal)

lemma bv_prepend_append2:
  "x < y  bv_prepend y b xs = (bv_prepend x b [])@(bv_prepend (y-x) b [])@xs"
  by (simp add: bv_prepend replicate_add [symmetric])

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 "[]"])
  by (simp add: length_bv_prepend)

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 "[]"])
  by (simp add: bv_prepend)

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"
  by (simp add: generate_DB_def sLen_def)

lemma length_generate_PS: "length (generate_PS emBits 160) = (roundup emBits 8)*8 - sLen - 160 - 16"
  by (simp add: generate_PS_def length_bv_prepend)

lemma length_bvxor: "length a = length b  length (bvxor a b) = length a"
  by (simp add: bvxor)

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 (simp add: MGF_def sha1len)
  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

lemma length_maskedDB_zero:
  " roundup emBits 8 * 8 - emBits  length maskedDB
   length (maskedDB_zero maskedDB emBits) = length maskedDB"
  by (simp add: maskedDB_zero_def length_bv_prepend)

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])
  apply (simp add: sha1len maskedDB_zero_def generate_DB_def generate_PS_def
    bv_prepend_split bv_prepend_drop)
  done

lemma lastbits_BC: "BC = show_rightmost_bits (xs @ ys @ BC) 8"
  by (simp add: show_rightmost_bits_def BC_def)

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: generate_DB_def generate_PS_def maskedDB_zero_def)
  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 (simp add: maskedDB_zero_def)
  apply (insert length_bv_prepend_drop [of "(roundup emBits 8 * 8 - emBits)" "x"])
  apply (simp add: generate_maskedDB_def)
  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 (simp add: maskedDB_zero_def)
  apply (insert length_bv_prepend_drop [of "roundup emBits 8 * 8 - emBits" "x"])
  apply (simp add: generate_H_def)
  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)"
  by (simp add: length_bv_prepend_drop)

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])
  apply (simp add: sha1len maskedDB_zero_def generate_DB_def generate_PS_def
    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 (auto simp add: bvxor)
    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)"
  by (simp add: maskedDB_zero_def bvxorxor_elim_help)

lemma verify: "(emsapss_encode M emBits)  []; EM=(emsapss_encode M emBits)  emsapss_decode M EM emBits = True"
  apply (simp add: emsapss_decode_def emsapss_encode_def)
  apply (safe, simp+)
  apply (simp add: emsapss_decode_help1_def emsapss_encode_help1_def)
  apply (safe, simp+)
  apply (simp add: emsapss_decode_help2_def emsapss_encode_help2_def)
  apply (safe)
  apply (simp add: emsapss_encode_help3_def emsapss_encode_help4_def
    emsapss_encode_help5_def emsapss_encode_help6_def)
  apply (safe)
  apply (simp add: emsapss_encode_help7_def emsapss_encode_help8_def lastbits_BC [symmetric])+
  apply (simp add: emsapss_decode_help3_def emsapss_encode_help3_def
    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 (simp add: generate_maskedDB_def emsapss_encode_help5_def emsapss_encode_help6_def)
  apply (safe)
  apply (simp)
  apply (simp add: emsapss_encode_help7_def)
  apply (simp only: emsapss_encode_help8_def)
  apply (simp only: maskedDB_zero_def)
  apply (simp only: take_bv_prepend2 min.absorb1)
  apply (simp)
  apply (simp add: emsapss_encode_help5_def emsapss_encode_help6_def)
  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 add: sha1len emsapss_decode_help5_def)
  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 (fold maskedDB_zero_def)
  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
    Copyright:  2005 - 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
    Copyright:  2005 - 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"
      by (simp add: power_mod)
    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
    Copyright:  2005 - 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))"
  by (auto simp add: nat_distrib)

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 (subst addconst [symmetric])
  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 (subst diff_add_assoc)
  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"
      by (simp add: diff_mult_distrib)
    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
    Copyright:  2005 - 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"
  by (simp add: specializedtoprimes1)
  
end

Theory Cryptinverts

(*  Title:      RSAPSS/Cryptinverts.thy
    Author:     Christina Lindenberg, Kai Wirt, Technische Universität Darmstadt
    Copyright:  2005 - 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 add: mod_mult_left_eq)
  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]
    by (simp_all add: ac_simps)
  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 (simp add: prime_nat_iff)
  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 (simp add: prime_nat_iff)
  apply (cases "q = 2")
   apply (simp add: prime_nat_iff)
  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: prime_nat_iff)
  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
    Copyright:  2005 - 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))
  apply (simp add: emsapss_encode_def)
  apply (simp add: emsapss_encode_help1_def)
  apply (simp add: emsapss_encode_help2_def)
  apply (simp add: emsapss_encode_help3_def)
  apply (simp add: emsapss_encode_help4_def)