kings-crown/FVELER_Isabelle huggingface dataset:
theory structures_proofs

lemma (in kernel_all_substitute) vm_attributes_new_spec:
  "\<forall> s. \<Gamma> \<turnstile> {s}
       \<acute>ret__struct_vm_attributes_C :== PROC vm_attributes_new(\<acute>armExecuteNever, \<acute>armParityEnabled, \<acute>armPageCacheable)
       \<lbrace> vm_attributes_lift \<acute>ret__struct_vm_attributes_C = \<lparr>
          vm_attributes_CL.armExecuteNever_CL = (\<^bsup>s\<^esup>armExecuteNever AND mask 1),
          vm_attributes_CL.armParityEnabled_CL = (\<^bsup>s\<^esup>armParityEnabled AND mask 1),
          vm_attributes_CL.armPageCacheable_CL = (\<^bsup>s\<^esup>armPageCacheable AND mask 1) \<rparr> \<rbrace>" apply (rule allI, rule conseqPre, vcg) apply (clarsimp simp: guard_simps) apply (simp add: vm_attributes_lift_def) apply ((intro conjI sign_extend_eq)?;
         (simp add: mask_def shift_over_ao_dists multi_shift_simps word_size
                    word_ao_dist word_bw_assocs word_and_max_simps)?) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> {s} Call vm_attributes_new_'proc \<lbrace>vm_attributes_lift \<acute>ret__struct_vm_attributes_C = \<lparr>armExecuteNever_CL = \<^bsup>s\<^esup>armExecuteNever && mask 1, armParityEnabled_CL = \<^bsup>s\<^esup>armParityEnabled && mask 1, armPageCacheable_CL = \<^bsup>s\<^esup>armPageCacheable && mask 1\<rparr>\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. {s} \<subseteq> \<lbrace>\<forall>v. 0 <s 1 \<and> 0 \<le>s 0 \<and> 0 <s 0x20 \<and> 0 \<le>s 1 \<and> 1 <s 0x20 \<and> 0 \<le>s 2 \<and> 2 <s 0x20 \<and> vm_attributes_lift (vm_attributes_C.words_C_update (\<lambda>v. Arrays.update v (unat 0) (((SCAST(32 signed \<rightarrow> 32) 0 || (\<acute>armExecuteNever && 1 << unat 2)) || (\<acute>armParityEnabled && 1 << unat 1)) || (\<acute>armPageCacheable && 1 << unat 0))) v) = \<lparr>armExecuteNever_CL = \<^bsup>s\<^esup>armExecuteNever && mask 1, armParityEnabled_CL = \<^bsup>s\<^esup>armParityEnabled && mask 1, armPageCacheable_CL = \<^bsup>s\<^esup>armPageCacheable && mask 1\<rparr>\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s v. vm_attributes_lift (vm_attributes_C.words_C_update (\<lambda>v. Arrays.update v 0 (((armExecuteNever_' s && 1 << 2) || (armParityEnabled_' s && 1 << Suc 0)) || armPageCacheable_' s && 1)) v) = \<lparr>armExecuteNever_CL = armExecuteNever_' s && 1, armParityEnabled_CL = armParityEnabled_' s && 1, armPageCacheable_CL = armPageCacheable_' s && 1\<rparr> proof (prove)
