1(*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: GPL-2.0-only
5 *)
6
7(*
8   Test proofs for corres methods. Builds on AInvs image.
9*)
10
11theory Corres_Test
12imports "Refine.VSpace_R" "Lib.Corres_Method"
13begin
14
15chapter \<open>The Corres Method\<close>
16
17section \<open>Introduction\<close>
18
19text \<open>The @{method corres} method tries to do for corres-style refinement proofs what
20@{method wp} did for hoare logic proofs. The intention is to automate the application
21of corres calculational rules, so that the bulk of the manual proof is now handling
22a verification condition. In general refinement proofs are difficult to automate, so here we
23exploit the fact that in l4v the abstract and executable specifications tend to be structurally
24similar. Corres proofs are based on the @{const corres_underlying} constant, which takes a number
25of parameters that allow it to be specialized for different flavours of refinement.
26
27A corres statement has the following form: @{term "corres_underlying sr nf nf' r P P' f f'"}, where
28@{term sr} is a state-relation, @{term nf} and @{term nf'} refer to whether or not the left and
29right hand functions may fail, @{term r} is a return value relation between the functions, @{term P}
30and @{term P'} are preconditions for the functions @{term f} and @{term f'} respectively. Informally
31the statement says that: under the given preconditions, for every execution of @{term f'} there exists
32an execution of @{term f} that is related by the given state relation @{term sr} and return-value
33relation @{term r}.
34
35If the left and right side of a corres statement share similar structure, we can "unzip" the function
36into one corres obligation for each atomic function. This is done through the application of
37  @{thm corres_split}.
38\<close>
39
40thm corres_split[no_vars]
41
42text \<open>Briefly this states that: given a corres goal proving refinement between @{term "a >>= b"} and
43  @{term "c >>= d"}, we can decompose this into a proof showing refinement between @{term a} and
44@{term c}, and between @{term a} and @{term c}. Additionally @{term a} and @{term c} must establish
45appropriate postconditions to satisfy the obligations of proving refinement between @{term b} and @{term d}.
46
47The first subgoal that is produced has an important characteristic: the preconditions for each
48side may only discuss the return value of its respective side. This means that rules such as
49@{term "corres_underlying sr nf nf' r (\<lambda>s. x = x') (\<lambda>_. True) (f x) (f' x')"} will not apply to a goal
50 if @{term x} and @{term x'} are variables generated by applying @{thm corres_split} (i.e. the
51return values of functions).
52
53This means that any such conditions must instead be phrased as an assumption to the rule, and our rule must be
54rephrased as follows:
55  @{term "x = x' \<Longrightarrow> corres_underlying sr nf nf' r (\<lambda>_. True) (\<lambda>_. True) (f x) (f' x')"}.
56The result is that we must solve @{term "x = x'"} immediately after applying our rule. While this
57is not a major concern for a manual proof, it proves to be a significant obstacle if we're trying
58to focus on automating the "corres" part of the refinement.
59\<close>
60
61section \<open>corres_underlyingK and corres_rv\<close>
62
63text \<open>To remedy this situation, we augment the @{const corres_underlying} definition to include
64yet another flag: a single boolean. This new constant: @{const corres_underlyingK},
65will form the basis of the calculus for our corres method.\<close>
66
67thm corres_underlyingK_def[no_vars]
68
69text \<open>The boolean in @{const corres_underlyingK} can be thought of as a stateless precondition. It
70is used to propagate additional proof obligations for rules that either do not need to discuss
71either the left or right hand state, or must discuss bound variables from both sides.\<close>
72
73thm corresK_split[no_vars]
74
75text \<open>In this split rule for @{const corres_underlyingK} we see that the additional precondition @{term F'}
76may discuss both @{term rv} and @{term rv'}. To show that this condition is satisified, however,
77we can't use hoare logic and instead need a new definition: @{const corres_rv}.\<close>
78
79thm corres_rv_def_I_know_what_I'm_doing[no_vars]
80
81text \<open>This is a weaker form of @{const corres_underlying} that is only interested in the return value
82of the functions. In essence, it states the given functions will establish @{term Q} after executing,
83assuming the given return-value relation @{term r} holds, along with the given stateless precondition
84@{term F} and left/right preconditions @{term P} and @{term P'}.
85
86The assumption in general is that corres_rv rules should never be written, instead corres_rv obligations
87should be propagated into either the stateless precondition (@{term F} from @{term corres_underlyingK}),
88the left precondition (@{term P}) or the right precondition @{term P'}. This is implicitly handled
89by @{method corres_rv} (called from @{method corres}) by applying one of the following rules to each conjunct:\<close>
90
91thm corres_rv_defer
92thm corres_rv_wp_left
93thm corres_rv_wp_right
94
95text \<open>If none of these rules can be safely applied, then @{method corres_rv} will leave the
96  obligation untouched. The user can manually apply one of them if desired, but this is liable to
97  create unsolvable proof obligations. In the worst case, the user may manually solve the goal in-place.\<close>
98
99thm corres_rv_proveT[no_vars]
100
101section \<open>The corres method\<close>
102
103text \<open>The core algorithm of the corres method is simple:
104  1) start by applying any necessary weakening rules to ensure the goal has schematic preconditions
105  2) apply a known @{thm corres} or @{thm corresK} rule (see next section)
106  3) if unsuccessful, apply a split rule (i.e. @{thm corresK_split}) and go to 2
107
108Importantly, @{method corres} will not split a goal if it ultimately is not able to apply at least
109one @{thm corres} or @{thm corresK} rule.
110\<close>
111
112subsection \<open>The corres and corresK named_theorems\<close>
113
114text \<open>To address the fact that existing refinement rules are phrased as @{const corres_underlying}
115and not @{const corres_underlyingK} there are two different named_theorems that are used for different
116kind of rules @{thm corres} and @{thm corresK}. A @{thm corres} rule is understood to be phrased
117with @{const corres_underlying} and may have additional assumptions. These assumptions will be
118propagated through the additional @{term F} flag in @{const corres_underlyingK}, rather than presented
119as proof obligations immediately. A @{thm corresK} rule is understood to be phrased with
120@{const corres_underlyingK}, and is meant for calculational rules which may have proper assumptions that
121should not be propagated.
122\<close>
123thm corresK
124thm corres
125
126subsection \<open>The corresc method\<close>
127
128text \<open>Similar to @{method wpc}, @{method corresc} can handle case statements in @{const corres_underlyingK}
129proof goals. Importantly, however, it is split into two sub-methods @{method corresc_left} and
130@{method corresc_right}, which perform case-splitting on each side respectively. The combined method
131@{method corresc}, however, attempts to discharge the contradictions that arise from the quadratic
132blowup of a case analysis on both the left and right sides.\<close>
133
134subsection \<open>corres_concrete_r, corres_concrete_rE\<close>
135
136text \<open>Some @{thm corresK} rules should only be applied if certain variables are concrete
137(i.e. not schematic) in the goal. These are classified separately with the named_theorems
138@{thm corres_concrete_r} and @{thm corres_concrete_rER}. The first
139indicates that the return value relation of the goal must be concrete, the second indicates that
140only the left side of the error relation must be concrete.\<close>
141
142thm corres_concrete_r
143thm corres_concrete_rER
144
145subsection \<open>The corres_search method\<close>
146
147text \<open>The purpose of @{method corres_search} is to address cases where there is non-trivial control flow.
148In particular: in the case where there is an "if" statement or either side needs to be symbolically
149executed. The core idea is that corres_search should be provided with a "search" rule that acts
150as an anchoring point. Symbolic execution and control flow is decomposed until either the given
151rule is successfully applied or all search branches are exhausted.\<close>
152
153subsubsection \<open>Symbolic Execution\<close>
154
155text \<open>Symbolic execution is handled by two named theorems:
156 @{thm corres_symb_exec_ls} and @{thm corres_symb_exec_rs}, which perform symbolic execution on
157the left and right hand sides of a corres goal.\<close>
158
159thm corres_symb_exec_ls
160thm corres_symb_exec_rs
161
162text \<open>A function may be symbolically executed if it does not modify the state, i.e. its only purpose
163is to compute some value and return it. After being symbolically executed,
164this value can only be discussed by the precondition of the associated side or the stateless
165precondition of corresK. The resulting @{const corres_rv} goal has @{const corres_noop} as the
166function on the alternate side. This gives @{method corres_rv} a hint that the resulting obligation
167should be aggressively re-written into a hoare triple over @{term m} if it can't be propagated
168back statelessly safely.
169\<close>
170
171
172section \<open>Demo\<close>
173
174
175context begin interpretation Arch .
176
177(* VSpace_R *)
178
179
180lemmas load_hw_asid_corres_args[corres] =
181  load_hw_asid_corres[@lift_corres_args]
182
183lemmas invalidate_asid_corres_args[corres] =
184  invalidate_asid_corres[@lift_corres_args]
185
186lemmas invalidate_hw_asid_entry_corres_args[corres] =
187  invalidate_hw_asid_entry_corres[@lift_corres_args]
188
189lemma invalidate_asid_entry_corres:
190  "corres dc (valid_vspace_objs and valid_asid_map
191                and K (asid \<le> mask asid_bits \<and> asid \<noteq> 0)
192                and vspace_at_asid asid pd and valid_vs_lookup
193                and unique_table_refs o caps_of_state
194                and valid_global_objs and valid_arch_state
195                and pspace_aligned and pspace_distinct)
196             (pspace_aligned' and pspace_distinct' and no_0_obj')
197             (invalidate_asid_entry asid) (invalidateASIDEntry asid)"
198  apply (simp add: invalidate_asid_entry_def invalidateASIDEntry_def)
199  apply_debug (trace) (* apply_trace between steps *)
200   (tags "corres") (* break at breakpoints labelled "corres" *)
201   corres (* weaken precondition *)
202   continue (* split *)
203   continue (* solve load_hw_asid *)
204   continue (* split *)
205   continue (* apply corres_when *)
206   continue (* trivial simplification *)
207   continue (* invalidate _hw_asid_entry *)
208   finish (* invalidate_asid *)
209
210  apply (corressimp wp: load_hw_asid_wp)+
211  apply clarsimp
212  apply (fastforce simp: pd_at_asid_uniq)
213  done
214
215
216crunch typ_at'[wp]: invalidateASIDEntry, flushSpace "typ_at' T t"
217crunch ksCurThread[wp]: invalidateASIDEntry, flushSpace "\<lambda>s. P (ksCurThread s)"
218crunch obj_at'[wp]: invalidateASIDEntry, flushSpace "obj_at' P p"
219
220lemmas flush_space_corres_args[corres] =
221  flush_space_corres[@lift_corres_args]
222
223lemmas invalidate_asid_entry_corres_args[corres] =
224  invalidate_asid_entry_corres[@lift_corres_args]
225
226
227lemma corres_inst_eq_ext:
228  "(\<And>x. corres_inst_eq (f x) (f' x)) \<Longrightarrow> corres_inst_eq f f'"
229  by (auto simp add: corres_inst_eq_def)
230
231lemma delete_asid_corresb:
232  notes [corres] = corres_gets_asid gct_corres set_asid_pool_corres and
233    [@lift_corres_args, corres] =  get_asid_pool_corres_inv'
234    invalidate_asid_entry_corres
235    set_vm_root_corres
236  notes [wp] = set_asid_pool_asid_map_unmap set_asid_pool_vs_lookup_unmap'
237    set_asid_pool_vspace_objs_unmap'
238    invalidate_asid_entry_invalidates
239    getASID_wp
240  notes if_weak_cong[cong] option.case_cong_weak[cong]
241  shows
242    "corres dc
243          (invs and valid_etcbs and K (asid \<le> mask asid_bits \<and> asid \<noteq> 0))
244          (pspace_aligned' and pspace_distinct' and no_0_obj'
245              and valid_arch_state' and cur_tcb')
246          (delete_asid asid pd) (deleteASID asid pd)"
247  apply (simp add: delete_asid_def deleteASID_def)
248  apply_debug (trace) (* apply_trace between steps *)
249    (tags "corres") (* break at breakpoints labelled "corres" *)
250    corres (* weaken precondition *)
251   continue (* split *)
252       continue (* gets rule *)
253      continue (* corresc *)
254       continue (* return rule *)
255      continue (* split *)
256          continue (* function application *)
257          continue (* liftM rule *)
258          continue (* get_asid_pool_corres_inv' *)
259         continue (* function application *)
260         continue (* function application *)
261         continue (* corresK_when *)
262         continue (* split *)
263             continue (* flush_space_corres *)
264            continue (* K_bind *)
265            continue (* K_bind *)
266            continue (* split *)
267                continue (* invalidate_asid_entry_corres *)
268               continue (* K_bind *)
269               continue (* return bind *)
270               continue (* K_bind *)
271               continue (* split *)
272                   continue (* backtracking *)
273               continue (* split *)
274                   continue (* function application *)
275                   continue (* set_asid_pool_corres *)
276                  continue (* K_bind *)
277                  continue (* K_bind *)
278                  continue (* split *)
279                      continue (* gct_corres *)
280                     continue (* set_vm_root_corres *)
281                    finish (* backtracking? *)
282                    apply (corressimp simp: mask_asid_low_bits_ucast_ucast
283      | fold cur_tcb_def | wps)+
284  apply (frule arm_asid_table_related,clarsimp)
285  apply (rule conjI)
286   apply (intro impI allI)
287    apply (rule conjI)
288     apply (safe; assumption?)
289     apply (rule ext)
290     apply (fastforce simp: inv_def dest: ucast_ucast_eq)
291    apply (rule context_conjI)
292    apply (fastforce simp: o_def dest: valid_asid_tableD invs_valid_asid_table)
293   apply (intro allI impI)
294   apply (subgoal_tac "vspace_at_asid asid pd s")
295    prefer 2
296    apply (simp add: vspace_at_asid_def)
297    apply (rule vs_lookupI)
298     apply (simp add: vs_asid_refs_def)
299     apply (rule image_eqI[OF refl])
300     apply (rule graph_ofI)
301     apply fastforce
302    apply (rule r_into_rtrancl)
303    apply simp
304    apply (rule vs_lookup1I [OF _ _ refl], assumption)
305    apply (simp add: vs_refs_def)
306    apply (rule image_eqI[rotated], erule graph_ofI)
307    apply (simp add: mask_asid_low_bits_ucast_ucast)
308   prefer 2
309   apply (intro allI impI context_conjI; assumption?)
310    apply (rule aligned_distinct_relation_asid_pool_atI'; fastforce?)
311    apply (fastforce simp: o_def dest: valid_asid_tableD invs_valid_asid_table)
312    apply (simp add: cur_tcb'_def)
313    apply (safe; assumption?)
314    apply (erule ko_at_weakenE)
315    apply (clarsimp simp: graph_of_def)
316    apply (fastforce split: if_split_asm)
317   apply (frule invs_vspace_objs)
318   apply (drule (2) valid_vspace_objsD)
319   apply (erule ranE)
320   apply (fastforce split: if_split_asm)
321  apply (erule ko_at_weakenE)
322  apply (clarsimp simp: graph_of_def)
323  apply (fastforce split: if_split_asm)
324  done
325
326lemma cte_wp_at_ex:
327  "cte_wp_at (\<lambda>_. True) p s \<Longrightarrow> (\<exists>cap. cte_wp_at ((=) cap) p s)"
328  by (simp add: cte_wp_at_def)
329
330(* Sadly broken:
331lemma set_vm_root_for_flush_corres:
332  notes [corres] = gct_corres getSlotCap_corres
333  shows
334  "corres (=)
335          (cur_tcb and vspace_at_asid asid pd
336           and K (asid \<noteq> 0 \<and> asid \<le> mask asid_bits)
337           and valid_asid_map and valid_vs_lookup
338           and valid_vspace_objs and valid_global_objs
339           and unique_table_refs o caps_of_state
340           and valid_arch_state
341           and pspace_aligned and pspace_distinct)
342          (pspace_aligned' and pspace_distinct' and no_0_obj')
343          (set_vm_root_for_flush pd asid)
344          (setVMRootForFlush pd asid)"
345  apply (simp add: set_vm_root_for_flush_def setVMRootForFlush_def getThreadVSpaceRoot_def locateSlot_conv)
346  apply corres
347         apply_debug (trace) (tags "corres_search") (corres_search search: arm_context_switch_corres)
348  continue (* step left *)
349  continue (* if rule *)
350  continue (* failed corres on first subgoal, trying next *)
351  continue (* fail corres on last subgoal, trying reverse if rule *)
352  continue (* can't make corres progress here, trying other goal *)
353  finish (* successful goal discharged by corres *)
354
355  apply (corressimp wp: get_cap_wp getSlotCap_wp)+
356  apply (rule context_conjI)
357  subgoal by (simp add: cte_map_def objBits_simps tcb_cnode_index_def
358                        tcbVTableSlot_def to_bl_1 cte_level_bits_def)
359  apply (rule context_conjI)
360  subgoal by (fastforce simp: cur_tcb_def intro!: tcb_at_cte_at_1[simplified])
361  apply (rule conjI)
362   subgoal by (fastforce simp: isCap_simps)
363  apply (drule cte_wp_at_ex)
364  apply clarsimp
365  apply (drule (1) pspace_relation_cte_wp_at[rotated 1]; (assumption | clarsimp)?)
366  apply (drule cte_wp_at_norm')
367  apply clarsimp
368  apply (rule_tac x="cteCap cte" in exI)
369  apply (auto elim: cte_wp_at_weakenE' dest!: curthread_relation)
370  done
371
372text \<open>Note we can wrap it all up in corressimp\<close>
373
374lemma set_vm_root_for_flush_corres':
375  notes [corres] = gct_corres getSlotCap_corres
376  shows
377  "corres (=)
378          (cur_tcb and vspace_at_asid asid pd
379           and K (asid \<noteq> 0 \<and> asid \<le> mask asid_bits)
380           and valid_asid_map and valid_vs_lookup
381           and valid_vspace_objs and valid_global_objs
382           and unique_table_refs o caps_of_state
383           and valid_arch_state
384           and pspace_aligned and pspace_distinct)
385          (pspace_aligned' and pspace_distinct' and no_0_obj')
386          (set_vm_root_for_flush pd asid)
387          (setVMRootForFlush pd asid)"
388  apply (simp add: set_vm_root_for_flush_def setVMRootForFlush_def getThreadVSpaceRoot_def locateSlot_conv)
389  apply (corressimp search: arm_context_switch_corres
390                        wp: get_cap_wp getSlotCap_wp
391                      simp: isCap_simps)
392  apply (rule context_conjI)
393  subgoal by (simp add: cte_map_def objBits_simps tcb_cnode_index_def
394                        tcbVTableSlot_def to_bl_1 cte_level_bits_def)
395  apply (rule context_conjI)
396  subgoal by (fastforce simp: cur_tcb_def intro!: tcb_at_cte_at_1[simplified])
397  apply (rule conjI)
398   subgoal by (fastforce)
399  apply (drule cte_wp_at_ex)
400  apply clarsimp
401  apply (drule (1) pspace_relation_cte_wp_at[rotated 1]; (assumption | clarsimp)?)
402  apply (drule cte_wp_at_norm')
403  apply clarsimp
404  apply (rule_tac x="cteCap cte" in exI)
405  apply (auto elim: cte_wp_at_weakenE' dest!: curthread_relation)
406  done
407*)
408
409end
410end
411