diff --git a/proof/ROOT b/proof/ROOT index 9569f27e5..2ef3ed8e6 100644 --- a/proof/ROOT +++ b/proof/ROOT @@ -56,17 +56,6 @@ session RefineOrphanage in "refine/$L4V_ARCH/orphanage" = Refine + theories "Orphanage" -(* FIXME isa -session BaseRefine2 = BaseRefine + - description \Intermediate point in refinement proof. Useful for machines with small RAM.\ - theories [condition = "SKIP_AINVS_PROOFS", quick_and_dirty, skip_proofs] - "refine/$L4V_ARCH/Untyped_R" - "refine/$L4V_ARCH/Schedule_R" - theories - "refine/$L4V_ARCH/Untyped_R" - "refine/$L4V_ARCH/Schedule_R" -*) - session BaseRefine in "refine/base" = AInvs + description \Background theory and libraries for refinement proof.\ sessions @@ -121,11 +110,9 @@ session CBaseRefine in "crefine" = CSpec + "lib/L4VerifiedLinks" "Include_C" -(* FIXME isa -session AutoCorresCRefine = CRefine + +session AutoCorresCRefine in "crefine/autocorres-test" = CRefine + theories - "crefine/$L4V_ARCH/AutoCorresTest" -*) + "AutoCorresTest" (* * CapDL Refinement @@ -211,16 +198,13 @@ session Bisim in bisim = AInvs + (* * Binary Verification Input Step *) -session SimplExportAndRefine in "asmrefine" = CSpec + +session SimplExportAndRefine in "asmrefine" = SimplExport + theories - "SEL4SimplExport" "SEL4GraphRefine" -(* FIXME isa -session SimplExportOnly = CSpec + +session SimplExport in "asmrefine/export" = CSpec + theories - "asmrefine/SEL4SimplExport" -*) + "SEL4SimplExport" (* * Libraries diff --git a/proof/asmrefine/README.md b/proof/asmrefine/README.md index 84f6bcaf8..4b06833c0 100644 --- a/proof/asmrefine/README.md +++ b/proof/asmrefine/README.md @@ -28,8 +28,8 @@ in the [tools directory](../../tools/asmrefine). Important Theories ------------------ -The [`SEL4SimplExport`](SEL4SimplExport.thy) theory, when executed, exports the -kernel's C semantics into the graph refinement language used by the external -graph refinement toolset. The [`SEL4GraphRefine`](SEL4GraphRefine.thy) theory -establishes that this exported graph semantics is a formal refinement of +The [`SEL4SimplExport`](export/SEL4SimplExport.thy) theory, when executed, +exports the kernel's C semantics into the graph refinement language used by the +external graph refinement toolset. The [`SEL4GraphRefine`](SEL4GraphRefine.thy) +theory establishes that this exported graph semantics is a formal refinement of the kernel's C semantics. diff --git a/proof/asmrefine/SEL4GraphRefine.thy b/proof/asmrefine/SEL4GraphRefine.thy index bed4bc78f..912240957 100644 --- a/proof/asmrefine/SEL4GraphRefine.thy +++ b/proof/asmrefine/SEL4GraphRefine.thy @@ -9,7 +9,7 @@ imports "AsmRefine.ProveGraphRefine" "CSpec.Substitute" "SEL4GlobalsSwap" - "SEL4SimplExport" + "SimplExport.SEL4SimplExport" begin declare ptr_add_assertion_uint [simp del] diff --git a/proof/asmrefine/TestGraphRefine.thy b/proof/asmrefine/TestGraphRefine.thy index 46c3a3af9..4b478d37f 100644 --- a/proof/asmrefine/TestGraphRefine.thy +++ b/proof/asmrefine/TestGraphRefine.thy @@ -9,7 +9,7 @@ imports "AsmRefine.ProveGraphRefine" "CSpec.Substitute" "SEL4GlobalsSwap" - "SEL4SimplExport" + "SimplExport.SEL4SimplExport" begin \\ Name of the C function to investigate. \ diff --git a/proof/asmrefine/SEL4SimplExport.thy b/proof/asmrefine/export/SEL4SimplExport.thy similarity index 100% rename from proof/asmrefine/SEL4SimplExport.thy rename to proof/asmrefine/export/SEL4SimplExport.thy diff --git a/proof/crefine/ARM_HYP/AutoCorresTest.thy b/proof/crefine/ARM_HYP/AutoCorresTest.thy deleted file mode 100644 index 68d9b5352..000000000 --- a/proof/crefine/ARM_HYP/AutoCorresTest.thy +++ /dev/null @@ -1,636 +0,0 @@ -(* - * Copyright 2014, General Dynamics C4 Systems - * - * SPDX-License-Identifier: GPL-2.0-only - *) - -(* Experimental AutoCorres proofs over CRefine: work in progress *) - -theory AutoCorresTest -imports Refine_C -begin - -section \Simple test case: handleYield\ - -autocorres - [ - skip_heap_abs, skip_word_abs, (* for compatibility *) - scope = handleYield doReplyTransfer, - scope_depth = 0, - c_locale = kernel_all_substitute, - no_c_termination - ] "../c/build/$L4V_ARCH/kernel_all.c_pp" - -context kernel_m begin - -text \Export corres_underlying rules for handleYield's callees.\ - -lemma corres_pre_getCurThread_wrapper: - assumes cc: "\rv. corres_underlying {(x, y). cstate_relation x y} True True R (P rv) (P' rv) - (f rv) (f' (tcb_ptr_to_ctcb_ptr rv))" - shows "corres_underlying {(x, y). cstate_relation x y} True True R - (\s. \rv. ksCurThread s = rv \ P rv s) - (\s. \rv. ksCurThread_' s = tcb_ptr_to_ctcb_ptr rv \ P' rv s) - (getCurThread >>= f) (gets ksCurThread_' >>= f')" - (* ugly but works -- corres_symb_exec_l doesn't *) - using cc - apply (clarsimp simp: corres_underlying_def getCurThread_def) - apply monad_eq - apply (clarsimp simp: cstate_relation_def Let_def) - done - -text \ - Proving handleYield_ccorres via handleYield'. - The handleYield spec has one less getCurThread, so we need to use the fact - that tcbSchedDequeue does not modify ksCurThread. -\ -local_setup \AutoCorresModifiesProofs.new_modifies_rules "../c/build/$L4V_ARCH/kernel_all.c_pp"\ -thm tcbSchedDequeue'_modifies - -text \Existing ccorres proof, for reference\ -lemma (* handleYield_ccorres: *) - "ccorres dc xfdc - (invs' and ct_active') - UNIV - [] - (handleYield) - (Call handleYield_'proc)" - apply cinit - apply (rule ccorres_pre_getCurThread) - apply (ctac add: tcbSchedDequeue_ccorres) - apply (ctac add: tcbSchedAppend_ccorres) - apply (ctac add: rescheduleRequired_ccorres) - apply (wp weak_sch_act_wf_lift_linear tcbSchedAppend_valid_objs') - apply (vcg exspec= tcbSchedAppend_modifies) - apply (wp weak_sch_act_wf_lift_linear tcbSchedDequeue_valid_queues) - apply (vcg exspec= tcbSchedDequeue_modifies) - apply (clarsimp simp: tcb_at_invs' invs_valid_objs' - valid_objs'_maxPriority valid_objs'_maxDomain) - apply (auto simp: obj_at'_def st_tcb_at'_def ct_in_state'_def) - done - -lemma reorder_gets: - "(\x. \ \s. x = f s \ g \ \_ s. x = f s \) \ - (do x \ gets f; - g; - h x od) = - (do g; - x \ gets f; - h x od)" - by (fastforce simp: bind_def' NonDetMonad.valid_def gets_def get_def return_def) - -thm - (* no arguments, no precondition, dc return *) - rescheduleRequired_ccorres rescheduleRequired_ccorres[ac] - (* one argument, simple precondition, dc return *) - tcbSchedDequeue_ccorres tcbSchedDequeue_ccorres[ac] - (* multiple arguments, complex precondition, non-dc return *) - handleFaultReply_ccorres handleFaultReply_ccorres[ac] - -text \Now the proof.\ -lemma (* handleYield_ccorres: *) - "ccorres dc xfdc - (invs' and ct_active') - UNIV - [] - (handleYield) - (Call handleYield_'proc)" - apply (ac_init) - apply (simp add: handleYield_def handleYield'_def) - (* Show that current thread is unmodified. - * FIXME: proper way to do this? *) - apply (subst reorder_gets[symmetric, unfolded K_bind_def]) - using tcbSchedDequeue'_modifies apply (fastforce simp: NonDetMonad.valid_def) - apply (subst double_gets_drop_regets) - apply (rule corres_pre_getCurThread_wrapper) - apply (rule corres_split[OF _ tcbSchedDequeue_ccorres[ac]]) - apply (rule corres_split[OF _ tcbSchedAppend_ccorres[ac]]) - apply (rule rescheduleRequired_ccorres[ac]) - apply (solves \wp tcbSchedAppend_valid_objs' weak_sch_act_wf_lift - tcbSchedDequeue_valid_queues - | simp\)+ - apply (clarsimp simp: invs_valid_objs' tcb_at_invs' - valid_objs'_maxPriority valid_objs'_maxDomain) - by (auto simp: obj_at'_def st_tcb_at'_def ct_in_state'_def) - -end - - -section \Function call testcase: handleFault and handleDoubleFault\ - -autocorres - [ - skip_heap_abs, skip_word_abs, (* for compatibility *) - scope = handleDoubleFault, - scope_depth = 0, - c_locale = kernel_all_substitute, - no_c_termination - ] "../c/build/$L4V_ARCH/kernel_all.c_pp" - -context kernel_m begin -local_setup \AutoCorresModifiesProofs.new_modifies_rules "../c/build/$L4V_ARCH/kernel_all.c_pp"\ - -text \Extra corres_underlying rules.\ - -lemma corres_add_noop_rhs2: - "corres_underlying sr nf nf' r P P' f (do _ \ g; return () od) - \ corres_underlying sr nf nf' r P P' f g" - by simp - -(* Use termination (nf=True) to avoid exs_valid *) -lemma corres_noop2_no_exs: - assumes x: "\s. P s \ \(=) s\ f \\r. (=) s\ \ empty_fail f" - assumes y: "\s. P' s \ \(=) s\ g \\r. (=) s\" - assumes z: "nf' \ no_fail P f" "no_fail P' g" - shows "corres_underlying sr True nf' dc P P' f g" - apply (clarsimp simp: corres_underlying_def) - apply (rule conjI) - apply (drule x, drule y) - apply (clarsimp simp: NonDetMonad.valid_def empty_fail_def Ball_def Bex_def) - apply fast - apply (insert z) - apply (clarsimp simp: no_fail_def) - done - -lemma corres_symb_exec_l_no_exs: - assumes z: "\rv. corres_underlying sr True nf' r (Q rv) P' (x rv) y" - assumes x: "\s. P s \ \(=) s\ m \\r. (=) s\ \ empty_fail m" - assumes y: "\P\ m \Q\" - assumes nf: "nf' \ no_fail P m" - shows "corres_underlying sr True nf' r P P' (m >>= (\rv. x rv)) y" - apply (rule corres_guard_imp) - apply (subst gets_bind_ign[symmetric], rule corres_split) - apply (rule z) - apply (rule corres_noop2_no_exs) - apply (erule x) - apply (rule gets_wp) - apply (erule nf) - apply (rule non_fail_gets) - apply (rule y) - apply (rule gets_wp) - apply simp+ - done - -text \Existing ccorres proof, for reference\ -lemma (* handleDoubleFault_ccorres: *) - "ccorres dc xfdc (invs' and tcb_at' tptr and (\s. weak_sch_act_wf (ksSchedulerAction s) s) and - sch_act_not tptr and (\s. \p. tptr \ set (ksReadyQueues s p))) - (UNIV \ {s. tptr_' s = tcb_ptr_to_ctcb_ptr tptr}) - [] (handleDoubleFault tptr ex1 ex2) - (Call handleDoubleFault_'proc)" - apply (cinit lift: tptr_') - apply (subst ccorres_seq_skip'[symmetric]) - apply (ctac (no_vcg)) - apply (rule ccorres_symb_exec_l) - apply (rule ccorres_return_Skip) - apply (wp asUser_inv getRestartPC_inv)+ - apply (rule empty_fail_asUser) - apply (simp add: getRestartPC_def) - apply wp - apply clarsimp - apply (simp add: ThreadState_Inactive_def) - apply (fastforce simp: valid_tcb_state'_def) - done - - -text \New proof of handleDoubleFault\ -lemma (* handleDoubleFault_ccorres: *) - "ccorres dc xfdc (invs' and tcb_at' tptr and (\s. weak_sch_act_wf (ksSchedulerAction s) s) and - sch_act_not tptr and (\s. \p. tptr \ set (ksReadyQueues s p))) - (UNIV \ {s. ex1_' s = ex1' \ tptr_' s = tcb_ptr_to_ctcb_ptr tptr}) - [] (handleDoubleFault tptr ex1 ex2) - (Call handleDoubleFault_'proc)" - apply ac_init - prefer 3 apply simp - apply (unfold handleDoubleFault_def handleDoubleFault'_def K_bind_def) - apply (rule corres_add_noop_rhs2) \ \split out extra haskell code\ - apply (rule corres_split[OF _ setThreadState_ccorres[ac]]) - apply (rule corres_symb_exec_l_no_exs) - apply simp - apply (rule conjI) - apply (wp asUser_inv getRestartPC_inv) - apply (wp empty_fail_asUser) - apply (rule hoare_TrueI) - apply (wpsimp simp: getRestartPC_def) - apply simp - apply (simp add: ThreadState_Inactive_def) - apply wp - apply (rule hoare_TrueI) - by (fastforce simp: valid_tcb_state'_def) - -end - -autocorres - [ - skip_heap_abs, skip_word_abs, (* for compatibility *) - scope = handleFault, - scope_depth = 0, - c_locale = kernel_all_substitute, - no_c_termination - ] "../c/build/$L4V_ARCH/kernel_all.c_pp" - -(* Prove and store modifies rules. *) -context kernel_m begin -local_setup \AutoCorresModifiesProofs.new_modifies_rules "../c/build/$L4V_ARCH/kernel_all.c_pp"\ - -(* TODO: proof for handleFault' *) -thm handleFault'_def -thm handleFault_ccorres - -end - - - - -section \Experiment: translating clzl\ -text \ - __builtin_clzl is defined using guarded_spec_body, - which is a bit hard to translate generically. - This is an experiment to translate clzl manually. -\ -context kernel_all_substitute begin - -thm kernel_m.clzl_spec clzl_body_def - -definition l1_clzl' :: "nat \ (globals myvars, unit + unit) nondet_monad" where - "l1_clzl' rec_measure' \ - L1_spec ({(s', t). (\s. s' \ \s. \<^bsup>s\<^esup>x \ 0\ \ t \ \\ret__long = of_nat (word_clz \<^bsup>s\<^esup>x)\) \ - (\s. s' \ \s. \<^bsup>s\<^esup>x \ 0\)} \ {(s, t). t may_not_modify_globals s})" - -lemma l1_clzl'_corres: - "L1corres ct \ (l1_clzl' rec_measure') (Call clzl_'proc)" - apply (unfold l1_clzl'_def) - apply (rule L1corres_Call) - apply (rule clzl_impl) - apply (unfold clzl_body_def) - apply (rule L1corres_guarded_spec) - done - -definition l2_clzl' :: "nat \ 32 word \ (globals, unit + 32 signed word) nondet_monad" where - "l2_clzl' rec_measure' x \ - L2_seq (L2_guard (\_. x \ 0)) - (\_. L2_gets (\_. of_nat (word_clz x)) [''ret''])" - -lemma l2_clzl'_corres: - "L2corres globals ret__long_' (\_. ()) (\s. x_' s = x) (l2_clzl' rec_measure' x) (l1_clzl' rec_measure')" - apply (unfold l2_clzl'_def l1_clzl'_def) - (* TODO: how to automate this? *) - apply (monad_eq simp: L1_defs L2_defs L2corres_def corresXF_def meq_def) - apply (subst myvars.splits) - apply simp - done - -definition clzl' :: "32 word \ (globals, 32 signed word) nondet_monad" where - "clzl' x \ do guard (\_. x \ 0); - return (of_nat (word_clz x)) od" - -lemma clzl'_TScorres: - "L2_call (l2_clzl' rec_measure' x) = liftE (clzl' x)" - apply (unfold l2_clzl'_def clzl'_def) - apply (tactic \simp_tac (@{context} addsimps - (#lift_rules (the (Monad_Types.get_monad_type "nondet" (Context.Proof @{context}))) - |> Thmtab.dest |> map fst)) 1\) - done - -lemma clzl'_ac_corres: "ac_corres globals ct \ ret__long_' (\s. x_' s = x) (liftE (clzl' x)) (Call clzl_'proc)" - apply (rule ac_corres_chain[OF _ _ L2Tcorres_id corresTA_trivial, simplified o_def, simplified]) - apply (rule l1_clzl'_corres) - apply (rule l2_clzl'_corres) - apply (rule clzl'_TScorres) - done -end - -text \Add our manual translation of clzl into the AutoCorres function info.\ -ML \ -fun phasetab_merge_with merge (tab1, tab2) = - sort_distinct FunctionInfo.phase_ord - (FunctionInfo.Phasetab.keys tab1 @ FunctionInfo.Phasetab.keys tab2) - |> map (fn k => (k, case (FunctionInfo.Phasetab.lookup tab1 k, FunctionInfo.Phasetab.lookup tab2 k) of - (SOME x1, SOME x2) => merge (x1, x2) - | (SOME x1, NONE) => x1 - | (NONE, SOME x2) => x2 - (* (NONE, NONE) impossible *))) - |> FunctionInfo.Phasetab.make; -\ -setup \ -fn thy => -let val clzl_cp = { - name = "clzl", - invented_body = false, - is_simpl_wrapper = false, - callees = Symset.empty, - rec_callees = Symset.empty, - phase = FunctionInfo.CP, - args = [("x", @{typ "32 word"})], - return_type = @{typ "32 signed word"}, - const = @{term "clzl_'proc"}, - raw_const = @{term "clzl_'proc"}, - definition = @{thm kernel_all_substitute.clzl_body_def}, - mono_thm = NONE, - corres_thm = @{thm TrueI} - }: FunctionInfo.function_info; - val clzl_l1 = clzl_cp - |> FunctionInfo.function_info_upd_phase FunctionInfo.L1 - |> FunctionInfo.function_info_upd_const @{term "kernel_all_substitute.l1_clzl'"} - |> FunctionInfo.function_info_upd_definition @{thm kernel_all_substitute.l1_clzl'_def} - |> FunctionInfo.function_info_upd_corres_thm @{thm "kernel_all_substitute.l1_clzl'_corres"}; - val clzl_l2 = clzl_l1 - |> FunctionInfo.function_info_upd_phase FunctionInfo.L2 - |> FunctionInfo.function_info_upd_const @{term "kernel_all_substitute.l2_clzl'"} - |> FunctionInfo.function_info_upd_definition @{thm kernel_all_substitute.l2_clzl'_def} - |> FunctionInfo.function_info_upd_corres_thm @{thm "kernel_all_substitute.l2_clzl'_corres"}; - val clzl_ts = clzl_l2 - |> FunctionInfo.function_info_upd_phase FunctionInfo.TS - |> FunctionInfo.function_info_upd_const @{term "kernel_all_substitute.clzl'"} - |> FunctionInfo.function_info_upd_definition @{thm kernel_all_substitute.clzl'_def} - |> FunctionInfo.function_info_upd_corres_thm @{thm "kernel_all_substitute.clzl'_TScorres"}; - val clzl_info = FunctionInfo.Phasetab.make - (map (fn info => (#phase info, Symtab.make [("clzl", info)])) - [clzl_cp, clzl_l1, clzl_l2, clzl_ts]); - val file = "../c/build/$L4V_ARCH/kernel_all.c_pp"; - val fn_info = the (Symtab.lookup (AutoCorresFunctionInfo.get thy) file); - val fn_info' = phasetab_merge_with (Symtab.merge (K false)) (fn_info, clzl_info); -in - thy - |> AutoCorresFunctionInfo.map (Symtab.update (file, fn_info')) -end -\ - -text \Now AutoCorres will use our specification in calls to clzl.\ -autocorres - [ - skip_heap_abs, skip_word_abs, (* for compatibility *) - scope = chooseThread, - scope_depth = 0, - c_locale = kernel_all_substitute, - no_c_termination - ] "../c/build/$L4V_ARCH/kernel_all.c_pp" - -context kernel_m begin -thm clzl'_def -thm chooseThread'_def -end - - - -subsection \Test recursion + call to previously translated (cap_get_capType)\ -autocorres - [ - skip_heap_abs, skip_word_abs, ts_rules = nondet, (* for compatibility *) - scope = cap_get_capType, - scope_depth = 0, - c_locale = kernel_all_substitute - ] "../c/build/$L4V_ARCH/kernel_all.c_pp" - -thm kernel_all_substitute.cap_get_capType'_def - kernel_all_substitute.cap_get_capType_body_def - -autocorres - [ - skip_heap_abs, skip_word_abs, ts_rules = nondet, (* for compatibility *) - scope = cteDelete finaliseSlot reduceZombie, - scope_depth = 0, - c_locale = kernel_all_substitute - ] "../c/build/$L4V_ARCH/kernel_all.c_pp" - -context kernel_m begin -thm cteDelete'.simps finaliseSlot'.simps reduceZombie'.simps -end - -text \Test call to recursive function group\ -autocorres - [ - skip_heap_abs, skip_word_abs, ts_rules = nondet, (* for compatibility *) - scope = cteRevoke, - scope_depth = 0, - c_locale = kernel_all_substitute - ] "../c/build/$L4V_ARCH/kernel_all.c_pp" - -context kernel_m begin -thm cteRevoke'_def -end - - - -subsection \Experiment with proving bitfield specs\ - -text \ - Here we translate some bitfield functions, then separately prove that - the translated functions satisfy the bitfield_gen specs. -\ -autocorres - [ - skip_heap_abs, skip_word_abs, ts_rules = nondet, (* for compatibility *) - scope = cap_capType_equals - cap_cnode_cap_get_capCNodePtr - cap_cnode_cap_get_capCNodeGuard - cap_cnode_cap_get_capCNodeRadix, - scope_depth = 0, - c_locale = kernel_all_substitute - ] "../c/build/$L4V_ARCH/kernel_all.c_pp" - -lemma of_bl_from_cond: - "(if C then 1 else 0) = of_bl [C]" - by (simp add: word_1_bl) -lemma of_bl_cond: - "(if C then of_bl [A] else of_bl [B]) = of_bl [if C then A else B]" - by (rule if_f) - -context kernel_m begin -lemma "\\_. cap_get_tag cap = scast cap_cnode_cap\ - cap_cnode_cap_get_capCNodePtr' cap - \\r _. r = capCNodePtr_CL (cap_cnode_cap_lift cap)\!" - apply (unfold cap_cnode_cap_get_capCNodePtr'_def) - apply wp - apply (simp add: cap_get_tag_def cap_cnode_cap_lift_def cap_lift_def cap_tag_values - shiftr_over_and_dist mask_def) - done - -lemma "\\_. cap_get_tag cap = scast cap_cnode_cap\ - cap_cnode_cap_get_capCNodeGuard' cap - \\r _. r = capCNodeGuard_CL (cap_cnode_cap_lift cap)\!" - apply (unfold cap_cnode_cap_get_capCNodeGuard'_def) - apply wp - apply (simp add: cap_get_tag_def cap_cnode_cap_lift_def cap_lift_def cap_tag_values - shiftr_over_and_dist mask_def) - done - -lemma "\\_. cap_get_tag cap = scast cap_cnode_cap\ - cap_cnode_cap_get_capCNodeRadix' cap - \\r _. r = capCNodeRadix_CL (cap_cnode_cap_lift cap)\!" - apply (unfold cap_cnode_cap_get_capCNodeRadix'_def) - apply wp - apply (simp add: cap_get_tag_def cap_cnode_cap_lift_def cap_lift_def cap_tag_values - shiftr_over_and_dist mask_def) - done - -end - - -subsection \Experiment with transferring bitfield specs\ - -text \ - For wrapped bitfield functions, the @{term hoarep} triples for them can be transferred - to @{term valid} triples. -\ -context kernel_m begin - -thm cap_zombie_cap_get_capZombiePtr_spec -lemma cap_zombie_cap_get_capZombiePtr'_spec: - "\\s. s = s0 \ cap_get_tag cap = scast cap_zombie_cap \ get_capZombieBits_CL (cap_zombie_cap_lift cap) < 0x1F\ - cap_zombie_cap_get_capZombiePtr' cap - \\r s. s = s0 \ r = get_capZombiePtr_CL (cap_zombie_cap_lift cap)\" - (* setup *) - apply (rule hoare_weaken_pre) - apply (rule hoare_strengthen_post) - (* generic transfer operation *) - thm autocorres_transfer_spec_no_modifies[OF - cap_zombie_cap_get_capZombiePtr'_def cap_zombie_cap_get_capZombiePtr_spec] - apply (rule autocorres_transfer_spec_no_modifies[OF - cap_zombie_cap_get_capZombiePtr'_def cap_zombie_cap_get_capZombiePtr_spec _ refl, - where cs="undefined\globals := s0, cap_' := cap\"]) - (* the standard tactics can't invent a suitable cs automatically *) - apply (rule cap_zombie_cap_get_capZombiePtr_modifies) - (* prove sanity conditions on local variables and preconds *) - apply auto - done - -thm cap_zombie_cap_get_capZombieType_spec -lemma cap_zombie_cap_get_capZombieType'_spec: - "\\s. s = s0 \ cap_get_tag cap = scast cap_zombie_cap \ - cap_zombie_cap_get_capZombieType' cap - \\r s. s = s0 \ r = capZombieType_CL (cap_zombie_cap_lift cap)\" - apply (rule hoare_weaken_pre) - apply (rule hoare_strengthen_post) - thm autocorres_transfer_spec_no_modifies[OF - cap_zombie_cap_get_capZombieType'_def cap_zombie_cap_get_capZombieType_spec] - apply (rule autocorres_transfer_spec_no_modifies[OF - cap_zombie_cap_get_capZombieType'_def cap_zombie_cap_get_capZombieType_spec _ refl, - where cs="undefined\globals := s0, cap_' := cap\"]) - apply (rule cap_zombie_cap_get_capZombieType_modifies) - apply auto - done - -text \There are some extra complications when transferring bitfield update specs\ -thm cap_zombie_cap_set_capZombieNumber_spec (* extra quantified var; precond talks about initial state *) -lemma cap_zombie_cap_set_capZombieNumber'_spec: - "\\s. s = s0 \ ccap_relation cap' cap \ isZombie cap' \ capAligned cap' \ unat n \ zombieCTEs (capZombieType cap')\ - cap_zombie_cap_set_capZombieNumber' cap n - \\r s. s = s0 \ ccap_relation (capZombieNumber_update (\_. unat n) cap') r\" - apply (rule hoare_weaken_pre) - apply (rule hoare_strengthen_post) - (* All_to_all' drops the extra quantifier. (rule_format would remove both) *) - thm autocorres_transfer_spec_no_modifies[OF - cap_zombie_cap_set_capZombieNumber'_def cap_zombie_cap_set_capZombieNumber_spec[THEN All_to_all']] - apply (rule autocorres_transfer_spec_no_modifies[OF - cap_zombie_cap_set_capZombieNumber'_def cap_zombie_cap_set_capZombieNumber_spec[THEN All_to_all'], - where cs="undefined\globals := s0, cap_' := cap, n_' := n\"]) - apply (rule cap_zombie_cap_set_capZombieNumber_modifies) - (* swap initial state var to allow unification *) - apply (rule collect_unlift) - apply auto - done - -thm cap_capType_equals_spec -lemma cap_capType_equals'_spec: - "\\s. s = s0 \ - AC_call_L1 (\s. cap_' s = cap \ cap_type_tag_' s = cap_type_tag) globals ret__int_' - (L1_call_simpl check_termination \ cap_capType_equals_'proc) - \\r s. s = s0 \ r = of_bl [cap_get_tag cap = cap_type_tag]\" - apply (rule hoare_weaken_pre) - apply (rule hoare_strengthen_post) - thm autocorres_transfer_spec_no_modifies[OF reflexive cap_capType_equals_spec] - apply (rule autocorres_transfer_spec_no_modifies[ - OF reflexive cap_capType_equals_spec, - where cs="undefined\globals := s0, cap_' := cap, cap_type_tag_' := cap_type_tag\"]) - apply (rule cap_capType_equals_modifies) - apply auto - done - -(* TODO: any other types of bitfield_gen functions? *) - -end - - - -context kernel_m begin -text \Termination proofs for use with @{thm ccorres_to_corres_with_termination}. Currently unused.\ - -lemma cap_get_capType_terminates: - "\ \ Call cap_get_capType_'proc \ Normal s" - apply (tactic \ALLGOALS (terminates_trivial_tac @{context})\; - fail) - done - -lemma thread_state_get_tcbQueued_terminates: - "\ \ Call thread_state_get_tcbQueued_'proc \ Normal s" - apply (tactic \ALLGOALS (terminates_trivial_tac @{context})\; - fail) - done - -lemma thread_state_ptr_set_tcbQueued_terminates: - "\ \ Call thread_state_ptr_set_tcbQueued_'proc \ Normal s" - apply (tactic \ALLGOALS (terminates_trivial_tac @{context})\; - fail) - done - -lemma ready_queues_index_terminates: - "\ \ Call ready_queues_index_'proc \ Normal s" - apply (tactic \ALLGOALS (terminates_trivial_tac @{context})\; - fail) - done - -lemma prio_to_l1index_terminates: - "\ \ Call prio_to_l1index_'proc \ Normal s" - apply (tactic \ALLGOALS (terminates_trivial_tac @{context})\; - fail) - done - -lemma removeFromBitmap_terminates: - "\ \ Call removeFromBitmap_'proc \ Normal s" - apply (tactic \ALLGOALS (terminates_trivial_tac @{context})\; - rule prio_to_l1index_terminates) - done - -lemma addToBitmap_terminates: - "\ \ Call addToBitmap_'proc \ Normal s" - apply (tactic \ALLGOALS (terminates_trivial_tac @{context})\; - rule prio_to_l1index_terminates) - done - -lemma tcbSchedDequeue_terminates: - "\ \ Call tcbSchedDequeue_'proc \ Normal s" - apply (tactic \ALLGOALS (terminates_trivial_tac @{context})\; - rule thread_state_get_tcbQueued_terminates - thread_state_ptr_set_tcbQueued_terminates - ready_queues_index_terminates - removeFromBitmap_terminates) - done - -lemma tcbSchedAppend_terminates: - "\ \ Call tcbSchedAppend_'proc \ Normal s" - apply (tactic \ALLGOALS (terminates_trivial_tac @{context})\; - rule thread_state_get_tcbQueued_terminates - thread_state_ptr_set_tcbQueued_terminates - ready_queues_index_terminates - addToBitmap_terminates) - done - -lemma tcbSchedEnqueue_terminates: - "\ \ Call tcbSchedEnqueue_'proc \ Normal s" - apply (tactic \ALLGOALS (terminates_trivial_tac @{context})\; - rule thread_state_get_tcbQueued_terminates - thread_state_ptr_set_tcbQueued_terminates - ready_queues_index_terminates - addToBitmap_terminates) - done - -lemma rescheduleRequired_terminates: - "\ \ Call rescheduleRequired_'proc \ Normal s" - apply (tactic \ALLGOALS (terminates_trivial_tac @{context})\; - rule tcbSchedEnqueue_terminates) - done - -end - -end diff --git a/proof/crefine/RISCV64/AutoCorresTest.thy b/proof/crefine/RISCV64/AutoCorresTest.thy deleted file mode 100644 index 9f8690cf6..000000000 --- a/proof/crefine/RISCV64/AutoCorresTest.thy +++ /dev/null @@ -1,13 +0,0 @@ -(* - * Copyright 2014, General Dynamics C4 Systems - * - * SPDX-License-Identifier: GPL-2.0-only - *) - -theory AutoCorresTest -imports Refine_C -begin - -(* empty stub, currently tested for ARM and ARM_HYP only *) - -end diff --git a/proof/crefine/X64/AutoCorresTest.thy b/proof/crefine/X64/AutoCorresTest.thy deleted file mode 100644 index 9f8690cf6..000000000 --- a/proof/crefine/X64/AutoCorresTest.thy +++ /dev/null @@ -1,13 +0,0 @@ -(* - * Copyright 2014, General Dynamics C4 Systems - * - * SPDX-License-Identifier: GPL-2.0-only - *) - -theory AutoCorresTest -imports Refine_C -begin - -(* empty stub, currently tested for ARM and ARM_HYP only *) - -end diff --git a/proof/crefine/ARM/AutoCorresTest.thy b/proof/crefine/autocorres-test/AutoCorresTest.thy similarity index 100% rename from proof/crefine/ARM/AutoCorresTest.thy rename to proof/crefine/autocorres-test/AutoCorresTest.thy