goal (1 subgoal):
 1. \<And>s. (((armExecuteNever_' s && 1 << 2) || (armParityEnabled_' s && 1 << Suc 0)) || armPageCacheable_' s && 1 >> 2) && 1 = armExecuteNever_' s && 1 \<and> (((armExecuteNever_' s && 1 << 2) || (armParityEnabled_' s && 1 << Suc 0)) || armPageCacheable_' s && 1 >> Suc 0) && 1 = armParityEnabled_' s && 1 \<and> (((armExecuteNever_' s && 1 << 2) || (armParityEnabled_' s && 1 << Suc 0)) || armPageCacheable_' s && 1) && 1 = armPageCacheable_' s && 1 proof (prove)
goal:
No subgoals!
theory structures_proofs

lemma (in kernel_all_substitute) vm_attributes_get_armExecuteNever_spec:
  "\<forall>s. \<Gamma> \<turnstile> {s}
       \<acute>ret__unsigned :== PROC vm_attributes_get_armExecuteNever(\<acute>vm_attributes)
       \<lbrace>\<acute>ret__unsigned = vm_attributes_CL.armExecuteNever_CL (vm_attributes_lift \<^bsup>s\<^esup>vm_attributes)\<rbrace>" apply (rule allI, rule conseqPre, vcg) apply clarsimp apply (simp add: vm_attributes_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 vm_attributes_get_armExecuteNever_'proc \<lbrace>\<acute>ret__unsigned = armExecuteNever_CL (vm_attributes_lift \<^bsup>s\<^esup>vm_attributes)\<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 (vm_attributes_C.words_C \<acute>vm_attributes.[unat 0] && 4 >> unat 2) && (1 << unat 0x1F) \<noteq> 0 then 1 else 0) \<noteq> 0 \<longrightarrow> (vm_attributes_C.words_C \<acute>vm_attributes.[unat 0] && 4 >> unat 2) || SCAST(32 signed \<rightarrow> 32) 0 = armExecuteNever_CL (vm_attributes_lift \<^bsup>s\<^esup>vm_attributes)) \<and> ((if (vm_attributes_C.words_C \<acute>vm_attributes.[unat 0] && 4 >> unat 2) && (1 << unat 0x1F) \<noteq> 0 then 1 else 0) = 0 \<longrightarrow> vm_attributes_C.words_C \<acute>vm_attributes.[unat 0] && 4 >> unat 2 = armExecuteNever_CL (vm_attributes_lift \<^bsup>s\<^esup>vm_attributes))) \<and> ((if False then 1 else 0) = 0 \<longrightarrow> vm_attributes_C.words_C \<acute>vm_attributes.[unat 0] && 4 >> unat 2 = armExecuteNever_CL (vm_attributes_lift \<^bsup>s\<^esup>vm_attributes))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. vm_attributes_C.words_C (vm_attributes_' s).[0] && 4 >> 2 = armExecuteNever_CL (vm_attributes_lift (vm_attributes_' s)) proof (prove)
goal:
No subgoals! proof (prove)
goal:
No subgoals!
theory structures_proofs

lemma (in kernel_all_substitute) vm_attributes_get_armParityEnabled_spec:
  "\<forall>s. \<Gamma> \<turnstile> {s}
       \<acute>ret__unsigned :== PROC vm_attributes_get_armParityEnabled(\<acute>vm_attributes)
       \<lbrace>\<acute>ret__unsigned = vm_attributes_CL.armParityEnabled_CL (vm_attributes_lift \<^bsup>s\<^esup>vm_attributes)\<rbrace>" apply (rule allI, rule conseqPre, vcg) apply clarsimp apply (simp add: vm_attributes_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 vm_attributes_get_armParityEnabled_'proc \<lbrace>\<acute>ret__unsigned = armParityEnabled_CL (vm_attributes_lift \<^bsup>s\<^esup>vm_attributes)\<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 (vm_attributes_C.words_C \<acute>vm_attributes.[unat 0] && 2 >> unat 1) && (1 << unat 0x1F) \<noteq> 0 then 1 else 0) \<noteq> 0 \<longrightarrow> (vm_attributes_C.words_C \<acute>vm_attributes.[unat 0] && 2 >> unat 1) || SCAST(32 signed \<rightarrow> 32) 0 = armParityEnabled_CL (vm_attributes_lift \<^bsup>s\<^esup>vm_attributes)) \<and> ((if (vm_attributes_C.words_C \<acute>vm_attributes.[unat 0] && 2 >> unat 1) && (1 << unat 0x1F) \<noteq> 0 then 1 else 0) = 0 \<longrightarrow> vm_attributes_C.words_C \<acute>vm_attributes.[unat 0] && 2 >> unat 1 = armParityEnabled_CL (vm_attributes_lift \<^bsup>s\<^esup>vm_attributes))) \<and> ((if False then 1 else 0) = 0 \<longrightarrow> vm_attributes_C.words_C \<acute>vm_attributes.[unat 0] && 2 >> unat 1 = armParityEnabled_CL (vm_attributes_lift \<^bsup>s\<^esup>vm_attributes))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. vm_attributes_C.words_C (vm_attributes_' s).[0] && 2 >> Suc 0 = armParityEnabled_CL (vm_attributes_lift (vm_attributes_' s)) proof (prove)
goal:
No subgoals! proof (prove)
goal:
No subgoals!
theory structures_proofs

lemma (in kernel_all_substitute) vm_attributes_get_armPageCacheable_spec:
  "\<forall>s. \<Gamma> \<turnstile> {s}
       \<acute>ret__unsigned :== PROC vm_attributes_get_armPageCacheable(\<acute>vm_attributes)
       \<lbrace>\<acute>ret__unsigned = vm_attributes_CL.armPageCacheable_CL (vm_attributes_lift \<^bsup>s\<^esup>vm_attributes)\<rbrace>" apply (rule allI, rule conseqPre, vcg) apply clarsimp apply (simp add: vm_attributes_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 vm_attributes_get_armPageCacheable_'proc \<lbrace>\<acute>ret__unsigned = armPageCacheable_CL (vm_attributes_lift \<^bsup>s\<^esup>vm_attributes)\<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 (vm_attributes_C.words_C \<acute>vm_attributes.[unat 0] && 1 >> unat 0) && (1 << unat 0x1F) \<noteq> 0 then 1 else 0) \<noteq> 0 \<longrightarrow> (vm_attributes_C.words_C \<acute>vm_attributes.[unat 0] && 1 >> unat 0) || SCAST(32 signed \<rightarrow> 32) 0 = armPageCacheable_CL (vm_attributes_lift \<^bsup>s\<^esup>vm_attributes)) \<and> ((if (vm_attributes_C.words_C \<acute>vm_attributes.[unat 0] && 1 >> unat 0) && (1 << unat 0x1F) \<noteq> 0 then 1 else 0) = 0 \<longrightarrow> vm_attributes_C.words_C \<acute>vm_attributes.[unat 0] && 1 >> unat 0 = armPageCacheable_CL (vm_attributes_lift \<^bsup>s\<^esup>vm_attributes))) \<and> ((if False then 1 else 0) = 0 \<longrightarrow> vm_attributes_C.words_C \<acute>vm_attributes.[unat 0] && 1 >> unat 0 = armPageCacheable_CL (vm_attributes_lift \<^bsup>s\<^esup>vm_attributes))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. vm_attributes_C.words_C (vm_attributes_' s).[0] && 1 = armPageCacheable_CL (vm_attributes_lift (vm_attributes_' s)) proof (prove)
goal:
No subgoals! proof (prove)
goal:
No subgoals!
theory structures_proofs

lemma cap_ptr_words_NULL:
  "c_guard (p::cap_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 cap_ptr_words_aligned:
  "c_guard (p::cap_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 cap_ptr_words_ptr_safe:
  "ptr_safe (p::cap_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) cap_capType_equals_spec:
  "\<forall>s. \<Gamma> \<turnstile> {s}
       \<acute>ret__int :==
       PROC cap_capType_equals(\<acute>cap, \<acute>cap_type_tag)
       \<lbrace>\<acute>ret__int = of_bl [cap_get_tag \<^bsup>s\<^esup>cap = \<^bsup>s\<^esup>cap_type_tag]\<rbrace>" apply(rule allI, rule conseqPre, vcg) apply (clarsimp) apply (simp add:cap_get_tag_eq_x mask_shift_simps guard_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> {s} Call cap_capType_equals_'proc \<lbrace>\<acute>ret__int = of_bl [cap_get_tag \<^bsup>s\<^esup>cap = \<^bsup>s\<^esup>cap_type_tag]\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. {s} \<subseteq> \<lbrace>(\<acute>cap_type_tag && SCAST(32 signed \<rightarrow> 32) 0xE \<noteq> SCAST(32 signed \<rightarrow> 32) 0xE \<longrightarrow> 0 \<le>s 0 \<and> 0 <s 0x20 \<and> 0 <s 2 \<and> 0 \<le>s 0 \<and> (if (cap_C.words_C \<acute>cap.[unat 0] >> unat 0) && 0xF = \<acute>cap_type_tag then 1 else 0) = of_bl [cap_get_tag \<^bsup>s\<^esup>cap = \<^bsup>s\<^esup>cap_type_tag]) \<and> (\<not> \<acute>cap_type_tag && SCAST(32 signed \<rightarrow> 32) 0xE \<noteq> SCAST(32 signed \<rightarrow> 32) 0xE \<longrightarrow> 0 \<le>s 0 \<and> 0 <s 0x20 \<and> 0 <s 2 \<and> 0 \<le>s 0 \<and> (if (cap_C.words_C \<acute>cap.[unat 0] >> unat 0) && 0xFF = \<acute>cap_type_tag then 1 else 0) = of_bl [cap_get_tag \<^bsup>s\<^esup>cap = \<^bsup>s\<^esup>cap_type_tag])\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (cap_C.words_C (cap_' s).[0] && 0xF = cap_type_tag_' s \<longrightarrow> (cap_C.words_C (cap_' s).[0] && 0xFF = cap_type_tag_' s \<longrightarrow> of_bl [cap_get_tag (cap_' s) = cap_type_tag_' s] = 1) \<and> (cap_C.words_C (cap_' s).[0] && 0xFF \<noteq> cap_type_tag_' s \<longrightarrow> (cap_type_tag_' s && 0xE \<noteq> 0xE \<longrightarrow> of_bl [cap_get_tag (cap_' s) = cap_type_tag_' s] = 1) \<and> (cap_type_tag_' s && 0xE = 0xE \<longrightarrow> of_bl [cap_get_tag (cap_' s) = cap_type_tag_' s] = 0))) \<and> (cap_C.words_C (cap_' s).[0] && 0xF \<noteq> cap_type_tag_' s \<longrightarrow> (cap_C.words_C (cap_' s).[0] && 0xFF = cap_type_tag_' s \<longrightarrow> (cap_type_tag_' s && 0xE \<noteq> 0xE \<longrightarrow> of_bl [cap_get_tag (cap_' s) = cap_type_tag_' s] = 0) \<and> (cap_type_tag_' s && 0xE = 0xE \<longrightarrow> of_bl [cap_get_tag (cap_' s) = cap_type_tag_' s] = 1)) \<and> (cap_C.words_C (cap_' s).[0] && 0xFF \<noteq> cap_type_tag_' s \<longrightarrow> of_bl [cap_get_tag (cap_' s) = cap_type_tag_' s] = 0)) proof (prove)
goal:
No subgoals!
theory structures_proofs

lemma (in kernel_all_substitute) cap_asid_control_cap_new_spec:
  "\<forall>s. \<Gamma> \<turnstile> {s}
       \<acute>ret__struct_cap_C :== PROC cap_asid_control_cap_new()
       \<lbrace>cap_get_tag \<acute>ret__struct_cap_C = scast cap_asid_control_cap\<rbrace>" apply(rule allI, rule conseqPre, vcg) by (clarsimp simp: guard_simps
                     cap_lift_def
                     Let_def
                     cap_get_tag_def
                     mask_shift_simps
                     cap_tag_defs
                     word_of_int_hom_syms)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> {s} Call cap_asid_control_cap_new_'proc \<lbrace>cap_get_tag \<acute>ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_asid_control_cap\<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> cap_get_tag (cap_C.words_C_update (\<lambda>v. Arrays.update v (unat 1) (SCAST(32 signed \<rightarrow> 32) 0)) (cap_C.words_C_update (\<lambda>v. Arrays.update v (unat 0) (SCAST(32 signed \<rightarrow> 32) 0 || (SCAST(32 signed \<rightarrow> 32) cap_asid_control_cap && 0xF << unat 0))) v)) = SCAST(32 signed \<rightarrow> 32) cap_asid_control_cap\<rbrace>
theory structures_proofs

lemma (in kernel_all_substitute) cap_irq_control_cap_new_spec:
  "\<forall>s. \<Gamma> \<turnstile> {s}
       \<acute>ret__struct_cap_C :== PROC cap_irq_control_cap_new()
       \<lbrace>cap_get_tag \<acute>ret__struct_cap_C = scast cap_irq_control_cap\<rbrace>" apply(rule allI, rule conseqPre, vcg) by (clarsimp simp: guard_simps
                     cap_lift_def
                     Let_def
                     cap_get_tag_def
                     mask_shift_simps
                     cap_tag_defs
                     word_of_int_hom_syms)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> {s} Call cap_irq_control_cap_new_'proc \<lbrace>cap_get_tag \<acute>ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_irq_control_cap\<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> cap_get_tag (cap_C.words_C_update (\<lambda>v. Arrays.update v (unat 1) (SCAST(32 signed \<rightarrow> 32) 0)) (cap_C.words_C_update (\<lambda>v. Arrays.update v (unat 0) (SCAST(32 signed \<rightarrow> 32) 0 || (SCAST(32 signed \<rightarrow> 32) cap_irq_control_cap && 0xFF << unat 0))) v)) = SCAST(32 signed \<rightarrow> 32) cap_irq_control_cap\<rbrace>
theory structures_proofs

lemma (in kernel_all_substitute) cap_domain_cap_new_spec:
  "\<forall>s. \<Gamma> \<turnstile> {s}
       \<acute>ret__struct_cap_C :== PROC cap_domain_cap_new()
       \<lbrace>cap_get_tag \<acute>ret__struct_cap_C = scast cap_domain_cap\<rbrace>" apply(rule allI, rule conseqPre, vcg) by (clarsimp simp: guard_simps
                     cap_lift_def
                     Let_def
                     cap_get_tag_def
                     mask_shift_simps
                     cap_tag_defs
                     word_of_int_hom_syms)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> {s} Call cap_domain_cap_new_'proc \<lbrace>cap_get_tag \<acute>ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_domain_cap\<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> cap_get_tag (cap_C.words_C_update (\<lambda>v. Arrays.update v (unat 1) (SCAST(32 signed \<rightarrow> 32) 0)) (cap_C.words_C_update (\<lambda>v. Arrays.update v (unat 0) (SCAST(32 signed \<rightarrow> 32) 0 || (SCAST(32 signed \<rightarrow> 32) cap_domain_cap && 0xFF << unat 0))) v)) = SCAST(32 signed \<rightarrow> 32) cap_domain_cap\<rbrace>
