Fix Access, InfoFlow and DRefine.

Author: Thomas Sewell

proof/access-control/ADT_AC.thy

@@ -41,7 +41,7 @@ lemma objs_valid_tcb_vtable:
   "\<lbrakk>valid_objs s; get_tcb t s = Some tcb\<rbrakk> \<Longrightarrow> s \<turnstile> tcb_vtable tcb"
   apply (clarsimp simp: get_tcb_def split: option.splits Structures_A.kernel_object.splits)
   apply (erule cte_wp_valid_cap[rotated])
-  apply (rule cte_wp_at_tcbI[where t="(a, b)" for a b, where b="tcb_cnode_index 1"])
+  apply (rule cte_wp_at_tcbI[where t="(a, b)" for a b, where b3="tcb_cnode_index 1"])
     apply fastforce+
   done
 
@@ -52,10 +52,9 @@ lemma pd_of_thread_page_directory_at:
   apply (clarsimp simp: get_pd_of_thread_def
                   split: option.splits kernel_object.splits cap.splits arch_cap.splits
                          if_splits)
-  apply (subgoal_tac "s \<turnstile> ArchObjectCap (PageDirectoryCap word (Some aa))")
-   apply (fastforce simp: valid_cap_def2 valid_cap_ref_def)
-  apply (cut_tac s=s and t=tcb and tcb=tcb_ext in objs_valid_tcb_vtable)
-    apply (simp add: invs_valid_objs get_tcb_def)+
+  apply (frule_tac t=tcb in objs_valid_tcb_vtable[OF invs_valid_objs])
+   apply (simp add: get_tcb_def)
+  apply (fastforce simp: valid_cap_def2 valid_cap_ref_def)
   done
 
 lemma ptr_offset_in_ptr_range:

proof/access-control/Access.thy

@@ -773,7 +773,7 @@ where
 lemma caps_of_state_tcb:
   "\<lbrakk> get_tcb p s = Some tcb; option_map fst (tcb_cap_cases idx) = Some getF \<rbrakk> \<Longrightarrow> caps_of_state s (p, idx) = Some (getF tcb)"
   apply (drule get_tcb_SomeD)
-  apply (clarsimp simp: option_map_eq_Some)
+  apply (clarsimp simp: map_option_eq_Some)
   apply (drule (1) cte_wp_at_tcbI [where t = "(p, idx)" and P = "op = (getF tcb)", simplified])
   apply simp
   apply (clarsimp simp: cte_wp_at_caps_of_state)
