lib: reorder assumptions of no_fail_bind

In order to aid wp-style reasoning Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
2024-01-09 19:36:05 +10:30 · 2024-01-09 19:36:05 +10:30 · 45cde7049b
parent 7a14a48ba5
commit 45cde7049b
15 changed files with 36 additions and 51 deletions
--- a/lib/Monads/nondet/Nondet_No_Fail.thy
+++ b/lib/Monads/nondet/Nondet_No_Fail.thy
@ -130,7 +130,7 @@ lemma no_fail_returnOK[simp, wp]:
  by (simp add: returnOk_def)

 lemma no_fail_bind[wp]:
-  "\<lbrakk> no_fail P f; \<And>rv. no_fail (R rv) (g rv); \<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace> \<rbrakk> \<Longrightarrow> no_fail (P and Q) (f >>= (\<lambda>rv. g rv))"
+  "\<lbrakk> \<And>rv. no_fail (R rv) (g rv); \<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>; no_fail P f \<rbrakk> \<Longrightarrow> no_fail (P and Q) (f >>= (\<lambda>rv. g rv))"
  unfolding no_fail_def bind_def
  using post_by_hoare by fastforce

--- a/proof/crefine/lib/AutoCorres_C.thy
+++ b/proof/crefine/lib/AutoCorres_C.thy
@ -934,10 +934,10 @@ lemma terminates_spec_no_fail:
      using normal by auto
    show ?thesis
      apply (clarsimp simp: ac AC_call_L1_def L2_call_L1_def)
-      apply (wpsimp wp: select_f_L1_call_simpl_no_fail no_fail_select
-                wp_del: select_f_wp)
-      apply (rule hoare_strengthen_post[OF select_f_L1_call_simpl_rv], fastforce)
-      apply (wpsimp wp: nf_pre)+
+      apply (wpsimp wp_del: select_f_wp)
+            apply (rule hoare_strengthen_post[OF select_f_L1_call_simpl_rv], fastforce)
+           apply (wpsimp wp: select_f_L1_call_simpl_no_fail no_fail_select)+
+      apply (fastforce simp: nf_pre)
      done
  qed

--- a/proof/infoflow/refine/ADT_IF_Refine_C.thy
+++ b/proof/infoflow/refine/ADT_IF_Refine_C.thy
@ -193,23 +193,20 @@ lemma handleInterrupt_no_fail:

 lemma handleEvent_Interrupt_no_fail: "no_fail (invs' and ex_abs einvs) (handleEvent Interrupt)"
  apply (simp add: handleEvent_def)
-  apply (rule no_fail_pre)
   apply wp
-    apply (rule handleInterrupt_no_fail)
-   apply (simp add: crunch_simps)
-   apply (rule_tac Q="\<lambda>r s. ex_abs (einvs) s \<and> invs' s \<and>
-                            (\<forall>irq. r = Some irq
-                                   \<longrightarrow> intStateIRQTable (ksInterruptState s) irq \<noteq> irqstate.IRQInactive)"
-                in hoare_strengthen_post)
-    apply (rule hoare_vcg_conj_lift)
-     apply (rule corres_ex_abs_lift)
-      apply (rule dmo_getActiveIRQ_corres)
-     apply wp
-     apply simp
-    apply wp
-     apply simp
-    apply (rule doMachineOp_getActiveIRQ_IRQ_active)
-   apply clarsimp
+     apply (rule handleInterrupt_no_fail)
+    apply (simp add: crunch_simps)
+    apply (rule_tac Q="\<lambda>r s. ex_abs (einvs) s \<and> invs' s \<and>
+                             (\<forall>irq. r = Some irq
+                                    \<longrightarrow> intStateIRQTable (ksInterruptState s) irq \<noteq> irqstate.IRQInactive)"
+                 in hoare_strengthen_post)
+     apply (rule hoare_vcg_conj_lift)
+      apply (rule corres_ex_abs_lift)
+       apply (rule dmo_getActiveIRQ_corres)
+      apply wpsimp
+     apply (wpsimp wp: doMachineOp_getActiveIRQ_IRQ_active)
+    apply clarsimp
+   apply wpsimp
  apply (clarsimp simp: invs'_def valid_state'_def)
  done

