[STATEMENT]
lemma length_emsapss_encode:
  "emsapss_encode m x \<noteq> [] \<Longrightarrow> length (emsapss_encode m x) = roundup x 8 * 8"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. emsapss_encode m x \<noteq> [] \<Longrightarrow> length (emsapss_encode m x) = roundup x 8 * 8
[PROOF STEP]
apply (atomize (full))
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. emsapss_encode m x \<noteq> [] \<longrightarrow> length (emsapss_encode m x) = roundup x 8 * 8
[PROOF STEP]
apply (simp add: emsapss_encode_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> 18446744073709551616 \<le> length m \<and> \<not> 687194767360 < x \<longrightarrow> emsapss_encode_help1 (sha1 m) x \<noteq> [] \<longrightarrow> length (emsapss_encode_help1 (sha1 m) x) = roundup x 8 * 8
[PROOF STEP]
apply (simp add: emsapss_encode_help1_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> x < length (sha1 m) + sLen + 16 \<longrightarrow> \<not> 18446744073709551616 \<le> length m \<and> \<not> 687194767360 < x \<longrightarrow> emsapss_encode_help2 (generate_M' (sha1 m) salt) x \<noteq> [] \<longrightarrow> length (emsapss_encode_help2 (generate_M' (sha1 m) salt) x) = roundup x 8 * 8
[PROOF STEP]
apply (simp add: emsapss_encode_help2_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> x < length (sha1 m) + sLen + 16 \<longrightarrow> \<not> 18446744073709551616 \<le> length m \<and> \<not> 687194767360 < x \<longrightarrow> emsapss_encode_help3 (sha1 (generate_M' (sha1 m) salt)) x \<noteq> [] \<longrightarrow> length (emsapss_encode_help3 (sha1 (generate_M' (sha1 m) salt)) x) = roundup x 8 * 8
[PROOF STEP]
apply (simp add: emsapss_encode_help3_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> x < length (sha1 m) + sLen + 16 \<longrightarrow> \<not> 18446744073709551616 \<le> length m \<and> \<not> 687194767360 < x \<longrightarrow> emsapss_encode_help4 (generate_PS x (length (sha1 (generate_M' (sha1 m) salt)))) (sha1 (generate_M' (sha1 m) salt)) x \<noteq> [] \<longrightarrow> length (emsapss_encode_help4 (generate_PS x (length (sha1 (generate_M' (sha1 m) salt)))) (sha1 (generate_M' (sha1 m) salt)) x) = roundup x 8 * 8
[PROOF STEP]
apply (simp add: emsapss_encode_help4_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> x < length (sha1 m) + sLen + 16 \<longrightarrow> \<not> 18446744073709551616 \<le> length m \<and> \<not> 687194767360 < x \<longrightarrow> emsapss_encode_help5 (generate_DB (generate_PS x (length (sha1 (generate_M' (sha1 m) salt))))) (sha1 (generate_M' (sha1 m) salt)) x \<noteq> [] \<longrightarrow> length (emsapss_encode_help5 (generate_DB (generate_PS x (length (sha1 (generate_M' (sha1 m) salt))))) (sha1 (generate_M' (sha1 m) salt)) x) = roundup x 8 * 8
[PROOF STEP]
apply (simp add: emsapss_encode_help5_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> x < length (sha1 m) + sLen + 16 \<longrightarrow> \<not> 18446744073709551616 \<le> length m \<and> \<not> 687194767360 < x \<longrightarrow> emsapss_encode_help6 (generate_DB (generate_PS x (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS x (length (sha1 (generate_M' (sha1 m) salt))))))) (sha1 (generate_M' (sha1 m) salt)) x \<noteq> [] \<longrightarrow> length (emsapss_encode_help6 (generate_DB (generate_PS x (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS x (length (sha1 (generate_M' (sha1 m) salt))))))) (sha1 (generate_M' (sha1 m) salt)) x) = roundup x 8 * 8
[PROOF STEP]
apply (simp add: emsapss_encode_help6_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS x (length (sha1 (generate_M' (sha1 m) salt)))))) \<noteq> [] \<longrightarrow> \<not> x < length (sha1 m) + sLen + 16 \<longrightarrow> \<not> 18446744073709551616 \<le> length m \<and> \<not> 687194767360 < x \<longrightarrow> emsapss_encode_help7 (bvxor (generate_DB (generate_PS x (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS x (length (sha1 (generate_M' (sha1 m) salt)))))))) (sha1 (generate_M' (sha1 m) salt)) x \<noteq> [] \<longrightarrow> length (emsapss_encode_help7 (bvxor (generate_DB (generate_PS x (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS x (length (sha1 (generate_M' (sha1 m) salt)))))))) (sha1 (generate_M' (sha1 m) salt)) x) = roundup x 8 * 8
[PROOF STEP]
apply (simp add: emsapss_encode_help7_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS x (length (sha1 (generate_M' (sha1 m) salt)))))) \<noteq> [] \<longrightarrow> \<not> x < length (sha1 m) + sLen + 16 \<longrightarrow> \<not> 18446744073709551616 \<le> length m \<and> \<not> 687194767360 < x \<longrightarrow> emsapss_encode_help8 (maskedDB_zero (bvxor (generate_DB (generate_PS x (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS x (length (sha1 (generate_M' (sha1 m) salt)))))))) x) (sha1 (generate_M' (sha1 m) salt)) \<noteq> [] \<longrightarrow> length (emsapss_encode_help8 (maskedDB_zero (bvxor (generate_DB (generate_PS x (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS x (length (sha1 (generate_M' (sha1 m) salt)))))))) x) (sha1 (generate_M' (sha1 m) salt))) = roundup x 8 * 8
[PROOF STEP]
apply (simp add: emsapss_encode_help8_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS x (length (sha1 (generate_M' (sha1 m) salt)))))) \<noteq> [] \<longrightarrow> \<not> x < length (sha1 m) + sLen + 16 \<longrightarrow> \<not> 18446744073709551616 \<le> length m \<and> \<not> 687194767360 < x \<longrightarrow> (sha1 (generate_M' (sha1 m) salt) = [] \<longrightarrow> maskedDB_zero (bvxor (generate_DB (generate_PS x 0)) (MGF [] (length (generate_DB (generate_PS x 0))))) x = [] \<longrightarrow> BC \<noteq> []) \<longrightarrow> length (maskedDB_zero (bvxor (generate_DB (generate_PS x (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS x (length (sha1 (generate_M' (sha1 m) salt)))))))) x) + (length (sha1 (generate_M' (sha1 m) salt)) + length BC) = roundup x 8 * 8
[PROOF STEP]
apply (simp add: maskedDB_zero_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS x (length (sha1 (generate_M' (sha1 m) salt)))))) \<noteq> [] \<longrightarrow> \<not> x < length (sha1 m) + sLen + 16 \<longrightarrow> \<not> 18446744073709551616 \<le> length m \<and> \<not> 687194767360 < x \<longrightarrow> (sha1 (generate_M' (sha1 m) salt) = [] \<longrightarrow> bv_prepend (roundup x 8 * 8 - x) \<zero> (drop (roundup x 8 * 8 - x) (bvxor (generate_DB (generate_PS x 0)) (MGF [] (length (generate_DB (generate_PS x 0)))))) = [] \<longrightarrow> BC \<noteq> []) \<longrightarrow> length (bv_prepend (roundup x 8 * 8 - x) \<zero> (drop (roundup x 8 * 8 - x) (bvxor (generate_DB (generate_PS x (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS x (length (sha1 (generate_M' (sha1 m) salt)))))))))) + (length (sha1 (generate_M' (sha1 m) salt)) + length BC) = roundup x 8 * 8
[PROOF STEP]
apply (simp add: length_generate_DB)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_PS x (length (sha1 (generate_M' (sha1 m) salt)))) + 8 + sLen) \<noteq> [] \<longrightarrow> \<not> x < length (sha1 m) + sLen + 16 \<longrightarrow> \<not> 18446744073709551616 \<le> length m \<and> \<not> 687194767360 < x \<longrightarrow> (sha1 (generate_M' (sha1 m) salt) = [] \<longrightarrow> bv_prepend (roundup x 8 * 8 - x) \<zero> (drop (roundup x 8 * 8 - x) (bvxor (generate_DB (generate_PS x 0)) (MGF [] (length (generate_PS x 0) + 8 + sLen)))) = [] \<longrightarrow> BC \<noteq> []) \<longrightarrow> length (bv_prepend (roundup x 8 * 8 - x) \<zero> (drop (roundup x 8 * 8 - x) (bvxor (generate_DB (generate_PS x (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_PS x (length (sha1 (generate_M' (sha1 m) salt)))) + 8 + sLen))))) + (length (sha1 (generate_M' (sha1 m) salt)) + length BC) = roundup x 8 * 8
[PROOF STEP]
apply (simp add: sha1len)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_PS x 160) + 8 + sLen) \<noteq> [] \<longrightarrow> \<not> x < 176 + sLen \<longrightarrow> \<not> 18446744073709551616 \<le> length m \<and> \<not> 687194767360 < x \<longrightarrow> (sha1 (generate_M' (sha1 m) salt) = [] \<longrightarrow> bv_prepend (roundup x 8 * 8 - x) \<zero> (drop (roundup x 8 * 8 - x) (bvxor (generate_DB (generate_PS x 0)) (MGF [] (length (generate_PS x 0) + 8 + sLen)))) = [] \<longrightarrow> BC \<noteq> []) \<longrightarrow> length (bv_prepend (roundup x 8 * 8 - x) \<zero> (drop (roundup x 8 * 8 - x) (bvxor (generate_DB (generate_PS x 160)) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_PS x 160) + 8 + sLen))))) + (160 + length BC) = roundup x 8 * 8
[PROOF STEP]
apply (simp add: bvxor)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_PS x 160) + 8 + sLen) \<noteq> [] \<longrightarrow> \<not> x < 176 + sLen \<longrightarrow> \<not> 18446744073709551616 \<le> length m \<and> \<not> 687194767360 < x \<longrightarrow> (sha1 (generate_M' (sha1 m) salt) = [] \<longrightarrow> bv_prepend (roundup x 8 * 8 - x) \<zero> (drop (roundup x 8 * 8 - x) (bv_mapzip (\<oplus>\<^sub>b) (generate_DB (generate_PS x 0)) (MGF [] (length (generate_PS x 0) + 8 + sLen)))) = [] \<longrightarrow> BC \<noteq> []) \<longrightarrow> length (bv_prepend (roundup x 8 * 8 - x) \<zero> (drop (roundup x 8 * 8 - x) (bv_mapzip (\<oplus>\<^sub>b) (generate_DB (generate_PS x 160)) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_PS x 160) + 8 + sLen))))) + (160 + length BC) = roundup x 8 * 8
[PROOF STEP]
apply (simp add: length_generate_PS)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MGF (sha1 (generate_M' (sha1 m) salt)) (roundup x 8 * 8 - (176 + sLen) + 8 + sLen) \<noteq> [] \<longrightarrow> \<not> x < 176 + sLen \<longrightarrow> \<not> 18446744073709551616 \<le> length m \<and> \<not> 687194767360 < x \<longrightarrow> (sha1 (generate_M' (sha1 m) salt) = [] \<longrightarrow> bv_prepend (roundup x 8 * 8 - x) \<zero> (drop (roundup x 8 * 8 - x) (bv_mapzip (\<oplus>\<^sub>b) (generate_DB (generate_PS x 0)) (MGF [] (length (generate_PS x 0) + 8 + sLen)))) = [] \<longrightarrow> BC \<noteq> []) \<longrightarrow> length (bv_prepend (roundup x 8 * 8 - x) \<zero> (drop (roundup x 8 * 8 - x) (bv_mapzip (\<oplus>\<^sub>b) (generate_DB (generate_PS x 160)) (MGF (sha1 (generate_M' (sha1 m) salt)) (roundup x 8 * 8 - (176 + sLen) + 8 + sLen))))) + (160 + length BC) = roundup x 8 * 8
[PROOF STEP]
apply (simp add: length_bv_prepend)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MGF (sha1 (generate_M' (sha1 m) salt)) (roundup x 8 * 8 - (176 + sLen) + 8 + sLen) \<noteq> [] \<longrightarrow> \<not> x < 176 + sLen \<longrightarrow> \<not> 18446744073709551616 \<le> length m \<and> \<not> 687194767360 < x \<longrightarrow> (sha1 (generate_M' (sha1 m) salt) = [] \<longrightarrow> bv_prepend (roundup x 8 * 8 - x) \<zero> (drop (roundup x 8 * 8 - x) (bv_mapzip (\<oplus>\<^sub>b) (generate_DB (generate_PS x 0)) (MGF [] (length (generate_PS x 0) + 8 + sLen)))) = [] \<longrightarrow> BC \<noteq> []) \<longrightarrow> roundup x 8 * 8 - x + (max (length (generate_DB (generate_PS x 160))) (length (MGF (sha1 (generate_M' (sha1 m) salt)) (roundup x 8 * 8 - (176 + sLen) + 8 + sLen))) - (roundup x 8 * 8 - x)) + (160 + length BC) = roundup x 8 * 8
[PROOF STEP]
apply (simp add: MGF_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (4294967296 * length (sha1 []) < length (generate_PS x 0) + 8 + sLen \<longrightarrow> \<not> 4294967296 * length (sha1 (sha1 (generate_M' (sha1 m) salt))) < roundup x 8 * 8 - (176 + sLen) + 8 + sLen \<longrightarrow> MGF1 (sha1 (generate_M' (sha1 m) salt)) (roundup (roundup x 8 * 8 - (176 + sLen) + 8 + sLen) (length (sha1 (sha1 (generate_M' (sha1 m) salt)))) - Suc 0) (roundup x 8 * 8 - (176 + sLen) + 8 + sLen) \<noteq> [] \<longrightarrow> \<not> x < 176 + sLen \<longrightarrow> \<not> 18446744073709551616 \<le> length m \<and> \<not> 687194767360 < x \<longrightarrow> (sha1 (generate_M' (sha1 m) salt) = [] \<longrightarrow> bv_prepend (roundup x 8 * 8 - x) \<zero> (drop (roundup x 8 * 8 - x) (bv_mapzip (\<oplus>\<^sub>b) (generate_DB (generate_PS x 0)) [])) = [] \<longrightarrow> BC \<noteq> []) \<longrightarrow> roundup x 8 * 8 - x + (max (length (generate_DB (generate_PS x 160))) (length (MGF1 (sha1 (generate_M' (sha1 m) salt)) (roundup (roundup x 8 * 8 - (176 + sLen) + 8 + sLen) (length (sha1 (sha1 (generate_M' (sha1 m) salt)))) - Suc 0) (roundup x 8 * 8 - (176 + sLen) + 8 + sLen))) - (roundup x 8 * 8 - x)) + (160 + length BC) = roundup x 8 * 8) \<and> (\<not> 4294967296 * length (sha1 []) < length (generate_PS x 0) + 8 + sLen \<longrightarrow> \<not> 4294967296 * length (sha1 (sha1 (generate_M' (sha1 m) salt))) < roundup x 8 * 8 - (176 + sLen) + 8 + sLen \<longrightarrow> MGF1 (sha1 (generate_M' (sha1 m) salt)) (roundup (roundup x 8 * 8 - (176 + sLen) + 8 + sLen) (length (sha1 (sha1 (generate_M' (sha1 m) salt)))) - Suc 0) (roundup x 8 * 8 - (176 + sLen) + 8 + sLen) \<noteq> [] \<longrightarrow> \<not> x < 176 + sLen \<longrightarrow> \<not> 18446744073709551616 \<le> length m \<and> \<not> 687194767360 < x \<longrightarrow> (sha1 (generate_M' (sha1 m) salt) = [] \<longrightarrow> bv_prepend (roundup x 8 * 8 - x) \<zero> (drop (roundup x 8 * 8 - x) (bv_mapzip (\<oplus>\<^sub>b) (generate_DB (generate_PS x 0)) (MGF1 [] (roundup (length (generate_PS x 0) + 8 + sLen) (length (sha1 [])) - Suc 0) (length (generate_PS x 0) + 8 + sLen)))) = [] \<longrightarrow> BC \<noteq> []) \<longrightarrow> roundup x 8 * 8 - x + (max (length (generate_DB (generate_PS x 160))) (length (MGF1 (sha1 (generate_M' (sha1 m) salt)) (roundup (roundup x 8 * 8 - (176 + sLen) + 8 + sLen) (length (sha1 (sha1 (generate_M' (sha1 m) salt)))) - Suc 0) (roundup x 8 * 8 - (176 + sLen) + 8 + sLen))) - (roundup x 8 * 8 - x)) + (160 + length BC) = roundup x 8 * 8)
[PROOF STEP]
apply (simp add: MGF1_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (4294967296 * length (sha1 []) < length (generate_PS x 0) + 8 + sLen \<longrightarrow> \<not> 4294967296 * length (sha1 (sha1 (generate_M' (sha1 m) salt))) < roundup x 8 * 8 - (176 + sLen) + 8 + sLen \<longrightarrow> MGF2 (sha1 (generate_M' (sha1 m) salt)) (roundup (roundup x 8 * 8 - (176 + sLen) + 8 + sLen) (length (sha1 (sha1 (generate_M' (sha1 m) salt)))) - Suc 0) \<noteq> [] \<longrightarrow> \<not> x < 176 + sLen \<longrightarrow> \<not> 18446744073709551616 \<le> length m \<and> \<not> 687194767360 < x \<longrightarrow> (sha1 (generate_M' (sha1 m) salt) = [] \<longrightarrow> bv_prepend (roundup x 8 * 8 - x) \<zero> (drop (roundup x 8 * 8 - x) (bv_mapzip (\<oplus>\<^sub>b) (generate_DB (generate_PS x 0)) [])) = [] \<longrightarrow> BC \<noteq> []) \<longrightarrow> roundup x 8 * 8 - x + (max (length (generate_DB (generate_PS x 160))) (min (length (MGF2 (sha1 (generate_M' (sha1 m) salt)) (roundup (roundup x 8 * 8 - (176 + sLen) + 8 + sLen) (length (sha1 (sha1 (generate_M' (sha1 m) salt)))) - Suc 0))) (roundup x 8 * 8 - (176 + sLen) + 8 + sLen)) - (roundup x 8 * 8 - x)) + (160 + length BC) = roundup x 8 * 8) \<and> (\<not> 4294967296 * length (sha1 []) < length (generate_PS x 0) + 8 + sLen \<longrightarrow> \<not> 4294967296 * length (sha1 (sha1 (generate_M' (sha1 m) salt))) < roundup x 8 * 8 - (176 + sLen) + 8 + sLen \<longrightarrow> MGF2 (sha1 (generate_M' (sha1 m) salt)) (roundup (roundup x 8 * 8 - (176 + sLen) + 8 + sLen) (length (sha1 (sha1 (generate_M' (sha1 m) salt)))) - Suc 0) \<noteq> [] \<longrightarrow> \<not> x < 176 + sLen \<longrightarrow> \<not> 18446744073709551616 \<le> length m \<and> \<not> 687194767360 < x \<longrightarrow> (sha1 (generate_M' (sha1 m) salt) = [] \<longrightarrow> bv_prepend (roundup x 8 * 8 - x) \<zero> (drop (roundup x 8 * 8 - x) (bv_mapzip (\<oplus>\<^sub>b) (generate_DB (generate_PS x 0)) (take (length (generate_PS x 0) + 8 + sLen) (MGF2 [] (roundup (length (generate_PS x 0) + 8 + sLen) (length (sha1 [])) - Suc 0))))) = [] \<longrightarrow> BC \<noteq> []) \<longrightarrow> roundup x 8 * 8 - x + (max (length (generate_DB (generate_PS x 160))) (min (length (MGF2 (sha1 (generate_M' (sha1 m) salt)) (roundup (roundup x 8 * 8 - (176 + sLen) + 8 + sLen) (length (sha1 (sha1 (generate_M' (sha1 m) salt)))) - Suc 0))) (roundup x 8 * 8 - (176 + sLen) + 8 + sLen)) - (roundup x 8 * 8 - x)) + (160 + length BC) = roundup x 8 * 8)
[PROOF STEP]
apply (simp add: length_MGF2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (4294967296 * length (sha1 []) < length (generate_PS x 0) + 8 + sLen \<longrightarrow> \<not> 4294967296 * length (sha1 (sha1 (generate_M' (sha1 m) salt))) < roundup x 8 * 8 - (176 + sLen) + 8 + sLen \<longrightarrow> MGF2 (sha1 (generate_M' (sha1 m) salt)) (roundup (roundup x 8 * 8 - (176 + sLen) + 8 + sLen) (length (sha1 (sha1 (generate_M' (sha1 m) salt)))) - Suc 0) \<noteq> [] \<longrightarrow> \<not> x < 176 + sLen \<longrightarrow> \<not> 18446744073709551616 \<le> length m \<and> \<not> 687194767360 < x \<longrightarrow> (sha1 (generate_M' (sha1 m) salt) = [] \<longrightarrow> bv_prepend (roundup x 8 * 8 - x) \<zero> (drop (roundup x 8 * 8 - x) (bv_mapzip (\<oplus>\<^sub>b) (generate_DB (generate_PS x 0)) [])) = [] \<longrightarrow> BC \<noteq> []) \<longrightarrow> roundup x 8 * 8 - x + (max (length (generate_DB (generate_PS x 160))) (min (length (sha1 (sha1 (generate_M' (sha1 m) salt) @ nat_to_bv_length (roundup (roundup x 8 * 8 - (176 + sLen) + 8 + sLen) (length (sha1 (sha1 (generate_M' (sha1 m) salt)))) - Suc 0) 32)) + (roundup (roundup x 8 * 8 - (176 + sLen) + 8 + sLen) (length (sha1 (sha1 (generate_M' (sha1 m) salt)))) - Suc 0) * length (sha1 (sha1 (generate_M' (sha1 m) salt) @ nat_to_bv_length (roundup (roundup x 8 * 8 - (176 + sLen) + 8 + sLen) (length (sha1 (sha1 (generate_M' (sha1 m) salt)))) - Suc 0) 32))) (roundup x 8 * 8 - (176 + sLen) + 8 + sLen)) - (roundup x 8 * 8 - x)) + (160 + length BC) = roundup x 8 * 8) \<and> (\<not> 4294967296 * length (sha1 []) < length (generate_PS x 0) + 8 + sLen \<longrightarrow> \<not> 4294967296 * length (sha1 (sha1 (generate_M' (sha1 m) salt))) < roundup x 8 * 8 - (176 + sLen) + 8 + sLen \<longrightarrow> MGF2 (sha1 (generate_M' (sha1 m) salt)) (roundup (roundup x 8 * 8 - (176 + sLen) + 8 + sLen) (length (sha1 (sha1 (generate_M' (sha1 m) salt)))) - Suc 0) \<noteq> [] \<longrightarrow> \<not> x < 176 + sLen \<longrightarrow> \<not> 18446744073709551616 \<le> length m \<and> \<not> 687194767360 < x \<longrightarrow> (sha1 (generate_M' (sha1 m) salt) = [] \<longrightarrow> bv_prepend (roundup x 8 * 8 - x) \<zero> (drop (roundup x 8 * 8 - x) (bv_mapzip (\<oplus>\<^sub>b) (generate_DB (generate_PS x 0)) (take (length (generate_PS x 0) + 8 + sLen) (MGF2 [] (roundup (length (generate_PS x 0) + 8 + sLen) (length (sha1 [])) - Suc 0))))) = [] \<longrightarrow> BC \<noteq> []) \<longrightarrow> roundup x 8 * 8 - x + (max (length (generate_DB (generate_PS x 160))) (min (length (sha1 (sha1 (generate_M' (sha1 m) salt) @ nat_to_bv_length (roundup (roundup x 8 * 8 - (176 + sLen) + 8 + sLen) (length (sha1 (sha1 (generate_M' (sha1 m) salt)))) - Suc 0) 32)) + (roundup (roundup x 8 * 8 - (176 + sLen) + 8 + sLen) (length (sha1 (sha1 (generate_M' (sha1 m) salt)))) - Suc 0) * length (sha1 (sha1 (generate_M' (sha1 m) salt) @ nat_to_bv_length (roundup (roundup x 8 * 8 - (176 + sLen) + 8 + sLen) (length (sha1 (sha1 (generate_M' (sha1 m) salt)))) - Suc 0) 32))) (roundup x 8 * 8 - (176 + sLen) + 8 + sLen)) - (roundup x 8 * 8 - x)) + (160 + length BC) = roundup x 8 * 8)
[PROOF STEP]
apply (simp add: sha1len)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (687194767352 < length (generate_PS x 0) + sLen \<longrightarrow> \<not> 687194767352 < roundup x 8 * 8 - (176 + sLen) + sLen \<longrightarrow> MGF2 (sha1 (generate_M' (sha1 m) salt)) (roundup (roundup x 8 * 8 - (176 + sLen) + 8 + sLen) 160 - Suc 0) \<noteq> [] \<longrightarrow> \<not> x < 176 + sLen \<longrightarrow> \<not> 18446744073709551616 \<le> length m \<and> \<not> 687194767360 < x \<longrightarrow> (sha1 (generate_M' (sha1 m) salt) = [] \<longrightarrow> bv_prepend (roundup x 8 * 8 - x) \<zero> (drop (roundup x 8 * 8 - x) (bv_mapzip (\<oplus>\<^sub>b) (generate_DB (generate_PS x 0)) [])) = [] \<longrightarrow> BC \<noteq> []) \<longrightarrow> roundup x 8 * 8 - x + (max (length (generate_DB (generate_PS x 160))) (min (160 + (roundup (roundup x 8 * 8 - (176 + sLen) + 8 + sLen) 160 - Suc 0) * 160) (roundup x 8 * 8 - (176 + sLen) + 8 + sLen)) - (roundup x 8 * 8 - x)) + (160 + length BC) = roundup x 8 * 8) \<and> (\<not> 687194767352 < length (generate_PS x 0) + sLen \<longrightarrow> \<not> 687194767352 < roundup x 8 * 8 - (176 + sLen) + sLen \<longrightarrow> MGF2 (sha1 (generate_M' (sha1 m) salt)) (roundup (roundup x 8 * 8 - (176 + sLen) + 8 + sLen) 160 - Suc 0) \<noteq> [] \<longrightarrow> \<not> x < 176 + sLen \<longrightarrow> \<not> 18446744073709551616 \<le> length m \<and> \<not> 687194767360 < x \<longrightarrow> (sha1 (generate_M' (sha1 m) salt) = [] \<longrightarrow> bv_prepend (roundup x 8 * 8 - x) \<zero> (drop (roundup x 8 * 8 - x) (bv_mapzip (\<oplus>\<^sub>b) (generate_DB (generate_PS x 0)) (take (length (generate_PS x 0) + 8 + sLen) (MGF2 [] (roundup (length (generate_PS x 0) + 8 + sLen) 160 - Suc 0))))) = [] \<longrightarrow> BC \<noteq> []) \<longrightarrow> roundup x 8 * 8 - x + (max (length (generate_DB (generate_PS x 160))) (min (160 + (roundup (roundup x 8 * 8 - (176 + sLen) + 8 + sLen) 160 - Suc 0) * 160) (roundup x 8 * 8 - (176 + sLen) + 8 + sLen)) - (roundup x 8 * 8 - x)) + (160 + length BC) = roundup x 8 * 8)
[PROOF STEP]
apply (simp add: length_generate_DB)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (687194767352 < length (generate_PS x 0) + sLen \<longrightarrow> \<not> 687194767352 < roundup x 8 * 8 - (176 + sLen) + sLen \<longrightarrow> MGF2 (sha1 (generate_M' (sha1 m) salt)) (roundup (roundup x 8 * 8 - (176 + sLen) + 8 + sLen) 160 - Suc 0) \<noteq> [] \<longrightarrow> \<not> x < 176 + sLen \<longrightarrow> \<not> 18446744073709551616 \<le> length m \<and> \<not> 687194767360 < x \<longrightarrow> (sha1 (generate_M' (sha1 m) salt) = [] \<longrightarrow> bv_prepend (roundup x 8 * 8 - x) \<zero> (drop (roundup x 8 * 8 - x) (bv_mapzip (\<oplus>\<^sub>b) (generate_DB (generate_PS x 0)) [])) = [] \<longrightarrow> BC \<noteq> []) \<longrightarrow> roundup x 8 * 8 - x + (max (length (generate_PS x 160) + 8 + sLen) (min (160 + (roundup (roundup x 8 * 8 - (176 + sLen) + 8 + sLen) 160 - Suc 0) * 160) (roundup x 8 * 8 - (176 + sLen) + 8 + sLen)) - (roundup x 8 * 8 - x)) + (160 + length BC) = roundup x 8 * 8) \<and> (\<not> 687194767352 < length (generate_PS x 0) + sLen \<longrightarrow> \<not> 687194767352 < roundup x 8 * 8 - (176 + sLen) + sLen \<longrightarrow> MGF2 (sha1 (generate_M' (sha1 m) salt)) (roundup (roundup x 8 * 8 - (176 + sLen) + 8 + sLen) 160 - Suc 0) \<noteq> [] \<longrightarrow> \<not> x < 176 + sLen \<longrightarrow> \<not> 18446744073709551616 \<le> length m \<and> \<not> 687194767360 < x \<longrightarrow> (sha1 (generate_M' (sha1 m) salt) = [] \<longrightarrow> bv_prepend (roundup x 8 * 8 - x) \<zero> (drop (roundup x 8 * 8 - x) (bv_mapzip (\<oplus>\<^sub>b) (generate_DB (generate_PS x 0)) (take (length (generate_PS x 0) + 8 + sLen) (MGF2 [] (roundup (length (generate_PS x 0) + 8 + sLen) 160 - Suc 0))))) = [] \<longrightarrow> BC \<noteq> []) \<longrightarrow> roundup x 8 * 8 - x + (max (length (generate_PS x 160) + 8 + sLen) (min (160 + (roundup (roundup x 8 * 8 - (176 + sLen) + 8 + sLen) 160 - Suc 0) * 160) (roundup x 8 * 8 - (176 + sLen) + 8 + sLen)) - (roundup x 8 * 8 - x)) + (160 + length BC) = roundup x 8 * 8)
[PROOF STEP]
apply (simp add: length_generate_PS)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (687194767352 < length (generate_PS x 0) + sLen \<longrightarrow> \<not> 687194767352 < roundup x 8 * 8 - (176 + sLen) + sLen \<longrightarrow> MGF2 (sha1 (generate_M' (sha1 m) salt)) (roundup (roundup x 8 * 8 - (176 + sLen) + 8 + sLen) 160 - Suc 0) \<noteq> [] \<longrightarrow> \<not> x < 176 + sLen \<longrightarrow> \<not> 18446744073709551616 \<le> length m \<and> \<not> 687194767360 < x \<longrightarrow> (sha1 (generate_M' (sha1 m) salt) = [] \<longrightarrow> bv_prepend (roundup x 8 * 8 - x) \<zero> (drop (roundup x 8 * 8 - x) (bv_mapzip (\<oplus>\<^sub>b) (generate_DB (generate_PS x 0)) [])) = [] \<longrightarrow> BC \<noteq> []) \<longrightarrow> 168 + (roundup x 8 * 8 - (176 + sLen) + (sLen + length BC)) = roundup x 8 * 8) \<and> (\<not> 687194767352 < length (generate_PS x 0) + sLen \<longrightarrow> \<not> 687194767352 < roundup x 8 * 8 - (176 + sLen) + sLen \<longrightarrow> MGF2 (sha1 (generate_M' (sha1 m) salt)) (roundup (roundup x 8 * 8 - (176 + sLen) + 8 + sLen) 160 - Suc 0) \<noteq> [] \<longrightarrow> \<not> x < 176 + sLen \<longrightarrow> \<not> 18446744073709551616 \<le> length m \<and> \<not> 687194767360 < x \<longrightarrow> (sha1 (generate_M' (sha1 m) salt) = [] \<longrightarrow> bv_prepend (roundup x 8 * 8 - x) \<zero> (drop (roundup x 8 * 8 - x) (bv_mapzip (\<oplus>\<^sub>b) (generate_DB (generate_PS x 0)) (take (length (generate_PS x 0) + 8 + sLen) (MGF2 [] (roundup (length (generate_PS x 0) + 8 + sLen) 160 - Suc 0))))) = [] \<longrightarrow> BC \<noteq> []) \<longrightarrow> 168 + (roundup x 8 * 8 - (176 + sLen) + (sLen + length BC)) = roundup x 8 * 8)
[PROOF STEP]
apply (simp add: BC_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> 687194767352 < roundup x 8 * 8 - (176 + sLen) + sLen \<longrightarrow> MGF2 (sha1 (generate_M' (sha1 m) salt)) (roundup (roundup x 8 * 8 - (176 + sLen) + 8 + sLen) 160 - Suc 0) \<noteq> [] \<longrightarrow> \<not> x < 176 + sLen \<longrightarrow> \<not> 18446744073709551616 \<le> length m \<and> \<not> 687194767360 < x \<longrightarrow> 176 + (roundup x 8 * 8 - (176 + sLen) + sLen) = roundup x 8 * 8
[PROOF STEP]
apply (insert roundup_ge_emBits [of x 8])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>0 < x; 0 < 8\<rbrakk> \<Longrightarrow> x \<le> roundup x 8 * 8) \<Longrightarrow> \<not> 687194767352 < roundup x 8 * 8 - (176 + sLen) + sLen \<longrightarrow> MGF2 (sha1 (generate_M' (sha1 m) salt)) (roundup (roundup x 8 * 8 - (176 + sLen) + 8 + sLen) 160 - Suc 0) \<noteq> [] \<longrightarrow> \<not> x < 176 + sLen \<longrightarrow> \<not> 18446744073709551616 \<le> length m \<and> \<not> 687194767360 < x \<longrightarrow> 176 + (roundup x 8 * 8 - (176 + sLen) + sLen) = roundup x 8 * 8
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>0 < x; 0 < 8\<rbrakk> \<Longrightarrow> x \<le> roundup x 8 * 8; \<not> 687194767352 < roundup x 8 * 8 - (176 + sLen) + sLen; MGF2 (sha1 (generate_M' (sha1 m) salt)) (roundup (roundup x 8 * 8 - (176 + sLen) + 8 + sLen) 160 - Suc 0) \<noteq> []; \<not> x < 176 + sLen; \<not> 18446744073709551616 \<le> length m; \<not> 687194767360 < x\<rbrakk> \<Longrightarrow> 176 + (roundup x 8 * 8 - (176 + sLen) + sLen) = roundup x 8 * 8
[PROOF STEP]
apply (simp add: max.absorb1)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma bv_to_nat_emsapss_encode_le: "emsapss_encode m x \<noteq> [] \<Longrightarrow> bv_to_nat (emsapss_encode m x) < 2^(roundup x 8 * 8)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. emsapss_encode m x \<noteq> [] \<Longrightarrow> bv_to_nat (emsapss_encode m x) < 2 ^ (roundup x 8 * 8)
[PROOF STEP]
apply (insert length_emsapss_encode [of m x])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>emsapss_encode m x \<noteq> []; emsapss_encode m x \<noteq> [] \<Longrightarrow> length (emsapss_encode m x) = roundup x 8 * 8\<rbrakk> \<Longrightarrow> bv_to_nat (emsapss_encode m x) < 2 ^ (roundup x 8 * 8)
[PROOF STEP]
apply (insert bv_to_nat_upper_range [of "emsapss_encode m x"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>emsapss_encode m x \<noteq> []; emsapss_encode m x \<noteq> [] \<Longrightarrow> length (emsapss_encode m x) = roundup x 8 * 8; bv_to_nat (emsapss_encode m x) < 2 ^ length (emsapss_encode m x)\<rbrakk> \<Longrightarrow> bv_to_nat (emsapss_encode m x) < 2 ^ (roundup x 8 * 8)
[PROOF STEP]
by (simp)


[STATEMENT]
lemma length_helper1: shows "length
  (bvxor
  (generate_DB
  (generate_PS (length (nat_to_bv (p * q)) - Suc 0)
  (length (sha1 (generate_M' (sha1 m) salt)))))
  (MGF (sha1 (generate_M' (sha1 m) salt))
  (length
  (generate_DB
  (generate_PS (length (nat_to_bv (p * q)) - Suc 0)
  (length (sha1 (generate_M' (sha1 m) salt)))))))@
  sha1 (generate_M' (sha1 m) salt) @ BC)
  = length
  (bvxor
  (generate_DB
  (generate_PS (length (nat_to_bv (p * q)) - Suc 0)
  (length (sha1 (generate_M' (sha1 m) salt)))))
  (MGF (sha1 (generate_M' (sha1 m) salt))
  (length
  (generate_DB
  (generate_PS (length (nat_to_bv (p * q)) - Suc 0)
  (length (sha1 (generate_M' (sha1 m) salt)))))))) + 168"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))))) @ sha1 (generate_M' (sha1 m) salt) @ BC) = length (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))))) + 168
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. length (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))))) @ sha1 (generate_M' (sha1 m) salt) @ BC) = length (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))))) + 168
[PROOF STEP]
have a: "length BC = 8"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length BC = 8
[PROOF STEP]
by (simp add: BC_def)
[PROOF STATE]
proof (state)
this:
length BC = 8

goal (1 subgoal):
 1. length (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))))) @ sha1 (generate_M' (sha1 m) salt) @ BC) = length (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))))) + 168
[PROOF STEP]
have b: "length (sha1 (generate_M' (sha1 m) salt)) = 160"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (sha1 (generate_M' (sha1 m) salt)) = 160
[PROOF STEP]
by (simp add: sha1len)
[PROOF STATE]
proof (state)
this:
length (sha1 (generate_M' (sha1 m) salt)) = 160

goal (1 subgoal):
 1. length (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))))) @ sha1 (generate_M' (sha1 m) salt) @ BC) = length (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))))) + 168
[PROOF STEP]
have c: "\<And> a b c. length (a@b@c) = length a + length b + length c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b c. length (a @ b @ c) = length a + length b + length c
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length (?a @ ?b @ ?c) = length ?a + length ?b + length ?c

goal (1 subgoal):
 1. length (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))))) @ sha1 (generate_M' (sha1 m) salt) @ BC) = length (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))))) + 168
[PROOF STEP]
from a and b
[PROOF STATE]
proof (chain)
picking this:
length BC = 8
length (sha1 (generate_M' (sha1 m) salt)) = 160
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
length BC = 8
length (sha1 (generate_M' (sha1 m) salt)) = 160

goal (1 subgoal):
 1. length (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))))) @ sha1 (generate_M' (sha1 m) salt) @ BC) = length (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))))) + 168
[PROOF STEP]
using c
[PROOF STATE]
proof (prove)
using this:
length BC = 8
length (sha1 (generate_M' (sha1 m) salt)) = 160
length (?a @ ?b @ ?c) = length ?a + length ?b + length ?c

goal (1 subgoal):
 1. length (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))))) @ sha1 (generate_M' (sha1 m) salt) @ BC) = length (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))))) + 168
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))))) @ sha1 (generate_M' (sha1 m) salt) @ BC) = length (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))))) + 168

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma MGFLen_helper: "MGF z l ~= [] \<Longrightarrow> l <= 2^32*(length (sha1 z))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MGF z l \<noteq> [] \<Longrightarrow> l \<le> 2 ^ 32 * length (sha1 z)
[PROOF STEP]
proof (cases "2^32*length (sha1 z) < l")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>MGF z l \<noteq> []; 2 ^ 32 * length (sha1 z) < l\<rbrakk> \<Longrightarrow> l \<le> 2 ^ 32 * length (sha1 z)
 2. \<lbrakk>MGF z l \<noteq> []; \<not> 2 ^ 32 * length (sha1 z) < l\<rbrakk> \<Longrightarrow> l \<le> 2 ^ 32 * length (sha1 z)
[PROOF STEP]
assume x: "MGF z l ~= []"
[PROOF STATE]
proof (state)
this:
MGF z l \<noteq> []

goal (2 subgoals):
 1. \<lbrakk>MGF z l \<noteq> []; 2 ^ 32 * length (sha1 z) < l\<rbrakk> \<Longrightarrow> l \<le> 2 ^ 32 * length (sha1 z)
 2. \<lbrakk>MGF z l \<noteq> []; \<not> 2 ^ 32 * length (sha1 z) < l\<rbrakk> \<Longrightarrow> l \<le> 2 ^ 32 * length (sha1 z)
[PROOF STEP]
assume a: "2 ^ 32 * length (sha1 z) < l"
[PROOF STATE]
proof (state)
this:
2 ^ 32 * length (sha1 z) < l

goal (2 subgoals):
 1. \<lbrakk>MGF z l \<noteq> []; 2 ^ 32 * length (sha1 z) < l\<rbrakk> \<Longrightarrow> l \<le> 2 ^ 32 * length (sha1 z)
 2. \<lbrakk>MGF z l \<noteq> []; \<not> 2 ^ 32 * length (sha1 z) < l\<rbrakk> \<Longrightarrow> l \<le> 2 ^ 32 * length (sha1 z)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
2 ^ 32 * length (sha1 z) < l
[PROOF STEP]
have "MGF z l = []"
[PROOF STATE]
proof (prove)
using this:
2 ^ 32 * length (sha1 z) < l

goal (1 subgoal):
 1. MGF z l = []
[PROOF STEP]
proof (cases "l=0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>2 ^ 32 * length (sha1 z) < l; l = 0\<rbrakk> \<Longrightarrow> MGF z l = []
 2. \<lbrakk>2 ^ 32 * length (sha1 z) < l; l \<noteq> 0\<rbrakk> \<Longrightarrow> MGF z l = []
[PROOF STEP]
assume "l=0"
[PROOF STATE]
proof (state)
this:
l = 0

goal (2 subgoals):
 1. \<lbrakk>2 ^ 32 * length (sha1 z) < l; l = 0\<rbrakk> \<Longrightarrow> MGF z l = []
 2. \<lbrakk>2 ^ 32 * length (sha1 z) < l; l \<noteq> 0\<rbrakk> \<Longrightarrow> MGF z l = []
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
l = 0
[PROOF STEP]
show "MGF z l = []"
[PROOF STATE]
proof (prove)
using this:
l = 0

goal (1 subgoal):
 1. MGF z l = []
[PROOF STEP]
by (simp add: MGF_def)
[PROOF STATE]
proof (state)
this:
MGF z l = []

goal (1 subgoal):
 1. \<lbrakk>2 ^ 32 * length (sha1 z) < l; l \<noteq> 0\<rbrakk> \<Longrightarrow> MGF z l = []
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>2 ^ 32 * length (sha1 z) < l; l \<noteq> 0\<rbrakk> \<Longrightarrow> MGF z l = []
[PROOF STEP]
assume "l~=0"
[PROOF STATE]
proof (state)
this:
l \<noteq> 0

goal (1 subgoal):
 1. \<lbrakk>2 ^ 32 * length (sha1 z) < l; l \<noteq> 0\<rbrakk> \<Longrightarrow> MGF z l = []
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
l \<noteq> 0
[PROOF STEP]
have "(l = 0 \<or> 2^32*length(sha1 z) < l) = True"
[PROOF STATE]
proof (prove)
using this:
l \<noteq> 0

goal (1 subgoal):
 1. (l = 0 \<or> 2 ^ 32 * length (sha1 z) < l) = True
[PROOF STEP]
using a
[PROOF STATE]
proof (prove)
using this:
l \<noteq> 0
2 ^ 32 * length (sha1 z) < l

goal (1 subgoal):
 1. (l = 0 \<or> 2 ^ 32 * length (sha1 z) < l) = True
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
(l = 0 \<or> 2 ^ 32 * length (sha1 z) < l) = True

goal (1 subgoal):
 1. \<lbrakk>2 ^ 32 * length (sha1 z) < l; l \<noteq> 0\<rbrakk> \<Longrightarrow> MGF z l = []
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(l = 0 \<or> 2 ^ 32 * length (sha1 z) < l) = True
[PROOF STEP]
show "MGF z l = []"
[PROOF STATE]
proof (prove)
using this:
(l = 0 \<or> 2 ^ 32 * length (sha1 z) < l) = True

goal (1 subgoal):
 1. MGF z l = []
[PROOF STEP]
apply (simp only: MGF_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (l = 0 \<or> 2 ^ 32 * length (sha1 z) < l) = True \<Longrightarrow> (if True then [] else MGF1 z (roundup l (length (sha1 z)) - 1) l) = []
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
MGF z l = []

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
MGF z l = []

goal (2 subgoals):
 1. \<lbrakk>MGF z l \<noteq> []; 2 ^ 32 * length (sha1 z) < l\<rbrakk> \<Longrightarrow> l \<le> 2 ^ 32 * length (sha1 z)
 2. \<lbrakk>MGF z l \<noteq> []; \<not> 2 ^ 32 * length (sha1 z) < l\<rbrakk> \<Longrightarrow> l \<le> 2 ^ 32 * length (sha1 z)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
MGF z l = []
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
MGF z l = []

goal (1 subgoal):
 1. l \<le> 2 ^ 32 * length (sha1 z)
[PROOF STEP]
using x
[PROOF STATE]
proof (prove)
using this:
MGF z l = []
MGF z l \<noteq> []

goal (1 subgoal):
 1. l \<le> 2 ^ 32 * length (sha1 z)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
l \<le> 2 ^ 32 * length (sha1 z)

goal (1 subgoal):
 1. \<lbrakk>MGF z l \<noteq> []; \<not> 2 ^ 32 * length (sha1 z) < l\<rbrakk> \<Longrightarrow> l \<le> 2 ^ 32 * length (sha1 z)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>MGF z l \<noteq> []; \<not> 2 ^ 32 * length (sha1 z) < l\<rbrakk> \<Longrightarrow> l \<le> 2 ^ 32 * length (sha1 z)
[PROOF STEP]
assume "\<not> 2 ^ 32 * length (sha1 z) < l"
[PROOF STATE]
proof (state)
this:
\<not> 2 ^ 32 * length (sha1 z) < l

goal (1 subgoal):
 1. \<lbrakk>MGF z l \<noteq> []; \<not> 2 ^ 32 * length (sha1 z) < l\<rbrakk> \<Longrightarrow> l \<le> 2 ^ 32 * length (sha1 z)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> 2 ^ 32 * length (sha1 z) < l
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> 2 ^ 32 * length (sha1 z) < l

goal (1 subgoal):
 1. l \<le> 2 ^ 32 * length (sha1 z)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
l \<le> 2 ^ 32 * length (sha1 z)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma length_helper2: assumes p: "prime p" and q: "prime q"
                      and mgf: "(MGF (sha1 (generate_M' (sha1 m) salt))
  (length
  (generate_DB
  (generate_PS (length (nat_to_bv (p * q)) - Suc 0)
  (length (sha1 (generate_M' (sha1 m) salt))))))) ~= []"
  and len: "length (sha1 M) + sLen + 16 \<le> (length (nat_to_bv (p * q))) - Suc 0"
  shows "length
  (
  (bvxor
  (generate_DB
  (generate_PS (length (nat_to_bv (p * q)) - Suc 0)
  (length (sha1 (generate_M' (sha1 m) salt)))))
  (MGF (sha1 (generate_M' (sha1 m) salt))
  (length
  (generate_DB
  (generate_PS (length (nat_to_bv (p * q)) - Suc 0)
  (length (sha1 (generate_M' (sha1 m) salt))))))))
  ) = (roundup (length (nat_to_bv (p * q)) - Suc 0) 8) * 8 - 168"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))))) = roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8 - 168
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. length (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))))) = roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8 - 168
[PROOF STEP]
have a: "length (MGF (sha1 (generate_M' (sha1 m) salt))
  (length
  (generate_DB
  (generate_PS (length (nat_to_bv (p * q)) - Suc 0)
  (length (sha1 (generate_M' (sha1 m) salt))))))) = (length
  (generate_DB
  (generate_PS (length (nat_to_bv (p * q)) - Suc 0)
  (length (sha1 (generate_M' (sha1 m) salt))))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))))) = length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. length (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))))) = length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))
[PROOF STEP]
have "0 < (length
  (generate_DB
  (generate_PS (length (nat_to_bv (p * q)) - Suc 0)
  (length (sha1 (generate_M' (sha1 m) salt))))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))
[PROOF STEP]
by (simp add: generate_DB_def)
[PROOF STATE]
proof (state)
this:
0 < length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))

goal (1 subgoal):
 1. length (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))))) = length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
0 < length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))

goal (1 subgoal):
 1. length (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))))) = length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))
[PROOF STEP]
have "(length
  (generate_DB
  (generate_PS (length (nat_to_bv (p * q)) - Suc 0)
  (length (sha1 (generate_M' (sha1 m) salt)))))) \<le> 2^32 * length (sha1 (sha1 (generate_M' (sha1 m) salt)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) \<le> 2 ^ 32 * length (sha1 (sha1 (generate_M' (sha1 m) salt)))
[PROOF STEP]
using mgf and MGFLen_helper
[PROOF STATE]
proof (prove)
using this:
MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))) \<noteq> []
MGF ?z ?l \<noteq> [] \<Longrightarrow> ?l \<le> 2 ^ 32 * length (sha1 ?z)

goal (1 subgoal):
 1. length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) \<le> 2 ^ 32 * length (sha1 (sha1 (generate_M' (sha1 m) salt)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) \<le> 2 ^ 32 * length (sha1 (sha1 (generate_M' (sha1 m) salt)))

goal (1 subgoal):
 1. length (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))))) = length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
0 < length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))
length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) \<le> 2 ^ 32 * length (sha1 (sha1 (generate_M' (sha1 m) salt)))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
0 < length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))
length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) \<le> 2 ^ 32 * length (sha1 (sha1 (generate_M' (sha1 m) salt)))

goal (1 subgoal):
 1. length (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))))) = length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))
[PROOF STEP]
using length_MGF
[PROOF STATE]
proof (prove)
using this:
0 < length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))
length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) \<le> 2 ^ 32 * length (sha1 (sha1 (generate_M' (sha1 m) salt)))
\<lbrakk>0 < ?l; ?l \<le> 2 ^ 32 * length (sha1 ?x)\<rbrakk> \<Longrightarrow> length (MGF ?x ?l) = ?l

goal (1 subgoal):
 1. length (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))))) = length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))))) = length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
length (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))))) = length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))

goal (1 subgoal):
 1. length (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))))) = roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8 - 168
[PROOF STEP]
have b: "length (generate_DB
  (generate_PS (length (nat_to_bv (p * q)) - Suc 0)
  (length (sha1 (generate_M' (sha1 m) salt))))) = ((roundup ((length (nat_to_bv (p * q))) - Suc 0) 8) * 8 - 168)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) = roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8 - 168
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) = roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8 - 168
[PROOF STEP]
have "0 <= (length (nat_to_bv (p * q))) - Suc 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> length (nat_to_bv (p * q)) - Suc 0
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 0 \<le> length (nat_to_bv (p * q)) - Suc 0
[PROOF STEP]
from p
[PROOF STATE]
proof (chain)
picking this:
prime p
[PROOF STEP]
have p2: "1<p"
[PROOF STATE]
proof (prove)
using this:
prime p

goal (1 subgoal):
 1. 1 < p
[PROOF STEP]
by (simp add: prime_nat_iff)
[PROOF STATE]
proof (state)
this:
1 < p

goal (1 subgoal):
 1. 0 \<le> length (nat_to_bv (p * q)) - Suc 0
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
1 < p

goal (1 subgoal):
 1. 0 \<le> length (nat_to_bv (p * q)) - Suc 0
[PROOF STEP]
from q
[PROOF STATE]
proof (chain)
picking this:
prime q
[PROOF STEP]
have "1<q"
[PROOF STATE]
proof (prove)
using this:
prime q

goal (1 subgoal):
 1. 1 < q
[PROOF STEP]
by (simp add: prime_nat_iff)
[PROOF STATE]
proof (state)
this:
1 < q

goal (1 subgoal):
 1. 0 \<le> length (nat_to_bv (p * q)) - Suc 0
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
1 < p
1 < q
[PROOF STEP]
have "p<p*q"
[PROOF STATE]
proof (prove)
using this:
1 < p
1 < q

goal (1 subgoal):
 1. p < p * q
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
p < p * q

goal (1 subgoal):
 1. 0 \<le> length (nat_to_bv (p * q)) - Suc 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p < p * q
[PROOF STEP]
have "1<p*q"
[PROOF STATE]
proof (prove)
using this:
p < p * q

goal (1 subgoal):
 1. 1 < p * q
[PROOF STEP]
using p2
[PROOF STATE]
proof (prove)
using this:
p < p * q
1 < p

goal (1 subgoal):
 1. 1 < p * q
[PROOF STEP]
by arith
[PROOF STATE]
proof (state)
this:
1 < p * q

goal (1 subgoal):
 1. 0 \<le> length (nat_to_bv (p * q)) - Suc 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
1 < p * q
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
1 < p * q

goal (1 subgoal):
 1. 0 \<le> length (nat_to_bv (p * q)) - Suc 0
[PROOF STEP]
using len_nat_to_bv_pos
[PROOF STATE]
proof (prove)
using this:
1 < p * q
1 < ?a \<Longrightarrow> 0 < length (nat_to_bv ?a)

goal (1 subgoal):
 1. 0 \<le> length (nat_to_bv (p * q)) - Suc 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 \<le> length (nat_to_bv (p * q)) - Suc 0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
0 \<le> length (nat_to_bv (p * q)) - Suc 0

goal (1 subgoal):
 1. length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) = roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8 - 168
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 \<le> length (nat_to_bv (p * q)) - Suc 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
0 \<le> length (nat_to_bv (p * q)) - Suc 0

goal (1 subgoal):
 1. length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) = roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8 - 168
[PROOF STEP]
using solve_length_generate_DB
[PROOF STATE]
proof (prove)
using this:
0 \<le> length (nat_to_bv (p * q)) - Suc 0
\<lbrakk>0 < ?emBits; length (sha1 ?M) + sLen + 16 \<le> ?emBits\<rbrakk> \<Longrightarrow> length (generate_DB (generate_PS ?emBits (length (sha1 ?x)))) = roundup ?emBits 8 * 8 - 168

goal (1 subgoal):
 1. length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) = roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8 - 168
[PROOF STEP]
using len
[PROOF STATE]
proof (prove)
using this:
0 \<le> length (nat_to_bv (p * q)) - Suc 0
\<lbrakk>0 < ?emBits; length (sha1 ?M) + sLen + 16 \<le> ?emBits\<rbrakk> \<Longrightarrow> length (generate_DB (generate_PS ?emBits (length (sha1 ?x)))) = roundup ?emBits 8 * 8 - 168
length (sha1 M) + sLen + 16 \<le> length (nat_to_bv (p * q)) - Suc 0

goal (1 subgoal):
 1. length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) = roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8 - 168
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) = roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8 - 168

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) = roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8 - 168

goal (1 subgoal):
 1. length (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))))) = roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8 - 168
[PROOF STEP]
have c: "length (bvxor
    (generate_DB
    (generate_PS (length (nat_to_bv (p * q)) - Suc 0)
    (length (sha1 (generate_M' (sha1 m) salt)))))
    (MGF (sha1 (generate_M' (sha1 m) salt))
    (length
    (generate_DB
    (generate_PS (length (nat_to_bv (p * q)) - Suc 0)
    (length (sha1 (generate_M' (sha1 m) salt)))))))) =
    roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8 - 168"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))))) = roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8 - 168
[PROOF STEP]
using a and b and length_bvxor
[PROOF STATE]
proof (prove)
using this:
length (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))))) = length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))
length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) = roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8 - 168
length ?a = length ?b \<Longrightarrow> length (bvxor ?a ?b) = length ?a

goal (1 subgoal):
 1. length (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))))) = roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8 - 168
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))))) = roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8 - 168

goal (1 subgoal):
 1. length (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))))) = roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8 - 168
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))))) = roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8 - 168
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
length (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))))) = roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8 - 168

goal (1 subgoal):
 1. length (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))))) = roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8 - 168
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))))) = roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8 - 168

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma emBits_roundup_cancel: "emBits mod 8 ~= 0 \<Longrightarrow> (roundup emBits 8)*8 - emBits = 8-(emBits mod 8)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. emBits mod 8 \<noteq> 0 \<Longrightarrow> roundup emBits 8 * 8 - emBits = 8 - emBits mod 8
[PROOF STEP]
apply (auto simp add: roundup)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < emBits mod 8 \<Longrightarrow> 8 + emBits div 8 * 8 - emBits = 8 - emBits mod 8
[PROOF STEP]
by (arith)


[STATEMENT]
lemma emBits_roundup_cancel2: "emBits mod 8 ~=0 \<Longrightarrow> (roundup emBits 8) * 8 - (8-(emBits mod 8)) = emBits"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. emBits mod 8 \<noteq> 0 \<Longrightarrow> roundup emBits 8 * 8 - (8 - emBits mod 8) = emBits
[PROOF STEP]
by (auto simp add: roundup)


[STATEMENT]
lemma length_bound: "\<lbrakk>emBits mod 8 ~=0; 8 <= (length maskedDB)\<rbrakk> \<Longrightarrow> length (remzero ((maskedDB_zero maskedDB emBits)@a@b)) <= length (maskedDB@a@b) - (8-(emBits mod 8))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>emBits mod 8 \<noteq> 0; 8 \<le> length maskedDB\<rbrakk> \<Longrightarrow> length (remzero (maskedDB_zero maskedDB emBits @ a @ b)) \<le> length (maskedDB @ a @ b) - (8 - emBits mod 8)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>emBits mod 8 \<noteq> 0; 8 \<le> length maskedDB\<rbrakk> \<Longrightarrow> length (remzero (maskedDB_zero maskedDB emBits @ a @ b)) \<le> length (maskedDB @ a @ b) - (8 - emBits mod 8)
[PROOF STEP]
assume a: "emBits mod 8 ~=0"
[PROOF STATE]
proof (state)
this:
emBits mod 8 \<noteq> 0

goal (1 subgoal):
 1. \<lbrakk>emBits mod 8 \<noteq> 0; 8 \<le> length maskedDB\<rbrakk> \<Longrightarrow> length (remzero (maskedDB_zero maskedDB emBits @ a @ b)) \<le> length (maskedDB @ a @ b) - (8 - emBits mod 8)
[PROOF STEP]
assume len: "8 <= (length maskedDB)"
[PROOF STATE]
proof (state)
this:
8 \<le> length maskedDB

goal (1 subgoal):
 1. \<lbrakk>emBits mod 8 \<noteq> 0; 8 \<le> length maskedDB\<rbrakk> \<Longrightarrow> length (remzero (maskedDB_zero maskedDB emBits @ a @ b)) \<le> length (maskedDB @ a @ b) - (8 - emBits mod 8)
[PROOF STEP]
have b:" \<And> a. length (remzero a) <= length a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. length (remzero a) \<le> length a
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. length (remzero a) \<le> length a
[PROOF STEP]
fix a
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. length (remzero a) \<le> length a
[PROOF STEP]
show "length (remzero a) <= length a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (remzero a) \<le> length a
[PROOF STEP]
proof (induct a)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. length (remzero []) \<le> length []
 2. \<And>a1 a2. length (remzero a2) \<le> length a2 \<Longrightarrow> length (remzero (a1 # a2)) \<le> length (a1 # a2)
[PROOF STEP]
show "(length (remzero [])) <= length []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (remzero []) \<le> length []
[PROOF STEP]
by (simp)
[PROOF STATE]
proof (state)
this:
length (remzero []) \<le> length []

goal (1 subgoal):
 1. \<And>a1 a2. length (remzero a2) \<le> length a2 \<Longrightarrow> length (remzero (a1 # a2)) \<le> length (a1 # a2)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a1 a2. length (remzero a2) \<le> length a2 \<Longrightarrow> length (remzero (a1 # a2)) \<le> length (a1 # a2)
[PROOF STEP]
case (Cons hd tl)
[PROOF STATE]
proof (state)
this:
length (remzero tl) \<le> length tl

goal (1 subgoal):
 1. \<And>a1 a2. length (remzero a2) \<le> length a2 \<Longrightarrow> length (remzero (a1 # a2)) \<le> length (a1 # a2)
[PROOF STEP]
show "(length (remzero (hd#tl))) <= length (hd#tl)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (remzero (hd # tl)) \<le> length (hd # tl)
[PROOF STEP]
proof (cases hd)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. hd = \<zero> \<Longrightarrow> length (remzero (hd # tl)) \<le> length (hd # tl)
 2. hd = \<one> \<Longrightarrow> length (remzero (hd # tl)) \<le> length (hd # tl)
[PROOF STEP]
assume "hd=\<zero>"
[PROOF STATE]
proof (state)
this:
hd = \<zero>

goal (2 subgoals):
 1. hd = \<zero> \<Longrightarrow> length (remzero (hd # tl)) \<le> length (hd # tl)
 2. hd = \<one> \<Longrightarrow> length (remzero (hd # tl)) \<le> length (hd # tl)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
hd = \<zero>
[PROOF STEP]
have "remzero (hd#tl) = remzero tl"
[PROOF STATE]
proof (prove)
using this:
hd = \<zero>

goal (1 subgoal):
 1. remzero (hd # tl) = remzero tl
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
remzero (hd # tl) = remzero tl

goal (2 subgoals):
 1. hd = \<zero> \<Longrightarrow> length (remzero (hd # tl)) \<le> length (hd # tl)
 2. hd = \<one> \<Longrightarrow> length (remzero (hd # tl)) \<le> length (hd # tl)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
remzero (hd # tl) = remzero tl
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
remzero (hd # tl) = remzero tl

goal (1 subgoal):
 1. length (remzero (hd # tl)) \<le> length (hd # tl)
[PROOF STEP]
using Cons
[PROOF STATE]
proof (prove)
using this:
remzero (hd # tl) = remzero tl
length (remzero tl) \<le> length tl

goal (1 subgoal):
 1. length (remzero (hd # tl)) \<le> length (hd # tl)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length (remzero (hd # tl)) \<le> length (hd # tl)

goal (1 subgoal):
 1. hd = \<one> \<Longrightarrow> length (remzero (hd # tl)) \<le> length (hd # tl)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. hd = \<one> \<Longrightarrow> length (remzero (hd # tl)) \<le> length (hd # tl)
[PROOF STEP]
assume "hd=\<one>"
[PROOF STATE]
proof (state)
this:
hd = \<one>

goal (1 subgoal):
 1. hd = \<one> \<Longrightarrow> length (remzero (hd # tl)) \<le> length (hd # tl)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
hd = \<one>
[PROOF STEP]
have "remzero (hd#tl) = hd#tl"
[PROOF STATE]
proof (prove)
using this:
hd = \<one>

goal (1 subgoal):
 1. remzero (hd # tl) = hd # tl
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
remzero (hd # tl) = hd # tl

goal (1 subgoal):
 1. hd = \<one> \<Longrightarrow> length (remzero (hd # tl)) \<le> length (hd # tl)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
remzero (hd # tl) = hd # tl
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
remzero (hd # tl) = hd # tl

goal (1 subgoal):
 1. length (remzero (hd # tl)) \<le> length (hd # tl)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length (remzero (hd # tl)) \<le> length (hd # tl)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
length (remzero (hd # tl)) \<le> length (hd # tl)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
length (remzero a) \<le> length a

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
length (remzero ?a) \<le> length ?a

goal (1 subgoal):
 1. \<lbrakk>emBits mod 8 \<noteq> 0; 8 \<le> length maskedDB\<rbrakk> \<Longrightarrow> length (remzero (maskedDB_zero maskedDB emBits @ a @ b)) \<le> length (maskedDB @ a @ b) - (8 - emBits mod 8)
[PROOF STEP]
from len
[PROOF STATE]
proof (chain)
picking this:
8 \<le> length maskedDB
[PROOF STEP]
show "length (remzero (maskedDB_zero maskedDB emBits @ a @ b)) \<le> length (maskedDB @ a @ b) - (8 - emBits mod 8)"
[PROOF STATE]
proof (prove)
using this:
8 \<le> length maskedDB

goal (1 subgoal):
 1. length (remzero (maskedDB_zero maskedDB emBits @ a @ b)) \<le> length (maskedDB @ a @ b) - (8 - emBits mod 8)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 8 \<le> length maskedDB \<Longrightarrow> length (remzero (maskedDB_zero maskedDB emBits @ a @ b)) \<le> length (maskedDB @ a @ b) - (8 - emBits mod 8)
[PROOF STEP]
have "remzero(bv_prepend ((roundup emBits 8) * 8 - emBits)
      \<zero> (drop ((roundup emBits 8)*8 - emBits) maskedDB)@a@b) = remzero ((drop ((roundup emBits 8)*8 -emBits) maskedDB)@a@b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. remzero (bv_prepend (roundup emBits 8 * 8 - emBits) \<zero> (drop (roundup emBits 8 * 8 - emBits) maskedDB) @ a @ b) = remzero (drop (roundup emBits 8 * 8 - emBits) maskedDB @ a @ b)
[PROOF STEP]
using remzero_replicate
[PROOF STATE]
proof (prove)
using this:
remzero (replicate ?n \<zero> @ ?l) = remzero ?l

goal (1 subgoal):
 1. remzero (bv_prepend (roundup emBits 8 * 8 - emBits) \<zero> (drop (roundup emBits 8 * 8 - emBits) maskedDB) @ a @ b) = remzero (drop (roundup emBits 8 * 8 - emBits) maskedDB @ a @ b)
[PROOF STEP]
by (simp add: bv_prepend)
[PROOF STATE]
proof (state)
this:
remzero (bv_prepend (roundup emBits 8 * 8 - emBits) \<zero> (drop (roundup emBits 8 * 8 - emBits) maskedDB) @ a @ b) = remzero (drop (roundup emBits 8 * 8 - emBits) maskedDB @ a @ b)

goal (1 subgoal):
 1. 8 \<le> length maskedDB \<Longrightarrow> length (remzero (maskedDB_zero maskedDB emBits @ a @ b)) \<le> length (maskedDB @ a @ b) - (8 - emBits mod 8)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
remzero (bv_prepend (roundup emBits 8 * 8 - emBits) \<zero> (drop (roundup emBits 8 * 8 - emBits) maskedDB) @ a @ b) = remzero (drop (roundup emBits 8 * 8 - emBits) maskedDB @ a @ b)

goal (1 subgoal):
 1. 8 \<le> length maskedDB \<Longrightarrow> length (remzero (maskedDB_zero maskedDB emBits @ a @ b)) \<le> length (maskedDB @ a @ b) - (8 - emBits mod 8)
[PROOF STEP]
from emBits_roundup_cancel
[PROOF STATE]
proof (chain)
picking this:
?emBits mod 8 \<noteq> 0 \<Longrightarrow> roundup ?emBits 8 * 8 - ?emBits = 8 - ?emBits mod 8
[PROOF STEP]
have "roundup emBits 8 * 8 - emBits = 8 - emBits mod 8"
[PROOF STATE]
proof (prove)
using this:
?emBits mod 8 \<noteq> 0 \<Longrightarrow> roundup ?emBits 8 * 8 - ?emBits = 8 - ?emBits mod 8

goal (1 subgoal):
 1. roundup emBits 8 * 8 - emBits = 8 - emBits mod 8
[PROOF STEP]
using a
[PROOF STATE]
proof (prove)
using this:
?emBits mod 8 \<noteq> 0 \<Longrightarrow> roundup ?emBits 8 * 8 - ?emBits = 8 - ?emBits mod 8
emBits mod 8 \<noteq> 0

goal (1 subgoal):
 1. roundup emBits 8 * 8 - emBits = 8 - emBits mod 8
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
roundup emBits 8 * 8 - emBits = 8 - emBits mod 8

goal (1 subgoal):
 1. 8 \<le> length maskedDB \<Longrightarrow> length (remzero (maskedDB_zero maskedDB emBits @ a @ b)) \<le> length (maskedDB @ a @ b) - (8 - emBits mod 8)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
roundup emBits 8 * 8 - emBits = 8 - emBits mod 8

goal (1 subgoal):
 1. 8 \<le> length maskedDB \<Longrightarrow> length (remzero (maskedDB_zero maskedDB emBits @ a @ b)) \<le> length (maskedDB @ a @ b) - (8 - emBits mod 8)
[PROOF STEP]
have "length ((drop (8-emBits mod 8) maskedDB)@a@b) = length (maskedDB@a@b) - (8-emBits mod 8)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (drop (8 - emBits mod 8) maskedDB @ a @ b) = length (maskedDB @ a @ b) - (8 - emBits mod 8)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. length (drop (8 - emBits mod 8) maskedDB @ a @ b) = length (maskedDB @ a @ b) - (8 - emBits mod 8)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (drop (8 - emBits mod 8) maskedDB @ a @ b) = length (maskedDB @ a @ b) - (8 - emBits mod 8)
[PROOF STEP]
using length_drop[of "(8-emBits mod 8)" maskedDB]
[PROOF STATE]
proof (prove)
using this:
length (drop (8 - emBits mod 8) maskedDB) = length maskedDB - (8 - emBits mod 8)

goal (1 subgoal):
 1. length (drop (8 - emBits mod 8) maskedDB @ a @ b) = length (maskedDB @ a @ b) - (8 - emBits mod 8)
[PROOF STEP]
proof (simp)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. length maskedDB + emBits mod 8 - 8 + (length a + length b) = length maskedDB + (length a + length b) + emBits mod 8 - 8
[PROOF STEP]
have "0 <= emBits mod 8"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> emBits mod 8
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 \<le> emBits mod 8

goal (1 subgoal):
 1. length maskedDB + emBits mod 8 - 8 + (length a + length b) = length maskedDB + (length a + length b) + emBits mod 8 - 8
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 \<le> emBits mod 8
[PROOF STEP]
have "8-(emBits mod 8) <= 8"
[PROOF STATE]
proof (prove)
using this:
0 \<le> emBits mod 8

goal (1 subgoal):
 1. 8 - emBits mod 8 \<le> 8
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
8 - emBits mod 8 \<le> 8

goal (1 subgoal):
 1. length maskedDB + emBits mod 8 - 8 + (length a + length b) = length maskedDB + (length a + length b) + emBits mod 8 - 8
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
8 - emBits mod 8 \<le> 8
[PROOF STEP]
show  "length maskedDB + emBits mod 8 - 8 + (length a + length b) =
          length maskedDB + (length a + length b) + emBits mod 8 - 8"
[PROOF STATE]
proof (prove)
using this:
8 - emBits mod 8 \<le> 8

goal (1 subgoal):
 1. length maskedDB + emBits mod 8 - 8 + (length a + length b) = length maskedDB + (length a + length b) + emBits mod 8 - 8
[PROOF STEP]
using len
[PROOF STATE]
proof (prove)
using this:
8 - emBits mod 8 \<le> 8
8 \<le> length maskedDB

goal (1 subgoal):
 1. length maskedDB + emBits mod 8 - 8 + (length a + length b) = length maskedDB + (length a + length b) + emBits mod 8 - 8
[PROOF STEP]
by arith
[PROOF STATE]
proof (state)
this:
length maskedDB + emBits mod 8 - 8 + (length a + length b) = length maskedDB + (length a + length b) + emBits mod 8 - 8

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
length (drop (8 - emBits mod 8) maskedDB @ a @ b) = length (maskedDB @ a @ b) - (8 - emBits mod 8)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
length (drop (8 - emBits mod 8) maskedDB @ a @ b) = length (maskedDB @ a @ b) - (8 - emBits mod 8)

goal (1 subgoal):
 1. 8 \<le> length maskedDB \<Longrightarrow> length (remzero (maskedDB_zero maskedDB emBits @ a @ b)) \<le> length (maskedDB @ a @ b) - (8 - emBits mod 8)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
remzero (bv_prepend (roundup emBits 8 * 8 - emBits) \<zero> (drop (roundup emBits 8 * 8 - emBits) maskedDB) @ a @ b) = remzero (drop (roundup emBits 8 * 8 - emBits) maskedDB @ a @ b)
roundup emBits 8 * 8 - emBits = 8 - emBits mod 8
length (drop (8 - emBits mod 8) maskedDB @ a @ b) = length (maskedDB @ a @ b) - (8 - emBits mod 8)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
remzero (bv_prepend (roundup emBits 8 * 8 - emBits) \<zero> (drop (roundup emBits 8 * 8 - emBits) maskedDB) @ a @ b) = remzero (drop (roundup emBits 8 * 8 - emBits) maskedDB @ a @ b)
roundup emBits 8 * 8 - emBits = 8 - emBits mod 8
length (drop (8 - emBits mod 8) maskedDB @ a @ b) = length (maskedDB @ a @ b) - (8 - emBits mod 8)

goal (1 subgoal):
 1. length (remzero (maskedDB_zero maskedDB emBits @ a @ b)) \<le> length (maskedDB @ a @ b) - (8 - emBits mod 8)
[PROOF STEP]
using b[of "(drop ((roundup emBits 8)*8 - emBits) maskedDB)@a@b"]
[PROOF STATE]
proof (prove)
using this:
remzero (bv_prepend (roundup emBits 8 * 8 - emBits) \<zero> (drop (roundup emBits 8 * 8 - emBits) maskedDB) @ a @ b) = remzero (drop (roundup emBits 8 * 8 - emBits) maskedDB @ a @ b)
roundup emBits 8 * 8 - emBits = 8 - emBits mod 8
length (drop (8 - emBits mod 8) maskedDB @ a @ b) = length (maskedDB @ a @ b) - (8 - emBits mod 8)
length (remzero (drop (roundup emBits 8 * 8 - emBits) maskedDB @ a @ b)) \<le> length (drop (roundup emBits 8 * 8 - emBits) maskedDB @ a @ b)

goal (1 subgoal):
 1. length (remzero (maskedDB_zero maskedDB emBits @ a @ b)) \<le> length (maskedDB @ a @ b) - (8 - emBits mod 8)
[PROOF STEP]
by (simp add: maskedDB_zero_def)
[PROOF STATE]
proof (state)
this:
length (remzero (maskedDB_zero maskedDB emBits @ a @ b)) \<le> length (maskedDB @ a @ b) - (8 - emBits mod 8)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
length (remzero (maskedDB_zero maskedDB emBits @ a @ b)) \<le> length (maskedDB @ a @ b) - (8 - emBits mod 8)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma length_bound2: "8<=length ( (bvxor
  (generate_DB
  (generate_PS (length (nat_to_bv (p * q)) - Suc 0)
  (length (sha1 (generate_M' (sha1 m) salt)))))
  (MGF (sha1 (generate_M' (sha1 m) salt))
  (length
  (generate_DB
  (generate_PS (length (nat_to_bv (p * q)) - Suc 0)
  (length (sha1 (generate_M' (sha1 m) salt)))))))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 8 \<le> length (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))))))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 8 \<le> length (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))))))
[PROOF STEP]
have "8 <= length (generate_DB
  (generate_PS (length (nat_to_bv (p * q)) - Suc 0)
  (length (sha1 (generate_M' (sha1 m) salt)))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 8 \<le> length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))
[PROOF STEP]
by (simp add: generate_DB_def)
[PROOF STATE]
proof (state)
this:
8 \<le> length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))

goal (1 subgoal):
 1. 8 \<le> length (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))))))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
8 \<le> length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
8 \<le> length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))

goal (1 subgoal):
 1. 8 \<le> length (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))))))
[PROOF STEP]
using length_bvxor_bound
[PROOF STATE]
proof (prove)
using this:
8 \<le> length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))
?a \<le> length ?l \<Longrightarrow> ?a \<le> length (bvxor ?l ?l2.0)

goal (1 subgoal):
 1. 8 \<le> length (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))))))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
8 \<le> length (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))))))

goal:
No subgoals!
[PROOF STEP]
qed