kings-crown/FVELER_Isabelle huggingface dataset:
theory structures_proofs

lemma (in kernel_all_substitute) mdb_node_get_mdbNext_spec:
  "\<forall>s. \<Gamma> \<turnstile> {s}
       \<acute>ret__unsigned :== PROC mdb_node_get_mdbNext(\<acute>mdb_node)
       \<lbrace>\<acute>ret__unsigned = mdb_node_CL.mdbNext_CL (mdb_node_lift \<^bsup>s\<^esup>mdb_node)\<rbrace>" apply (rule allI, rule conseqPre, vcg) apply clarsimp apply (simp add: mdb_node_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 mdb_node_get_mdbNext_'proc \<lbrace>\<acute>ret__unsigned = mdbNext_CL (mdb_node_lift \<^bsup>s\<^esup>mdb_node)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. {s} \<subseteq> \<lbrace>\<forall>v. 0 \<le>s 0 \<and> 0 <s 0x20 \<and> 1 <s 2 \<and> 0 \<le>s 1 \<and> ((if False then 1 else 0) \<noteq> 0 \<longrightarrow> 0 \<le>s 0x1F \<and> 0x1F <s 0x20 \<and> ((if (mdb_node_C.words_C \<acute>mdb_node.[unat 1] && 0xFFFFFFF8 << unat 0) && (1 << unat 0x1F) \<noteq> 0 then 1 else 0) \<noteq> 0 \<longrightarrow> (mdb_node_C.words_C \<acute>mdb_node.[unat 1] && 0xFFFFFFF8 << unat 0) || SCAST(32 signed \<rightarrow> 32) 0 = mdbNext_CL (mdb_node_lift \<^bsup>s\<^esup>mdb_node)) \<and> ((if (mdb_node_C.words_C \<acute>mdb_node.[unat 1] && 0xFFFFFFF8 << unat 0) && (1 << unat 0x1F) \<noteq> 0 then 1 else 0) = 0 \<longrightarrow> mdb_node_C.words_C \<acute>mdb_node.[unat 1] && 0xFFFFFFF8 << unat 0 = mdbNext_CL (mdb_node_lift \<^bsup>s\<^esup>mdb_node))) \<and> ((if False then 1 else 0) = 0 \<longrightarrow> mdb_node_C.words_C \<acute>mdb_node.[unat 1] && 0xFFFFFFF8 << unat 0 = mdbNext_CL (mdb_node_lift \<^bsup>s\<^esup>mdb_node))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. mdb_node_C.words_C (mdb_node_' s).[Suc 0] && 0xFFFFFFF8 = mdbNext_CL (mdb_node_lift (mdb_node_' s)) proof (prove)
goal:
No subgoals! proof (prove)
goal:
No subgoals!
theory structures_proofs

lemma (in kernel_all_substitute) mdb_node_get_mdbRevocable_spec:
  "\<forall>s. \<Gamma> \<turnstile> {s}
       \<acute>ret__unsigned :== PROC mdb_node_get_mdbRevocable(\<acute>mdb_node)
       \<lbrace>\<acute>ret__unsigned = mdb_node_CL.mdbRevocable_CL (mdb_node_lift \<^bsup>s\<^esup>mdb_node)\<rbrace>" apply (rule allI, rule conseqPre, vcg) apply clarsimp apply (simp add: mdb_node_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 mdb_node_get_mdbRevocable_'proc \<lbrace>\<acute>ret__unsigned = mdbRevocable_CL (mdb_node_lift \<^bsup>s\<^esup>mdb_node)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. {s} \<subseteq> \<lbrace>\<forall>v. 0 \<le>s 1 \<and> 1 <s 0x20 \<and> 1 <s 2 \<and> 0 \<le>s 1 \<and> ((if False then 1 else 0) \<noteq> 0 \<longrightarrow> 0 \<le>s 0x1F \<and> 0x1F <s 0x20 \<and> ((if (mdb_node_C.words_C \<acute>mdb_node.[unat 1] && 2 >> unat 1) && (1 << unat 0x1F) \<noteq> 0 then 1 else 0) \<noteq> 0 \<longrightarrow> (mdb_node_C.words_C \<acute>mdb_node.[unat 1] && 2 >> unat 1) || SCAST(32 signed \<rightarrow> 32) 0 = mdbRevocable_CL (mdb_node_lift \<^bsup>s\<^esup>mdb_node)) \<and> ((if (mdb_node_C.words_C \<acute>mdb_node.[unat 1] && 2 >> unat 1) && (1 << unat 0x1F) \<noteq> 0 then 1 else 0) = 0 \<longrightarrow> mdb_node_C.words_C \<acute>mdb_node.[unat 1] && 2 >> unat 1 = mdbRevocable_CL (mdb_node_lift \<^bsup>s\<^esup>mdb_node))) \<and> ((if False then 1 else 0) = 0 \<longrightarrow> mdb_node_C.words_C \<acute>mdb_node.[unat 1] && 2 >> unat 1 = mdbRevocable_CL (mdb_node_lift \<^bsup>s\<^esup>mdb_node))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. mdb_node_C.words_C (mdb_node_' s).[Suc 0] && 2 >> Suc 0 = mdbRevocable_CL (mdb_node_lift (mdb_node_' s)) proof (prove)
