kings-crown/FVELER_Isabelle huggingface dataset:
theory structures_proofs

lemma (in kernel_all_substitute) pte_ptr_get_pteSize_spec:
           defines "ptrval s \<equiv> cslift s \<^bsup>s\<^esup>pte_ptr"
           shows "\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. s \<Turnstile>\<^sub>c \<^bsup>s\<^esup>pte_ptr\<rbrace>
            \<acute>ret__unsigned :== PROC pte_ptr_get_pteSize(\<acute>pte_ptr)
            \<lbrace>\<acute>ret__unsigned = pte_get_tag ((the (ptrval s)))\<rbrace> " unfolding ptrval_def apply (rule allI, rule conseqPre, vcg) apply (clarsimp simp:guard_simps) apply (frule h_t_valid_field[where f="[''words_C'']"], simp+) apply (frule iffD1[OF h_t_valid_clift_Some_iff], rule exE, assumption, simp) apply (simp add:h_val_clift' clift_field) apply (simp add:pte_get_tag_def) apply (simp add:mask_shift_simps)? done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> \<lbrace>s. s \<Turnstile>\<^sub>c \<^bsup>s\<^esup>pte_ptr\<rbrace> Call pte_ptr_get_pteSize_'proc \<lbrace>\<acute>ret__unsigned = pte_get_tag (the (ptrval s))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> \<lbrace>s. s \<Turnstile>\<^sub>c \<^bsup>s\<^esup>pte_ptr\<rbrace> Call pte_ptr_get_pteSize_'proc \<lbrace>\<acute>ret__unsigned = pte_get_tag (the (cslift s \<^bsup>s\<^esup>pte_ptr))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrace>s. s \<Turnstile>\<^sub>c \<^bsup>s\<^esup>pte_ptr\<rbrace> \<subseteq> {sa. 0 \<le>s 1 \<and> 1 <s 0x20 \<and> 0 <s 1 \<and> 0 \<le>s 0 \<and> sa \<Turnstile>\<^sub>c pte_ptr_' sa \<and> (h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word[1]) &(pte_ptr_' sa\<rightarrow>[''words_C''])).[unat 0] >> unat 1) && 1 = pte_get_tag (the (cslift s (pte_ptr_' s)))} proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<Turnstile>\<^sub>c pte_ptr_' x \<Longrightarrow> (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[1]) &(pte_ptr_' x\<rightarrow>[''words_C''])).[0] >> Suc 0) && 1 = pte_get_tag (the (cslift x (pte_ptr_' x))) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<Turnstile>\<^sub>c pte_ptr_' x; x \<Turnstile>\<^sub>c PTR(32 word[1]) &(pte_ptr_' x\<rightarrow>[''words_C''])\<rbrakk> \<Longrightarrow> (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[1]) &(pte_ptr_' x\<rightarrow>[''words_C''])).[0] >> Suc 0) && 1 = pte_get_tag (the (cslift x (pte_ptr_' x))) proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x \<Turnstile>\<^sub>c pte_ptr_' x; x \<Turnstile>\<^sub>c PTR(32 word[1]) &(pte_ptr_' x\<rightarrow>[''words_C'']); cslift x (pte_ptr_' x) = Some xa\<rbrakk> \<Longrightarrow> (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[1]) &(pte_ptr_' x\<rightarrow>[''words_C''])).[0] >> Suc 0) && 1 = pte_get_tag xa proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x \<Turnstile>\<^sub>c pte_ptr_' x; x \<Turnstile>\<^sub>c PTR(32 word[1]) &(pte_ptr_' x\<rightarrow>[''words_C'']); cslift x (pte_ptr_' x) = Some xa\<rbrakk> \<Longrightarrow> (pte_C.words_C xa.[0] >> Suc 0) && 1 = pte_get_tag xa proof (prove)
goal:
No subgoals! proof (prove)
goal:
No subgoals!
theory structures_proofs

