theory structures_proofs

lemma (in kernel_all_substitute) mdb_node_new_spec:
  "\<forall> s. \<Gamma> \<turnstile> {s}
       \<acute>ret__struct_mdb_node_C :== PROC mdb_node_new(\<acute>mdbNext, \<acute>mdbRevocable, \<acute>mdbFirstBadged, \<acute>mdbPrev)
       \<lbrace> mdb_node_lift \<acute>ret__struct_mdb_node_C = \<lparr>
          mdb_node_CL.mdbNext_CL = (\<^bsup>s\<^esup>mdbNext AND NOT (mask 3)),
          mdb_node_CL.mdbRevocable_CL = (\<^bsup>s\<^esup>mdbRevocable AND mask 1),
          mdb_node_CL.mdbFirstBadged_CL = (\<^bsup>s\<^esup>mdbFirstBadged AND mask 1),
          mdb_node_CL.mdbPrev_CL = (\<^bsup>s\<^esup>mdbPrev AND NOT (mask 3)) \<rparr> \<rbrace>" apply (rule allI, rule conseqPre, vcg) apply (clarsimp simp: guard_simps) apply (simp add: mdb_node_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 mdb_node_new_'proc \<lbrace>mdb_node_lift \<acute>ret__struct_mdb_node_C = \<lparr>mdbNext_CL = \<^bsup>s\<^esup>mdbNext && ~~ mask 3, mdbRevocable_CL = \<^bsup>s\<^esup>mdbRevocable && mask 1, mdbFirstBadged_CL = \<^bsup>s\<^esup>mdbFirstBadged && mask 1, mdbPrev_CL = \<^bsup>s\<^esup>mdbPrev && ~~ mask 3\<rparr>\<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> 0 \<le>s 0 \<and> 0 <s 0x20 \<and> 0 \<le>s 1 \<and> 1 <s 0x20 \<and> 0 \<le>s 0 \<and> 0 <s 0x20 \<and> mdb_node_lift (mdb_node_C.words_C_update (\<lambda>v. Arrays.update v (unat 1) (((SCAST(32 signed \<rightarrow> 32) 0 || (\<acute>mdbNext && 0xFFFFFFF8 >> unat 0)) || (\<acute>mdbRevocable && 1 << unat 1)) || (\<acute>mdbFirstBadged && 1 << unat 0))) (mdb_node_C.words_C_update (\<lambda>v. Arrays.update v (unat 0) (SCAST(32 signed \<rightarrow> 32) 0 || (\<acute>mdbPrev && 0xFFFFFFF8 >> unat 0))) v)) = \<lparr>mdbNext_CL = \<^bsup>s\<^esup>mdbNext && ~~ mask 3, mdbRevocable_CL = \<^bsup>s\<^esup>mdbRevocable && mask 1, mdbFirstBadged_CL = \<^bsup>s\<^esup>mdbFirstBadged && mask 1, mdbPrev_CL = \<^bsup>s\<^esup>mdbPrev && ~~ mask 3\<rparr>\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s v. mdb_node_lift (mdb_node_C.words_C_update ((\<lambda>v. Arrays.update v (Suc 0) ((mdbNext_' s && 0xFFFFFFF8 || (mdbRevocable_' s && 1 << Suc 0)) || mdbFirstBadged_' s && 1)) \<circ> (\<lambda>v. Arrays.update v 0 (mdbPrev_' s && 0xFFFFFFF8))) v) = \<lparr>mdbNext_CL = mdbNext_' s && ~~ mask 3, mdbRevocable_CL = mdbRevocable_' s && 1, mdbFirstBadged_CL = mdbFirstBadged_' s && 1, mdbPrev_CL = mdbPrev_' s && ~~ mask 3\<rparr> proof (prove)
goal (1 subgoal):
 1. \<And>s. ((mdbNext_' s && 0xFFFFFFF8 || (mdbRevocable_' s && 1 << Suc 0)) || mdbFirstBadged_' s && 1) && ~~ mask 3 = mdbNext_' s && ~~ mask 3 \<and> ((mdbNext_' s && 0xFFFFFFF8 || (mdbRevocable_' s && 1 << Suc 0)) || mdbFirstBadged_' s && 1 >> Suc 0) && 1 = mdbRevocable_' s && 1 \<and> ((mdbNext_' s && 0xFFFFFFF8 || (mdbRevocable_' s && 1 << Suc 0)) || mdbFirstBadged_' s && 1) && 1 = mdbFirstBadged_' s && 1 \<and> (mdbPrev_' s && 0xFFFFFFF8) && ~~ mask 3 = mdbPrev_' s && ~~ mask 3 proof (prove)
goal:
No subgoals!