theory structures_proofs

lemma lookup_fault_ptr_words_NULL:
  "c_guard (p::lookup_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 lookup_fault_ptr_words_aligned:
  "c_guard (p::lookup_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 (in kernel_all_substitute) lookup_fault_invalid_root_new_spec:
  "\<forall>s. \<Gamma> \<turnstile> {s}
       \<acute>ret__struct_lookup_fault_C :== PROC lookup_fault_invalid_root_new()
       \<lbrace>lookup_fault_get_tag \<acute>ret__struct_lookup_fault_C = scast lookup_fault_invalid_root\<rbrace>" apply(rule allI, rule conseqPre, vcg) by (clarsimp simp: guard_simps
                     lookup_fault_lift_def
                     Let_def
                     lookup_fault_get_tag_def
                     mask_shift_simps
                     lookup_fault_tag_defs
                     word_of_int_hom_syms)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> {s} Call lookup_fault_invalid_root_new_'proc \<lbrace>lookup_fault_get_tag \<acute>ret__struct_lookup_fault_C = SCAST(32 signed \<rightarrow> 32) lookup_fault_invalid_root\<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> lookup_fault_get_tag (lookup_fault_C.words_C_update (\<lambda>v. Arrays.update v (unat 1) (SCAST(32 signed \<rightarrow> 32) 0)) (lookup_fault_C.words_C_update (\<lambda>v. Arrays.update v (unat 0) (SCAST(32 signed \<rightarrow> 32) 0 || (SCAST(32 signed \<rightarrow> 32) lookup_fault_invalid_root && 3 << unat 0))) v)) = SCAST(32 signed \<rightarrow> 32) lookup_fault_invalid_root\<rbrace>
