From 99fb0e728e2c6244cd9b89735e1effa84d067fc4 Mon Sep 17 00:00:00 2001 From: Rafal Kolanski Date: Wed, 25 May 2022 12:59:41 +1000 Subject: [PATCH] aarch64 ainvs: add hyp machine op crunches to Machine_AI This indicates potential for using `crunches` to shorten many of the empty_fail, no_fail and no_irq proofs for most machine ops. Signed-off-by: Rafal Kolanski --- .../invariant-abstract/AARCH64/Machine_AI.thy | 25 +++++++++++++++++++ 1 file changed, 25 insertions(+) diff --git a/proof/invariant-abstract/AARCH64/Machine_AI.thy b/proof/invariant-abstract/AARCH64/Machine_AI.thy index 91bd840fd..3c53d9f42 100644 --- a/proof/invariant-abstract/AARCH64/Machine_AI.thy +++ b/proof/invariant-abstract/AARCH64/Machine_AI.thy @@ -196,6 +196,10 @@ lemma no_fail_maskInterrupt[wp]: "no_fail \ (maskInterrupt irq bool)" by (simp add: maskInterrupt_def) +lemma no_irq_bind: + "\ no_irq f; \rv. no_irq (g rv) \ \ no_irq (f >>= g)" + unfolding no_irq_def + by (wpsimp, blast+) lemma no_irq_use: "\ no_irq f; (rv,s') \ fst (f s) \ \ irq_masks s' = irq_masks s" @@ -232,6 +236,27 @@ lemma no_irq_resetTimer: "no_irq resetTimer" lemma no_irq_debugPrint: "no_irq (debugPrint $ xs)" by (simp add: no_irq_def) +(* hyp-related machine op no_irq/no_fail/empty_fail rules + FIXME: names are not in legacy no_irq_* form, so relying on adding them to relevant sets *) + +crunch_ignore (empty_fail) + (add: writeVCPUHardwareReg_impl set_gic_vcpu_ctrl_vmcr_impl set_gic_vcpu_ctrl_apr_impl + set_gic_vcpu_ctrl_lr_impl get_gic_vcpu_ctrl_lr_impl set_gic_vcpu_ctrl_hcr_impl + setSCTLR_impl addressTranslateS1_impl) +crunch_ignore (no_fail) + (add: writeVCPUHardwareReg_impl set_gic_vcpu_ctrl_vmcr_impl set_gic_vcpu_ctrl_apr_impl + set_gic_vcpu_ctrl_lr_impl get_gic_vcpu_ctrl_lr_impl set_gic_vcpu_ctrl_hcr_impl + setSCTLR_impl addressTranslateS1_impl) + +crunches getSCTLR, setSCTLR, addressTranslateS1, + readVCPUHardwareReg, writeVCPUHardwareReg, + get_gic_vcpu_ctrl_vmcr, set_gic_vcpu_ctrl_vmcr, get_gic_vcpu_ctrl_apr, set_gic_vcpu_ctrl_apr, + set_gic_vcpu_ctrl_lr, get_gic_vcpu_ctrl_lr, get_gic_vcpu_ctrl_hcr, set_gic_vcpu_ctrl_hcr + for (no_fail) no_fail[intro!, wp, simp] + and (empty_fail) empty_fail[intro!, wp, simp] + and (no_irq) no_irq[intro!, wp, simp] + (wp: no_irq_bind ignore: empty_fail NonDetMonad.bind) + context notes no_irq[wp] begin lemma no_irq_ackInterrupt: "no_irq (ackInterrupt irq)"