theory Recycle_C

lemma coerce_memset_to_heap_update_user_data:
  "heap_update_list x (replicateHider 4096 0)
      = heap_update (Ptr x :: user_data_C ptr)
             (user_data_C (FCP (\<lambda>_. 0)))" apply (intro ext, simp add: heap_update_def) apply (rule_tac f="\<lambda>xs. heap_update_list x xs a b" for a b in arg_cong) apply (simp add: to_bytes_def size_of_def typ_info_simps user_data_C_tag_def) apply (simp add: ti_typ_pad_combine_empty_ti ti_typ_pad_combine_td align_of_def padup_def
                   final_pad_def size_td_lt_ti_typ_pad_combine Let_def size_of_def) apply (simp add: typ_info_simps
                   user_context_C_tag_def thread_state_C_tag_def seL4_Fault_C_tag_def
                   lookup_fault_C_tag_def update_ti_t_ptr_0s
                   ti_typ_pad_combine_empty_ti ti_typ_pad_combine_td
                   align_of_def padup_def
                   final_pad_def size_td_lt_ti_typ_pad_combine Let_def size_of_def
                   align_td_array' size_td_array) apply (simp add: typ_info_array') apply (subst access_ti_list_array) apply simp apply simp apply (simp add: typ_info_word typ_info_ptr word_rsplit_0) apply fastforce apply (simp add: collapse_foldl_replicate word_bits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. heap_update_list x (replicateHider 4096 0) = heap_update (PTR(user_data_C) x) (user_data_C (ARRAY _. 0)) proof (prove)
goal (1 subgoal):
 1. \<And>xa xaa. heap_update_list x (replicateHider 4096 0) xa xaa = heap_update_list x (to_bytes (user_data_C (ARRAY _. 0)) (heap_list xa 4096 x)) xa xaa proof (prove)
goal (1 subgoal):
 1. \<And>xa xaa. replicateHider 4096 0 = to_bytes (user_data_C (ARRAY _. 0)) (heap_list xa 4096 x) proof (prove)
goal (1 subgoal):
 1. \<And>xa. replicateHider 4096 0 = access_ti (final_pad (ti_typ_pad_combine TYPE(32 word[1024]) user_data_C.words_C (user_data_C.words_C_update \<circ> (\<lambda>x _. x)) ''words_C'' (empty_typ_info ''user_data_C''))) (user_data_C (ARRAY _. 0)) (heap_list xa 4096 x) proof (prove)
goal (1 subgoal):
 1. \<And>xa. replicateHider 4096 0 = access_ti (if 0 < (2 ^ align_td (typ_info_t TYPE(32 word[1024])) - size_td (typ_info_t TYPE(32 word[1024])) mod 2 ^ align_td (typ_info_t TYPE(32 word[1024]))) mod 2 ^ align_td (typ_info_t TYPE(32 word[1024])) then ti_pad_combine ((2 ^ align_td (typ_info_t TYPE(32 word[1024])) - size_td (typ_info_t TYPE(32 word[1024])) mod 2 ^ align_td (typ_info_t TYPE(32 word[1024]))) mod 2 ^ align_td (typ_info_t TYPE(32 word[1024]))) (TypDesc (TypAggregate [DTPair (adjust_ti (typ_info_t TYPE(32 word[1024])) user_data_C.words_C (user_data_C.words_C_update \<circ> (\<lambda>x _. x))) ''words_C'']) ''user_data_C'') else TypDesc (TypAggregate [DTPair (adjust_ti (typ_info_t TYPE(32 word[1024])) user_data_C.words_C (user_data_C.words_C_update \<circ> (\<lambda>x _. x))) ''words_C'']) ''user_data_C'') (user_data_C (ARRAY _. 0)) (heap_list xa 4096 x) proof (prove)
goal (1 subgoal):
 1. \<And>xa. replicateHider 4096 0 = access_ti (typ_info_t TYPE(32 word[1024])) (ARRAY _. 0) (heap_list xa 4096 x) proof (prove)
goal (1 subgoal):
 1. \<And>xa. replicateHider 4096 0 = access_ti_list (map (\<lambda>n. DTPair (adjust_ti (typ_info_t TYPE(32 word)) (\<lambda>x. x.[n]) (\<lambda>x f. Arrays.update f n x)) (replicate n CHR ''1'')) [0..<1024]) (ARRAY _. 0) (heap_list xa 4096 x) proof (prove)
goal (4 subgoals):
 1. \<And>x. \<forall>n. size_td_pair (DTPair (adjust_ti (typ_info_t TYPE(32 word)) (\<lambda>x. x.[n]) (\<lambda>x f. Arrays.update f n x)) (replicate n CHR ''1'')) = ?v3.6 x
 2. \<And>xa. length (heap_list xa 4096 x) = ?v3.6 xa * 1024
 3. \<And>xa. \<forall>m. m < 1024 \<and> ?v3.6 xa \<le> length (drop (?v3.6 xa * m) (heap_list xa 4096 x)) \<longrightarrow> access_ti_pair (DTPair (adjust_ti (typ_info_t TYPE(32 word)) (\<lambda>x. x.[m]) (\<lambda>x f. Arrays.update f m x)) (replicate m CHR ''1'')) (ARRAY _. 0) (take (?v3.6 xa) (drop (?v3.6 xa * m) (heap_list xa 4096 x))) = ?h6 xa m
 4. \<And>x. replicateHider 4096 0 = foldl (@) [] (map (?h6 x) [0..<1024]) proof (prove)
goal (3 subgoals):
 1. \<And>xa. length (heap_list xa 4096 x) = 4 * 1024
 2. \<And>xa. \<forall>m. m < 1024 \<and> 4 \<le> length (drop (4 * m) (heap_list xa 4096 x)) \<longrightarrow> access_ti_pair (DTPair (adjust_ti (typ_info_t TYPE(32 word)) (\<lambda>x. x.[m]) (\<lambda>x f. Arrays.update f m x)) (replicate m CHR ''1'')) (ARRAY _. 0) (take 4 (drop (4 * m) (heap_list xa 4096 x))) = ?h6 xa m
 3. \<And>x. replicateHider 4096 0 = foldl (@) [] (map (?h6 x) [0..<1024]) proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<forall>m. m < 1024 \<and> 4 \<le> length (drop (4 * m) (heap_list xa 4096 x)) \<longrightarrow> access_ti_pair (DTPair (adjust_ti (typ_info_t TYPE(32 word)) (\<lambda>x. x.[m]) (\<lambda>x f. Arrays.update f m x)) (replicate m CHR ''1'')) (ARRAY _. 0) (take 4 (drop (4 * m) (heap_list xa 4096 x))) = ?h6 xa m
 2. \<And>x. replicateHider 4096 0 = foldl (@) [] (map (?h6 x) [0..<1024]) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<forall>m. m < 1024 \<and> 4 \<le> 4096 - 4 * m \<longrightarrow> [0, 0, 0, 0] = ?h6 x m
 2. \<And>x. replicateHider 4096 0 = foldl (@) [] (map (?h6 x) [0..<1024]) proof (prove)
goal (1 subgoal):
 1. \<And>x. replicateHider 4096 0 = foldl (@) [] (map (\<lambda>m. [0, 0, 0, 0]) [0..<1024]) proof (prove)
goal:
No subgoals!