kings-crown/FVELER_Isabelle huggingface dataset:
theory Retype_C

lemma region_actually_is_bytes_retyp_disjoint:
  "{ptr ..+ sz} \<inter> {ptr_val (p :: 'a ptr)..+n * size_of TYPE('a :: mem_type)} = {}
    \<Longrightarrow> region_actually_is_bytes' ptr sz htd
    \<Longrightarrow> region_actually_is_bytes' ptr sz (ptr_retyps_gen n p arr htd)" apply (clarsimp simp: region_actually_is_bytes'_def del: impI) apply (subst ptr_retyps_gen_out) apply blast apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>{ptr..+sz} \<inter> {ptr_val p..+n * size_of TYPE('a)} = {}; region_actually_is_bytes' ptr sz htd\<rbrakk> \<Longrightarrow> region_actually_is_bytes' ptr sz (ptr_retyps_gen n p arr htd) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>{ptr..+sz} \<inter> {ptr_val p..+n * size_of TYPE('a)} = {}; \<forall>x\<in>{ptr..+sz}. htd x = (True, [0 \<mapsto> (typ_uinfo_t TYPE(8 word), True)]); x \<in> {ptr..+sz}\<rbrakk> \<Longrightarrow> ptr_retyps_gen n p arr htd x = (True, [0 \<mapsto> (typ_uinfo_t TYPE(8 word), True)]) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>{ptr..+sz} \<inter> {ptr_val p..+n * size_of TYPE('a)} = {}; \<forall>x\<in>{ptr..+sz}. htd x = (True, [0 \<mapsto> (typ_uinfo_t TYPE(8 word), True)]); x \<in> {ptr..+sz}\<rbrakk> \<Longrightarrow> x \<notin> {ptr_val p..+n * size_of TYPE('a)}
 2. \<And>x. \<lbrakk>{ptr..+sz} \<inter> {ptr_val p..+n * size_of TYPE('a)} = {}; \<forall>x\<in>{ptr..+sz}. htd x = (True, [0 \<mapsto> (typ_uinfo_t TYPE(8 word), True)]); x \<in> {ptr..+sz}\<rbrakk> \<Longrightarrow> htd x = (True, [0 \<mapsto> (typ_uinfo_t TYPE(8 word), True)]) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>{ptr..+sz} \<inter> {ptr_val p..+n * size_of TYPE('a)} = {}; \<forall>x\<in>{ptr..+sz}. htd x = (True, [0 \<mapsto> (typ_uinfo_t TYPE(8 word), True)]); x \<in> {ptr..+sz}\<rbrakk> \<Longrightarrow> htd x = (True, [0 \<mapsto> (typ_uinfo_t TYPE(8 word), True)]) proof (prove)
goal:
No subgoals!
theory Retype_C

lemma intvl_plus_unat_eq:
  "p \<le> p + x - 1 \<Longrightarrow> x \<noteq> 0
    \<Longrightarrow> {p ..+ unat x} = {p .. p + x - 1}" apply (subst upto_intvl_eq', simp_all add: unat_eq_0 field_simps) apply (rule order_less_imp_le, simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<le> p + x - 1; x \<noteq> 0\<rbrakk> \<Longrightarrow> {p..+unat x} = {p..p + x - 1} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<le> p + x - 1; x \<noteq> 0\<rbrakk> \<Longrightarrow> unat x \<le> 2 ^ LENGTH('a) proof (prove)
goal:
No subgoals!
theory Retype_C

lemma getCTE_pre_cte_at:
  "\<lbrace>\<lambda>s. \<not> cte_at' p s \<rbrace> getCTE p \<lbrace> \<lambda>_ _. False \<rbrace>" apply (wp getCTE_wp) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<not> cte_wp_at' (\<lambda>_. True) p s\<rbrace> getCTE p \<lbrace>\<lambda>_ _. False\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<not> cte_wp_at' (\<lambda>_. True) p s \<Longrightarrow> cte_wp_at' (\<lambda>_. True) p s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) p s \<and> False) proof (prove)
goal:
No subgoals!
theory Retype_C