goal:
No subgoals! proof (prove)
goal:
No subgoals!
theory structures_proofs

lemma (in kernel_all_substitute) mdb_node_set_mdbRevocable_spec:
  "\<forall>s. \<Gamma> \<turnstile> {s}
       \<acute>ret__struct_mdb_node_C :== PROC mdb_node_set_mdbRevocable(\<acute>mdb_node, \<acute>v32)
       \<lbrace>mdb_node_lift \<acute>ret__struct_mdb_node_C = mdb_node_lift \<^bsup>s\<^esup>mdb_node \<lparr> mdb_node_CL.mdbRevocable_CL :=  (\<^bsup>s\<^esup>v32 AND mask 1) \<rparr>\<rbrace>" apply(rule allI, rule conseqPre, vcg) apply (clarsimp simp: guard_simps ucast_id
                        mdb_node_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 mdb_node_set_mdbRevocable_'proc \<lbrace>mdb_node_lift \<acute>ret__struct_mdb_node_C = mdb_node_lift \<^bsup>s\<^esup>mdb_node\<lparr>mdbRevocable_CL := \<^bsup>s\<^esup>v32 && mask 1\<rparr>\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. {s} \<subseteq> \<lbrace>1 <s 2 \<and> 0 \<le>s 1 \<and> 1 <s 2 \<and> 0 \<le>s 1 \<and> 1 <s 2 \<and> 0 \<le>s 1 \<and> 1 <s 0x20 \<and> 1 <s 2 \<and> 0 \<le>s 1 \<and> mdb_node_lift (mdb_node_C.words_C_update (\<lambda>v. Arrays.update v (unat 1) (v.[unat 1] || (\<acute>v32 << unat 1) && 2)) (mdb_node_C.words_C_update (\<lambda>v. Arrays.update v (unat 1) (v.[unat 1] && ~~ 2)) \<acute>mdb_node)) = mdb_node_lift \<^bsup>s\<^esup>mdb_node\<lparr>mdbRevocable_CL := \<^bsup>s\<^esup>v32 && mask 1\<rparr>\<rbrace> proof (prove)
goal:
No subgoals! proof (prove)
goal:
No subgoals!
theory structures_proofs

lemma (in kernel_all_substitute) mdb_node_get_mdbFirstBadged_spec:
  "\<forall>s. \<Gamma> \<turnstile> {s}
       \<acute>ret__unsigned :== PROC mdb_node_get_mdbFirstBadged(\<acute>mdb_node)
       \<lbrace>\<acute>ret__unsigned = mdb_node_CL.mdbFirstBadged_CL (mdb_node_lift \<^bsup>s\<^esup>mdb_node)\<rbrace>" apply (rule allI, rule conseqPre, vcg) apply clarsimp apply (simp add: mdb_node_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 mdb_node_get_mdbFirstBadged_'proc \<lbrace>\<acute>ret__unsigned = mdbFirstBadged_CL (mdb_node_lift \<^bsup>s\<^esup>mdb_node)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. {s} \<subseteq> \<lbrace>\<forall>v. 0 \<le>s 0 \<and> 0 <s 0x20 \<and> 1 <s 2 \<and> 0 \<le>s 1 \<and> ((if False then 1 else 0) \<noteq> 0 \<longrightarrow> 0 \<le>s 0x1F \<and> 0x1F <s 0x20 \<and> ((if (mdb_node_C.words_C \<acute>mdb_node.[unat 1] && 1 >> unat 0) && (1 << unat 0x1F) \<noteq> 0 then 1 else 0) \<noteq> 0 \<longrightarrow> (mdb_node_C.words_C \<acute>mdb_node.[unat 1] && 1 >> unat 0) || SCAST(32 signed \<rightarrow> 32) 0 = mdbFirstBadged_CL (mdb_node_lift \<^bsup>s\<^esup>mdb_node)) \<and> ((if (mdb_node_C.words_C \<acute>mdb_node.[unat 1] && 1 >> unat 0) && (1 << unat 0x1F) \<noteq> 0 then 1 else 0) = 0 \<longrightarrow> mdb_node_C.words_C \<acute>mdb_node.[unat 1] && 1 >> unat 0 = mdbFirstBadged_CL (mdb_node_lift \<^bsup>s\<^esup>mdb_node))) \<and> ((if False then 1 else 0) = 0 \<longrightarrow> mdb_node_C.words_C \<acute>mdb_node.[unat 1] && 1 >> unat 0 = mdbFirstBadged_CL (mdb_node_lift \<^bsup>s\<^esup>mdb_node))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. mdb_node_C.words_C (mdb_node_' s).[Suc 0] && 1 = mdbFirstBadged_CL (mdb_node_lift (mdb_node_' s)) proof (prove)