@@ -1495,7 +1495,7 @@ next
     apply (intro range_subsetI)
      apply (rule is_aligned_no_wrap' [OF al xsz])
     apply (simp only: add_diff_eq[symmetric])
-    apply (subst add.commute add.left_commute, rule word_plus_mono_right)
+    apply (subst add.assoc, rule word_plus_mono_right)
     apply (subst iffD1 [OF le_m1_iff_lt])
     apply (simp add: p2_gt_0 word_bits_conv)
     apply (rule is_aligned_add_less_t2n[OF al' _ szv xsz])

proof/access-control/CNode_AC.thy

@@ -198,7 +198,7 @@ lemma decode_cnode_inv_authorised:
   apply (rule hoare_pre)
    apply (wp hoare_vcg_all_lift hoare_vcg_const_imp_lift_R hoare_vcg_all_lift_R
              get_cap_prop_imp[where Q=has_recycle_rights] lsfco_cte_at
-        | simp only: simp_thms if_simps fst_conv snd_conv Invocations_A.cnode_invocation.cases
+        | simp only: simp_thms if_simps fst_conv snd_conv Invocations_A.cnode_invocation.simps
         | wpc
         | wp_once hoare_drop_imps)+
   apply clarsimp
@@ -406,9 +406,7 @@ lemma set_irq_state_respects[wp]:
 crunch respects[wp]: deleted_irq_handler "integrity aag X st"
 
 lemmas cases_simp_options
-    = cases_simp_option cases_simp_option[where 'a="'b \<times> 'c", simplified, standard]
-
-
+    = cases_simp_option cases_simp_option[where 'a="'b \<times> 'c", simplified]
 
 lemma empty_slointegrity_spec:
   notes split_paired_All[simp del]

proof/access-control/Deterministic_AC.thy

@@ -120,7 +120,7 @@ lemma empty_slot_list_integrity:
   apply (simp add: empty_slot_ext_def split del: split_if)
   apply (wp update_cdt_list_wp)
   apply (intro impI conjI allI | simp add: list_filter_replace_list list_filter_remove split: option.splits | elim conjE  | simp add: list_integ_def)+
-  apply (drule_tac x=a in spec)
+  apply (drule_tac x="the slot_p" in spec)
   apply (elim disjE)
    apply (simp add: all_children_def valid_list_2_def list_filter_replace_list)+
   done

proof/access-control/Finalise_AC.thy

@@ -20,7 +20,7 @@ apply (simp add: tcb_sched_action_def)
 apply wp
 apply (clarsimp simp: integrity_def integrity_ready_queues_def pas_refined_def tcb_domain_map_wellformed_aux_def etcb_at_def get_etcb_def
            split: option.splits)
-apply (erule_tac x="(thread, tcb_domain a)" in ballE)
+apply (erule_tac x="(thread, tcb_domain (the (ekheap s thread)))" in ballE)
 apply (auto intro: domtcbs)
 done
 
@@ -43,7 +43,7 @@ apply (simp add: tcb_sched_action_def)
 apply wp
 apply (clarsimp simp: integrity_def integrity_ready_queues_def pas_refined_def tcb_domain_map_wellformed_aux_def etcb_at_def get_etcb_def
            split: option.splits)
-apply (erule_tac x="(thread, tcb_domain a)" in ballE)
+apply (erule_tac x="(thread, tcb_domain (the (ekheap s thread)))" in ballE)
 apply (auto intro: domtcbs)
 done
 
@@ -437,7 +437,7 @@ proof (induct arbitrary: st rule: rec_del.induct,
     apply (rule spec_valid_conj_liftE1, rule valid_validE_R, rule rec_del_valid_list, rule preemption_point_inv')
       apply simp
      apply simp
-    apply (rule "1.hyps"[simplified rec_del_call.cases slot_rdcall.simps])
+    apply (rule "1.hyps"[simplified rec_del_call.simps slot_rdcall.simps])
    apply auto
     done
 
@@ -504,7 +504,7 @@ next
    by (clarsimp simp: replicate_not_True)
   case (3 ptr bits n slot s)
   show ?case
-    apply (simp add: rec_del_call.cases simp_thms spec_validE_def)
+    apply (simp add: rec_del_call.simps simp_thms spec_validE_def)
     apply (rule hoare_pre, wp static_imp_wp)
     apply clarsimp
     done

proof/access-control/Ipc_AC.thy

@@ -59,7 +59,6 @@ lemma receive_async_ipc_pas_refined:
   apply (simp add: receive_async_ipc_def)
   apply (cases cap, simp_all)
   apply (rule hoare_seq_ext [OF _ get_aep_sp])
-  apply clarsimp
   apply (rule hoare_pre)
   apply (wp set_async_ep_pas_refined set_thread_state_pas_refined
        | wpc)+
@@ -237,7 +236,6 @@ lemma receive_async_ipc_integrity_autarch:
   apply (simp add: receive_async_ipc_def)
   apply (cases cap, simp_all)
   apply (rule hoare_seq_ext [OF _ get_aep_sp])
-  apply clarsimp
   apply (rule hoare_pre)
   apply (wp set_async_ep_respects[where auth=Receive] set_thread_state_integrity_autarch
          do_async_transfer_integrity_autarch
@@ -817,12 +815,12 @@ lemma send_ipc_pas_refined:
   apply (wp set_thread_state_pas_refined
        | wpc
        | simp add: hoare_if_r_and)+
-  apply (rule_tac Q="\<lambda>rv. pas_refined aag and K (can_grant \<longrightarrow> is_subject aag a)" in hoare_strengthen_post[rotated])
+  apply (rule_tac Q="\<lambda>rv. pas_refined aag and K (can_grant \<longrightarrow> is_subject aag (hd list))" in hoare_strengthen_post[rotated])
    apply (clarsimp simp: cli_no_irqs pas_refined_refl aag_cap_auth_def clas_no_asid)
   apply (wp set_thread_state_pas_refined do_ipc_transfer_pas_refined static_imp_wp
        | wpc
        | simp add: hoare_if_r_and)+
-  apply (rule_tac Q="\<lambda>rv. valid_objs and  pas_refined aag and K (can_grant \<longrightarrow> is_subject aag a)" in hoare_strengthen_post[rotated])
+  apply (rule_tac Q="\<lambda>rv. valid_objs and  pas_refined aag and K (can_grant \<longrightarrow> is_subject aag (hd list))" in hoare_strengthen_post[rotated])
    apply (clarsimp simp: cli_no_irqs pas_refined_refl aag_cap_auth_def clas_no_asid)
   apply (wp set_thread_state_pas_refined do_ipc_transfer_pas_refined static_imp_wp
        | wpc
@@ -1700,7 +1698,7 @@ lemma send_ipc_integrity_autarch:
    apply (rule hoare_pre)
     apply (wp setup_caller_cap_integrity_autarch set_thread_state_integrity_autarch thread_get_wp'
                   | wpc)+
-          apply (rule_tac Q="\<lambda>rv s. integrity aag X st s\<and> (can_grant \<longrightarrow> is_subject aag a)" in hoare_strengthen_post[rotated])
+          apply (rule_tac Q="\<lambda>rv s. integrity aag X st s\<and> (can_grant \<longrightarrow> is_subject aag (hd list))" in hoare_strengthen_post[rotated])
           apply simp+
           apply (wp set_thread_state_integrity_autarch thread_get_wp' do_ipc_transfer_integrity_autarch
                     hoare_vcg_all_lift hoare_drop_imps set_endpoinintegrity
@@ -1723,7 +1721,7 @@ lemma send_ipc_integrity_autarch:
    apply (wp set_endpoinintegrity set_thread_state_integrity_autarch setup_caller_cap_integrity_autarch
              hoare_vcg_ex_lift sts_typ_ats thread_get_wp'
         | wpc)+
-         apply (rule_tac Q="\<lambda>rv sa. integrity aag X s sa \<and> (can_grant \<longrightarrow> is_subject aag a)" in hoare_strengthen_post[rotated])
+         apply (rule_tac Q="\<lambda>rv sa. integrity aag X s sa \<and> (can_grant \<longrightarrow> is_subject aag (hd list))" in hoare_strengthen_post[rotated])
           apply simp+
          apply (wp thread_get_inv put_wp get_object_wp get_endpoint_wp thread_get_wp'
                    set_thread_state_running_respects_in_ipc[where epptr=epptr]

proof/access-control/Retype_AC.thy

@@ -759,7 +759,7 @@ lemma use_retype_region_proofs_ext':
    done
 
 lemmas use_retype_region_proofs_ext
-    = use_retype_region_proofs_ext'[where Q="\<lambda>_. Q" and P=Q for Q, simplified, OF _ _ _ _ TrueI]
+    = use_retype_region_proofs_ext'[where Q="\<lambda>_. Q" and P=Q, simplified, OF _ _ _ _ TrueI] for Q
 
 lemma (in is_extended) pas_refined_tcb_domain_map_wellformed':
   assumes tdmw: "\<lbrace>tcb_domain_map_wellformed aag and P\<rbrace> f \<lbrace>\<lambda>_. tcb_domain_map_wellformed aag\<rbrace>"
@@ -797,6 +797,7 @@ lemma retype_region_pas_refined:
    \<lbrace>\<lambda>rv. pas_refined aag\<rbrace>"
   apply (rule hoare_gen_asm)
   apply (rule hoare_pre)
+thm use_retype_region_proofs_ext
   apply(rule use_retype_region_proofs_ext)
      apply(erule (1) retype_region_proofs'.pas_refined[OF retype_region_proofs'.intro])
     apply (wp retype_region_ext_pas_refined)
@@ -893,7 +894,7 @@ lemma freeMemory_vms:
   apply (clarsimp simp: valid_machine_state_def
                         disj_commute[of "in_user_frame p s" for p s])
   apply (drule_tac x=p in spec, simp)
-  apply (drule_tac P="\<lambda>m'. underlying_memory m' p = 0"
+  apply (drule_tac P4="\<lambda>m'. underlying_memory m' p = 0"
          in use_valid[where P=P and Q="\<lambda>_. P" for P], simp_all)
   apply (simp add: freeMemory_def machine_op_lift_def
                    machine_rest_lift_def split_def)

proof/access-control/Syscall_AC.thy

@@ -219,7 +219,6 @@ lemma set_thread_state_authorised[wp]:
             hoare_vcg_ex_lift sts_obj_at_impossible
             set_thread_state_authorised_untyped_inv_state
        | simp)+
-  apply clarsimp
   apply (case_tac tcb_invocation, simp_all)
   apply (wp hoare_case_option_wp sts_typ_ats set_thread_state_cte_wp_at
             hoare_vcg_conj_lift static_imp_wp
@@ -891,15 +890,15 @@ lemma schedule_integrity:
           apply (clarsimp simp: valid_sched_def valid_sched_action_def weak_valid_sched_action_2_def switch_in_cur_domain_2_def in_cur_domain_2_def valid_etcbs_def invs_def valid_etcbs_def etcb_at_def st_tcb_at_def obj_at_def is_etcb_at_def split: option.splits)
            apply force
           apply (clarsimp simp: pas_refined_def tcb_domain_map_wellformed_aux_def)
-          apply (drule_tac x="(x, tcb_domain a)" in bspec)
+          apply (drule_tac x="(x, cur_domain s)" in bspec)
            apply (force intro: domtcbs)
           apply force
          prefer 10
          (* direct clag *)
          apply (clarsimp simp: valid_sched_def valid_sched_action_def weak_valid_sched_action_2_def switch_in_cur_domain_2_def in_cur_domain_2_def valid_etcbs_def invs_def valid_etcbs_def etcb_at_def st_tcb_at_def obj_at_def is_etcb_at_def split: option.splits)
           apply force
          apply (clarsimp simp: pas_refined_def tcb_domain_map_wellformed_aux_def)
-         apply (drule_tac x="(x, tcb_domain a)" in bspec)
+         apply (drule_tac x="(x, cur_domain s)" in bspec)
           apply (force intro: domtcbs)
          apply force
         apply (auto simp: obj_at_def st_tcb_at_def not_cur_thread_2_def valid_sched_def)

proof/access-control/Tcb_AC.thy

@@ -79,14 +79,14 @@ lemmas itr_wps = restart_integrity_autarch as_user_integrity_autarch thread_set_
               option_update_thread_integrity_autarch thread_set_pas_refined_triv
               cap_insert_integrity_autarch cap_insert_pas_refined
               hoare_vcg_all_liftE hoare_weak_lift_impE hoare_weak_lift_imp hoare_vcg_all_lift
-              check_cap_inv[where P="valid_cap c", standard]
-              check_cap_inv[where P="tcb_cap_valid c p", standard]
-              check_cap_inv[where P="cte_at p0", standard]
-              check_cap_inv[where P="tcb_at p0", standard]
-              check_cap_inv[where P="ex_cte_cap_wp_to P p", standard]
-              check_cap_inv[where P="ex_nonz_cap_to p", standard]
-              check_cap_inv2[where Q="\<lambda>_. integrity aag X st", standard]
-              check_cap_inv2[where Q="\<lambda>_. pas_refined aag", standard]
+              check_cap_inv[where P="valid_cap c" for c]
+              check_cap_inv[where P="tcb_cap_valid c p" for c p]
+              check_cap_inv[where P="cte_at p0" for p0]
+              check_cap_inv[where P="tcb_at p0" for p0]
+              check_cap_inv[where P="ex_cte_cap_wp_to P p" for P p]
+              check_cap_inv[where P="ex_nonz_cap_to p" for p]
+              check_cap_inv2[where Q="\<lambda>_. integrity aag X st" for aag X st]
+              check_cap_inv2[where Q="\<lambda>_. pas_refined aag" for aag]
               checked_insert_no_cap_to cap_insert_ex_cap
               cap_delete_valid_cap cap_delete_deletes
               hoare_case_option_wp thread_set_valid_cap
@@ -166,7 +166,7 @@ lemma set_priority_pas_refined[wp]:
   apply (simp add: tcb_sched_action_def | wp)+
   apply (clarsimp simp: etcb_at_def pas_refined_def tcb_domain_map_wellformed_aux_def
           split: option.splits)
-  apply (erule_tac x="(aa, b)" in ballE)
+  apply (erule_tac x="(a, b)" in ballE)
    apply simp
   apply (erule domains_of_state_aux.cases)
   apply (force intro: domtcbs split: split_if_asm)
@@ -247,13 +247,13 @@ lemma invoke_tcb_tc_respects_aag:
              thread_set_tcb_ipc_buffer_cap_cleared_invs
              thread_set_invs_trivial[OF ball_tcb_cap_casesI]
              hoare_vcg_all_lift thread_set_valid_cap out_emptyable
-             check_cap_inv [where P="valid_cap c", standard]
-             check_cap_inv [where P="tcb_cap_valid c p", standard]
-             check_cap_inv[where P="cte_at p0", standard]
-             check_cap_inv[where P="tcb_at p0", standard]
-             check_cap_inv[where P="simple_sched_action", standard]
-             check_cap_inv[where P="valid_list", standard]
-             check_cap_inv[where P="valid_sched", standard]
+             check_cap_inv [where P="valid_cap c" for c]
+             check_cap_inv [where P="tcb_cap_valid c p" for c p]
+             check_cap_inv[where P="cte_at p0" for p0]
+             check_cap_inv[where P="tcb_at p0" for p0]
+             check_cap_inv[where P="simple_sched_action"]
+             check_cap_inv[where P="valid_list"]
+             check_cap_inv[where P="valid_sched"]
              thread_set_cte_at
              thread_set_cte_wp_at_trivial[where Q="\<lambda>x. x", OF ball_tcb_cap_casesI]
              thread_set_no_cap_to_trivial[OF ball_tcb_cap_casesI]

proof/drefine/Arch_DR.thy

@@ -289,7 +289,7 @@ proof -
 
 
   show ?thesis using pdid vp_aligned
-    apply clarsimp
+    apply hypsubst_thin
     proof (induct pgsz)
       case ARMSmallPage
       show ?case using ARMSmallPage.prems
@@ -445,7 +445,7 @@ proof -
         apply (cut_tac less_kernel_base_mapping_slots[OF kb pd_aligned])
         apply (drule_tac x="ucast (lookup_pd_slot pd_ptr vptr && mask pd_bits >> 2)" in bspec)
          apply simp
-        apply (drule sym, simp)
+        apply (drule_tac t="pda ?v" in sym, simp)
         apply (clarsimp simp: obj_at_def a_type_def del: disjCI)
         apply (clarsimp split: Structures_A.kernel_object.split_asm split_if_asm
                                arch_kernel_obj.split_asm del: disjCI)
@@ -487,7 +487,7 @@ proof -
         apply (cut_tac less_kernel_base_mapping_slots[OF kb pd_aligned])
         apply (drule_tac x="ucast (lookup_pd_slot pd_ptr vptr && mask pd_bits >> 2)" in bspec)
          apply simp
-        apply (drule sym, simp)
+        apply (drule_tac t="pda ?v" in sym, simp)
         apply (clarsimp simp: obj_at_def a_type_def del: disjCI)
         apply (clarsimp split: Structures_A.kernel_object.split_asm split_if_asm
                                arch_kernel_obj.split_asm del: disjCI)
@@ -764,7 +764,7 @@ next
                                             apply (clarsimp simp: neq_Nil_conv valid_cap_simps obj_at_def
                                                                   opt_object_page_directory invs_valid_idle label_to_flush_type_def InvocationLabels_H.isPageFlush_def
                                                            dest!: a_type_pdD)+
-             apply (rule_tac r'=dc and P'="?I" and Q'="\<lambda>rv. ?I and (\<exists>\<rhd> (lookup_pd_slot rv a && ~~ mask pd_bits))"
+             apply (rule_tac r'=dc and P'="?I" and Q'="\<lambda>rv. ?I and (\<exists>\<rhd> (lookup_pd_slot rv x21 && ~~ mask pd_bits))"
                       in corres_alternative_throw_splitE[OF _ _ returnOk_wp[where x="()"], simplified])
                  apply (rule corres_from_rdonly, simp_all)[1]
                    apply (wp | simp)+
@@ -849,7 +849,6 @@ next
                             translate_arch_invocation_def transform_page_inv_def)
           apply (clarsimp)
           apply (rule corres_from_rdonly)
-             apply (clarsimp)
              apply (wp, clarsimp)
             apply ( simp only: Let_unfold, wp, clarsimp, rule valid_validE, wp whenE_inv, clarsimp, wp)
             apply (assumption)
@@ -861,7 +860,6 @@ next
                   apply blast
                  apply (metis flush.exhaust)
                 apply (rule corres_from_rdonly)
-                   apply (clarsimp)
                    apply (wp, clarsimp)
                   apply ( simp only: Let_unfold, wp, clarsimp, rule valid_validE, wp whenE_inv, clarsimp, wp)
                   apply (assumption)
@@ -873,7 +871,6 @@ next
                  apply blast
                 apply (metis flush.exhaust)
                apply (rule corres_from_rdonly)
-                  apply (clarsimp)
                   apply (wp, clarsimp)
                  apply ( simp only: Let_unfold, wp, clarsimp, rule valid_validE, wp whenE_inv, clarsimp, wp)
                  apply (assumption)
@@ -885,7 +882,6 @@ next
                 apply blast
                apply (metis flush.exhaust)
               apply (rule corres_from_rdonly)
-                 apply (clarsimp)
                  apply (wp, clarsimp)
                 apply ( simp only: Let_unfold, wp, clarsimp, rule valid_validE, wp whenE_inv, clarsimp, wp)
                 apply (assumption)
@@ -1888,6 +1884,7 @@ proof -
     apply (clarsimp simp:perform_asid_control_invocation_def)
     apply (simp add:arch_invocation_relation_def translate_arch_invocation_def)
     apply (cases asid_inv, clarsimp)
+    apply hypsubst_thin
     apply (drule sym)
     apply (drule sym)
     apply (drule sym)