415 lines
18 KiB
Plaintext
Executable File
415 lines
18 KiB
Plaintext
Executable File
(*
|
|
*
|
|
* Copyright 2017, Data61, CSIRO
|
|
*
|
|
* This software may be distributed and modified according to the terms of
|
|
* the GNU General Public License version 2. Note that NO WARRANTY is provided.
|
|
* See "LICENSE_GPLv2.txt" for details.
|
|
*
|
|
* @TAG(DATA61_GPL)
|
|
*)
|
|
|
|
(*
|
|
Test proofs for corres methods. Builds on AInvs image.
|
|
*)
|
|
|
|
theory Corres_Test
|
|
imports "Refine.VSpace_R" "Lib.Corres_Method"
|
|
begin
|
|
|
|
chapter \<open>The Corres Method\<close>
|
|
|
|
section \<open>Introduction\<close>
|
|
|
|
text \<open>The @{method corres} method tries to do for corres-style refinement proofs what
|
|
@{method wp} did for hoare logic proofs. The intention is to automate the application
|
|
of corres calculational rules, so that the bulk of the manual proof is now handling
|
|
a verification condition. In general refinement proofs are difficult to automate, so here we
|
|
exploit the fact that in l4v the abstract and executable specifications tend to be structurally
|
|
similar. Corres proofs are based on the @{const corres_underlying} constant, which takes a number
|
|
of parameters that allow it to be specialized for different flavours of refinement.
|
|
|
|
A corres statement has the following form: @{term "corres_underlying sr nf nf' r P P' f f'"}, where
|
|
@{term sr} is a state-relation, @{term nf} and @{term nf'} refer to whether or not the left and
|
|
right hand functions may fail, @{term r} is a return value relation between the functions, @{term P}
|
|
and @{term P'} are preconditions for the functions @{term f} and @{term f'} respectively. Informally
|
|
the statement says that: under the given preconditions, for every execution of @{term f'} there exists
|
|
an execution of @{term f} that is related by the given state relation @{term sr} and return-value
|
|
relation @{term r}.
|
|
|
|
If the left and right side of a corres statement share similar structure, we can "unzip" the function
|
|
into one corres obligation for each atomic function. This is done through the application of
|
|
@{thm corres_split}.
|
|
\<close>
|
|
|
|
thm corres_split[no_vars]
|
|
|
|
text \<open>Briefly this states that: given a corres goal proving refinement between @{term "a >>= b"} and
|
|
@{term "c >>= d"}, we can decompose this into a proof showing refinement between @{term a} and
|
|
@{term c}, and between @{term a} and @{term c}. Additionally @{term a} and @{term c} must establish
|
|
appropriate postconditions to satisfy the obligations of proving refinement between @{term b} and @{term d}.
|
|
|
|
The first subgoal that is produced has an important characteristic: the preconditions for each
|
|
side may only discuss the return value of its respective side. This means that rules such as
|
|
@{term "corres_underlying sr nf nf' r (\<lambda>s. x = x') (\<lambda>_. True) (f x) (f' x')"} will not apply to a goal
|
|
if @{term x} and @{term x'} are variables generated by applying @{thm corres_split} (i.e. the
|
|
return values of functions).
|
|
|
|
This means that any such conditions must instead be phrased as an assumption to the rule, and our rule must be
|
|
rephrased as follows:
|
|
@{term "x = x' \<Longrightarrow> corres_underlying sr nf nf' r (\<lambda>_. True) (\<lambda>_. True) (f x) (f' x')"}.
|
|
The result is that we must solve @{term "x = x'"} immediately after applying our rule. While this
|
|
is not a major concern for a manual proof, it proves to be a significant obstacle if we're trying
|
|
to focus on automating the "corres" part of the refinement.
|
|
\<close>
|
|
|
|
section \<open>corres_underlyingK and corres_rv\<close>
|
|
|
|
text \<open>To remedy this situation, we augment the @{const corres_underlying} definition to include
|
|
yet another flag: a single boolean. This new constant: @{const corres_underlyingK},
|
|
will form the basis of the calculus for our corres method.\<close>
|
|
|
|
thm corres_underlyingK_def[no_vars]
|
|
|
|
text \<open>The boolean in @{const corres_underlyingK} can be thought of as a stateless precondition. It
|
|
is used to propagate additional proof obligations for rules that either do not need to discuss
|
|
either the left or right hand state, or must discuss bound variables from both sides.\<close>
|
|
|
|
thm corresK_split[no_vars]
|
|
|
|
text \<open>In this split rule for @{const corres_underlyingK} we see that the additional precondition @{term F'}
|
|
may discuss both @{term rv} and @{term rv'}. To show that this condition is satisified, however,
|
|
we can't use hoare logic and instead need a new definition: @{const corres_rv}.\<close>
|
|
|
|
thm corres_rv_def_I_know_what_I'm_doing[no_vars]
|
|
|
|
text \<open>This is a weaker form of @{const corres_underlying} that is only interested in the return value
|
|
of the functions. In essence, it states the given functions will establish @{term Q} after executing,
|
|
assuming the given return-value relation @{term r} holds, along with the given stateless precondition
|
|
@{term F} and left/right preconditions @{term P} and @{term P'}.
|
|
|
|
The assumption in general is that corres_rv rules should never be written, instead corres_rv obligations
|
|
should be propagated into either the stateless precondition (@{term F} from @{term corres_underlyingK}),
|
|
the left precondition (@{term P}) or the right precondition @{term P'}. This is implicitly handled
|
|
by @{method corres_rv} (called from @{method corres}) by applying one of the following rules to each conjunct:\<close>
|
|
|
|
thm corres_rv_defer
|
|
thm corres_rv_wp_left
|
|
thm corres_rv_wp_right
|
|
|
|
text \<open>If none of these rules can be safely applied, then @{method corres_rv} will leave the
|
|
obligation untouched. The user can manually apply one of them if desired, but this is liable to
|
|
create unsolvable proof obligations. In the worst case, the user may manually solve the goal in-place.\<close>
|
|
|
|
thm corres_rv_proveT[no_vars]
|
|
|
|
section \<open>The corres method\<close>
|
|
|
|
text \<open>The core algorithm of the corres method is simple:
|
|
1) start by applying any necessary weakening rules to ensure the goal has schematic preconditions
|
|
2) apply a known @{thm corres} or @{thm corresK} rule (see next section)
|
|
3) if unsuccessful, apply a split rule (i.e. @{thm corresK_split}) and go to 2
|
|
|
|
Importantly, @{method corres} will not split a goal if it ultimately is not able to apply at least
|
|
one @{thm corres} or @{thm corresK} rule.
|
|
\<close>
|
|
|
|
subsection \<open>The corres and corresK named_theorems\<close>
|
|
|
|
text \<open>To address the fact that existing refinement rules are phrased as @{const corres_underlying}
|
|
and not @{const corres_underlyingK} there are two different named_theorems that are used for different
|
|
kind of rules @{thm corres} and @{thm corresK}. A @{thm corres} rule is understood to be phrased
|
|
with @{const corres_underlying} and may have additional assumptions. These assumptions will be
|
|
propagated through the additional @{term F} flag in @{const corres_underlyingK}, rather than presented
|
|
as proof obligations immediately. A @{thm corresK} rule is understood to be phrased with
|
|
@{const corres_underlyingK}, and is meant for calculational rules which may have proper assumptions that
|
|
should not be propagated.
|
|
\<close>
|
|
thm corresK
|
|
thm corres
|
|
|
|
subsection \<open>The corresc method\<close>
|
|
|
|
text \<open>Similar to @{method wpc}, @{method corresc} can handle case statements in @{const corres_underlyingK}
|
|
proof goals. Importantly, however, it is split into two sub-methods @{method corresc_left} and
|
|
@{method corresc_right}, which perform case-splitting on each side respectively. The combined method
|
|
@{method corresc}, however, attempts to discharge the contradictions that arise from the quadratic
|
|
blowup of a case analysis on both the left and right sides.\<close>
|
|
|
|
subsection \<open>corres_concrete_r, corres_concrete_rE\<close>
|
|
|
|
text \<open>Some @{thm corresK} rules should only be applied if certain variables are concrete
|
|
(i.e. not schematic) in the goal. These are classified separately with the named_theorems
|
|
@{thm corres_concrete_r} and @{thm corres_concrete_rER}. The first
|
|
indicates that the return value relation of the goal must be concrete, the second indicates that
|
|
only the left side of the error relation must be concrete.\<close>
|
|
|
|
thm corres_concrete_r
|
|
thm corres_concrete_rER
|
|
|
|
subsection \<open>The corres_search method\<close>
|
|
|
|
text \<open>The purpose of @{method corres_search} is to address cases where there is non-trivial control flow.
|
|
In particular: in the case where there is an "if" statement or either side needs to be symbolically
|
|
executed. The core idea is that corres_search should be provided with a "search" rule that acts
|
|
as an anchoring point. Symbolic execution and control flow is decomposed until either the given
|
|
rule is successfully applied or all search branches are exhausted.\<close>
|
|
|
|
subsubsection \<open>Symbolic Execution\<close>
|
|
|
|
text \<open>Symbolic execution is handled by two named theorems:
|
|
@{thm corres_symb_exec_ls} and @{thm corres_symb_exec_rs}, which perform symbolic execution on
|
|
the left and right hand sides of a corres goal.\<close>
|
|
|
|
thm corres_symb_exec_ls
|
|
thm corres_symb_exec_rs
|
|
|
|
text \<open>A function may be symbolically executed if it does not modify the state, i.e. its only purpose
|
|
is to compute some value and return it. After being symbolically executed,
|
|
this value can only be discussed by the precondition of the associated side or the stateless
|
|
precondition of corresK. The resulting @{const corres_rv} goal has @{const corres_noop} as the
|
|
function on the alternate side. This gives @{method corres_rv} a hint that the resulting obligation
|
|
should be aggressively re-written into a hoare triple over @{term m} if it can't be propagated
|
|
back statelessly safely.
|
|
\<close>
|
|
|
|
|
|
section \<open>Demo\<close>
|
|
|
|
|
|
context begin interpretation Arch .
|
|
|
|
(* VSpace_R *)
|
|
|
|
|
|
lemmas load_hw_asid_corres_args[corres] =
|
|
load_hw_asid_corres[@lift_corres_args]
|
|
|
|
lemmas invalidate_asid_corres_args[corres] =
|
|
invalidate_asid_corres[@lift_corres_args]
|
|
|
|
lemmas invalidate_hw_asid_entry_corres_args[corres] =
|
|
invalidate_hw_asid_entry_corres[@lift_corres_args]
|
|
|
|
lemma invalidate_asid_entry_corres:
|
|
"corres dc (valid_vspace_objs and valid_asid_map
|
|
and K (asid \<le> mask asid_bits \<and> asid \<noteq> 0)
|
|
and vspace_at_asid asid pd and valid_vs_lookup
|
|
and unique_table_refs o caps_of_state
|
|
and valid_global_objs and valid_arch_state
|
|
and pspace_aligned and pspace_distinct)
|
|
(pspace_aligned' and pspace_distinct' and no_0_obj')
|
|
(invalidate_asid_entry asid) (invalidateASIDEntry asid)"
|
|
apply (simp add: invalidate_asid_entry_def invalidateASIDEntry_def)
|
|
apply_debug (trace) (* apply_trace between steps *)
|
|
(tags "corres") (* break at breakpoints labelled "corres" *)
|
|
corres (* weaken precondition *)
|
|
continue (* split *)
|
|
continue (* solve load_hw_asid *)
|
|
continue (* split *)
|
|
continue (* apply corres_when *)
|
|
continue (* trivial simplification *)
|
|
continue (* invalidate _hw_asid_entry *)
|
|
finish (* invalidate_asid *)
|
|
|
|
apply (corressimp wp: load_hw_asid_wp)+
|
|
apply clarsimp
|
|
apply (fastforce simp: pd_at_asid_uniq)
|
|
done
|
|
|
|
|
|
crunch typ_at'[wp]: invalidateASIDEntry, flushSpace "typ_at' T t"
|
|
crunch ksCurThread[wp]: invalidateASIDEntry, flushSpace "\<lambda>s. P (ksCurThread s)"
|
|
crunch obj_at'[wp]: invalidateASIDEntry, flushSpace "obj_at' P p"
|
|
|
|
lemmas flush_space_corres_args[corres] =
|
|
flush_space_corres[@lift_corres_args]
|
|
|
|
lemmas invalidate_asid_entry_corres_args[corres] =
|
|
invalidate_asid_entry_corres[@lift_corres_args]
|
|
|
|
|
|
lemma corres_inst_eq_ext:
|
|
"(\<And>x. corres_inst_eq (f x) (f' x)) \<Longrightarrow> corres_inst_eq f f'"
|
|
by (auto simp add: corres_inst_eq_def)
|
|
|
|
lemma delete_asid_corresb:
|
|
notes [corres] = corres_gets_asid gct_corres set_asid_pool_corres and
|
|
[@lift_corres_args, corres] = get_asid_pool_corres_inv'
|
|
invalidate_asid_entry_corres
|
|
set_vm_root_corres
|
|
notes [wp] = set_asid_pool_asid_map_unmap set_asid_pool_vs_lookup_unmap'
|
|
set_asid_pool_vspace_objs_unmap'
|
|
invalidate_asid_entry_invalidates
|
|
getASID_wp
|
|
shows
|
|
"corres dc
|
|
(invs and valid_etcbs and K (asid \<le> mask asid_bits \<and> asid \<noteq> 0))
|
|
(pspace_aligned' and pspace_distinct' and no_0_obj'
|
|
and valid_arch_state' and cur_tcb')
|
|
(delete_asid asid pd) (deleteASID asid pd)"
|
|
apply (simp add: delete_asid_def deleteASID_def)
|
|
apply_debug (trace) (* apply_trace between steps *)
|
|
(tags "corres") (* break at breakpoints labelled "corres" *)
|
|
corres (* weaken precondition *)
|
|
continue (* split *)
|
|
continue (* gets rule *)
|
|
continue (* corresc *)
|
|
continue (* return rule *)
|
|
continue (* split *)
|
|
continue (* function application *)
|
|
continue (* liftM rule *)
|
|
continue (* get_asid_pool_corres_inv' *)
|
|
continue (* function application *)
|
|
continue (* function application *)
|
|
continue (* corresK_when *)
|
|
continue (* split *)
|
|
continue (* flush_space_corres *)
|
|
continue (* K_bind *)
|
|
continue (* K_bind *)
|
|
continue (* split *)
|
|
continue (* invalidate_asid_entry_corres *)
|
|
continue (* K_bind *)
|
|
continue (* return bind *)
|
|
continue (* K_bind *)
|
|
continue (* split *)
|
|
continue (* backtracking *)
|
|
continue (* split *)
|
|
continue (* function application *)
|
|
continue (* set_asid_pool_corres *)
|
|
continue (* K_bind *)
|
|
continue (* K_bind *)
|
|
continue (* split *)
|
|
continue (* gct_corres *)
|
|
continue (* set_vm_root_corres *)
|
|
finish (* backtracking? *)
|
|
apply (corressimp simp: mask_asid_low_bits_ucast_ucast
|
|
| fold cur_tcb_def | wps)+
|
|
apply (frule arm_asid_table_related,clarsimp)
|
|
apply (rule conjI)
|
|
apply (intro impI allI)
|
|
apply (rule conjI)
|
|
apply (safe; assumption?)
|
|
apply (rule ext)
|
|
apply (fastforce simp: inv_def dest: ucast_ucast_eq)
|
|
apply (rule context_conjI)
|
|
apply (fastforce simp: o_def dest: valid_asid_tableD invs_valid_asid_table)
|
|
apply (intro allI impI)
|
|
apply (subgoal_tac "vspace_at_asid asid pd s")
|
|
prefer 2
|
|
apply (simp add: vspace_at_asid_def)
|
|
apply (rule vs_lookupI)
|
|
apply (simp add: vs_asid_refs_def)
|
|
apply (rule image_eqI[OF refl])
|
|
apply (rule graph_ofI)
|
|
apply fastforce
|
|
apply (rule r_into_rtrancl)
|
|
apply simp
|
|
apply (rule vs_lookup1I [OF _ _ refl], assumption)
|
|
apply (simp add: vs_refs_def)
|
|
apply (rule image_eqI[rotated], erule graph_ofI)
|
|
apply (simp add: mask_asid_low_bits_ucast_ucast)
|
|
prefer 2
|
|
apply (intro allI impI context_conjI; assumption?)
|
|
apply (rule aligned_distinct_relation_asid_pool_atI'; fastforce?)
|
|
apply (fastforce simp: o_def dest: valid_asid_tableD invs_valid_asid_table)
|
|
apply (simp add: cur_tcb'_def)
|
|
apply (safe; assumption?)
|
|
apply (erule ko_at_weakenE)
|
|
apply (clarsimp simp: graph_of_def)
|
|
apply (fastforce split: if_split_asm)
|
|
apply (frule invs_vspace_objs)
|
|
apply (drule (2) valid_vspace_objsD)
|
|
apply (erule ranE)
|
|
apply (fastforce split: if_split_asm)
|
|
apply (erule ko_at_weakenE)
|
|
apply (clarsimp simp: graph_of_def)
|
|
apply (fastforce split: if_split_asm)
|
|
done
|
|
|
|
lemma cte_wp_at_ex:
|
|
"cte_wp_at (\<lambda>_. True) p s \<Longrightarrow> (\<exists>cap. cte_wp_at ((=) cap) p s)"
|
|
by (simp add: cte_wp_at_def)
|
|
|
|
(* Sadly broken:
|
|
lemma set_vm_root_for_flush_corres:
|
|
notes [corres] = gct_corres getSlotCap_corres
|
|
shows
|
|
"corres (=)
|
|
(cur_tcb and vspace_at_asid asid pd
|
|
and K (asid \<noteq> 0 \<and> asid \<le> mask asid_bits)
|
|
and valid_asid_map and valid_vs_lookup
|
|
and valid_vspace_objs and valid_global_objs
|
|
and unique_table_refs o caps_of_state
|
|
and valid_arch_state
|
|
and pspace_aligned and pspace_distinct)
|
|
(pspace_aligned' and pspace_distinct' and no_0_obj')
|
|
(set_vm_root_for_flush pd asid)
|
|
(setVMRootForFlush pd asid)"
|
|
apply (simp add: set_vm_root_for_flush_def setVMRootForFlush_def getThreadVSpaceRoot_def locateSlot_conv)
|
|
apply corres
|
|
apply_debug (trace) (tags "corres_search") (corres_search search: arm_context_switch_corres)
|
|
continue (* step left *)
|
|
continue (* if rule *)
|
|
continue (* failed corres on first subgoal, trying next *)
|
|
continue (* fail corres on last subgoal, trying reverse if rule *)
|
|
continue (* can't make corres progress here, trying other goal *)
|
|
finish (* successful goal discharged by corres *)
|
|
|
|
apply (corressimp wp: get_cap_wp getSlotCap_wp)+
|
|
apply (rule context_conjI)
|
|
subgoal by (simp add: cte_map_def objBits_simps tcb_cnode_index_def
|
|
tcbVTableSlot_def to_bl_1 cte_level_bits_def)
|
|
apply (rule context_conjI)
|
|
subgoal by (fastforce simp: cur_tcb_def intro!: tcb_at_cte_at_1[simplified])
|
|
apply (rule conjI)
|
|
subgoal by (fastforce simp: isCap_simps)
|
|
apply (drule cte_wp_at_ex)
|
|
apply clarsimp
|
|
apply (drule (1) pspace_relation_cte_wp_at[rotated 1]; (assumption | clarsimp)?)
|
|
apply (drule cte_wp_at_norm')
|
|
apply clarsimp
|
|
apply (rule_tac x="cteCap cte" in exI)
|
|
apply (auto elim: cte_wp_at_weakenE' dest!: curthread_relation)
|
|
done
|
|
|
|
text \<open>Note we can wrap it all up in corressimp\<close>
|
|
|
|
lemma set_vm_root_for_flush_corres':
|
|
notes [corres] = gct_corres getSlotCap_corres
|
|
shows
|
|
"corres (=)
|
|
(cur_tcb and vspace_at_asid asid pd
|
|
and K (asid \<noteq> 0 \<and> asid \<le> mask asid_bits)
|
|
and valid_asid_map and valid_vs_lookup
|
|
and valid_vspace_objs and valid_global_objs
|
|
and unique_table_refs o caps_of_state
|
|
and valid_arch_state
|
|
and pspace_aligned and pspace_distinct)
|
|
(pspace_aligned' and pspace_distinct' and no_0_obj')
|
|
(set_vm_root_for_flush pd asid)
|
|
(setVMRootForFlush pd asid)"
|
|
apply (simp add: set_vm_root_for_flush_def setVMRootForFlush_def getThreadVSpaceRoot_def locateSlot_conv)
|
|
apply (corressimp search: arm_context_switch_corres
|
|
wp: get_cap_wp getSlotCap_wp
|
|
simp: isCap_simps)
|
|
apply (rule context_conjI)
|
|
subgoal by (simp add: cte_map_def objBits_simps tcb_cnode_index_def
|
|
tcbVTableSlot_def to_bl_1 cte_level_bits_def)
|
|
apply (rule context_conjI)
|
|
subgoal by (fastforce simp: cur_tcb_def intro!: tcb_at_cte_at_1[simplified])
|
|
apply (rule conjI)
|
|
subgoal by (fastforce)
|
|
apply (drule cte_wp_at_ex)
|
|
apply clarsimp
|
|
apply (drule (1) pspace_relation_cte_wp_at[rotated 1]; (assumption | clarsimp)?)
|
|
apply (drule cte_wp_at_norm')
|
|
apply clarsimp
|
|
apply (rule_tac x="cteCap cte" in exI)
|
|
apply (auto elim: cte_wp_at_weakenE' dest!: curthread_relation)
|
|
done
|
|
*)
|
|
|
|
end
|
|
end
|