lemma (in kernel_all_substitute) pte_pte_large_ptr_get_reserved_spec:
    defines "ptrval s \<equiv> cslift s \<^bsup>s\<^esup>pte_ptr"
    shows "\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. s \<Turnstile>\<^sub>c \<^bsup>s\<^esup>pte_ptr \<and> pte_get_tag (the (ptrval s)) = scast pte_pte_large\<rbrace>
            \<acute>ret__unsigned :== PROC pte_pte_large_ptr_get_reserved(\<acute>pte_ptr)
            \<lbrace>\<acute>ret__unsigned = pte_pte_large_CL.reserved_CL (pte_pte_large_lift (the (ptrval s)))\<rbrace> " unfolding ptrval_def apply (rule allI, rule conseqPre, vcg) apply (clarsimp simp: typ_heap_simps h_t_valid_clift_Some_iff guard_simps
                        mask_shift_simps sign_extend_def' nth_is_and_neq_0
                        pte_lift_pte_large pte_pte_large_lift_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> \<lbrace>s. s \<Turnstile>\<^sub>c \<^bsup>s\<^esup>pte_ptr \<and> pte_get_tag (the (ptrval s)) = SCAST(32 signed \<rightarrow> 32) pte_pte_large\<rbrace> Call pte_pte_large_ptr_get_reserved_'proc \<lbrace>\<acute>ret__unsigned = reserved_CL (pte_pte_large_lift (the (ptrval s)))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> \<lbrace>s. s \<Turnstile>\<^sub>c \<^bsup>s\<^esup>pte_ptr \<and> pte_get_tag (the (cslift s \<^bsup>s\<^esup>pte_ptr)) = SCAST(32 signed \<rightarrow> 32) pte_pte_large\<rbrace> Call pte_pte_large_ptr_get_reserved_'proc \<lbrace>\<acute>ret__unsigned = reserved_CL (pte_pte_large_lift (the (cslift s \<^bsup>s\<^esup>pte_ptr)))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrace>s. s \<Turnstile>\<^sub>c \<^bsup>s\<^esup>pte_ptr \<and> pte_get_tag (the (cslift s \<^bsup>s\<^esup>pte_ptr)) = SCAST(32 signed \<rightarrow> 32) pte_pte_large\<rbrace> \<subseteq> {sa. \<forall>v. 0 \<le>s 0 \<and> 0 <s 0x20 \<and> 0 <s 1 \<and> 0 \<le>s 0 \<and> sa \<Turnstile>\<^sub>c pte_ptr_' sa \<and> ((if False then 1 else 0) \<noteq> 0 \<longrightarrow> 0 \<le>s 0x1F \<and> 0x1F <s 0x20 \<and> ((if (h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word[1]) &(pte_ptr_' sa\<rightarrow>[''words_C''])).[unat 0] && 1 >> unat 0) && (1 << unat 0x1F) \<noteq> 0 then 1 else 0) \<noteq> 0 \<longrightarrow> (h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word[1]) &(pte_ptr_' sa\<rightarrow>[''words_C''])).[unat 0] && 1 >> unat 0) || SCAST(32 signed \<rightarrow> 32) 0 = reserved_CL (pte_pte_large_lift (the (cslift s (pte_ptr_' s))))) \<and> ((if (h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word[1]) &(pte_ptr_' sa\<rightarrow>[''words_C''])).[unat 0] && 1 >> unat 0) && (1 << unat 0x1F) \<noteq> 0 then 1 else 0) = 0 \<longrightarrow> h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word[1]) &(pte_ptr_' sa\<rightarrow>[''words_C''])).[unat 0] && 1 >> unat 0 = reserved_CL (pte_pte_large_lift (the (cslift s (pte_ptr_' s)))))) \<and> ((if False then 1 else 0) = 0 \<longrightarrow> h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word[1]) &(pte_ptr_' sa\<rightarrow>[''words_C''])).[unat 0] && 1 >> unat 0 = reserved_CL (pte_pte_large_lift (the (cslift s (pte_ptr_' s)))))} proof (prove)
goal:
No subgoals!
theory structures_proofs

lemma seL4_Fault_ptr_words_NULL:
  "c_guard (p::seL4_Fault_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 structures_proofs

lemma seL4_Fault_ptr_words_aligned:
  "c_guard (p::seL4_Fault_C ptr) \<Longrightarrow>
   ptr_aligned ((Ptr &(p\<rightarrow>[''words_C'']))::((word32[2]) 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[2]) &(p\<rightarrow>[''words_C'']))
theory structures_proofs

lemma seL4_Fault_ptr_words_ptr_safe:
  "ptr_safe (p::seL4_Fault_C ptr) d \<Longrightarrow>
   ptr_safe (Ptr &(p\<rightarrow>[''words_C''])::((word32[2]) 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[2]) &(p\<rightarrow>[''words_C''])) d
theory structures_proofs

lemma (in kernel_all_substitute) seL4_Fault_get_seL4_FaultType_spec:
  "\<forall>s. \<Gamma> \<turnstile> {s}
       \<acute>ret__unsigned :== PROC seL4_Fault_get_seL4_FaultType(\<acute>seL4_Fault)
       \<lbrace>\<acute>ret__unsigned = seL4_Fault_get_tag \<^bsup>s\<^esup>seL4_Fault\<rbrace>" apply(rule allI, rule conseqPre, vcg) apply (clarsimp) apply (simp add:seL4_Fault_get_tag_def mask_shift_simps guard_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> {s} Call seL4_Fault_get_seL4_FaultType_'proc \<lbrace>\<acute>ret__unsigned = seL4_Fault_get_tag \<^bsup>s\<^esup>seL4_Fault\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. {s} \<subseteq> \<lbrace>0 \<le>s 0 \<and> 0 <s 0x20 \<and> 0 <s 2 \<and> 0 \<le>s 0 \<and> (seL4_Fault_C.words_C \<acute>seL4_Fault.[unat 0] >> unat 0) && 0xF = seL4_Fault_get_tag \<^bsup>s\<^esup>seL4_Fault\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. seL4_Fault_C.words_C (seL4_Fault_' s).[0] && 0xF = seL4_Fault_get_tag (seL4_Fault_' s) proof (prove)
goal:
No subgoals!
theory structures_proofs

lemma (in kernel_all_substitute) seL4_Fault_NullFault_new_spec:
  "\<forall>s. \<Gamma> \<turnstile> {s}
       \<acute>ret__struct_seL4_Fault_C :== PROC seL4_Fault_NullFault_new()
       \<lbrace>seL4_Fault_get_tag \<acute>ret__struct_seL4_Fault_C = scast seL4_Fault_NullFault\<rbrace>" apply(rule allI, rule conseqPre, vcg) by (clarsimp simp: guard_simps
                     seL4_Fault_lift_def
                     Let_def
                     seL4_Fault_get_tag_def
                     mask_shift_simps
                     seL4_Fault_tag_defs
                     word_of_int_hom_syms)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> {s} Call seL4_Fault_NullFault_new_'proc \<lbrace>seL4_Fault_get_tag \<acute>ret__struct_seL4_Fault_C = SCAST(32 signed \<rightarrow> 32) seL4_Fault_NullFault\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. {s} \<subseteq> \<lbrace>\<forall>v. 0 <s 2 \<and> 0 \<le>s 0 \<and> 0 <s 0x20 \<and> 1 <s 2 \<and> 0 \<le>s 1 \<and> seL4_Fault_get_tag (seL4_Fault_C.words_C_update (\<lambda>v. Arrays.update v (unat 1) (SCAST(32 signed \<rightarrow> 32) 0)) (seL4_Fault_C.words_C_update (\<lambda>v. Arrays.update v (unat 0) (SCAST(32 signed \<rightarrow> 32) 0 || (SCAST(32 signed \<rightarrow> 32) seL4_Fault_NullFault && 0xF << unat 0))) v)) = SCAST(32 signed \<rightarrow> 32) seL4_Fault_NullFault\<rbrace>
theory shared_types_defs

lemma word_sub_mask:
  "\<lbrakk> w && m1 = v1; m1 && m2 = m2; v1 && m2 = v2 \<rbrakk>
     \<Longrightarrow> w && m2 = v2" by (clarsimp simp: word_bw_assocs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>w && m1 = v1; m1 && m2 = m2; v1 && m2 = v2\<rbrakk> \<Longrightarrow> w && m2 = v2
theory shared_types_proofs

lemma seL4_CNode_CapData_ptr_words_NULL:
  "c_guard (p::seL4_CNode_CapData_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_CNode_CapData_ptr_words_aligned:
  "c_guard (p::seL4_CNode_CapData_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_CNode_CapData_ptr_words_ptr_safe:
  "ptr_safe (p::seL4_CNode_CapData_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_CNode_CapData_get_guard_spec:
  "\<forall>s. \<Gamma> \<turnstile> {s}
       \<acute>ret__unsigned :== PROC seL4_CNode_CapData_get_guard(\<acute>seL4_CNode_CapData)
       \<lbrace>\<acute>ret__unsigned = seL4_CNode_CapData_CL.guard_CL (seL4_CNode_CapData_lift \<^bsup>s\<^esup>seL4_CNode_CapData)\<rbrace>" apply (rule allI, rule conseqPre, vcg) apply clarsimp apply (simp add: seL4_CNode_CapData_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_CNode_CapData_get_guard_'proc \<lbrace>\<acute>ret__unsigned = guard_CL (seL4_CNode_CapData_lift \<^bsup>s\<^esup>seL4_CNode_CapData)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. {s} \<subseteq> \<lbrace>\<forall>v. 0 \<le>s 8 \<and> 8 <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_CNode_CapData_C.words_C \<acute>seL4_CNode_CapData.[unat 0] && 0x3FFFF00 >> unat 8) && (1 << unat 0x1F) \<noteq> 0 then 1 else 0) \<noteq> 0 \<longrightarrow> (seL4_CNode_CapData_C.words_C \<acute>seL4_CNode_CapData.[unat 0] && 0x3FFFF00 >> unat 8) || SCAST(32 signed \<rightarrow> 32) 0 = guard_CL (seL4_CNode_CapData_lift \<^bsup>s\<^esup>seL4_CNode_CapData)) \<and> ((if (seL4_CNode_CapData_C.words_C \<acute>seL4_CNode_CapData.[unat 0] && 0x3FFFF00 >> unat 8) && (1 << unat 0x1F) \<noteq> 0 then 1 else 0) = 0 \<longrightarrow> seL4_CNode_CapData_C.words_C \<acute>seL4_CNode_CapData.[unat 0] && 0x3FFFF00 >> unat 8 = guard_CL (seL4_CNode_CapData_lift \<^bsup>s\<^esup>seL4_CNode_CapData))) \<and> ((if False then 1 else 0) = 0 \<longrightarrow> seL4_CNode_CapData_C.words_C \<acute>seL4_CNode_CapData.[unat 0] && 0x3FFFF00 >> unat 8 = guard_CL (seL4_CNode_CapData_lift \<^bsup>s\<^esup>seL4_CNode_CapData))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. seL4_CNode_CapData_C.words_C (seL4_CNode_CapData_' s).[0] && 0x3FFFF00 >> 8 = guard_CL (seL4_CNode_CapData_lift (seL4_CNode_CapData_' s)) proof (prove)
goal:
No subgoals! proof (prove)
goal:
No subgoals!
theory shared_types_proofs

lemma (in kernel_all_substitute) seL4_CNode_CapData_get_guardSize_spec:
  "\<forall>s. \<Gamma> \<turnstile> {s}
       \<acute>ret__unsigned :== PROC seL4_CNode_CapData_get_guardSize(\<acute>seL4_CNode_CapData)
       \<lbrace>\<acute>ret__unsigned = seL4_CNode_CapData_CL.guardSize_CL (seL4_CNode_CapData_lift \<^bsup>s\<^esup>seL4_CNode_CapData)\<rbrace>" apply (rule allI, rule conseqPre, vcg) apply clarsimp apply (simp add: seL4_CNode_CapData_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_CNode_CapData_get_guardSize_'proc \<lbrace>\<acute>ret__unsigned = guardSize_CL (seL4_CNode_CapData_lift \<^bsup>s\<^esup>seL4_CNode_CapData)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. {s} \<subseteq> \<lbrace>\<forall>v. 0 \<le>s 3 \<and> 3 <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_CNode_CapData_C.words_C \<acute>seL4_CNode_CapData.[unat 0] && 0xF8 >> unat 3) && (1 << unat 0x1F) \<noteq> 0 then 1 else 0) \<noteq> 0 \<longrightarrow> (seL4_CNode_CapData_C.words_C \<acute>seL4_CNode_CapData.[unat 0] && 0xF8 >> unat 3) || SCAST(32 signed \<rightarrow> 32) 0 = guardSize_CL (seL4_CNode_CapData_lift \<^bsup>s\<^esup>seL4_CNode_CapData)) \<and> ((if (seL4_CNode_CapData_C.words_C \<acute>seL4_CNode_CapData.[unat 0] && 0xF8 >> unat 3) && (1 << unat 0x1F) \<noteq> 0 then 1 else 0) = 0 \<longrightarrow> seL4_CNode_CapData_C.words_C \<acute>seL4_CNode_CapData.[unat 0] && 0xF8 >> unat 3 = guardSize_CL (seL4_CNode_CapData_lift \<^bsup>s\<^esup>seL4_CNode_CapData))) \<and> ((if False then 1 else 0) = 0 \<longrightarrow> seL4_CNode_CapData_C.words_C \<acute>seL4_CNode_CapData.[unat 0] && 0xF8 >> unat 3 = guardSize_CL (seL4_CNode_CapData_lift \<^bsup>s\<^esup>seL4_CNode_CapData))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. seL4_CNode_CapData_C.words_C (seL4_CNode_CapData_' s).[0] && 0xF8 >> 3 = guardSize_CL (seL4_CNode_CapData_lift (seL4_CNode_CapData_' s)) proof (prove)
goal:
No subgoals! proof (prove)
goal:
No subgoals!
theory shared_types_proofs

lemma seL4_CapRights_ptr_words_NULL:
  "c_guard (p::seL4_CapRights_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_CapRights_ptr_words_aligned:
  "c_guard (p::seL4_CapRights_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_CapRights_ptr_words_ptr_safe:
  "ptr_safe (p::seL4_CapRights_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_CapRights_get_capAllowGrantReply_spec:
  "\<forall>s. \<Gamma> \<turnstile> {s}
       \<acute>ret__unsigned :== PROC seL4_CapRights_get_capAllowGrantReply(\<acute>seL4_CapRights)
       \<lbrace>\<acute>ret__unsigned = seL4_CapRights_CL.capAllowGrantReply_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_capAllowGrantReply_'proc \<lbrace>\<acute>ret__unsigned = capAllowGrantReply_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 3 \<and> 3 <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] && 8 >> unat 3) && (1 << unat 0x1F) \<noteq> 0 then 1 else 0) \<noteq> 0 \<longrightarrow> (seL4_CapRights_C.words_C \<acute>seL4_CapRights.[unat 0] && 8 >> unat 3) || SCAST(32 signed \<rightarrow> 32) 0 = capAllowGrantReply_CL (seL4_CapRights_lift \<^bsup>s\<^esup>seL4_CapRights)) \<and> ((if (seL4_CapRights_C.words_C \<acute>seL4_CapRights.[unat 0] && 8 >> unat 3) && (1 << unat 0x1F) \<noteq> 0 then 1 else 0) = 0 \<longrightarrow> seL4_CapRights_C.words_C \<acute>seL4_CapRights.[unat 0] && 8 >> unat 3 = capAllowGrantReply_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] && 8 >> unat 3 = capAllowGrantReply_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] && 8 >> 3 = capAllowGrantReply_CL (seL4_CapRights_lift (seL4_CapRights_' s)) proof (prove)
goal:
No subgoals! proof (prove)
goal:
No subgoals!
theory shared_types_proofs

lemma (in kernel_all_substitute) seL4_CapRights_get_capAllowGrant_spec:
  "\<forall>s. \<Gamma> \<turnstile> {s}
       \<acute>ret__unsigned :== PROC seL4_CapRights_get_capAllowGrant(\<acute>seL4_CapRights)
       \<lbrace>\<acute>ret__unsigned = seL4_CapRights_CL.capAllowGrant_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_capAllowGrant_'proc \<lbrace>\<acute>ret__unsigned = capAllowGrant_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 2 \<and> 2 <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] && 4 >> unat 2) && (1 << unat 0x1F) \<noteq> 0 then 1 else 0) \<noteq> 0 \<longrightarrow> (seL4_CapRights_C.words_C \<acute>seL4_CapRights.[unat 0] && 4 >> unat 2) || SCAST(32 signed \<rightarrow> 32) 0 = capAllowGrant_CL (seL4_CapRights_lift \<^bsup>s\<^esup>seL4_CapRights)) \<and> ((if (seL4_CapRights_C.words_C \<acute>seL4_CapRights.[unat 0] && 4 >> unat 2) && (1 << unat 0x1F) \<noteq> 0 then 1 else 0) = 0 \<longrightarrow> seL4_CapRights_C.words_C \<acute>seL4_CapRights.[unat 0] && 4 >> unat 2 = capAllowGrant_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] && 4 >> unat 2 = capAllowGrant_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] && 4 >> 2 = capAllowGrant_CL (seL4_CapRights_lift (seL4_CapRights_' s)) proof (prove)
goal:
No subgoals! proof (prove)
goal:
No subgoals!
theory shared_types_proofs

lemma (in kernel_all_substitute) seL4_CapRights_get_capAllowRead_spec:
  "\<forall>s. \<Gamma> \<turnstile> {s}
       \<acute>ret__unsigned :== PROC seL4_CapRights_get_capAllowRead(\<acute>seL4_CapRights)
       \<lbrace>\<acute>ret__unsigned = seL4_CapRights_CL.capAllowRead_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_capAllowRead_'proc \<lbrace>\<acute>ret__unsigned = capAllowRead_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 1 \<and> 1 <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] && 2 >> unat 1) && (1 << unat 0x1F) \<noteq> 0 then 1 else 0) \<noteq> 0 \<longrightarrow> (seL4_CapRights_C.words_C \<acute>seL4_CapRights.[unat 0] && 2 >> unat 1) || SCAST(32 signed \<rightarrow> 32) 0 = capAllowRead_CL (seL4_CapRights_lift \<^bsup>s\<^esup>seL4_CapRights)) \<and> ((if (seL4_CapRights_C.words_C \<acute>seL4_CapRights.[unat 0] && 2 >> unat 1) && (1 << unat 0x1F) \<noteq> 0 then 1 else 0) = 0 \<longrightarrow> seL4_CapRights_C.words_C \<acute>seL4_CapRights.[unat 0] && 2 >> unat 1 = capAllowRead_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] && 2 >> unat 1 = capAllowRead_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] && 2 >> Suc 0 = capAllowRead_CL (seL4_CapRights_lift (seL4_CapRights_' s)) proof (prove)
goal:
No subgoals! proof (prove)
goal:
No subgoals!