Merge branch 'master' into corres-method-test

docs/setup.md

@@ -91,12 +91,13 @@ pip3 install --user sel4-deps
 
 After installing [haskell-stack](https://docs.haskellstack.org/en/stable/)
 (already included in the packages above on Mac and Ubuntu), make sure you've
-adjusted your `PATH` to include `$HOME/.local/bin`, and that you're running an
-up-to-date version:
+adjusted your `PATH` to include `$HOME/.local/bin`, that you're running an
+up-to-date version, and that you have installed cabal:
 
 ```bash
 stack upgrade --binary-only
 which stack # should be $HOME/.local/bin/stack
+stack install cabal-install
 ```
 
 ## Checking out the repository collection

lib/Monads/NonDetMonadVCG.thy

@@ -306,6 +306,8 @@ lemma hoare_gen_asm:
   "(P \<Longrightarrow> \<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace>) \<Longrightarrow> \<lbrace>P' and K P\<rbrace> f \<lbrace>Q\<rbrace>"
   by (fastforce simp add: valid_def)
 
+lemmas hoare_gen_asm_single = hoare_gen_asm[where P'="\<top>", simplified pred_conj_def simp_thms]
+
 lemma hoare_gen_asm_lk:
   "(P \<Longrightarrow> \<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace>) \<Longrightarrow> \<lbrace>K P and P'\<rbrace> f \<lbrace>Q\<rbrace>"
   by (fastforce simp add: valid_def)

lib/Monads/OptionMonadWP.thy

@@ -21,8 +21,10 @@ begin
    TODO: design a sensible syntax for them. *)
 
 (* Partial correctness. *)
-definition ovalid :: "('s \<Rightarrow> bool) \<Rightarrow> ('s \<Rightarrow> 'a option) \<Rightarrow> ('a \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> bool" where
-  "ovalid P f Q \<equiv> \<forall>s r. P s \<and> f s = Some r \<longrightarrow> Q r s"
+definition ovalid :: "('s \<Rightarrow> bool) \<Rightarrow> ('s \<Rightarrow> 'a option) \<Rightarrow> ('a \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> bool"
+  ("\<lblot>_\<rblot>/ _ /\<lblot>_\<rblot>") where
+  "\<lblot>P\<rblot> f \<lblot>Q\<rblot> \<equiv> \<forall>s r. P s \<and> f s = Some r \<longrightarrow> Q r s"
+
 (* Total correctness. *)
 definition ovalidNF :: "('s \<Rightarrow> bool) \<Rightarrow> ('s \<Rightarrow> 'a option) \<Rightarrow> ('a \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> bool" where
   "ovalidNF P f Q \<equiv> \<forall>s. P s \<longrightarrow> (f s \<noteq> None \<and> (\<forall>r. f s = Some r \<longrightarrow> Q r s))"
@@ -57,6 +59,10 @@ lemmas owhile_add_inv = owhile_inv_def[symmetric]
 
 
 (* WP rules for ovalid. *)
+lemma ovalid_inv[wp]:
+  "ovalid P f (\<lambda>_. P)"
+  by (simp add: ovalid_def)
+
 lemma obind_wp[wp]:
   "\<lbrakk> \<And>r. ovalid (R r) (g r) Q; ovalid P f R \<rbrakk> \<Longrightarrow> ovalid P (obind f g) Q"
   by (simp add: ovalid_def obind_def split: option.splits, fast)

lib/Monads/WhileLoopRules.thy

@@ -383,6 +383,22 @@ lemma whileLoop_wp:
   \<lbrace> I r \<rbrace> whileLoop C B r \<lbrace> Q \<rbrace>"
   by (rule valid_whileLoop)
 
+lemma whileLoop_valid_inv:
+  "(\<And>r. \<lbrace> \<lambda>s. I r s \<and> C r s \<rbrace> B r \<lbrace> I \<rbrace>) \<Longrightarrow> \<lbrace> I r \<rbrace> whileLoop C B r \<lbrace> I \<rbrace>"
+  apply (fastforce intro: whileLoop_wp)
+  done
+
+lemma valid_whileLoop_cond_fail:
+  assumes pre_implies_post: "\<And>s. P r s \<Longrightarrow> Q r s"
+      and pre_implies_fail: "\<And>s. P r s \<Longrightarrow> \<not> C r s"
+    shows "\<lbrace> P r \<rbrace> whileLoop C B r \<lbrace> Q \<rbrace>"
+  using assms
+  apply (clarsimp simp: valid_def)
+  apply (subst (asm) whileLoop_cond_fail)
+   apply blast
+  apply (clarsimp simp: return_def)
+  done
+
 lemma whileLoop_wp_inv [wp]:
   "\<lbrakk> \<And>r. \<lbrace>\<lambda>s. I r s \<and> C r s\<rbrace> B r \<lbrace>I\<rbrace>; \<And>r s. \<lbrakk>I r s; \<not> C r s\<rbrakk> \<Longrightarrow> Q r s \<rbrakk>
    \<Longrightarrow> \<lbrace> I r \<rbrace> whileLoop_inv C B r I M \<lbrace> Q \<rbrace>"

lib/clib/CCorres_Rewrite.thy

@@ -17,7 +17,7 @@ lemma ccorres_com_eq_hom:
            elim: ccorres_semantic_equivD2)
 
 method ccorres_rewrite declares C_simp C_simp_pre C_simp_simps C_simp_throws