--- a/proof/invariant-abstract/ARM/Machine_AI.thy
+++ b/proof/invariant-abstract/ARM/Machine_AI.thy
@ -271,8 +271,7 @@ lemma no_fail_invalidateCacheRange_I[simp, wp]:
 lemma no_fail_invalidateCacheRange_RAM[simp, wp]:
  "no_fail \<top> (invalidateCacheRange_RAM s e p)"
  apply (simp add: invalidateCacheRange_RAM_def lineStart_def cacheLineBits_def)
-  apply (rule no_fail_pre, wp no_fail_invalidateL2Range no_fail_invalidateByVA no_fail_dsb, simp)
-   apply (auto intro: hoare_post_taut)
+  apply (wpsimp wp: no_fail_invalidateL2Range no_fail_invalidateByVA no_fail_dsb)
  done

 lemma no_fail_branchFlushRange[simp, wp]:
--- a/proof/invariant-abstract/ARM_HYP/Machine_AI.thy
+++ b/proof/invariant-abstract/ARM_HYP/Machine_AI.thy
@ -280,8 +280,7 @@ lemma no_fail_invalidateCacheRange_I[simp, wp]:
 lemma no_fail_invalidateCacheRange_RAM[simp, wp]:
  "no_fail \<top> (invalidateCacheRange_RAM s e p)"
  apply (simp add: invalidateCacheRange_RAM_def lineStart_def cacheLineBits_def)
-  apply (rule no_fail_pre, wp no_fail_invalidateL2Range no_fail_invalidateByVA no_fail_dsb, simp)
-   apply (auto intro: hoare_post_taut)
+  apply (wpsimp wp: no_fail_invalidateL2Range no_fail_invalidateByVA no_fail_dsb)
  done

 lemma no_fail_branchFlushRange[simp, wp]:
--- a/proof/refine/AARCH64/TcbAcc_R.thy
+++ b/proof/refine/AARCH64/TcbAcc_R.thy
@ -1599,9 +1599,8 @@ lemma no_fail_asUser [wp]:
  "no_fail \<top> f \<Longrightarrow> no_fail (tcb_at' t) (asUser t f)"
  apply (simp add: asUser_def split_def)
  apply wp
-   apply (simp add: no_fail_def)
-   apply (wp hoare_drop_imps)
-  apply simp
+    apply (simp add: no_fail_def)
+    apply (wpsimp wp: hoare_drop_imps no_fail_threadGet)+
  done

 lemma asUser_setRegister_corres:
--- a/proof/refine/ARM/TcbAcc_R.thy
+++ b/proof/refine/ARM/TcbAcc_R.thy
@ -1534,9 +1534,8 @@ lemma no_fail_asUser [wp]:
  "no_fail \<top> f \<Longrightarrow> no_fail (tcb_at' t) (asUser t f)"
  apply (simp add: asUser_def split_def)
  apply wp
-   apply (simp add: no_fail_def)
-   apply (wp hoare_drop_imps)
-  apply simp
+    apply (simp add: no_fail_def)
+    apply (wpsimp wp: hoare_drop_imps no_fail_threadGet)+
  done

 lemma asUser_setRegister_corres:
--- a/proof/refine/ARM/Tcb_R.thy
+++ b/proof/refine/ARM/Tcb_R.thy
@ -341,9 +341,7 @@ lemma invokeTCB_WriteRegisters_corres:
         apply (rule asUser_corres)
         apply (simp add: zipWithM_mapM getRestartPC_def setNextPC_def)
         apply (rule corres_Id, simp+)
-         apply (rule no_fail_pre, wp no_fail_mapM)
-            apply clarsimp
-            apply (wp no_fail_setRegister | simp)+
+         apply (wpsimp wp: no_fail_mapM no_fail_setRegister)+
        apply (rule corres_split_nor[OF asUser_postModifyRegisters_corres[simplified]])
          apply (rule corres_split_nor[OF corres_when[OF refl restart_corres]])
            apply (rule corres_split_nor[OF corres_when[OF refl rescheduleRequired_corres]])
--- a/proof/refine/ARM_HYP/TcbAcc_R.thy
+++ b/proof/refine/ARM_HYP/TcbAcc_R.thy
@ -1581,9 +1581,8 @@ lemma no_fail_asUser [wp]:
  "no_fail \<top> f \<Longrightarrow> no_fail (tcb_at' t) (asUser t f)"
  apply (simp add: asUser_def split_def)
  apply wp