lemma byte_regions_unmodified_refl[iff]:
  "byte_regions_unmodified hrs hrs" by (simp add: byte_regions_unmodified_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. byte_regions_unmodified hrs hrs
theory Retype_C

lemma byte_regions_unmodified_trans:
  "byte_regions_unmodified hrs hrs'
    \<Longrightarrow> byte_regions_unmodified hrs' hrs''
    \<Longrightarrow> hrs_htd hrs' = hrs_htd hrs
    \<Longrightarrow> byte_regions_unmodified hrs hrs''" by (simp add: byte_regions_unmodified_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>byte_regions_unmodified hrs hrs'; byte_regions_unmodified hrs' hrs''; hrs_htd hrs' = hrs_htd hrs\<rbrakk> \<Longrightarrow> byte_regions_unmodified hrs hrs''
theory Retype_C

lemma byte_regions_unmodified_hrs_htd_update[iff]:
  "byte_regions_unmodified
      (hrs_htd_update h hrs) hrs" by (clarsimp simp: byte_regions_unmodified_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. byte_regions_unmodified (hrs_htd_update h hrs) hrs
theory Retype_C

lemma byte_regions_unmodified_flip:
  "byte_regions_unmodified (hrs_htd_update (\<lambda>_. hrs_htd hrs) hrs') hrs
    \<Longrightarrow> byte_regions_unmodified hrs hrs'" by (simp add: byte_regions_unmodified_def hrs_htd_update)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. byte_regions_unmodified (hrs_htd_update (\<lambda>_. hrs_htd hrs) hrs') hrs \<Longrightarrow> byte_regions_unmodified hrs hrs'
theory Retype_C

lemma byte_regions_unmodified_region_is_bytes:
  "byte_regions_unmodified hrs hrs'
    \<Longrightarrow> region_actually_is_bytes' y n (hrs_htd hrs)
    \<Longrightarrow> x \<in> {y ..+ n}
    \<Longrightarrow> hrs_mem hrs' x = hrs_mem hrs x" apply (clarsimp simp: byte_regions_unmodified_def imp_conjL[symmetric]) apply (drule spec, erule mp) apply (clarsimp simp: region_actually_is_bytes'_def) apply (drule(1) bspec, simp split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>byte_regions_unmodified hrs hrs'; region_actually_is_bytes' y n (hrs_htd hrs); x \<in> {y..+n}\<rbrakk> \<Longrightarrow> hrs_mem hrs' x = hrs_mem hrs x proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x. (\<forall>n td. (\<exists>b. snd (hrs_htd hrs x) n = Some (td, b)) \<longrightarrow> td = typ_uinfo_t TYPE(8 word)) \<and> (\<exists>a b. snd (hrs_htd hrs x) 0 = Some (a, b)) \<longrightarrow> hrs_mem hrs' x = hrs_mem hrs x; region_actually_is_bytes' y n (hrs_htd hrs); x \<in> {y..+n}\<rbrakk> \<Longrightarrow> hrs_mem hrs' x = hrs_mem hrs x proof (prove)
goal (1 subgoal):
 1. \<lbrakk>region_actually_is_bytes' y n (hrs_htd hrs); x \<in> {y..+n}\<rbrakk> \<Longrightarrow> (\<forall>n td. (\<exists>b. snd (hrs_htd hrs x) n = Some (td, b)) \<longrightarrow> td = typ_uinfo_t TYPE(8 word)) \<and> (\<exists>a b. snd (hrs_htd hrs x) 0 = Some (a, b)) proof (prove)
goal (1 subgoal):
 1. \<And>na td b. \<lbrakk>\<forall>x\<in>{y..+n}. hrs_htd hrs x = (True, [0 \<mapsto> (typ_uinfo_t TYPE(8 word), True)]); x \<in> {y..+n}; (if na = 0 then Some (typ_uinfo_t TYPE(8 word), True) else None) = Some (td, b)\<rbrakk> \<Longrightarrow> td = typ_uinfo_t TYPE(8 word) proof (prove)
goal:
No subgoals!
theory Retype_C

lemma mdb_node_get_mdbNext_spec:
  "\<forall>s. \<Gamma> \<turnstile>\<^bsub>/UNIV\<^esub> {s} Call mdb_node_get_mdbNext_'proc {t. i_' t = i_' s}" apply (rule allI) apply (hoare_rule HoarePartial.ProcNoRec1) apply vcg apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} Call mdb_node_get_mdbNext_'proc \<lbrace>\<acute>i = \<^bsup>s\<^esup>i\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} Call mdb_node_get_mdbNext_'proc \<lbrace>\<acute>i = \<^bsup>s\<^esup>i\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} TRY
  lvar_nondet_init ret_' ret_'_update;;
