theory Retype_C

lemma ccte_relation_makeObject:
  notes option.case_cong_weak [cong]
  shows "ccte_relation makeObject (from_bytes (replicate (size_of TYPE(cte_C)) 0))" apply (simp add: Let_def makeObject_cte size_of_def ccte_relation_def map_option_Some_eq2) apply (simp add: from_bytes_def) apply (simp add: typ_info_simps cte_C_tag_def  cte_lift_def
    size_td_lt_final_pad size_td_lt_ti_typ_pad_combine Let_def size_of_def) apply (simp add: final_pad_def Let_def size_td_lt_ti_typ_pad_combine
    size_of_def padup_def align_td_array' size_td_array update_ti_adjust_ti
    ti_typ_pad_combine_def ti_typ_combine_def empty_typ_info_def align_of_def
    typ_info_simps cap_C_tag_def mdb_node_C_tag_def split: option.splits) apply (simp add: typ_info_array array_tag_def eval_nat_numeral array_tag_n.simps) apply (simp add: final_pad_def Let_def size_td_lt_ti_typ_pad_combine
    size_of_def padup_def align_td_array' size_td_array update_ti_adjust_ti
    ti_typ_pad_combine_def ti_typ_combine_def empty_typ_info_def update_ti_t_word32_0s) apply (simp add: cap_lift_def Let_def cap_get_tag_def cap_tag_defs cte_to_H_def cap_to_H_def mdb_node_to_H_def
    mdb_node_lift_def nullMDBNode_def c_valid_cte_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccte_relation makeObject (from_bytes (replicate (size_of TYPE(cte_C)) 0)) proof (prove)
goal (1 subgoal):
 1. (\<exists>z. cte_lift (from_bytes [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]) = Some z \<and> cte_to_H z = CTE capability.NullCap nullMDBNode) \<and> c_valid_cte (from_bytes [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]) proof (prove)
goal (1 subgoal):
 1. (\<exists>z. cte_lift (update_ti_t (typ_info_t TYPE(cte_C)) [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] undefined) = Some z \<and> cte_to_H z = CTE capability.NullCap nullMDBNode) \<and> c_valid_cte (update_ti_t (typ_info_t TYPE(cte_C)) [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] undefined) proof (prove)
goal (1 subgoal):
 1. (\<exists>z. (case cap_lift (cte_C.cap_C (update_ti_t (final_pad (ti_typ_pad_combine TYPE(mdb_node_C) cteMDBNode_C (cteMDBNode_C_update \<circ> (\<lambda>x _. x)) ''cteMDBNode_C'' (ti_typ_pad_combine TYPE(cap_C) cte_C.cap_C (cte_C.cap_C_update \<circ> (\<lambda>x _. x)) ''cap_C'' (empty_typ_info ''cte_C'')))) [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] undefined)) of None \<Rightarrow> None | Some cap \<Rightarrow> Some \<lparr>cap_CL = cap, cteMDBNode_CL = mdb_node_lift (cteMDBNode_C (update_ti_t (final_pad (ti_typ_pad_combine TYPE(mdb_node_C) cteMDBNode_C (cteMDBNode_C_update \<circ> (\<lambda>x _. x)) ''cteMDBNode_C'' (ti_typ_pad_combine TYPE(cap_C) cte_C.cap_C (cte_C.cap_C_update \<circ> (\<lambda>x _. x)) ''cap_C'' (empty_typ_info ''cte_C'')))) [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] undefined))\<rparr>) = Some z \<and> cte_to_H z = CTE capability.NullCap nullMDBNode) \<and> c_valid_cte (update_ti_t (final_pad (ti_typ_pad_combine TYPE(mdb_node_C) cteMDBNode_C (cteMDBNode_C_update \<circ> (\<lambda>x _. x)) ''cteMDBNode_C'' (ti_typ_pad_combine TYPE(cap_C) cte_C.cap_C (cte_C.cap_C_update \<circ> (\<lambda>x _. x)) ''cap_C'' (empty_typ_info ''cte_C'')))) [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] undefined) proof (prove)
goal (1 subgoal):
 1. (\<exists>y. cap_lift (cap_C.words_C_update (\<lambda>_. update_ti_t (typ_info_t TYPE(32 word[2])) [0, 0, 0, 0, 0, 0, 0, 0] (cap_C.words_C (cte_C.cap_C undefined))) (cte_C.cap_C undefined)) = Some y) \<and> (\<forall>x2. cap_lift (cap_C.words_C_update (\<lambda>_. update_ti_t (typ_info_t TYPE(32 word[2])) [0, 0, 0, 0, 0, 0, 0, 0] (cap_C.words_C (cte_C.cap_C undefined))) (cte_C.cap_C undefined)) = Some x2 \<longrightarrow> cte_to_H \<lparr>cap_CL = x2, cteMDBNode_CL = mdb_node_lift (mdb_node_C.words_C_update (\<lambda>_. update_ti_t (typ_info_t TYPE(32 word[2])) [0, 0, 0, 0, 0, 0, 0, 0] (mdb_node_C.words_C (cteMDBNode_C undefined))) (cteMDBNode_C undefined))\<rparr> = CTE capability.NullCap nullMDBNode \<and> c_valid_cte (cteMDBNode_C_update (\<lambda>_. mdb_node_C.words_C_update (\<lambda>_. update_ti_t (typ_info_t TYPE(32 word[2])) [0, 0, 0, 0, 0, 0, 0, 0] (mdb_node_C.words_C (cteMDBNode_C undefined))) (cteMDBNode_C undefined)) (cte_C.cap_C_update (\<lambda>_. cap_C.words_C_update (\<lambda>_. update_ti_t (typ_info_t TYPE(32 word[2])) [0, 0, 0, 0, 0, 0, 0, 0] (cap_C.words_C (cte_C.cap_C undefined))) (cte_C.cap_C undefined)) undefined))) proof (prove)
goal (1 subgoal):
 1. (\<exists>y. cap_lift (cap_C.words_C_update (\<lambda>_. update_ti_t (ti_typ_combine TYPE(32 word) (\<lambda>x. x.[Suc 0]) (\<lambda>x f. Arrays.update f (Suc 0) x) ''1'' (ti_typ_combine TYPE(32 word) (\<lambda>x. x.[0]) (\<lambda>x f. Arrays.update f 0 x) [] (empty_typ_info (CHR ''w'' # CHR ''o'' # CHR ''r'' # CHR ''d'' # CHR ''0'' # CHR ''0'' # CHR ''0'' # CHR ''0'' # CHR ''0'' # CHR ''1'' # CHR ''0'' # CHR ''_'' # CHR ''a'' # CHR ''r'' # CHR ''r'' # CHR ''a'' # CHR ''y'' # CHR ''_'' # nat_to_bin_string (Suc (Suc 0)))))) [0, 0, 0, 0, 0, 0, 0, 0] (cap_C.words_C (cte_C.cap_C undefined))) (cte_C.cap_C undefined)) = Some y) \<and> (\<forall>x2. cap_lift (cap_C.words_C_update (\<lambda>_. update_ti_t (ti_typ_combine TYPE(32 word) (\<lambda>x. x.[Suc 0]) (\<lambda>x f. Arrays.update f (Suc 0) x) ''1'' (ti_typ_combine TYPE(32 word) (\<lambda>x. x.[0]) (\<lambda>x f. Arrays.update f 0 x) [] (empty_typ_info (CHR ''w'' # CHR ''o'' # CHR ''r'' # CHR ''d'' # CHR ''0'' # CHR ''0'' # CHR ''0'' # CHR ''0'' # CHR ''0'' # CHR ''1'' # CHR ''0'' # CHR ''_'' # CHR ''a'' # CHR ''r'' # CHR ''r'' # CHR ''a'' # CHR ''y'' # CHR ''_'' # nat_to_bin_string (Suc (Suc 0)))))) [0, 0, 0, 0, 0, 0, 0, 0] (cap_C.words_C (cte_C.cap_C undefined))) (cte_C.cap_C undefined)) = Some x2 \<longrightarrow> cte_to_H \<lparr>cap_CL = x2, cteMDBNode_CL = mdb_node_lift (mdb_node_C.words_C_update (\<lambda>_. update_ti_t (ti_typ_combine TYPE(32 word) (\<lambda>x. x.[Suc 0]) (\<lambda>x f. Arrays.update f (Suc 0) x) ''1'' (ti_typ_combine TYPE(32 word) (\<lambda>x. x.[0]) (\<lambda>x f. Arrays.update f 0 x) [] (empty_typ_info (CHR ''w'' # CHR ''o'' # CHR ''r'' # CHR ''d'' # CHR ''0'' # CHR ''0'' # CHR ''0'' # CHR ''0'' # CHR ''0'' # CHR ''1'' # CHR ''0'' # CHR ''_'' # CHR ''a'' # CHR ''r'' # CHR ''r'' # CHR ''a'' # CHR ''y'' # CHR ''_'' # nat_to_bin_string (Suc (Suc 0)))))) [0, 0, 0, 0, 0, 0, 0, 0] (mdb_node_C.words_C (cteMDBNode_C undefined))) (cteMDBNode_C undefined))\<rparr> = CTE capability.NullCap nullMDBNode \<and> c_valid_cte (cteMDBNode_C_update (\<lambda>_. mdb_node_C.words_C_update (\<lambda>_. update_ti_t (ti_typ_combine TYPE(32 word) (\<lambda>x. x.[Suc 0]) (\<lambda>x f. Arrays.update f (Suc 0) x) ''1'' (ti_typ_combine TYPE(32 word) (\<lambda>x. x.[0]) (\<lambda>x f. Arrays.update f 0 x) [] (empty_typ_info (CHR ''w'' # CHR ''o'' # CHR ''r'' # CHR ''d'' # CHR ''0'' # CHR ''0'' # CHR ''0'' # CHR ''0'' # CHR ''0'' # CHR ''1'' # CHR ''0'' # CHR ''_'' # CHR ''a'' # CHR ''r'' # CHR ''r'' # CHR ''a'' # CHR ''y'' # CHR ''_'' # nat_to_bin_string (Suc (Suc 0)))))) [0, 0, 0, 0, 0, 0, 0, 0] (mdb_node_C.words_C (cteMDBNode_C undefined))) (cteMDBNode_C undefined)) (cte_C.cap_C_update (\<lambda>_. cap_C.words_C_update (\<lambda>_. update_ti_t (ti_typ_combine TYPE(32 word) (\<lambda>x. x.[Suc 0]) (\<lambda>x f. Arrays.update f (Suc 0) x) ''1'' (ti_typ_combine TYPE(32 word) (\<lambda>x. x.[0]) (\<lambda>x f. Arrays.update f 0 x) [] (empty_typ_info (CHR ''w'' # CHR ''o'' # CHR ''r'' # CHR ''d'' # CHR ''0'' # CHR ''0'' # CHR ''0'' # CHR ''0'' # CHR ''0'' # CHR ''1'' # CHR ''0'' # CHR ''_'' # CHR ''a'' # CHR ''r'' # CHR ''r'' # CHR ''a'' # CHR ''y'' # CHR ''_'' # nat_to_bin_string (Suc (Suc 0)))))) [0, 0, 0, 0, 0, 0, 0, 0] (cap_C.words_C (cte_C.cap_C undefined))) (cte_C.cap_C undefined)) undefined))) proof (prove)
goal (1 subgoal):
 1. (\<exists>y. cap_lift (cap_C.words_C_update (\<lambda>_. Arrays.update (Arrays.update (cap_C.words_C (cte_C.cap_C undefined)) 0 0) (Suc 0) 0) (cte_C.cap_C undefined)) = Some y) \<and> (\<forall>x2. cap_lift (cap_C.words_C_update (\<lambda>_. Arrays.update (Arrays.update (cap_C.words_C (cte_C.cap_C undefined)) 0 0) (Suc 0) 0) (cte_C.cap_C undefined)) = Some x2 \<longrightarrow> cte_to_H \<lparr>cap_CL = x2, cteMDBNode_CL = mdb_node_lift (mdb_node_C.words_C_update (\<lambda>_. Arrays.update (Arrays.update (mdb_node_C.words_C (cteMDBNode_C undefined)) 0 0) (Suc 0) 0) (cteMDBNode_C undefined))\<rparr> = CTE capability.NullCap nullMDBNode \<and> c_valid_cte (cteMDBNode_C_update (\<lambda>_. mdb_node_C.words_C_update (\<lambda>_. Arrays.update (Arrays.update (mdb_node_C.words_C (cteMDBNode_C undefined)) 0 0) (Suc 0) 0) (cteMDBNode_C undefined)) (cte_C.cap_C_update (\<lambda>_. cap_C.words_C_update (\<lambda>_. Arrays.update (Arrays.update (cap_C.words_C (cte_C.cap_C undefined)) 0 0) (Suc 0) 0) (cte_C.cap_C undefined)) undefined))) proof (prove)
goal:
No subgoals!