goal:
No subgoals! proof (prove)
goal:
No subgoals!
theory structures_proofs

lemma (in kernel_all_substitute) mdb_node_set_mdbFirstBadged_spec:
  "\<forall>s. \<Gamma> \<turnstile> {s}
       \<acute>ret__struct_mdb_node_C :== PROC mdb_node_set_mdbFirstBadged(\<acute>mdb_node, \<acute>v32)
       \<lbrace>mdb_node_lift \<acute>ret__struct_mdb_node_C = mdb_node_lift \<^bsup>s\<^esup>mdb_node \<lparr> mdb_node_CL.mdbFirstBadged_CL :=  (\<^bsup>s\<^esup>v32 AND mask 1) \<rparr>\<rbrace>" apply(rule allI, rule conseqPre, vcg) apply (clarsimp simp: guard_simps ucast_id
                        mdb_node_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 mdb_node_set_mdbFirstBadged_'proc \<lbrace>mdb_node_lift \<acute>ret__struct_mdb_node_C = mdb_node_lift \<^bsup>s\<^esup>mdb_node\<lparr>mdbFirstBadged_CL := \<^bsup>s\<^esup>v32 && mask 1\<rparr>\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. {s} \<subseteq> \<lbrace>1 <s 2 \<and> 0 \<le>s 1 \<and> 1 <s 2 \<and> 0 \<le>s 1 \<and> 1 <s 2 \<and> 0 \<le>s 1 \<and> 0 \<le>s 0 \<and> 0 <s 0x20 \<and> 1 <s 2 \<and> 0 \<le>s 1 \<and> mdb_node_lift (mdb_node_C.words_C_update (\<lambda>v. Arrays.update v (unat 1) (v.[unat 1] || (\<acute>v32 << unat 0) && 1)) (mdb_node_C.words_C_update (\<lambda>v. Arrays.update v (unat 1) (v.[unat 1] && ~~ 1)) \<acute>mdb_node)) = mdb_node_lift \<^bsup>s\<^esup>mdb_node\<lparr>mdbFirstBadged_CL := \<^bsup>s\<^esup>v32 && mask 1\<rparr>\<rbrace> proof (prove)
goal:
No subgoals! proof (prove)
goal:
No subgoals!
theory structures_proofs

lemma (in kernel_all_substitute) mdb_node_get_mdbPrev_spec:
  "\<forall>s. \<Gamma> \<turnstile> {s}
       \<acute>ret__unsigned :== PROC mdb_node_get_mdbPrev(\<acute>mdb_node)
       \<lbrace>\<acute>ret__unsigned = mdb_node_CL.mdbPrev_CL (mdb_node_lift \<^bsup>s\<^esup>mdb_node)\<rbrace>" apply (rule allI, rule conseqPre, vcg) apply clarsimp apply (simp add: mdb_node_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 mdb_node_get_mdbPrev_'proc \<lbrace>\<acute>ret__unsigned = mdbPrev_CL (mdb_node_lift \<^bsup>s\<^esup>mdb_node)\<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 2 \<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 (mdb_node_C.words_C \<acute>mdb_node.[unat 0] && 0xFFFFFFF8 << unat 0) && (1 << unat 0x1F) \<noteq> 0 then 1 else 0) \<noteq> 0 \<longrightarrow> (mdb_node_C.words_C \<acute>mdb_node.[unat 0] && 0xFFFFFFF8 << unat 0) || SCAST(32 signed \<rightarrow> 32) 0 = mdbPrev_CL (mdb_node_lift \<^bsup>s\<^esup>mdb_node)) \<and> ((if (mdb_node_C.words_C \<acute>mdb_node.[unat 0] && 0xFFFFFFF8 << unat 0) && (1 << unat 0x1F) \<noteq> 0 then 1 else 0) = 0 \<longrightarrow> mdb_node_C.words_C \<acute>mdb_node.[unat 0] && 0xFFFFFFF8 << unat 0 = mdbPrev_CL (mdb_node_lift \<^bsup>s\<^esup>mdb_node))) \<and> ((if False then 1 else 0) = 0 \<longrightarrow> mdb_node_C.words_C \<acute>mdb_node.[unat 0] && 0xFFFFFFF8 << unat 0 = mdbPrev_CL (mdb_node_lift \<^bsup>s\<^esup>mdb_node))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. mdb_node_C.words_C (mdb_node_' s).[0] && 0xFFFFFFF8 = mdbPrev_CL (mdb_node_lift (mdb_node_' s)) proof (prove)