Guard ShiftError \<lbrace>0 \<le>s 0\<rbrace> (Guard ShiftError \<lbrace>0 <s 0x20\<rbrace> (Guard ArrayBounds \<lbrace>1 <s 2\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s 1\<rbrace> (\<acute>ret :== mdb_node_C.words_C \<acute>mdb_node.[unat 1] && 0xFFFFFFF8 << unat 0))));;
\<acute>ret__int :== (if 0 \<noteq> 0 then 1 else 0);;
IF \<acute>ret__int \<noteq> 0 THEN
  Guard ShiftError \<lbrace>0 \<le>s 0x1F\<rbrace> (Guard ShiftError \<lbrace>0x1F <s 0x20\<rbrace> (\<acute>ret__int :== (if \<acute>ret && (1 << unat 0x1F) \<noteq> 0 then 1 else 0)))
FI;;
IF \<not> \<not> \<acute>ret__int \<noteq> 0 THEN
  \<acute>ret :== \<acute>ret || SCAST(32 signed \<rightarrow> 32) 0
FI;;
return_C ret__unsigned_'_update ret_';;
Guard DontReach {} SKIP
CATCH SKIP
END \<lbrace>\<acute>i = \<^bsup>s\<^esup>i\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>mdb_node i. 0 \<le>s 0 \<longrightarrow> 0 <s 0x20 \<longrightarrow> 1 <s 2 \<longrightarrow> 0 \<le>s 1 \<longrightarrow> ((if False then 1 else 0) \<noteq> 0 \<longrightarrow> 0 \<le>s 0x1F \<longrightarrow> 0x1F <s 0x20 \<longrightarrow> ((if (mdb_node_C.words_C mdb_node.[unat 1] && 0xFFFFFFF8 << unat 0) && (1 << unat 0x1F) \<noteq> 0 then 1 else 0) \<noteq> 0 \<longrightarrow> i = i) \<and> ((if (mdb_node_C.words_C mdb_node.[unat 1] && 0xFFFFFFF8 << unat 0) && (1 << unat 0x1F) \<noteq> 0 then 1 else 0) = 0 \<longrightarrow> i = i)) \<and> ((if False then 1 else 0) = 0 \<longrightarrow> i = i) proof (prove)
goal:
No subgoals!
theory Retype_C

lemma mdb_node_new_spec:
  "\<forall>s. \<Gamma> \<turnstile>\<^bsub>/UNIV\<^esub> {s} Call mdb_node_new_'proc {t. i_' t = i_' s}" apply (rule allI) apply (hoare_rule HoarePartial.ProcNoRec1) apply vcg apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} Call mdb_node_new_'proc \<lbrace>\<acute>i = \<^bsup>s\<^esup>i\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} Call mdb_node_new_'proc \<lbrace>\<acute>i = \<^bsup>s\<^esup>i\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} TRY
  lvar_nondet_init mdb_node_' mdb_node_'_update;;
SKIP;;
SKIP;;
SKIP;;
SKIP;;
Guard ArrayBounds \<lbrace>0 <s 2\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s 0\<rbrace> (Guard ShiftError \<lbrace>0 \<le>s 0\<rbrace> (Guard ShiftError \<lbrace>0 <s 0x20\<rbrace> (\<acute>mdb_node :== mdb_node_C.words_C_update (\<lambda>_. Arrays.update (mdb_node_C.words_C \<acute>mdb_node) (unat 0) (SCAST(32 signed \<rightarrow> 32) 0 || (\<acute>mdbPrev && 0xFFFFFFF8 >> unat 0))) \<acute>mdb_node))));;
Guard ArrayBounds \<lbrace>1 <s 2\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s 1\<rbrace> (Guard ShiftError \<lbrace>0 \<le>s 0\<rbrace> (Guard ShiftError \<lbrace>0 <s 0x20\<rbrace> (Guard ShiftError \<lbrace>0 \<le>s 1\<rbrace> (Guard ShiftError \<lbrace>1 <s 0x20\<rbrace> (Guard ShiftError \<lbrace>0 \<le>s 0\<rbrace> (Guard ShiftError \<lbrace>0 <s 0x20\<rbrace> (\<acute>mdb_node :== mdb_node_C.words_C_update (\<lambda>_. Arrays.update (mdb_node_C.words_C \<acute>mdb_node) (unat 1) (((SCAST(32 signed \<rightarrow> 32) 0 || (\<acute>mdbNext && 0xFFFFFFF8 >> unat 0)) || (\<acute>mdbRevocable && 1 << unat 1)) || (\<acute>mdbFirstBadged && 1 << unat 0))) \<acute>mdb_node))))))));;
return_C ret__struct_mdb_node_C_'_update mdb_node_';;
Guard DontReach {} SKIP
CATCH SKIP
END \<lbrace>\<acute>i = \<^bsup>s\<^esup>i\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>i. 0 <s 2 \<longrightarrow> 0 \<le>s 0 \<longrightarrow> 0 <s 0x20 \<longrightarrow> 1 <s 2 \<longrightarrow> 0 \<le>s 1 \<longrightarrow> 1 <s 0x20 \<longrightarrow> i = i proof (prove)
goal:
No subgoals!
theory Retype_C