-   apply (simp add: no_fail_def)
-   apply (wp hoare_drop_imps)
-  apply simp
+    apply (simp add: no_fail_def)
+    apply (wpsimp wp: hoare_drop_imps no_fail_threadGet)+
  done

 lemma asUser_setRegister_corres:
--- a/proof/refine/RISCV64/TcbAcc_R.thy
+++ b/proof/refine/RISCV64/TcbAcc_R.thy
@ -1568,9 +1568,8 @@ lemma no_fail_asUser [wp]:
  "no_fail \<top> f \<Longrightarrow> no_fail (tcb_at' t) (asUser t f)"
  apply (simp add: asUser_def split_def)
  apply wp
-   apply (simp add: no_fail_def)
-   apply (wp hoare_drop_imps)
-  apply simp
+    apply (simp add: no_fail_def)
+    apply (wpsimp wp: hoare_drop_imps no_fail_threadGet)+
  done

 lemma asUser_setRegister_corres:
--- a/proof/refine/RISCV64/Tcb_R.thy
+++ b/proof/refine/RISCV64/Tcb_R.thy
@ -329,8 +329,8 @@ lemma invokeTCB_WriteRegisters_corres:
           apply (clarsimp simp: mask_def user_vtop_def
                           cong: if_cong)
          apply simp
-         apply (rule no_fail_pre, wp no_fail_mapM)
-            apply (clarsimp, (wp no_fail_setRegister | simp)+)
+         apply (wpsimp wp: no_fail_mapM no_fail_setRegister)
+        apply simp
        apply (rule corres_split_nor[OF asUser_postModifyRegisters_corres[simplified]])
          apply (rule corres_split_nor[OF corres_when[OF refl restart_corres]])
            apply (rule corres_split_nor[OF corres_when[OF refl rescheduleRequired_corres]])
--- a/proof/refine/X64/IpcCancel_R.thy
+++ b/proof/refine/X64/IpcCancel_R.thy
@ -1448,10 +1448,7 @@ lemma no_fail_nativeThreadUsingFPU[wp]:
  "no_fail (\<top> and \<top>) (X64.nativeThreadUsingFPU thread)"
  supply Collect_const[simp del]
  apply (simp only: X64.nativeThreadUsingFPU_def)
-  apply (rule no_fail_bind)
-    apply (simp add: Arch.no_fail_machine_op_lift)
-   apply simp
-  apply wp
+  apply (wpsimp wp: Arch.no_fail_machine_op_lift)
  done

 lemma (in delete_one) prepareThreadDelete_corres:
--- a/proof/refine/X64/TcbAcc_R.thy
+++ b/proof/refine/X64/TcbAcc_R.thy
@ -1561,9 +1561,8 @@ lemma no_fail_asUser [wp]:
  "no_fail \<top> f \<Longrightarrow> no_fail (tcb_at' t) (asUser t f)"
  apply (simp add: asUser_def split_def)
  apply wp
-   apply (simp add: no_fail_def)
-   apply (wp hoare_drop_imps)
-  apply simp
+    apply (simp add: no_fail_def)
+    apply (wpsimp wp: hoare_drop_imps no_fail_threadGet)+
  done

 lemma asUser_setRegister_corres:
--- a/proof/refine/X64/Tcb_R.thy
+++ b/proof/refine/X64/Tcb_R.thy
@ -344,7 +344,7 @@ lemma invokeTCB_WriteRegisters_corres:
                                 mask_def user_vtop_def
                           cong: if_cong)
          apply simp
-         apply (rule no_fail_pre, wp no_fail_mapM)
+         apply (wpsimp wp: no_fail_mapM no_fail_setRegister)
            apply (clarsimp simp: sanitiseOrFlags_def sanitiseAndFlags_def)
            apply ((safe)[1], (wp no_fail_setRegister | simp)+)
        apply (rule corres_split_nor[OF asUser_postModifyRegisters_corres[simplified]])
--- a/tools/autocorres/tests/examples/FactorialTest.thy
+++ b/tools/autocorres/tests/examples/FactorialTest.thy
@ -47,7 +47,7 @@ proof (induct n arbitrary: m rule: less_induct)

   show "no_ofail (\<lambda>_. unat x < m) (factorial' m x)"
     apply (subst factorial'.simps)
-     apply (wp induct_asm ovalid_post_triv)
+     apply (wpsimp wp: induct_asm ovalid_post_triv)
     apply unat_arith
    done
 qed