theory structures_proofs

lemma pde_ptr_words_NULL:
  "c_guard (p::pde_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 pde_ptr_words_aligned:
  "c_guard (p::pde_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 structures_proofs

lemma pde_ptr_words_ptr_safe:
  "ptr_safe (p::pde_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 structures_proofs

lemma (in kernel_all_substitute) pde_get_pdeType_spec:
  "\<forall>s. \<Gamma> \<turnstile> {s}
       \<acute>ret__unsigned :== PROC pde_get_pdeType(\<acute>pde)
       \<lbrace>\<acute>ret__unsigned = pde_get_tag \<^bsup>s\<^esup>pde\<rbrace>" apply(rule allI, rule conseqPre, vcg) apply (clarsimp) apply (simp add:pde_get_tag_def mask_shift_simps guard_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> {s} Call pde_get_pdeType_'proc \<lbrace>\<acute>ret__unsigned = pde_get_tag \<^bsup>s\<^esup>pde\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. {s} \<subseteq> \<lbrace>0 \<le>s 0 \<and> 0 <s 0x20 \<and> 0 <s 1 \<and> 0 \<le>s 0 \<and> (pde_C.words_C \<acute>pde.[unat 0] >> unat 0) && 3 = pde_get_tag \<^bsup>s\<^esup>pde\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. pde_C.words_C (pde_' s).[0] && 3 = pde_get_tag (pde_' s) proof (prove)