goal:
No subgoals! proof (prove)
goal:
No subgoals!
theory structures_proofs

lemma (in kernel_all_substitute) mdb_node_set_mdbPrev_spec:
  "\<forall>s. \<Gamma> \<turnstile> {s}
       \<acute>ret__struct_mdb_node_C :== PROC mdb_node_set_mdbPrev(\<acute>mdb_node, \<acute>v32)
       \<lbrace>mdb_node_lift \<acute>ret__struct_mdb_node_C = mdb_node_lift \<^bsup>s\<^esup>mdb_node \<lparr> mdb_node_CL.mdbPrev_CL :=  (\<^bsup>s\<^esup>v32 AND NOT (mask 3)) \<rparr>\<rbrace>" apply(rule allI, rule conseqPre, vcg) apply (clarsimp simp: guard_simps ucast_id
                        mdb_node_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 mdb_node_set_mdbPrev_'proc \<lbrace>mdb_node_lift \<acute>ret__struct_mdb_node_C = mdb_node_lift \<^bsup>s\<^esup>mdb_node\<lparr>mdbPrev_CL := \<^bsup>s\<^esup>v32 && ~~ mask 3\<rparr>\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. {s} \<subseteq> \<lbrace>0 <s 2 \<and> 0 \<le>s 0 \<and> 0 <s 2 \<and> 0 \<le>s 0 \<and> 0 <s 2 \<and> 0 \<le>s 0 \<and> 0 <s 0x20 \<and> 0 <s 2 \<and> 0 \<le>s 0 \<and> mdb_node_lift (mdb_node_C.words_C_update (\<lambda>v. Arrays.update v (unat 0) (v.[unat 0] || (\<acute>v32 >> unat 0) && 0xFFFFFFF8)) (mdb_node_C.words_C_update (\<lambda>v. Arrays.update v (unat 0) (v.[unat 0] && ~~ 0xFFFFFFF8)) \<acute>mdb_node)) = mdb_node_lift \<^bsup>s\<^esup>mdb_node\<lparr>mdbPrev_CL := \<^bsup>s\<^esup>v32 && ~~ mask 3\<rparr>\<rbrace> proof (prove)
goal:
No subgoals! proof (prove)
goal:
No subgoals!
theory structures_proofs

lemma notification_ptr_words_NULL:
  "c_guard (p::notification_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 notification_ptr_words_aligned:
  "c_guard (p::notification_C ptr) \<Longrightarrow>
   ptr_aligned ((Ptr &(p\<rightarrow>[''words_C'']))::((word32[4]) 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[4]) &(p\<rightarrow>[''words_C'']))
theory structures_proofs

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

lemma stored_hw_asid_ptr_words_NULL:
  "c_guard (p::stored_hw_asid_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 stored_hw_asid_ptr_words_aligned:
  "c_guard (p::stored_hw_asid_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 stored_hw_asid_ptr_words_ptr_safe:
  "ptr_safe (p::stored_hw_asid_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 thread_state_ptr_words_NULL:
  "c_guard (p::thread_state_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 thread_state_ptr_words_aligned:
  "c_guard (p::thread_state_C ptr) \<Longrightarrow>
   ptr_aligned ((Ptr &(p\<rightarrow>[''words_C'']))::((word32[3]) 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[3]) &(p\<rightarrow>[''words_C'']))
theory structures_proofs

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