lemma mdb_node_ptr_set_mdbPrev_spec:
  "\<forall>s. \<Gamma> \<turnstile>\<^bsub>/UNIV\<^esub> {s} Call mdb_node_ptr_set_mdbPrev_'proc {t. i_' t = i_' s}" apply (rule allI) apply (hoare_rule HoarePartial.ProcNoRec1) apply vcg apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} Call mdb_node_ptr_set_mdbPrev_'proc \<lbrace>\<acute>i = \<^bsup>s\<^esup>i\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} Call mdb_node_ptr_set_mdbPrev_'proc \<lbrace>\<acute>i = \<^bsup>s\<^esup>i\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} TRY
  SKIP;;
Guard ArrayBounds \<lbrace>0 <s 2\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s 0\<rbrace> (Guard C_Guard {s. s \<Turnstile>\<^sub>c mdb_node_ptr_' s} (Guard ArrayBounds \<lbrace>0 <s 2\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s 0\<rbrace> (Guard C_Guard {s. s \<Turnstile>\<^sub>c mdb_node_ptr_' s} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word[2]) &(\<acute>mdb_node_ptr\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem \<acute>t_hrs) (PTR(32 word[2]) &(\<acute>mdb_node_ptr\<rightarrow>[''words_C'']))) (unat 0) (h_val (hrs_mem \<acute>t_hrs) (PTR(32 word[2]) &(\<acute>mdb_node_ptr\<rightarrow>[''words_C''])).[unat 0] && ~~ 0xFFFFFFF8))))))))));;
Guard ArrayBounds \<lbrace>0 <s 2\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s 0\<rbrace> (Guard C_Guard {s. s \<Turnstile>\<^sub>c mdb_node_ptr_' s} (Guard ShiftError \<lbrace>0 \<le>s 0\<rbrace> (Guard ShiftError \<lbrace>0 <s 0x20\<rbrace> (Guard ArrayBounds \<lbrace>0 <s 2\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s 0\<rbrace> (Guard C_Guard {s. s \<Turnstile>\<^sub>c mdb_node_ptr_' s} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word[2]) &(\<acute>mdb_node_ptr\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem \<acute>t_hrs) (PTR(32 word[2]) &(\<acute>mdb_node_ptr\<rightarrow>[''words_C'']))) (unat 0) (h_val (hrs_mem \<acute>t_hrs) (PTR(32 word[2]) &(\<acute>mdb_node_ptr\<rightarrow>[''words_C''])).[unat 0] || (\<acute>v32 >> unat 0) && 0xFFFFFFF8))))))))))))
CATCH SKIP
END \<lbrace>\<acute>i = \<^bsup>s\<^esup>i\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>t_hrs mdb_node_ptr i. 0 <s 2 \<longrightarrow> 0 \<le>s 0 \<longrightarrow> hrs_htd t_hrs \<Turnstile>\<^sub>t mdb_node_ptr \<longrightarrow> hrs_htd (hrs_mem_update (heap_update (PTR(32 word[2]) &(mdb_node_ptr\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem t_hrs) (PTR(32 word[2]) &(mdb_node_ptr\<rightarrow>[''words_C'']))) (unat 0) (h_val (hrs_mem t_hrs) (PTR(32 word[2]) &(mdb_node_ptr\<rightarrow>[''words_C''])).[unat 0] && ~~ 0xFFFFFFF8))) t_hrs) \<Turnstile>\<^sub>t mdb_node_ptr \<longrightarrow> 0 <s 0x20 \<longrightarrow> i = i proof (prove)
goal:
No subgoals!
theory Retype_C