goal:
No subgoals!
theory structures_proofs

lemma pte_ptr_words_NULL:
  "c_guard (p::pte_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 pte_ptr_words_aligned:
  "c_guard (p::pte_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 structures_proofs

lemma pte_ptr_words_ptr_safe:
  "ptr_safe (p::pte_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 structures_proofs

lemma (in kernel_all_substitute) pte_get_pteSize_spec:
  "\<forall>s. \<Gamma> \<turnstile> {s}
       \<acute>ret__unsigned :== PROC pte_get_pteSize(\<acute>pte)
       \<lbrace>\<acute>ret__unsigned = pte_get_tag \<^bsup>s\<^esup>pte\<rbrace>" apply(rule allI, rule conseqPre, vcg) apply (clarsimp) apply (simp add:pte_get_tag_def mask_shift_simps guard_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> {s} Call pte_get_pteSize_'proc \<lbrace>\<acute>ret__unsigned = pte_get_tag \<^bsup>s\<^esup>pte\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. {s} \<subseteq> \<lbrace>0 \<le>s 1 \<and> 1 <s 0x20 \<and> 0 <s 1 \<and> 0 \<le>s 0 \<and> (pte_C.words_C \<acute>pte.[unat 0] >> unat 1) && 1 = pte_get_tag \<^bsup>s\<^esup>pte\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (pte_C.words_C (pte_' s).[0] >> Suc 0) && 1 = pte_get_tag (pte_' s) proof (prove)
goal:
No subgoals!