kings-crown/FVELER_Isabelle huggingface dataset:
theory GlobalsSwap

lemma h_val_globals_swap_in_const_global:
  "\<lbrakk> global_acc_valid g_hrs g_hrs_upd;
        globals_list_distinct D symtab xs;
        const_global_data s (v :: 'a :: c_type) \<in> set xs;
        unat offs + size_of TYPE('b) \<le> size_of TYPE('a) \<rbrakk>
    \<Longrightarrow> h_val (hrs_mem (g_hrs (globals_swap g_hrs g_hrs_upd symtab xs gs)))
            (Ptr (symtab s + offs) :: ('b :: c_type) ptr)
         = h_val (hrs_mem (g_hrs gs)) (Ptr (symtab s + offs))" apply (erule disjoint_h_val_globals_swap_filter,
    erule(1) globals_list_distinct_filter_member) apply simp apply (rule order_trans, rule s_footprint_intvl_subset) apply (simp add: global_data_region_def const_global_data_def
                   Times_subset_cancel2) apply (erule intvl_sub_offset) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>global_acc_valid g_hrs g_hrs_upd; globals_list_distinct D symtab xs; const_global_data s v \<in> set xs; unat offs + size_of TYPE('b) \<le> size_of TYPE('a)\<rbrakk> \<Longrightarrow> h_val (hrs_mem (g_hrs (globals_swap g_hrs g_hrs_upd symtab xs gs))) (PTR('b) (symtab s + offs)) = h_val (hrs_mem (g_hrs gs)) (PTR('b) (symtab s + offs)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>globals_list_distinct D symtab xs; unat offs + size_of TYPE('b) \<le> size_of TYPE('a)\<rbrakk> \<Longrightarrow> \<not> is_global_data (const_global_data s v)
 2. \<lbrakk>globals_list_distinct D symtab xs; const_global_data s v \<in> set xs; unat offs + size_of TYPE('b) \<le> size_of TYPE('a)\<rbrakk> \<Longrightarrow> s_footprint (PTR('b) (symtab s + offs)) \<subseteq> global_data_region symtab (const_global_data s v) \<times> UNIV proof (prove)
goal (1 subgoal):
 1. \<lbrakk>globals_list_distinct D symtab xs; const_global_data s v \<in> set xs; unat offs + size_of TYPE('b) \<le> size_of TYPE('a)\<rbrakk> \<Longrightarrow> s_footprint (PTR('b) (symtab s + offs)) \<subseteq> global_data_region symtab (const_global_data s v) \<times> UNIV proof (prove)
goal (1 subgoal):
 1. \<lbrakk>globals_list_distinct D symtab xs; const_global_data s v \<in> set xs; unat offs + size_of TYPE('b) \<le> size_of TYPE('a)\<rbrakk> \<Longrightarrow> {ptr_val (PTR('b) (symtab s + offs))..+size_of TYPE('b)} \<times> UNIV \<subseteq> global_data_region symtab (const_global_data s v) \<times> UNIV proof (prove)
goal (1 subgoal):
 1. \<lbrakk>globals_list_distinct D symtab xs; ConstGlobalData s (size_of TYPE('a)) (\<lambda>addr. c_guard (PTR('a) addr)) (to_bytes_p v) (\<lambda>xs. from_bytes xs = v) \<in> set xs; unat offs + size_of TYPE('b) \<le> size_of TYPE('a)\<rbrakk> \<Longrightarrow> {symtab s + offs..+size_of TYPE('b)} \<subseteq> {symtab s..+size_of TYPE('a)} proof (prove)
goal:
No subgoals!
theory GlobalsSwap

lemma global_data_implies_ptr_inverse_safe:
  "\<lbrakk>  global_data nm (accr :: 'a \<Rightarrow> ('b :: packed_type)) updr \<in> set glist;
        globals_list_distinct D symtab glist;
        globals_list_valid symtab t_hrs t_hrs_upd glist;
        htd_safe D htd
        \<rbrakk>
    \<Longrightarrow> ptr_inverse_safe (Ptr (symtab nm) :: 'b ptr) htd" apply (clarsimp simp add: ptr_inverse_safe_def globals_list_valid_def
                            htd_safe_def globals_list_distinct_def) apply (drule(1) bspec)+ apply (simp add: global_data_region_def global_data_ok_def global_data_def) apply (auto dest!: s_footprint_intvl_subset[THEN subsetD]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>global_data nm accr updr \<in> set glist; globals_list_distinct D symtab glist; globals_list_valid symtab t_hrs t_hrs_upd glist; htd_safe D htd\<rbrakk> \<Longrightarrow> ptr_inverse_safe (PTR('b) (symtab nm)) htd proof (prove)
goal (1 subgoal):
 1. \<lbrakk>global_data nm accr updr \<in> set glist; dom_s htd \<subseteq> D \<times> UNIV; \<forall>y\<in>set glist. D \<inter> global_data_region symtab y = {}; distinct_prop (\<lambda>S T. S \<inter> T = {}) (map (global_data_region symtab) glist); distinct_prop global_data_swappable glist; \<forall>x\<in>set glist. global_data_valid t_hrs t_hrs_upd x; \<forall>x\<in>set glist. global_data_ok symtab x\<rbrakk> \<Longrightarrow> c_guard (PTR('b) (symtab nm)) \<and> fst ` s_footprint (PTR('b) (symtab nm)) \<inter> fst ` dom_s htd = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>global_data nm accr updr \<in> set glist; dom_s htd \<subseteq> D \<times> UNIV; distinct_prop (\<lambda>S T. S \<inter> T = {}) (map (global_data_region symtab) glist); distinct_prop global_data_swappable glist; D \<inter> global_data_region symtab (global_data nm accr updr) = {}; global_data_valid t_hrs t_hrs_upd (global_data nm accr updr); global_data_ok symtab (global_data nm accr updr)\<rbrakk> \<Longrightarrow> c_guard (PTR('b) (symtab nm)) \<and> fst ` s_footprint (PTR('b) (symtab nm)) \<inter> fst ` dom_s htd = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>GlobalData nm (size_of TYPE('b)) (\<lambda>addr. c_guard (PTR('b) addr)) (to_bytes_p \<circ> accr) (updr \<circ> (\<lambda>x y. x) \<circ> from_bytes) \<in> set glist; dom_s htd \<subseteq> D \<times> UNIV; distinct_prop (\<lambda>S T. S \<inter> T = {}) (map (global_data_region symtab) glist); distinct_prop global_data_swappable glist; D \<inter> {symtab nm..+size_of TYPE('b)} = {}; global_data_valid t_hrs t_hrs_upd (GlobalData nm (size_of TYPE('b)) (\<lambda>addr. c_guard (PTR('b) addr)) (to_bytes_p \<circ> accr) (updr \<circ> (\<lambda>x y. x) \<circ> from_bytes)); c_guard (PTR('b) (symtab nm))\<rbrakk> \<Longrightarrow> fst ` s_footprint (PTR('b) (symtab nm)) \<inter> fst ` dom_s htd = {} proof (prove)
goal:
No subgoals!
theory BitFieldProofsLib

lemma word_and_t2_dist[simp]:
  "(a && b) * 2 = (a * 2) && (b * 2)" for a::"'a::len word" proof - have "a && b << 1 = (a << 1) && (b << 1)" by (simp only: shift_over_ao_dists) thus ?thesis by simp qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (a && b) * 2 = a * 2 && b * 2 proof (state)
goal (1 subgoal):
 1. (a && b) * 2 = a * 2 && b * 2 proof (prove)
goal (1 subgoal):
 1. a && b << 1 = (a << 1) && (b << 1) proof (state)
this:
a && b << 1 = (a << 1) && (b << 1)

goal (1 subgoal):
 1. (a && b) * 2 = a * 2 && b * 2 proof (prove)
using this:
a && b << 1 = (a << 1) && (b << 1)

goal (1 subgoal):
 1. (a && b) * 2 = a * 2 && b * 2 proof (state)
this:
(a && b) * 2 = a * 2 && b * 2

goal:
No subgoals!
theory BitFieldProofsLib

lemma word_t2_shiftr[simp]:
  "c \<le> 1 \<Longrightarrow> (a * 2) >> c = a && mask (size a - 1) << 1 - c" for a::"'a::len word" by (drule shiftl_shiftr1) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. c \<le> 1 \<Longrightarrow> a * 2 >> c = a && mask (size a - 1) << 1 - c
theory BitFieldProofsLib

lemma tag_eq_to_tag_masked_eq:
  "tag == v ==> tag && m = v && m" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tag \<equiv> v \<Longrightarrow> tag && m = v && m
theory BitFieldProofsLib

lemma clift_heap_update_footprint:
  "\<forall>p' :: 'a ptr. hrs_htd hp,g \<Turnstile>\<^sub>t p' \<longrightarrow> s_footprint p \<inter> s_footprint p' = {}
    \<Longrightarrow> (lift_t g (hrs_mem_update (heap_update p (v :: 'b :: wf_type)) hp)
        :: ('a :: mem_type) typ_heap) = lift_t g hp" apply (cases hp, simp add: lift_t_if fun_eq_iff hrs_mem_update_def hrs_htd_def) apply clarsimp apply (drule spec, drule(1) mp) apply (simp add: h_val_def heap_update_def) apply (subst heap_list_update_disjoint_same, simp_all) apply (simp add: set_eq_iff s_footprint_intvl[symmetric]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>p'. hrs_htd hp,g \<Turnstile>\<^sub>t p' \<longrightarrow> s_footprint p \<inter> s_footprint p' = {} \<Longrightarrow> lift_t g (hrs_mem_update (heap_update p v) hp) = lift_t g hp proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>p'. b,g \<Turnstile>\<^sub>t p' \<longrightarrow> s_footprint p \<inter> s_footprint p' = {}; hp = (a, b)\<rbrakk> \<Longrightarrow> \<forall>x. b,g \<Turnstile>\<^sub>t x \<longrightarrow> h_val (heap_update p v a) x = h_val a x proof (prove)
goal (1 subgoal):
 1. \<And>a b x. \<lbrakk>\<forall>p'. b,g \<Turnstile>\<^sub>t p' \<longrightarrow> s_footprint p \<inter> s_footprint p' = {}; hp = (a, b); b,g \<Turnstile>\<^sub>t x\<rbrakk> \<Longrightarrow> h_val (heap_update p v a) x = h_val a x proof (prove)
goal (1 subgoal):
 1. \<And>a b x. \<lbrakk>hp = (a, b); b,g \<Turnstile>\<^sub>t x; s_footprint p \<inter> s_footprint x = {}\<rbrakk> \<Longrightarrow> h_val (heap_update p v a) x = h_val a x proof (prove)
goal (1 subgoal):
 1. \<And>a b x. \<lbrakk>hp = (a, b); b,g \<Turnstile>\<^sub>t x; s_footprint p \<inter> s_footprint x = {}\<rbrakk> \<Longrightarrow> from_bytes (heap_list (heap_update_list (ptr_val p) (to_bytes v (heap_list a (size_of TYPE('b)) (ptr_val p))) a) (size_of TYPE('a)) (ptr_val x)) = from_bytes (heap_list a (size_of TYPE('a)) (ptr_val x)) proof (prove)
goal (1 subgoal):
 1. \<And>a b x. \<lbrakk>hp = (a, b); b,g \<Turnstile>\<^sub>t x; s_footprint p \<inter> s_footprint x = {}\<rbrakk> \<Longrightarrow> {ptr_val p..+size_of TYPE('b)} \<inter> {ptr_val x..+size_of TYPE('a)} = {} proof (prove)
goal:
No subgoals!
theory BitFieldProofsLib

lemma s_footprint_field_lvalue_disj_helper:
  "field_lookup (typ_info_t TYPE('b::mem_type)) f 0 = Some (ti,b)
      \<Longrightarrow> export_uinfo ti = typ_uinfo_t TYPE('a)
      \<Longrightarrow> (\<forall>x. P x \<longrightarrow> s_footprint (p::'b ptr) \<inter> S x = {})
      \<Longrightarrow> (\<forall>x. P x \<longrightarrow> s_footprint ((Ptr &(p\<rightarrow>f))::'a::mem_type ptr) \<inter> S x = {})" apply (drule field_lookup_export_uinfo_Some) apply simp apply (drule field_ti_s_sub_typ) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>field_lookup (typ_info_t TYPE('b)) f 0 = Some (ti, b); export_uinfo ti = typ_uinfo_t TYPE('a); \<forall>x. P x \<longrightarrow> s_footprint p \<inter> S x = {}\<rbrakk> \<Longrightarrow> \<forall>x. P x \<longrightarrow> s_footprint (PTR('a) &(p\<rightarrow>f)) \<inter> S x = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>export_uinfo ti = typ_uinfo_t TYPE('a); \<forall>x. P x \<longrightarrow> s_footprint p \<inter> S x = {}; field_lookup (export_uinfo (typ_info_t TYPE('b))) f 0 = Some (export_uinfo ti, b)\<rbrakk> \<Longrightarrow> \<forall>x. P x \<longrightarrow> s_footprint (PTR('a) &(p\<rightarrow>f)) \<inter> S x = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>export_uinfo ti = typ_uinfo_t TYPE('a); \<forall>x. P x \<longrightarrow> s_footprint p \<inter> S x = {}; field_lookup (export_uinfo (typ_info_t TYPE('b))) f 0 = Some (typ_uinfo_t TYPE('a), b)\<rbrakk> \<Longrightarrow> \<forall>x. P x \<longrightarrow> s_footprint (PTR('a) &(p\<rightarrow>f)) \<inter> S x = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>export_uinfo ti = typ_uinfo_t TYPE('a); \<forall>x. P x \<longrightarrow> s_footprint p \<inter> S x = {}; s_footprint (PTR('a) &(?p2\<rightarrow>f)) \<subseteq> s_footprint ?p2\<rbrakk> \<Longrightarrow> \<forall>x. P x \<longrightarrow> s_footprint (PTR('a) &(p\<rightarrow>f)) \<inter> S x = {} proof (prove)
goal:
No subgoals!
theory KernelState_C

lemma cslift_def: "is_an_abbreviation" by (simp add: is_an_abbreviation_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_an_abbreviation
theory structures_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 structures_defs

lemma cap_get_tag_eq_x:
  "(cap_get_tag c = x) = ((if ((x << 0) AND 0xe \<noteq> 0xe)
      then ((index (cap_C.words_C c) 0) >> 0) AND mask 4
      else ((index (cap_C.words_C c) 0) >> 0) AND mask 8) = x)" by (auto simp add: cap_get_tag_def mask_def word_bw_assocs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (cap_get_tag c = x) = ((if (x << 0) && 0xE \<noteq> 0xE then (cap_C.words_C c.[0] >> 0) && mask 4 else (cap_C.words_C c.[0] >> 0) && mask 8) = x)
theory structures_defs

lemma cap_irq_control_cap_tag_mask_helpers:
  "w && 0xff = 0xe \<Longrightarrow> w && 0xf = 0xe" by (auto elim: word_sub_mask simp: mask_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. w && 0xFF = 0xE \<Longrightarrow> w && 0xF = 0xE
theory structures_defs

lemma cap_irq_handler_cap_tag_mask_helpers:
  "w && 0xff = 0x1e \<Longrightarrow> w && 0xf = 0xe" by (auto elim: word_sub_mask simp: mask_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. w && 0xFF = 0x1E \<Longrightarrow> w && 0xF = 0xE
theory structures_defs

lemma cap_zombie_cap_tag_mask_helpers:
  "w && 0xff = 0x2e \<Longrightarrow> w && 0xf = 0xe" by (auto elim: word_sub_mask simp: mask_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. w && 0xFF = 0x2E \<Longrightarrow> w && 0xF = 0xE
theory structures_defs

lemma cap_domain_cap_tag_mask_helpers:
  "w && 0xff = 0x3e \<Longrightarrow> w && 0xf = 0xe" by (auto elim: word_sub_mask simp: mask_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. w && 0xFF = 0x3E \<Longrightarrow> w && 0xF = 0xE
theory structures_defs

lemma cap_lift_null_cap:
  "cap_get_tag cap = scast cap_null_cap \<Longrightarrow>
  cap_lift cap =
  Some (Cap_null_cap)" by (simp add:cap_lift_def cap_tag_defs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_null_cap \<Longrightarrow> cap_lift cap = Some Cap_null_cap
theory structures_defs

lemma cap_lift_untyped_cap:
  "cap_get_tag cap = scast cap_untyped_cap \<Longrightarrow>
  cap_lift cap =
  Some (Cap_untyped_cap \<lparr> 
       cap_untyped_cap_CL.capFreeIndex_CL = (((index (cap_C.words_C cap) 1) >> 6) AND mask 26),
       cap_untyped_cap_CL.capIsDevice_CL = (((index (cap_C.words_C cap) 1) >> 5) AND mask 1),
       cap_untyped_cap_CL.capBlockSize_CL = (((index (cap_C.words_C cap) 1) >> 0) AND mask 5),
       cap_untyped_cap_CL.capPtr_CL = (((index (cap_C.words_C cap) 0) << 0) AND NOT (mask 4)) \<rparr>)" by (simp add:cap_lift_def cap_tag_defs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<Longrightarrow> cap_lift cap = Some (Cap_untyped_cap \<lparr>capFreeIndex_CL = (cap_C.words_C cap.[1] >> 6) && mask 26, capIsDevice_CL = (cap_C.words_C cap.[1] >> 5) && mask 1, capBlockSize_CL = (cap_C.words_C cap.[1] >> 0) && mask 5, capPtr_CL = (cap_C.words_C cap.[0] << 0) && ~~ mask 4\<rparr>)
theory structures_defs

lemma cap_lift_endpoint_cap:
  "cap_get_tag cap = scast cap_endpoint_cap \<Longrightarrow>
  cap_lift cap =
  Some (Cap_endpoint_cap \<lparr> 
       cap_endpoint_cap_CL.capEPBadge_CL = (((index (cap_C.words_C cap) 0) >> 4) AND mask 28),
       cap_endpoint_cap_CL.capCanGrantReply_CL = (((index (cap_C.words_C cap) 1) >> 3) AND mask 1),
       cap_endpoint_cap_CL.capCanGrant_CL = (((index (cap_C.words_C cap) 1) >> 2) AND mask 1),
       cap_endpoint_cap_CL.capCanSend_CL = (((index (cap_C.words_C cap) 1) >> 0) AND mask 1),
       cap_endpoint_cap_CL.capCanReceive_CL = (((index (cap_C.words_C cap) 1) >> 1) AND mask 1),
       cap_endpoint_cap_CL.capEPPtr_CL = (((index (cap_C.words_C cap) 1) << 0) AND NOT (mask 4)) \<rparr>)" by (simp add:cap_lift_def cap_tag_defs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap \<Longrightarrow> cap_lift cap = Some (Cap_endpoint_cap \<lparr>capEPBadge_CL = (cap_C.words_C cap.[0] >> 4) && mask 28, capCanGrantReply_CL = (cap_C.words_C cap.[1] >> 3) && mask 1, capCanGrant_CL = (cap_C.words_C cap.[1] >> 2) && mask 1, capCanSend_CL = (cap_C.words_C cap.[1] >> 0) && mask 1, capCanReceive_CL = (cap_C.words_C cap.[1] >> 1) && mask 1, capEPPtr_CL = (cap_C.words_C cap.[1] << 0) && ~~ mask 4\<rparr>)
theory structures_defs

lemma cap_lift_notification_cap:
  "cap_get_tag cap = scast cap_notification_cap \<Longrightarrow>
  cap_lift cap =
  Some (Cap_notification_cap \<lparr> 
       cap_notification_cap_CL.capNtfnBadge_CL = (((index (cap_C.words_C cap) 1) >> 4) AND mask 28),
       cap_notification_cap_CL.capNtfnCanReceive_CL = (((index (cap_C.words_C cap) 1) >> 1) AND mask 1),
       cap_notification_cap_CL.capNtfnCanSend_CL = (((index (cap_C.words_C cap) 1) >> 0) AND mask 1),
       cap_notification_cap_CL.capNtfnPtr_CL = (((index (cap_C.words_C cap) 0) << 0) AND NOT (mask 4)) \<rparr>)" by (simp add:cap_lift_def cap_tag_defs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_notification_cap \<Longrightarrow> cap_lift cap = Some (Cap_notification_cap \<lparr>capNtfnBadge_CL = (cap_C.words_C cap.[1] >> 4) && mask 28, capNtfnCanReceive_CL = (cap_C.words_C cap.[1] >> 1) && mask 1, capNtfnCanSend_CL = (cap_C.words_C cap.[1] >> 0) && mask 1, capNtfnPtr_CL = (cap_C.words_C cap.[0] << 0) && ~~ mask 4\<rparr>)
theory structures_defs

lemma cap_lift_reply_cap:
  "cap_get_tag cap = scast cap_reply_cap \<Longrightarrow>
  cap_lift cap =
  Some (Cap_reply_cap \<lparr> 
       cap_reply_cap_CL.capReplyCanGrant_CL = (((index (cap_C.words_C cap) 0) >> 5) AND mask 1),
       cap_reply_cap_CL.capReplyMaster_CL = (((index (cap_C.words_C cap) 0) >> 4) AND mask 1),
       cap_reply_cap_CL.capTCBPtr_CL = (((index (cap_C.words_C cap) 0) << 0) AND NOT (mask 6)) \<rparr>)" by (simp add:cap_lift_def cap_tag_defs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_reply_cap \<Longrightarrow> cap_lift cap = Some (Cap_reply_cap \<lparr>capReplyCanGrant_CL = (cap_C.words_C cap.[0] >> 5) && mask 1, capReplyMaster_CL = (cap_C.words_C cap.[0] >> 4) && mask 1, capTCBPtr_CL = (cap_C.words_C cap.[0] << 0) && ~~ mask 6\<rparr>)
theory structures_defs

lemma cap_lift_cnode_cap:
  "cap_get_tag cap = scast cap_cnode_cap \<Longrightarrow>
  cap_lift cap =
  Some (Cap_cnode_cap \<lparr> 
       cap_cnode_cap_CL.capCNodeRadix_CL = (((index (cap_C.words_C cap) 1) >> 18) AND mask 5),
       cap_cnode_cap_CL.capCNodeGuardSize_CL = (((index (cap_C.words_C cap) 1) >> 23) AND mask 5),
       cap_cnode_cap_CL.capCNodeGuard_CL = (((index (cap_C.words_C cap) 1) >> 0) AND mask 18),
       cap_cnode_cap_CL.capCNodePtr_CL = (((index (cap_C.words_C cap) 0) << 0) AND NOT (mask 5)) \<rparr>)" by (simp add:cap_lift_def cap_tag_defs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_cnode_cap \<Longrightarrow> cap_lift cap = Some (Cap_cnode_cap \<lparr>capCNodeRadix_CL = (cap_C.words_C cap.[1] >> 18) && mask 5, capCNodeGuardSize_CL = (cap_C.words_C cap.[1] >> 23) && mask 5, capCNodeGuard_CL = (cap_C.words_C cap.[1] >> 0) && mask 18, capCNodePtr_CL = (cap_C.words_C cap.[0] << 0) && ~~ mask 5\<rparr>)
theory structures_defs

lemma cap_lift_thread_cap:
  "cap_get_tag cap = scast cap_thread_cap \<Longrightarrow>
  cap_lift cap =
  Some (Cap_thread_cap \<lparr> 
       cap_thread_cap_CL.capTCBPtr_CL = (((index (cap_C.words_C cap) 0) << 0) AND NOT (mask 4)) \<rparr>)" by (simp add:cap_lift_def cap_tag_defs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_thread_cap \<Longrightarrow> cap_lift cap = Some (Cap_thread_cap \<lparr>cap_thread_cap_CL.capTCBPtr_CL = (cap_C.words_C cap.[0] << 0) && ~~ mask 4\<rparr>)
theory structures_defs

lemma cap_lift_frame_cap:
  "cap_get_tag cap = scast cap_frame_cap \<Longrightarrow>
  cap_lift cap =
  Some (Cap_frame_cap \<lparr> 
       cap_frame_cap_CL.capFSize_CL = (((index (cap_C.words_C cap) 1) >> 30) AND mask 2),
       cap_frame_cap_CL.capFMappedASIDLow_CL = (((index (cap_C.words_C cap) 1) >> 20) AND mask 10),
       cap_frame_cap_CL.capFVMRights_CL = (((index (cap_C.words_C cap) 1) >> 18) AND mask 2),
       cap_frame_cap_CL.capFMappedAddress_CL = (((index (cap_C.words_C cap) 1) << 14) AND NOT (mask 14)),
       cap_frame_cap_CL.capFIsDevice_CL = (((index (cap_C.words_C cap) 0) >> 29) AND mask 1),
       cap_frame_cap_CL.capFMappedASIDHigh_CL = (((index (cap_C.words_C cap) 0) >> 22) AND mask 7),
       cap_frame_cap_CL.capFBasePtr_CL = (((index (cap_C.words_C cap) 0) << 10) AND NOT (mask 14)) \<rparr>)" by (simp add:cap_lift_def cap_tag_defs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap \<Longrightarrow> cap_lift cap = Some (Cap_frame_cap \<lparr>capFSize_CL = (cap_C.words_C cap.[1] >> 30) && mask 2, capFMappedASIDLow_CL = (cap_C.words_C cap.[1] >> 20) && mask 10, capFVMRights_CL = (cap_C.words_C cap.[1] >> 18) && mask 2, capFMappedAddress_CL = (cap_C.words_C cap.[1] << 14) && ~~ mask 14, capFIsDevice_CL = (cap_C.words_C cap.[0] >> 29) && mask 1, capFMappedASIDHigh_CL = (cap_C.words_C cap.[0] >> 22) && mask 7, capFBasePtr_CL = (cap_C.words_C cap.[0] << 10) && ~~ mask 14\<rparr>)
theory structures_defs

lemma cap_lift_asid_pool_cap:
  "cap_get_tag cap = scast cap_asid_pool_cap \<Longrightarrow>
  cap_lift cap =
  Some (Cap_asid_pool_cap \<lparr> 
       cap_asid_pool_cap_CL.capASIDBase_CL = (((index (cap_C.words_C cap) 1) >> 0) AND mask 17),
       cap_asid_pool_cap_CL.capASIDPool_CL = (((index (cap_C.words_C cap) 0) << 0) AND NOT (mask 4)) \<rparr>)" by (simp add:cap_lift_def cap_tag_defs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_asid_pool_cap \<Longrightarrow> cap_lift cap = Some (Cap_asid_pool_cap \<lparr>capASIDBase_CL = (cap_C.words_C cap.[1] >> 0) && mask 17, capASIDPool_CL = (cap_C.words_C cap.[0] << 0) && ~~ mask 4\<rparr>)
theory structures_defs

lemma cap_lift_page_table_cap:
  "cap_get_tag cap = scast cap_page_table_cap \<Longrightarrow>
  cap_lift cap =
  Some (Cap_page_table_cap \<lparr> 
       cap_page_table_cap_CL.capPTIsMapped_CL = (((index (cap_C.words_C cap) 1) >> 29) AND mask 1),
       cap_page_table_cap_CL.capPTMappedASID_CL = (((index (cap_C.words_C cap) 1) >> 12) AND mask 17),
       cap_page_table_cap_CL.capPTMappedAddress_CL = (((index (cap_C.words_C cap) 1) << 20) AND NOT (mask 20)),
       cap_page_table_cap_CL.capPTBasePtr_CL = (((index (cap_C.words_C cap) 0) << 0) AND NOT (mask 10)) \<rparr>)" by (simp add:cap_lift_def cap_tag_defs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_page_table_cap \<Longrightarrow> cap_lift cap = Some (Cap_page_table_cap \<lparr>capPTIsMapped_CL = (cap_C.words_C cap.[1] >> 29) && mask 1, capPTMappedASID_CL = (cap_C.words_C cap.[1] >> 12) && mask 17, capPTMappedAddress_CL = (cap_C.words_C cap.[1] << 20) && ~~ mask 20, capPTBasePtr_CL = (cap_C.words_C cap.[0] << 0) && ~~ mask 10\<rparr>)
theory structures_defs

lemma cap_lift_page_directory_cap:
  "cap_get_tag cap = scast cap_page_directory_cap \<Longrightarrow>
  cap_lift cap =
  Some (Cap_page_directory_cap \<lparr> 
       cap_page_directory_cap_CL.capPDMappedASID_CL = (((index (cap_C.words_C cap) 1) >> 0) AND mask 17),
       cap_page_directory_cap_CL.capPDIsMapped_CL = (((index (cap_C.words_C cap) 0) >> 4) AND mask 1),
       cap_page_directory_cap_CL.capPDBasePtr_CL = (((index (cap_C.words_C cap) 0) << 0) AND NOT (mask 14)) \<rparr>)" by (simp add:cap_lift_def cap_tag_defs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<Longrightarrow> cap_lift cap = Some (Cap_page_directory_cap \<lparr>capPDMappedASID_CL = (cap_C.words_C cap.[1] >> 0) && mask 17, capPDIsMapped_CL = (cap_C.words_C cap.[0] >> 4) && mask 1, capPDBasePtr_CL = (cap_C.words_C cap.[0] << 0) && ~~ mask 14\<rparr>)
theory structures_defs

lemma cap_lift_asid_control_cap:
  "cap_get_tag cap = scast cap_asid_control_cap \<Longrightarrow>
  cap_lift cap =
  Some (Cap_asid_control_cap)" by (simp add:cap_lift_def cap_tag_defs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_asid_control_cap \<Longrightarrow> cap_lift cap = Some Cap_asid_control_cap