lemma mdb_node_ptr_set_mdbNext_spec:
  "\<forall>s. \<Gamma> \<turnstile>\<^bsub>/UNIV\<^esub> {s} Call mdb_node_ptr_set_mdbNext_'proc {t. i_' t = i_' s}" apply (rule allI) apply (hoare_rule HoarePartial.ProcNoRec1) apply vcg apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} Call mdb_node_ptr_set_mdbNext_'proc \<lbrace>\<acute>i = \<^bsup>s\<^esup>i\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} Call mdb_node_ptr_set_mdbNext_'proc \<lbrace>\<acute>i = \<^bsup>s\<^esup>i\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} TRY
  SKIP;;
Guard ArrayBounds \<lbrace>1 <s 2\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s 1\<rbrace> (Guard C_Guard {s. s \<Turnstile>\<^sub>c mdb_node_ptr_' s} (Guard ArrayBounds \<lbrace>1 <s 2\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s 1\<rbrace> (Guard C_Guard {s. s \<Turnstile>\<^sub>c mdb_node_ptr_' s} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word[2]) &(\<acute>mdb_node_ptr\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem \<acute>t_hrs) (PTR(32 word[2]) &(\<acute>mdb_node_ptr\<rightarrow>[''words_C'']))) (unat 1) (h_val (hrs_mem \<acute>t_hrs) (PTR(32 word[2]) &(\<acute>mdb_node_ptr\<rightarrow>[''words_C''])).[unat 1] && ~~ 0xFFFFFFF8))))))))));;
Guard ArrayBounds \<lbrace>1 <s 2\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s 1\<rbrace> (Guard C_Guard {s. s \<Turnstile>\<^sub>c mdb_node_ptr_' s} (Guard ShiftError \<lbrace>0 \<le>s 0\<rbrace> (Guard ShiftError \<lbrace>0 <s 0x20\<rbrace> (Guard ArrayBounds \<lbrace>1 <s 2\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s 1\<rbrace> (Guard C_Guard {s. s \<Turnstile>\<^sub>c mdb_node_ptr_' s} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word[2]) &(\<acute>mdb_node_ptr\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem \<acute>t_hrs) (PTR(32 word[2]) &(\<acute>mdb_node_ptr\<rightarrow>[''words_C'']))) (unat 1) (h_val (hrs_mem \<acute>t_hrs) (PTR(32 word[2]) &(\<acute>mdb_node_ptr\<rightarrow>[''words_C''])).[unat 1] || (\<acute>v32 >> unat 0) && 0xFFFFFFF8))))))))))))
CATCH SKIP
END \<lbrace>\<acute>i = \<^bsup>s\<^esup>i\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>t_hrs mdb_node_ptr i. 1 <s 2 \<longrightarrow> 0 \<le>s 1 \<longrightarrow> hrs_htd t_hrs \<Turnstile>\<^sub>t mdb_node_ptr \<longrightarrow> hrs_htd (hrs_mem_update (heap_update (PTR(32 word[2]) &(mdb_node_ptr\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem t_hrs) (PTR(32 word[2]) &(mdb_node_ptr\<rightarrow>[''words_C'']))) (unat 1) (h_val (hrs_mem t_hrs) (PTR(32 word[2]) &(mdb_node_ptr\<rightarrow>[''words_C''])).[unat 1] && ~~ 0xFFFFFFF8))) t_hrs) \<Turnstile>\<^sub>t mdb_node_ptr \<longrightarrow> 0 \<le>s 0 \<longrightarrow> 0 <s 0x20 \<longrightarrow> i = i proof (prove)
goal:
No subgoals!
theory Retype_C