-  = simpl_rewrite hom: ccorres_com_eq_hom
+  = (simpl_rewrite hom: ccorres_com_eq_hom, no_name_eta)
 
 lemma hoarep_com_eq_hom:
   "com_eq_hom \<Gamma> (\<lambda>c. hoarep \<Gamma> {} F P c Q A)"

proof/crefine/ARM/Arch_C.thy

@@ -397,7 +397,9 @@ shows
       apply (rule ccorres_rhs_assoc2)
       apply (rule ccorres_abstract_cleanup)
       apply (rule ccorres_symb_exec_l)
-        apply (rule_tac P = "rva = (capability.UntypedCap isdev frame pageBits idx)" in ccorres_gen_asm)
+        apply (rename_tac pcap)
+        apply (rule_tac P = "pcap = (capability.UntypedCap isdev frame pageBits idx)"
+                 in ccorres_gen_asm)
         apply (simp add: hrs_htd_update del:fun_upd_apply)
         apply (rule ccorres_split_nothrow)
 
@@ -1466,13 +1468,13 @@ lemma pdeCheckIfMapped_ccorres:
     (Call pdeCheckIfMapped_'proc)"
   apply (cinit lift: pde___ptr_to_struct_pde_C_')
    apply (rule ccorres_pre_getObject_pde)
-   apply (rule_tac P'="{s. \<exists>pde'. cslift s (pde_Ptr slot) = Some pde' \<and> cpde_relation rv pde'}"
+   apply (rule_tac P'="{s. \<exists>pde'. cslift s (pde_Ptr slot) = Some pde' \<and> cpde_relation pd pde'}"
      in ccorres_from_vcg_throws[where P="\<lambda>s. True"])
    apply simp_all
   apply clarsimp
   apply (rule conseqPre, vcg)
   apply (clarsimp simp: typ_heap_simps' return_def)
-  apply (case_tac rv, simp_all add: cpde_relation_invalid isInvalidPDE_def
+  apply (case_tac pd, simp_all add: cpde_relation_invalid isInvalidPDE_def
                              split: if_split)
   done
 
@@ -1793,7 +1795,7 @@ lemma performPageInvocationMapPDE_ccorres:
              apply (clarsimp simp: pde_range_relation_def ptr_range_to_list_def)
             apply vcg
             apply simp
-           apply (wp valid_pde_slots_lift2)
+           apply (wpsimp wp: valid_pde_slots_lift2)
           apply clarsimp
           apply (clarsimp simp: pde_range_relation_def ptr_range_to_list_def)
           apply (rule order_less_le_trans)

proof/crefine/ARM/CSpace_C.thy

@@ -770,7 +770,7 @@ lemma update_freeIndex':
       supply if_cong[cong]
       apply (cinit lift: cap_ptr_' v32_')
        apply (rule ccorres_pre_getCTE)
-       apply (rule_tac P="\<lambda>s. ctes_of s srcSlot = Some rv \<and> (\<exists>i. cteCap rv = UntypedCap d p sz i)"
+       apply (rule_tac P="\<lambda>s. ctes_of s srcSlot = Some cte \<and> (\<exists>i. cteCap cte = UntypedCap d p sz i)"
                 in ccorres_from_vcg[where P' = UNIV])
        apply (rule allI)
        apply (rule conseqPre)
@@ -2055,8 +2055,7 @@ lemma emptySlot_ccorres:
             apply csymbr
             apply (rule ccorres_move_c_guard_cte)
                 \<comment> \<open>--- instruction y \<leftarrow> updateMDB slot (\<lambda>a. nullMDBNode);\<close>
-                apply (ctac (no_vcg)
-                  add: ccorres_updateMDB_const [unfolded const_def])
+                apply (ctac (no_vcg) add: ccorres_updateMDB_const)
 
                   \<comment> \<open>the post_cap_deletion case\<close>
 
@@ -2132,7 +2131,7 @@ lemma capSwapForDelete_ccorres:
   \<comment> \<open>--- instruction: when (slot1 \<noteq> slot2) \<dots> / IF Ptr slot1 = Ptr slot2 THEN \<dots>\<close>
    apply (simp add:when_def)
    apply (rule ccorres_if_cond_throws2 [where Q = \<top> and Q' = \<top>])
-      apply (case_tac "slot1=slot2", simp+)
+      apply (case_tac "slot1=slot2"; simp)
      apply (rule ccorres_return_void_C)
 
   \<comment> \<open>***Main goal***\<close>

proof/crefine/ARM/Finalise_C.thy

@@ -277,10 +277,10 @@ lemma cancelAllIPC_ccorres:
   apply (cinit lift: epptr_')
    apply (rule ccorres_symb_exec_l [OF _ getEndpoint_inv _ empty_fail_getEndpoint])
     apply (rule_tac xf'=ret__unsigned_'
-                and val="case rv of IdleEP \<Rightarrow> scast EPState_Idle
+                and val="case ep of IdleEP \<Rightarrow> scast EPState_Idle
                             | RecvEP _ \<Rightarrow> scast EPState_Recv | SendEP _ \<Rightarrow> scast EPState_Send"
-                and R="ko_at' rv epptr"
-                 in ccorres_symb_exec_r_known_rv_UNIV[where R'=UNIV])
+                and R="ko_at' ep epptr"
+             in ccorres_symb_exec_r_known_rv_UNIV[where R'=UNIV])
        apply vcg
        apply clarsimp
        apply (erule cmap_relationE1 [OF cmap_relation_ep])
@@ -289,8 +289,8 @@ lemma cancelAllIPC_ccorres:
        apply (simp add: cendpoint_relation_def Let_def
                  split: endpoint.split_asm)
       apply ceqv
-     apply (rule_tac A="invs' and ko_at' rv epptr"
-                  in ccorres_guard_imp2[where A'=UNIV])
+     apply (rule_tac A="invs' and ko_at' ep epptr"
+              in ccorres_guard_imp2[where A'=UNIV])
       apply wpc
         apply (rename_tac list)
         apply (simp add: endpoint_state_defs
@@ -404,10 +404,10 @@ lemma cancelAllSignals_ccorres:
   apply (cinit lift: ntfnPtr_')
    apply (rule ccorres_symb_exec_l [OF _ get_ntfn_inv' _ empty_fail_getNotification])
     apply (rule_tac xf'=ret__unsigned_'
-                and val="case ntfnObj rv of IdleNtfn \<Rightarrow> scast NtfnState_Idle
+                and val="case ntfnObj ntfn of IdleNtfn \<Rightarrow> scast NtfnState_Idle
                             | ActiveNtfn _ \<Rightarrow> scast NtfnState_Active | WaitingNtfn _ \<Rightarrow> scast NtfnState_Waiting"
-                and R="ko_at' rv ntfnptr"
-                 in ccorres_symb_exec_r_known_rv_UNIV[where R'=UNIV])
+                and R="ko_at' ntfn ntfnptr"
+             in ccorres_symb_exec_r_known_rv_UNIV[where R'=UNIV])
        apply vcg
        apply clarsimp
        apply (erule cmap_relationE1 [OF cmap_relation_ntfn])
@@ -416,8 +416,8 @@ lemma cancelAllSignals_ccorres:
        apply (simp add: cnotification_relation_def Let_def
                  split: ntfn.split_asm)
       apply ceqv
-     apply (rule_tac A="invs' and ko_at' rv ntfnptr"
-                  in ccorres_guard_imp2[where A'=UNIV])
+     apply (rule_tac A="invs' and ko_at' ntfn ntfnptr"
+              in ccorres_guard_imp2[where A'=UNIV])
       apply wpc
         apply (simp add: notification_state_defs ccorres_cond_iffs)
         apply (rule ccorres_return_Skip)
@@ -432,8 +432,8 @@ lemma cancelAllSignals_ccorres:
       apply csymbr
       apply (rule ccorres_rhs_assoc2, rule ccorres_rhs_assoc2)
       apply (rule_tac r'=dc and xf'=xfdc in ccorres_split_nothrow)
-          apply (rule_tac P="ko_at' rv ntfnptr and invs'"
-                    in ccorres_from_vcg[where P'=UNIV])
+          apply (rule_tac P="ko_at' ntfn ntfnptr and invs'"
+                   in ccorres_from_vcg[where P'=UNIV])
           apply (rule allI, rule conseqPre, vcg)
           apply clarsimp
           apply (rule_tac x=ntfnptr in cmap_relationE1 [OF cmap_relation_ntfn], assumption)
@@ -643,8 +643,8 @@ lemma doUnbindNotification_ccorres:
    (Call doUnbindNotification_'proc)"
   apply (cinit' lift: ntfnPtr_' tcbptr_')
    apply (rule ccorres_symb_exec_l [OF _ get_ntfn_inv' _ empty_fail_getNotification])
-    apply (rule_tac P="invs' and ko_at' rv ntfnptr" and P'=UNIV
-                in ccorres_split_nothrow_novcg)
+    apply (rule_tac P="invs' and ko_at' ntfn ntfnptr" and P'=UNIV
+             in ccorres_split_nothrow_novcg)
         apply (rule ccorres_from_vcg[where rrel=dc and xf=xfdc])
         apply (rule allI, rule conseqPre, vcg)
         apply (clarsimp simp: option_to_ptr_def option_to_0_def)
@@ -663,7 +663,7 @@ lemma doUnbindNotification_ccorres:
               apply (rule cpspace_relation_ntfn_update_ntfn, assumption+)
                apply (clarsimp simp: cnotification_relation_def Let_def
                                      mask_def [where n=2] NtfnState_Waiting_def)
-               apply (case_tac "ntfnObj rv", ((simp add: option_to_ctcb_ptr_def)+)[4])
+               apply (case_tac "ntfnObj ntfn", ((simp add: option_to_ctcb_ptr_def)+)[4])
              subgoal by (simp add: carch_state_relation_def typ_heap_simps')
             subgoal by (simp add: cmachine_state_relation_def)
            subgoal by (simp add: h_t_valid_clift_Some_iff)
@@ -778,13 +778,13 @@ lemma unbindMaybeNotification_ccorres:
   apply (cinit lift: ntfnPtr_')
    apply (rule ccorres_symb_exec_l [OF _ get_ntfn_inv' _ empty_fail_getNotification])
     apply (rule ccorres_rhs_assoc2)
-    apply (rule_tac P="ntfnBoundTCB rv \<noteq> None \<longrightarrow>
-                             option_to_ctcb_ptr (ntfnBoundTCB rv) \<noteq> NULL"
-                     in ccorres_gen_asm)
+    apply (rule_tac P="ntfnBoundTCB ntfn \<noteq> None \<longrightarrow>
+                         option_to_ctcb_ptr (ntfnBoundTCB ntfn) \<noteq> NULL"
+             in ccorres_gen_asm)
     apply (rule_tac xf'=boundTCB_'
-                           and val="option_to_ctcb_ptr (ntfnBoundTCB rv)"
-                           and R="ko_at' rv ntfnptr and valid_bound_tcb' (ntfnBoundTCB rv)"
-                            in ccorres_symb_exec_r_known_rv_UNIV[where R'=UNIV])
+                and val="option_to_ctcb_ptr (ntfnBoundTCB ntfn)"
+                and R="ko_at' ntfn ntfnptr and valid_bound_tcb' (ntfnBoundTCB ntfn)"
+             in ccorres_symb_exec_r_known_rv_UNIV[where R'=UNIV])
        apply vcg
        apply clarsimp
        apply (erule cmap_relationE1[OF cmap_relation_ntfn])

proof/crefine/ARM/Invoke_C.thy

@@ -65,7 +65,7 @@ lemma setDomain_ccorres:
            apply (ctac add: tcbSchedEnqueue_ccorres)
           apply (rule ccorres_return_Skip)
          apply (simp add: when_def)
-         apply (rule_tac R="\<lambda>s. rv = ksCurThread s"
+         apply (rule_tac R="\<lambda>s. curThread = ksCurThread s"
                     in ccorres_cond2)
            apply (clarsimp simp: rf_sr_ksCurThread)
           apply (ctac add: rescheduleRequired_ccorres)
@@ -76,14 +76,16 @@ lemma setDomain_ccorres:
       apply simp
       apply wp
      apply (rule_tac Q="\<lambda>_. all_invs_but_sch_extra and tcb_at' t and sch_act_simple
-                        and (\<lambda>s. rv = ksCurThread s)" in hoare_strengthen_post)
+                            and (\<lambda>s. curThread = ksCurThread s)"
+              in hoare_strengthen_post)
       apply (wp threadSet_all_invs_but_sch_extra)
      apply (clarsimp simp: valid_pspace_valid_objs' st_tcb_at_def[symmetric]
                            sch_act_simple_def st_tcb_at'_def weak_sch_act_wf_def
                     split: if_splits)
     apply (simp add: guard_is_UNIV_def)
    apply (rule_tac Q="\<lambda>_. invs' and tcb_at' t and sch_act_simple
-      and (\<lambda>s. rv = ksCurThread s \<and> (\<forall>p. t \<notin> set (ksReadyQueues s p)))" in hoare_strengthen_post)
+                          and (\<lambda>s. curThread = ksCurThread s \<and> (\<forall>p. t \<notin> set (ksReadyQueues s p)))"
+            in hoare_strengthen_post)
     apply (wp weak_sch_act_wf_lift_linear tcbSchedDequeue_not_queued
               tcbSchedDequeue_not_in_queue hoare_vcg_imp_lift hoare_vcg_all_lift)
    apply (clarsimp simp: invs'_def valid_pspace'_def valid_state'_def)
@@ -619,7 +621,7 @@ lemma decodeCNodeInvocation_ccorres:
                        del: Collect_const cong: call_ignore_cong)
            apply (rule ccorres_split_throws)
             apply (rule ccorres_rhs_assoc | csymbr)+
-            apply (simp add: invocationCatch_use_injection_handler[symmetric, unfolded o_def]
+            apply (simp add: invocationCatch_use_injection_handler[symmetric]
                         del: Collect_const cong: call_ignore_cong)
             apply (rule ccorres_Cond_rhs_Seq)
              apply (simp add:if_P del: Collect_const)
@@ -1089,7 +1091,7 @@ lemma decodeCNodeInvocation_ccorres:
             apply (simp add: throwError_def return_def exception_defs
                              syscall_error_rel_def syscall_error_to_H_cases)
             apply clarsimp
-           apply (simp add: invocationCatch_use_injection_handler[symmetric, unfolded o_def]
+           apply (simp add: invocationCatch_use_injection_handler[symmetric]
                        del: Collect_const)
            apply csymbr
            apply (simp add: interpret_excaps_test_null excaps_map_def

proof/crefine/ARM/Ipc_C.thy

@@ -2951,9 +2951,10 @@ proof -
                    del: Collect_const)
        apply csymbr
        apply (rename_tac "lngth")
-       apply (simp add: mi_from_H_def mapME_def del: Collect_const cong: bind_apply_cong)
+       apply (unfold mapME_def)[1]
+       apply (simp add: mi_from_H_def del: Collect_const)
        apply (rule ccorres_symb_exec_l)
-          apply (rule_tac P="length rv = unat word2" in ccorres_gen_asm)
+          apply (rule_tac P="length xs = unat word2" in ccorres_gen_asm)
           apply csymbr
           apply (rule ccorres_rhs_assoc2)
           apply (rule ccorres_add_returnOk2,
@@ -2963,7 +2964,7 @@ proof -
                         and   Q="UNIV"
                         and   F="\<lambda>n s. valid_pspace' s \<and> tcb_at' thread s \<and>
                                        (case buffer of Some x \<Rightarrow> valid_ipc_buffer_ptr' x | _ \<Rightarrow> \<top>) s \<and>
-                                        (\<forall>m < length rv. user_word_at (rv ! m)
+                                        (\<forall>m < length xs. user_word_at (xs ! m)
                                                       (x2 + (of_nat m + (msgMaxLength + 2)) * 4) s)"
                            in ccorres_sequenceE_while')
                    apply (simp add: split_def)
@@ -2973,7 +2974,7 @@ proof -
                       apply (rule_tac xf'=cptr_' in ccorres_abstract, ceqv)
                       apply (ctac add: capFaultOnFailure_ccorres
                                 [OF lookupSlotForThread_ccorres'])
-                         apply (rule_tac P="is_aligned rva 4" in ccorres_gen_asm)
+                         apply (rule_tac P="is_aligned rv 4" in ccorres_gen_asm)
                          apply (simp add: ccorres_cond_iffs liftE_bindE)
                          apply (rule ccorres_symb_exec_l [OF _ _ _ empty_fail_getSlotCap])
                            apply (rule_tac P'="UNIV \<inter> {s. excaps_map ys
@@ -2994,7 +2995,7 @@ proof -
                         apply (clarsimp simp: ccorres_cond_iffs)
                         apply (rule_tac  P= \<top>
                                  and P'="{x. errstate x= lu_ret___struct_lookupSlot_raw_ret_C \<and>
-                                             rv' = (rv ! length ys)}"
+                                             rv' = (xs ! length ys)}"
                                    in ccorres_from_vcg_throws)
                         apply (rule allI, rule conseqPre, vcg)
                         apply (clarsimp simp: throwError_def return_def)
@@ -3035,7 +3036,7 @@ proof -
              apply ceqv
             apply (simp del: Collect_const)
             apply (rule_tac P'="{s. snd rv'=?curr s}"
-                        and P="\<lambda>s. length rva = length rv \<and> (\<forall>x \<in> set rva. snd x \<noteq> 0)"
+                        and P="\<lambda>s. length rv = length xs \<and> (\<forall>x \<in> set rv. snd x \<noteq> 0)"
                         in ccorres_from_vcg_throws)
             apply (rule allI, rule conseqPre, vcg)
             apply (clarsimp simp: returnOk_def return_def
@@ -3357,7 +3358,7 @@ proof -
      apply (rule ccorres_rhs_assoc2)
      apply (simp add: MessageID_Exception_def)
      apply ccorres_rewrite
-     apply (subst bind_return_unit)
+     apply (rule ccorres_add_return2)
      apply (rule ccorres_split_nothrow_novcg)
          apply (rule ccorres_zipWithM_x_while)
              apply clarsimp