lib: fix further no_fail errors squash

Signed-off-by: Michael McInerney <[email protected]>
seL4 · Jan 14, 2024 · e48e495 · e48e495
1 parent 4b8866e
commit e48e495
Show file tree

Hide file tree

Showing 2 changed files with 14 additions and 17 deletions.
diff --git 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
 

diff --git 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