kings-crown/FVELER_Isabelle huggingface dataset:
theory shared_types_proofs

lemma (in kernel_all_substitute) seL4_CapRights_get_capAllowWrite_spec:
  "\<forall>s. \<Gamma> \<turnstile> {s}
       \<acute>ret__unsigned :== PROC seL4_CapRights_get_capAllowWrite(\<acute>seL4_CapRights)
       \<lbrace>\<acute>ret__unsigned = seL4_CapRights_CL.capAllowWrite_CL (seL4_CapRights_lift \<^bsup>s\<^esup>seL4_CapRights)\<rbrace>" apply (rule allI, rule conseqPre, vcg) apply clarsimp apply (simp add: seL4_CapRights_lift_def mask_shift_simps guard_simps) apply (simp add: sign_extend_def' mask_def nth_is_and_neq_0 word_bw_assocs
                   shift_over_ao_dists word_oa_dist word_and_max_simps)? done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> {s} Call seL4_CapRights_get_capAllowWrite_'proc \<lbrace>\<acute>ret__unsigned = capAllowWrite_CL (seL4_CapRights_lift \<^bsup>s\<^esup>seL4_CapRights)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. {s} \<subseteq> \<lbrace>\<forall>v. 0 \<le>s 0 \<and> 0 <s 0x20 \<and> 0 <s 1 \<and> 0 \<le>s 0 \<and> ((if False then 1 else 0) \<noteq> 0 \<longrightarrow> 0 \<le>s 0x1F \<and> 0x1F <s 0x20 \<and> ((if (seL4_CapRights_C.words_C \<acute>seL4_CapRights.[unat 0] && 1 >> unat 0) && (1 << unat 0x1F) \<noteq> 0 then 1 else 0) \<noteq> 0 \<longrightarrow> (seL4_CapRights_C.words_C \<acute>seL4_CapRights.[unat 0] && 1 >> unat 0) || SCAST(32 signed \<rightarrow> 32) 0 = capAllowWrite_CL (seL4_CapRights_lift \<^bsup>s\<^esup>seL4_CapRights)) \<and> ((if (seL4_CapRights_C.words_C \<acute>seL4_CapRights.[unat 0] && 1 >> unat 0) && (1 << unat 0x1F) \<noteq> 0 then 1 else 0) = 0 \<longrightarrow> seL4_CapRights_C.words_C \<acute>seL4_CapRights.[unat 0] && 1 >> unat 0 = capAllowWrite_CL (seL4_CapRights_lift \<^bsup>s\<^esup>seL4_CapRights))) \<and> ((if False then 1 else 0) = 0 \<longrightarrow> seL4_CapRights_C.words_C \<acute>seL4_CapRights.[unat 0] && 1 >> unat 0 = capAllowWrite_CL (seL4_CapRights_lift \<^bsup>s\<^esup>seL4_CapRights))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. seL4_CapRights_C.words_C (seL4_CapRights_' s).[0] && 1 = capAllowWrite_CL (seL4_CapRights_lift (seL4_CapRights_' s)) proof (prove)
goal:
No subgoals! proof (prove)
goal:
No subgoals!
theory shared_types_proofs

lemma seL4_MessageInfo_ptr_words_NULL:
  "c_guard (p::seL4_MessageInfo_C ptr) \<Longrightarrow>
   0 < &(p\<rightarrow>[''words_C''])" by (fastforce intro:c_guard_NULL_fl simp:typ_uinfo_t_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. c_guard p \<Longrightarrow> 0 < &(p\<rightarrow>[''words_C''])
theory shared_types_proofs

lemma seL4_MessageInfo_ptr_words_aligned:
  "c_guard (p::seL4_MessageInfo_C ptr) \<Longrightarrow>
   ptr_aligned ((Ptr &(p\<rightarrow>[''words_C'']))::((word32[1]) ptr))" by (fastforce intro:c_guard_ptr_aligned_fl simp:typ_uinfo_t_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. c_guard p \<Longrightarrow> ptr_aligned (PTR(32 word[1]) &(p\<rightarrow>[''words_C'']))
theory shared_types_proofs

lemma seL4_MessageInfo_ptr_words_ptr_safe:
  "ptr_safe (p::seL4_MessageInfo_C ptr) d \<Longrightarrow>
   ptr_safe (Ptr &(p\<rightarrow>[''words_C''])::((word32[1]) ptr)) d" by (fastforce intro:ptr_safe_mono simp:typ_uinfo_t_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ptr_safe p d \<Longrightarrow> ptr_safe (PTR(32 word[1]) &(p\<rightarrow>[''words_C''])) d
theory shared_types_proofs

lemma (in kernel_all_substitute) seL4_MessageInfo_get_label_spec:
  "\<forall>s. \<Gamma> \<turnstile> {s}
       \<acute>ret__unsigned :== PROC seL4_MessageInfo_get_label(\<acute>seL4_MessageInfo)
       \<lbrace>\<acute>ret__unsigned = seL4_MessageInfo_CL.label_CL (seL4_MessageInfo_lift \<^bsup>s\<^esup>seL4_MessageInfo)\<rbrace>" apply (rule allI, rule conseqPre, vcg) apply clarsimp apply (simp add: seL4_MessageInfo_lift_def mask_shift_simps guard_simps) apply (simp add: sign_extend_def' mask_def nth_is_and_neq_0 word_bw_assocs
                   shift_over_ao_dists word_oa_dist word_and_max_simps)? done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> {s} Call seL4_MessageInfo_get_label_'proc \<lbrace>\<acute>ret__unsigned = label_CL (seL4_MessageInfo_lift \<^bsup>s\<^esup>seL4_MessageInfo)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. {s} \<subseteq> \<lbrace>\<forall>v. 0 \<le>s 0xC \<and> 0xC <s 0x20 \<and> 0 <s 1 \<and> 0 \<le>s 0 \<and> ((if False then 1 else 0) \<noteq> 0 \<longrightarrow> 0 \<le>s 0x1F \<and> 0x1F <s 0x20 \<and> ((if (seL4_MessageInfo_C.words_C \<acute>seL4_MessageInfo.[unat 0] && 0xFFFFF000 >> unat 0xC) && (1 << unat 0x1F) \<noteq> 0 then 1 else 0) \<noteq> 0 \<longrightarrow> (seL4_MessageInfo_C.words_C \<acute>seL4_MessageInfo.[unat 0] && 0xFFFFF000 >> unat 0xC) || SCAST(32 signed \<rightarrow> 32) 0 = label_CL (seL4_MessageInfo_lift \<^bsup>s\<^esup>seL4_MessageInfo)) \<and> ((if (seL4_MessageInfo_C.words_C \<acute>seL4_MessageInfo.[unat 0] && 0xFFFFF000 >> unat 0xC) && (1 << unat 0x1F) \<noteq> 0 then 1 else 0) = 0 \<longrightarrow> seL4_MessageInfo_C.words_C \<acute>seL4_MessageInfo.[unat 0] && 0xFFFFF000 >> unat 0xC = label_CL (seL4_MessageInfo_lift \<^bsup>s\<^esup>seL4_MessageInfo))) \<and> ((if False then 1 else 0) = 0 \<longrightarrow> seL4_MessageInfo_C.words_C \<acute>seL4_MessageInfo.[unat 0] && 0xFFFFF000 >> unat 0xC = label_CL (seL4_MessageInfo_lift \<^bsup>s\<^esup>seL4_MessageInfo))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. seL4_MessageInfo_C.words_C (seL4_MessageInfo_' s).[0] && 0xFFFFF000 >> 12 = label_CL (seL4_MessageInfo_lift (seL4_MessageInfo_' s)) proof (prove)
goal:
No subgoals! proof (prove)
goal:
No subgoals!
theory shared_types_proofs

lemma (in kernel_all_substitute) seL4_MessageInfo_get_capsUnwrapped_spec:
  "\<forall>s. \<Gamma> \<turnstile> {s}
       \<acute>ret__unsigned :== PROC seL4_MessageInfo_get_capsUnwrapped(\<acute>seL4_MessageInfo)
       \<lbrace>\<acute>ret__unsigned = seL4_MessageInfo_CL.capsUnwrapped_CL (seL4_MessageInfo_lift \<^bsup>s\<^esup>seL4_MessageInfo)\<rbrace>" apply (rule allI, rule conseqPre, vcg) apply clarsimp apply (simp add: seL4_MessageInfo_lift_def mask_shift_simps guard_simps) apply (simp add: sign_extend_def' mask_def nth_is_and_neq_0 word_bw_assocs
                   shift_over_ao_dists word_oa_dist word_and_max_simps)? done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> {s} Call seL4_MessageInfo_get_capsUnwrapped_'proc \<lbrace>\<acute>ret__unsigned = capsUnwrapped_CL (seL4_MessageInfo_lift \<^bsup>s\<^esup>seL4_MessageInfo)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. {s} \<subseteq> \<lbrace>\<forall>v. 0 \<le>s 9 \<and> 9 <s 0x20 \<and> 0 <s 1 \<and> 0 \<le>s 0 \<and> ((if False then 1 else 0) \<noteq> 0 \<longrightarrow> 0 \<le>s 0x1F \<and> 0x1F <s 0x20 \<and> ((if (seL4_MessageInfo_C.words_C \<acute>seL4_MessageInfo.[unat 0] && 0xE00 >> unat 9) && (1 << unat 0x1F) \<noteq> 0 then 1 else 0) \<noteq> 0 \<longrightarrow> (seL4_MessageInfo_C.words_C \<acute>seL4_MessageInfo.[unat 0] && 0xE00 >> unat 9) || SCAST(32 signed \<rightarrow> 32) 0 = capsUnwrapped_CL (seL4_MessageInfo_lift \<^bsup>s\<^esup>seL4_MessageInfo)) \<and> ((if (seL4_MessageInfo_C.words_C \<acute>seL4_MessageInfo.[unat 0] && 0xE00 >> unat 9) && (1 << unat 0x1F) \<noteq> 0 then 1 else 0) = 0 \<longrightarrow> seL4_MessageInfo_C.words_C \<acute>seL4_MessageInfo.[unat 0] && 0xE00 >> unat 9 = capsUnwrapped_CL (seL4_MessageInfo_lift \<^bsup>s\<^esup>seL4_MessageInfo))) \<and> ((if False then 1 else 0) = 0 \<longrightarrow> seL4_MessageInfo_C.words_C \<acute>seL4_MessageInfo.[unat 0] && 0xE00 >> unat 9 = capsUnwrapped_CL (seL4_MessageInfo_lift \<^bsup>s\<^esup>seL4_MessageInfo))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. seL4_MessageInfo_C.words_C (seL4_MessageInfo_' s).[0] && 0xE00 >> 9 = capsUnwrapped_CL (seL4_MessageInfo_lift (seL4_MessageInfo_' s)) proof (prove)
goal:
No subgoals! proof (prove)
goal:
No subgoals!
theory shared_types_proofs

lemma (in kernel_all_substitute) seL4_MessageInfo_set_capsUnwrapped_spec:
  "\<forall>s. \<Gamma> \<turnstile> {s}
       \<acute>ret__struct_seL4_MessageInfo_C :== PROC seL4_MessageInfo_set_capsUnwrapped(\<acute>seL4_MessageInfo, \<acute>v32)
       \<lbrace>seL4_MessageInfo_lift \<acute>ret__struct_seL4_MessageInfo_C = seL4_MessageInfo_lift \<^bsup>s\<^esup>seL4_MessageInfo \<lparr> seL4_MessageInfo_CL.capsUnwrapped_CL :=  (\<^bsup>s\<^esup>v32 AND mask 3) \<rparr>\<rbrace>" apply(rule allI, rule conseqPre, vcg) apply (clarsimp simp: guard_simps ucast_id
                        seL4_MessageInfo_lift_def
                        mask_def shift_over_ao_dists
                        multi_shift_simps word_size
                        word_ao_dist word_bw_assocs
                        NOT_eq) apply (simp add: sign_extend_def' mask_def nth_is_and_neq_0 word_bw_assocs
                   shift_over_ao_dists word_and_max_simps)? done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> {s} Call seL4_MessageInfo_set_capsUnwrapped_'proc \<lbrace>seL4_MessageInfo_lift \<acute>ret__struct_seL4_MessageInfo_C = seL4_MessageInfo_lift \<^bsup>s\<^esup>seL4_MessageInfo\<lparr>capsUnwrapped_CL := \<^bsup>s\<^esup>v32 && mask 3\<rparr>\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. {s} \<subseteq> \<lbrace>0 <s 1 \<and> 0 \<le>s 0 \<and> 0 <s 1 \<and> 0 \<le>s 0 \<and> 0 <s 1 \<and> 0 \<le>s 0 \<and> 0 \<le>s 9 \<and> 9 <s 0x20 \<and> 0 <s 1 \<and> 0 \<le>s 0 \<and> seL4_MessageInfo_lift (seL4_MessageInfo_C.words_C_update (\<lambda>v. Arrays.update v (unat 0) (v.[unat 0] || (\<acute>v32 << unat 9) && 0xE00)) (seL4_MessageInfo_C.words_C_update (\<lambda>v. Arrays.update v (unat 0) (v.[unat 0] && ~~ 0xE00)) \<acute>seL4_MessageInfo)) = seL4_MessageInfo_lift \<^bsup>s\<^esup>seL4_MessageInfo\<lparr>capsUnwrapped_CL := \<^bsup>s\<^esup>v32 && mask 3\<rparr>\<rbrace> proof (prove)
goal:
No subgoals! proof (prove)
goal:
No subgoals!
theory shared_types_proofs

lemma (in kernel_all_substitute) seL4_MessageInfo_get_extraCaps_spec:
  "\<forall>s. \<Gamma> \<turnstile> {s}
       \<acute>ret__unsigned :== PROC seL4_MessageInfo_get_extraCaps(\<acute>seL4_MessageInfo)
       \<lbrace>\<acute>ret__unsigned = seL4_MessageInfo_CL.extraCaps_CL (seL4_MessageInfo_lift \<^bsup>s\<^esup>seL4_MessageInfo)\<rbrace>" apply (rule allI, rule conseqPre, vcg) apply clarsimp apply (simp add: seL4_MessageInfo_lift_def mask_shift_simps guard_simps) apply (simp add: sign_extend_def' mask_def nth_is_and_neq_0 word_bw_assocs
                   shift_over_ao_dists word_oa_dist word_and_max_simps)? done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> {s} Call seL4_MessageInfo_get_extraCaps_'proc \<lbrace>\<acute>ret__unsigned = extraCaps_CL (seL4_MessageInfo_lift \<^bsup>s\<^esup>seL4_MessageInfo)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. {s} \<subseteq> \<lbrace>\<forall>v. 0 \<le>s 7 \<and> 7 <s 0x20 \<and> 0 <s 1 \<and> 0 \<le>s 0 \<and> ((if False then 1 else 0) \<noteq> 0 \<longrightarrow> 0 \<le>s 0x1F \<and> 0x1F <s 0x20 \<and> ((if (seL4_MessageInfo_C.words_C \<acute>seL4_MessageInfo.[unat 0] && 0x180 >> unat 7) && (1 << unat 0x1F) \<noteq> 0 then 1 else 0) \<noteq> 0 \<longrightarrow> (seL4_MessageInfo_C.words_C \<acute>seL4_MessageInfo.[unat 0] && 0x180 >> unat 7) || SCAST(32 signed \<rightarrow> 32) 0 = extraCaps_CL (seL4_MessageInfo_lift \<^bsup>s\<^esup>seL4_MessageInfo)) \<and> ((if (seL4_MessageInfo_C.words_C \<acute>seL4_MessageInfo.[unat 0] && 0x180 >> unat 7) && (1 << unat 0x1F) \<noteq> 0 then 1 else 0) = 0 \<longrightarrow> seL4_MessageInfo_C.words_C \<acute>seL4_MessageInfo.[unat 0] && 0x180 >> unat 7 = extraCaps_CL (seL4_MessageInfo_lift \<^bsup>s\<^esup>seL4_MessageInfo))) \<and> ((if False then 1 else 0) = 0 \<longrightarrow> seL4_MessageInfo_C.words_C \<acute>seL4_MessageInfo.[unat 0] && 0x180 >> unat 7 = extraCaps_CL (seL4_MessageInfo_lift \<^bsup>s\<^esup>seL4_MessageInfo))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. seL4_MessageInfo_C.words_C (seL4_MessageInfo_' s).[0] && 0x180 >> 7 = extraCaps_CL (seL4_MessageInfo_lift (seL4_MessageInfo_' s)) proof (prove)
goal:
No subgoals! proof (prove)
goal:
No subgoals!
theory shared_types_proofs

lemma (in kernel_all_substitute) seL4_MessageInfo_set_extraCaps_spec:
  "\<forall>s. \<Gamma> \<turnstile> {s}
       \<acute>ret__struct_seL4_MessageInfo_C :== PROC seL4_MessageInfo_set_extraCaps(\<acute>seL4_MessageInfo, \<acute>v32)
       \<lbrace>seL4_MessageInfo_lift \<acute>ret__struct_seL4_MessageInfo_C = seL4_MessageInfo_lift \<^bsup>s\<^esup>seL4_MessageInfo \<lparr> seL4_MessageInfo_CL.extraCaps_CL :=  (\<^bsup>s\<^esup>v32 AND mask 2) \<rparr>\<rbrace>" apply(rule allI, rule conseqPre, vcg) apply (clarsimp simp: guard_simps ucast_id
                        seL4_MessageInfo_lift_def
                        mask_def shift_over_ao_dists
                        multi_shift_simps word_size
                        word_ao_dist word_bw_assocs
                        NOT_eq) apply (simp add: sign_extend_def' mask_def nth_is_and_neq_0 word_bw_assocs
                   shift_over_ao_dists word_and_max_simps)? done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> {s} Call seL4_MessageInfo_set_extraCaps_'proc \<lbrace>seL4_MessageInfo_lift \<acute>ret__struct_seL4_MessageInfo_C = seL4_MessageInfo_lift \<^bsup>s\<^esup>seL4_MessageInfo\<lparr>extraCaps_CL := \<^bsup>s\<^esup>v32 && mask 2\<rparr>\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. {s} \<subseteq> \<lbrace>0 <s 1 \<and> 0 \<le>s 0 \<and> 0 <s 1 \<and> 0 \<le>s 0 \<and> 0 <s 1 \<and> 0 \<le>s 0 \<and> 0 \<le>s 7 \<and> 7 <s 0x20 \<and> 0 <s 1 \<and> 0 \<le>s 0 \<and> seL4_MessageInfo_lift (seL4_MessageInfo_C.words_C_update (\<lambda>v. Arrays.update v (unat 0) (v.[unat 0] || (\<acute>v32 << unat 7) && 0x180)) (seL4_MessageInfo_C.words_C_update (\<lambda>v. Arrays.update v (unat 0) (v.[unat 0] && ~~ 0x180)) \<acute>seL4_MessageInfo)) = seL4_MessageInfo_lift \<^bsup>s\<^esup>seL4_MessageInfo\<lparr>extraCaps_CL := \<^bsup>s\<^esup>v32 && mask 2\<rparr>\<rbrace> proof (prove)
goal:
No subgoals! proof (prove)
goal:
No subgoals!
theory shared_types_proofs

lemma (in kernel_all_substitute) seL4_MessageInfo_get_length_spec:
  "\<forall>s. \<Gamma> \<turnstile> {s}
       \<acute>ret__unsigned :== PROC seL4_MessageInfo_get_length(\<acute>seL4_MessageInfo)
       \<lbrace>\<acute>ret__unsigned = seL4_MessageInfo_CL.length_CL (seL4_MessageInfo_lift \<^bsup>s\<^esup>seL4_MessageInfo)\<rbrace>" apply (rule allI, rule conseqPre, vcg) apply clarsimp apply (simp add: seL4_MessageInfo_lift_def mask_shift_simps guard_simps) apply (simp add: sign_extend_def' mask_def nth_is_and_neq_0 word_bw_assocs
                   shift_over_ao_dists word_oa_dist word_and_max_simps)? done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> {s} Call seL4_MessageInfo_get_length_'proc \<lbrace>\<acute>ret__unsigned = length_CL (seL4_MessageInfo_lift \<^bsup>s\<^esup>seL4_MessageInfo)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. {s} \<subseteq> \<lbrace>\<forall>v. 0 \<le>s 0 \<and> 0 <s 0x20 \<and> 0 <s 1 \<and> 0 \<le>s 0 \<and> ((if False then 1 else 0) \<noteq> 0 \<longrightarrow> 0 \<le>s 0x1F \<and> 0x1F <s 0x20 \<and> ((if (seL4_MessageInfo_C.words_C \<acute>seL4_MessageInfo.[unat 0] && 0x7F >> unat 0) && (1 << unat 0x1F) \<noteq> 0 then 1 else 0) \<noteq> 0 \<longrightarrow> (seL4_MessageInfo_C.words_C \<acute>seL4_MessageInfo.[unat 0] && 0x7F >> unat 0) || SCAST(32 signed \<rightarrow> 32) 0 = length_CL (seL4_MessageInfo_lift \<^bsup>s\<^esup>seL4_MessageInfo)) \<and> ((if (seL4_MessageInfo_C.words_C \<acute>seL4_MessageInfo.[unat 0] && 0x7F >> unat 0) && (1 << unat 0x1F) \<noteq> 0 then 1 else 0) = 0 \<longrightarrow> seL4_MessageInfo_C.words_C \<acute>seL4_MessageInfo.[unat 0] && 0x7F >> unat 0 = length_CL (seL4_MessageInfo_lift \<^bsup>s\<^esup>seL4_MessageInfo))) \<and> ((if False then 1 else 0) = 0 \<longrightarrow> seL4_MessageInfo_C.words_C \<acute>seL4_MessageInfo.[unat 0] && 0x7F >> unat 0 = length_CL (seL4_MessageInfo_lift \<^bsup>s\<^esup>seL4_MessageInfo))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. seL4_MessageInfo_C.words_C (seL4_MessageInfo_' s).[0] && 0x7F = length_CL (seL4_MessageInfo_lift (seL4_MessageInfo_' s)) proof (prove)
goal:
No subgoals! proof (prove)
goal:
No subgoals!
theory shared_types_proofs

lemma (in kernel_all_substitute) seL4_MessageInfo_set_length_spec:
  "\<forall>s. \<Gamma> \<turnstile> {s}
       \<acute>ret__struct_seL4_MessageInfo_C :== PROC seL4_MessageInfo_set_length(\<acute>seL4_MessageInfo, \<acute>v32)
       \<lbrace>seL4_MessageInfo_lift \<acute>ret__struct_seL4_MessageInfo_C = seL4_MessageInfo_lift \<^bsup>s\<^esup>seL4_MessageInfo \<lparr> seL4_MessageInfo_CL.length_CL :=  (\<^bsup>s\<^esup>v32 AND mask 7) \<rparr>\<rbrace>" apply(rule allI, rule conseqPre, vcg) apply (clarsimp simp: guard_simps ucast_id
                        seL4_MessageInfo_lift_def
                        mask_def shift_over_ao_dists
                        multi_shift_simps word_size
                        word_ao_dist word_bw_assocs
                        NOT_eq) apply (simp add: sign_extend_def' mask_def nth_is_and_neq_0 word_bw_assocs
                   shift_over_ao_dists word_and_max_simps)? done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> {s} Call seL4_MessageInfo_set_length_'proc \<lbrace>seL4_MessageInfo_lift \<acute>ret__struct_seL4_MessageInfo_C = seL4_MessageInfo_lift \<^bsup>s\<^esup>seL4_MessageInfo\<lparr>length_CL := \<^bsup>s\<^esup>v32 && mask 7\<rparr>\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. {s} \<subseteq> \<lbrace>0 <s 1 \<and> 0 \<le>s 0 \<and> 0 <s 1 \<and> 0 \<le>s 0 \<and> 0 <s 1 \<and> 0 \<le>s 0 \<and> 0 <s 0x20 \<and> 0 <s 1 \<and> 0 \<le>s 0 \<and> seL4_MessageInfo_lift (seL4_MessageInfo_C.words_C_update (\<lambda>v. Arrays.update v (unat 0) (v.[unat 0] || (\<acute>v32 << unat 0) && 0x7F)) (seL4_MessageInfo_C.words_C_update (\<lambda>v. Arrays.update v (unat 0) (v.[unat 0] && ~~ 0x7F)) \<acute>seL4_MessageInfo)) = seL4_MessageInfo_lift \<^bsup>s\<^esup>seL4_MessageInfo\<lparr>length_CL := \<^bsup>s\<^esup>v32 && mask 7\<rparr>\<rbrace> proof (prove)
goal:
No subgoals! proof (prove)
goal:
No subgoals!
theory Types_D

lemma cap_type_simps [simp]:
  "is_untyped_cap    (UntypedCap dev a a')"
  "is_ep_cap         (EndpointCap b c d)"
  "is_ntfn_cap        (NotificationCap e f g)"
  "is_tcb_cap        (TcbCap h)"
  "is_cnode_cap      (CNodeCap j k l m)"
  "is_asidpool_cap   (AsidPoolCap n p)"
  "is_pd_cap         (PageDirectoryCap r s t)"
  "is_pt_cap         (PageTableCap u v w)"
  "is_frame_cap      (FrameCap dev a1 a2 a3 a4 a5)"
  "is_irqhandler_cap (IrqHandlerCap a6)"
  "cap_type (FrameCap dev obj_id rights sz rs asid) = Some (FrameType sz)" by (clarsimp simp: cap_type_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((is_untyped_cap (UntypedCap dev a a') &&& is_ep_cap (EndpointCap b c d)) &&& is_ntfn_cap (NotificationCap e f g) &&& is_tcb_cap (TcbCap h) &&& is_cnode_cap (CNodeCap j k l m)) &&& (is_asidpool_cap (AsidPoolCap n p) &&& is_pd_cap (PageDirectoryCap r s t) &&& is_pt_cap (PageTableCap u v w)) &&& is_frame_cap (FrameCap dev a1 a2 a3 a4 a5) &&& is_irqhandler_cap (IrqHandlerCap a6) &&& cap_type (FrameCap dev obj_id rights sz rs asid) = Some (FrameType sz)
theory Types_D

lemma cap_type_update_cap_badge [simp]:
  "cap_type (update_cap_badge x cap) = cap_type cap" by (clarsimp simp: update_cap_badge_def cap_type_def split: cdl_cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_type (update_cap_badge x cap) = cap_type cap
theory Types_D

lemma cap_type_update_cap_rights [simp]:
  "cap_type (update_cap_rights x cap) = cap_type cap" by (clarsimp simp: update_cap_rights_def cap_type_def split: cdl_cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_type (update_cap_rights x cap) = cap_type cap
theory Types_D

lemma cap_type_update_mapping_cap_status [simp]:
  "cap_type (update_mapping_cap_status x cap) = cap_type cap" by (clarsimp simp: update_mapping_cap_status_def cap_type_def split: cdl_cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_type (update_mapping_cap_status x cap) = cap_type cap
theory Types_D

lemma cap_type_update_cap_guard [simp]:
  "cap_type (update_cap_guard x cap) = cap_type cap" by (clarsimp simp: update_cap_guard_def cap_type_def split: cdl_cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_type (update_cap_guard x cap) = cap_type cap
theory Types_D

lemma update_cap_guard_size [simp]:
  "cap_type (update_cap_guard_size x cap) = cap_type cap" by (clarsimp simp: update_cap_guard_size_def cap_type_def split: cdl_cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_type (update_cap_guard_size x cap) = cap_type cap
theory CSpace_D

lemma fast_finalise_def2:
  "fast_finalise cap final = do
     assert (can_fast_finalise cap);
     result \<leftarrow> finalise_cap cap final;
     assert (result = (NullCap, NullCap))
   od" unfolding can_fast_finalise_def by (rule finalise_cap.cases[of "(cap,final)"]; simp add: assert_def liftM_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. fast_finalise cap final = do assert (can_fast_finalise cap);
result <- finalise_cap cap final;
assert (result = (NullCap, NullCap))
od proof (prove)
goal (1 subgoal):
 1. fast_finalise cap final = do assert (case cap of NullCap \<Rightarrow> True | EndpointCap r b R \<Rightarrow> True | NotificationCap r b R \<Rightarrow> True | ReplyCap r R \<Rightarrow> True | MasterReplyCap r \<Rightarrow> True | DomainCap \<Rightarrow> True | PendingSyncSendCap r x xa xb xc xd \<Rightarrow> True | PendingSyncRecvCap r x xa \<Rightarrow> True | PendingNtfnRecvCap r \<Rightarrow> True | RestartCap \<Rightarrow> True | RunningCap \<Rightarrow> True | FrameCap xa xb xc xd x xe \<Rightarrow> x \<noteq> Real | PageTableCap xa x xb \<Rightarrow> x \<noteq> Real | PageDirectoryCap xa x xb \<Rightarrow> x \<noteq> Real | _ \<Rightarrow> False);
result <- finalise_cap cap final;
assert (result = (NullCap, NullCap))
od
theory CSpace_D

lemma use_option_form:
  "f x = (\<lambda>s. monadic_option_dest  (monadic_rel_optionation_form f `` {Some (x, s)}))" by (simp add: monadic_rel_optionation_form_def monadic_option_dest_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. f x = (\<lambda>s. monadic_option_dest (monadic_rel_optionation_form f `` {Some (x, s)}))
theory CSpace_D

lemma ex_option: " (\<exists>x. P x) = ((\<exists>y. P (Some y)) \<or> P None)" apply safe apply (case_tac x, auto) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<exists>x. P x) = ((\<exists>y. P (Some y)) \<or> P None) proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>P x; \<not> P None\<rbrakk> \<Longrightarrow> \<exists>y. P (Some y)
 2. \<And>y. P (Some y) \<Longrightarrow> \<exists>x. P x
 3. P None \<Longrightarrow> \<exists>x. P x proof (prove)
goal:
No subgoals!