lemma (in kernel_all_substitute) thread_state_get_tcbQueued_spec:
  "\<forall>s. \<Gamma> \<turnstile> {s}
       \<acute>ret__unsigned :== PROC thread_state_get_tcbQueued(\<acute>thread_state)
       \<lbrace>\<acute>ret__unsigned = thread_state_CL.tcbQueued_CL (thread_state_lift \<^bsup>s\<^esup>thread_state)\<rbrace>" apply (rule allI, rule conseqPre, vcg) apply clarsimp apply (simp add: thread_state_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 thread_state_get_tcbQueued_'proc \<lbrace>\<acute>ret__unsigned = tcbQueued_CL (thread_state_lift \<^bsup>s\<^esup>thread_state)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. {s} \<subseteq> \<lbrace>\<forall>v. 0 \<le>s 0 \<and> 0 <s 0x20 \<and> 1 <s 3 \<and> 0 \<le>s 1 \<and> ((if False then 1 else 0) \<noteq> 0 \<longrightarrow> 0 \<le>s 0x1F \<and> 0x1F <s 0x20 \<and> ((if (thread_state_C.words_C \<acute>thread_state.[unat 1] && 1 >> unat 0) && (1 << unat 0x1F) \<noteq> 0 then 1 else 0) \<noteq> 0 \<longrightarrow> (thread_state_C.words_C \<acute>thread_state.[unat 1] && 1 >> unat 0) || SCAST(32 signed \<rightarrow> 32) 0 = tcbQueued_CL (thread_state_lift \<^bsup>s\<^esup>thread_state)) \<and> ((if (thread_state_C.words_C \<acute>thread_state.[unat 1] && 1 >> unat 0) && (1 << unat 0x1F) \<noteq> 0 then 1 else 0) = 0 \<longrightarrow> thread_state_C.words_C \<acute>thread_state.[unat 1] && 1 >> unat 0 = tcbQueued_CL (thread_state_lift \<^bsup>s\<^esup>thread_state))) \<and> ((if False then 1 else 0) = 0 \<longrightarrow> thread_state_C.words_C \<acute>thread_state.[unat 1] && 1 >> unat 0 = tcbQueued_CL (thread_state_lift \<^bsup>s\<^esup>thread_state))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. thread_state_C.words_C (thread_state_' s).[Suc 0] && 1 = tcbQueued_CL (thread_state_lift (thread_state_' s)) proof (prove)
goal:
No subgoals! proof (prove)
goal:
No subgoals!
theory structures_proofs

lemma (in kernel_all_substitute) thread_state_get_tsType_spec:
  "\<forall>s. \<Gamma> \<turnstile> {s}
       \<acute>ret__unsigned :== PROC thread_state_get_tsType(\<acute>thread_state)
       \<lbrace>\<acute>ret__unsigned = thread_state_CL.tsType_CL (thread_state_lift \<^bsup>s\<^esup>thread_state)\<rbrace>" apply (rule allI, rule conseqPre, vcg) apply clarsimp apply (simp add: thread_state_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 thread_state_get_tsType_'proc \<lbrace>\<acute>ret__unsigned = tsType_CL (thread_state_lift \<^bsup>s\<^esup>thread_state)\<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 3 \<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 (thread_state_C.words_C \<acute>thread_state.[unat 0] && 0xF >> unat 0) && (1 << unat 0x1F) \<noteq> 0 then 1 else 0) \<noteq> 0 \<longrightarrow> (thread_state_C.words_C \<acute>thread_state.[unat 0] && 0xF >> unat 0) || SCAST(32 signed \<rightarrow> 32) 0 = tsType_CL (thread_state_lift \<^bsup>s\<^esup>thread_state)) \<and> ((if (thread_state_C.words_C \<acute>thread_state.[unat 0] && 0xF >> unat 0) && (1 << unat 0x1F) \<noteq> 0 then 1 else 0) = 0 \<longrightarrow> thread_state_C.words_C \<acute>thread_state.[unat 0] && 0xF >> unat 0 = tsType_CL (thread_state_lift \<^bsup>s\<^esup>thread_state))) \<and> ((if False then 1 else 0) = 0 \<longrightarrow> thread_state_C.words_C \<acute>thread_state.[unat 0] && 0xF >> unat 0 = tsType_CL (thread_state_lift \<^bsup>s\<^esup>thread_state))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. thread_state_C.words_C (thread_state_' s).[0] && 0xF = tsType_CL (thread_state_lift (thread_state_' s)) proof (prove)
goal:
No subgoals! proof (prove)
goal:
No subgoals!
theory structures_proofs

lemma vm_attributes_ptr_words_NULL:
  "c_guard (p::vm_attributes_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 vm_attributes_ptr_words_aligned:
  "c_guard (p::vm_attributes_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 vm_attributes_ptr_words_ptr_safe:
  "ptr_safe (p::vm_attributes_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