lemma insertNewCap_spec:
  "\<forall>s. \<Gamma> \<turnstile>\<^bsub>/UNIV\<^esub> {s} Call insertNewCap_'proc {t. i_' t = i_' s}" apply vcg apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} Call insertNewCap_'proc \<lbrace>\<acute>i = \<^bsup>s\<^esup>i\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>t_hrs parent slot cap i. hrs_htd t_hrs \<Turnstile>\<^sub>t parent \<longrightarrow> (\<forall>ret__unsigned ia. ia = i \<longrightarrow> hrs_htd t_hrs \<Turnstile>\<^sub>t slot \<longrightarrow> (\<forall>ret__struct_mdb_node_C ia. ia = i \<longrightarrow> hrs_htd (hrs_mem_update (heap_update (cap_Ptr &(slot\<rightarrow>[''cap_C''])) cap) t_hrs) \<Turnstile>\<^sub>t slot \<longrightarrow> (cte_Ptr (UCAST(32 \<rightarrow> 32) ret__unsigned) \<noteq> NULL \<longrightarrow> hrs_htd (hrs_mem_update (heap_update (mdb_Ptr &(slot\<rightarrow>[''cteMDBNode_C''])) ret__struct_mdb_node_C) (hrs_mem_update (heap_update (cap_Ptr &(slot\<rightarrow>[''cap_C''])) cap) t_hrs)) \<Turnstile>\<^sub>t cte_Ptr (UCAST(32 \<rightarrow> 32) ret__unsigned) \<longrightarrow> (\<forall>t_hrs ia. ia = i \<longrightarrow> hrs_htd t_hrs \<Turnstile>\<^sub>t parent \<longrightarrow> (\<forall>ia. ia = i \<longrightarrow> i = i))) \<and> (cte_Ptr (UCAST(32 \<rightarrow> 32) ret__unsigned) = NULL \<longrightarrow> hrs_htd (hrs_mem_update (heap_update (mdb_Ptr &(slot\<rightarrow>[''cteMDBNode_C''])) ret__struct_mdb_node_C) (hrs_mem_update (heap_update (cap_Ptr &(slot\<rightarrow>[''cap_C''])) cap) t_hrs)) \<Turnstile>\<^sub>t parent \<longrightarrow> (\<forall>ia. ia = i \<longrightarrow> i = i)))) proof (prove)
goal:
No subgoals!
theory Retype_C

lemma ccorres_fail:
  "ccorres r xf \<top> UNIV hs fail c" apply (rule ccorresI') apply (simp add: fail_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres r xf (\<lambda>_. True) UNIV hs fail c proof (prove)
goal (1 subgoal):
 1. \<And>s s' n z. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> UNIV; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (fail s)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst (fail s). (t, t') \<in> rf_sr \<and> unif_rrel (n = length hs) r xf r xf ra t') proof (prove)
goal:
No subgoals!
theory Retype_C

lemma object_type_from_H_toAPIType_simps:
  "(object_type_from_H tp = scast seL4_UntypedObject) = (toAPIType tp = Some ArchTypes_H.apiobject_type.Untyped)"
  "(object_type_from_H tp = scast seL4_TCBObject) = (toAPIType tp = Some ArchTypes_H.apiobject_type.TCBObject)"
  "(object_type_from_H tp = scast seL4_EndpointObject) = (toAPIType tp = Some ArchTypes_H.apiobject_type.EndpointObject)"
  "(object_type_from_H tp = scast seL4_NotificationObject) = (toAPIType tp = Some ArchTypes_H.apiobject_type.NotificationObject)"
  "(object_type_from_H tp = scast seL4_CapTableObject) = (toAPIType tp = Some ArchTypes_H.apiobject_type.CapTableObject)"
  "(object_type_from_H tp = scast seL4_ARM_SmallPageObject) = (tp = ARM_H.SmallPageObject)"
  "(object_type_from_H tp = scast seL4_ARM_LargePageObject) = (tp = ARM_H.LargePageObject)"
  "(object_type_from_H tp = scast seL4_ARM_SectionObject) = (tp = ARM_H.SectionObject)"
  "(object_type_from_H tp = scast seL4_ARM_SuperSectionObject) = (tp = ARM_H.SuperSectionObject)"
  "(object_type_from_H tp = scast seL4_ARM_PageTableObject) = (tp = ARM_H.PageTableObject)"
  "(object_type_from_H tp = scast seL4_ARM_PageDirectoryObject) = (tp = ARM_H.PageDirectoryObject)" by (auto simp: toAPIType_def
                 object_type_from_H_def "StrictC'_object_defs" api_object_defs
          split: object_type.splits ArchTypes_H.apiobject_type.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (((object_type_from_H tp = SCAST(32 signed \<rightarrow> 32) seL4_UntypedObject) = (toAPIType tp = Some ArchTypes_H.apiobject_type.Untyped) &&& (object_type_from_H tp = SCAST(32 signed \<rightarrow> 32) seL4_TCBObject) = (toAPIType tp = Some ArchTypes_H.apiobject_type.TCBObject)) &&& (object_type_from_H tp = SCAST(32 signed \<rightarrow> 32) seL4_EndpointObject) = (toAPIType tp = Some ArchTypes_H.apiobject_type.EndpointObject) &&& (object_type_from_H tp = SCAST(32 signed \<rightarrow> 32) seL4_NotificationObject) = (toAPIType tp = Some ArchTypes_H.apiobject_type.NotificationObject) &&& (object_type_from_H tp = SCAST(32 signed \<rightarrow> 32) seL4_CapTableObject) = (toAPIType tp = Some ArchTypes_H.apiobject_type.CapTableObject)) &&& ((object_type_from_H tp = SCAST(32 signed \<rightarrow> 32) seL4_ARM_SmallPageObject) = (tp = object_type.SmallPageObject) &&& (object_type_from_H tp = SCAST(32 signed \<rightarrow> 32) seL4_ARM_LargePageObject) = (tp = object_type.LargePageObject) &&& (object_type_from_H tp = SCAST(32 signed \<rightarrow> 32) seL4_ARM_SectionObject) = (tp = object_type.SectionObject)) &&& (object_type_from_H tp = SCAST(32 signed \<rightarrow> 32) seL4_ARM_SuperSectionObject) = (tp = object_type.SuperSectionObject) &&& (object_type_from_H tp = SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageTableObject) = (tp = object_type.PageTableObject) &&& (object_type_from_H tp = SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageDirectoryObject) = (tp = object_type.PageDirectoryObject)
theory Retype_C

lemma option_noneI: "\<lbrakk> \<And>x. a = Some x \<Longrightarrow> False \<rbrakk> \<Longrightarrow> a = None" apply (case_tac a) apply clarsimp apply atomize apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x. a = Some x \<Longrightarrow> False) \<Longrightarrow> a = None proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>x. a = Some x \<Longrightarrow> False; a = None\<rbrakk> \<Longrightarrow> a = None
 2. \<And>aa. \<lbrakk>\<And>x. a = Some x \<Longrightarrow> False; a = Some aa\<rbrakk> \<Longrightarrow> a = None proof (prove)
goal (1 subgoal):
 1. \<And>aa. \<lbrakk>\<And>x. a = Some x \<Longrightarrow> False; a = Some aa\<rbrakk> \<Longrightarrow> a = None proof (prove)
goal (1 subgoal):
 1. \<And>aa. \<lbrakk>\<forall>x. a = Some x \<longrightarrow> False; a = Some aa\<rbrakk> \<Longrightarrow> a = None proof (prove)
goal:
No subgoals!
theory Retype_C

lemma dom_tcb_cte_cases_iff:
  "(x \<in> dom tcb_cte_cases) = (\<exists>y < 5. unat x = y * 16)" unfolding tcb_cte_cases_def by (auto simp: unat_arith_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x \<in> dom tcb_cte_cases) = (\<exists>y<5. unat x = y * 16) proof (prove)
goal (1 subgoal):
 1. (x \<in> dom [0 \<mapsto> (tcb.tcbCTable, tcbCTable_update), 0x10 \<mapsto> (tcb.tcbVTable, tcbVTable_update), 0x20 \<mapsto> (tcb.tcbReply, tcbReply_update), 0x30 \<mapsto> (tcb.tcbCaller, tcbCaller_update), 0x40 \<mapsto> (tcbIPCBufferFrame, tcbIPCBufferFrame_update)]) = (\<exists>y<5. unat x = y * 16)
theory Retype_C

lemma update_ti_t_ptr_0s:
  "update_ti_t (typ_info_t TYPE('a :: c_type ptr)) [0,0,0,0] X = NULL" apply (simp add: typ_info_ptr word_rcat_def bin_rcat_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. update_ti_t (typ_info_t TYPE('a ptr)) [0, 0, 0, 0] X = NULL proof (prove)
goal:
No subgoals!