Corres_Test.thy

(*
 *
 * 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 "../proof/refine/ARM/VSpace_R" 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[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 that assuming all other refinement conditions hold, the given
functions will establish @{term F'} after executing.

It turns out that in most cases (certainly those from existing corres proofs), the @{const corres_rv}
obligations will simply be solved in-place and reduce to
  @{term "corres_rv sr (\<lambda>_ _. True) (\<lambda>_. True) (\<lambda>_. True) f f'"} through simplification, or proved
 directly with @{thm corres_rv_proveT}.
\<close>
thm corres_rv_proveT[no_vars]

text \<open>Additionally, the obligation can be pushed into the precondition for either the left or right side.\<close>

thm corres_rv_defer_left
thm corres_rv_defer_right

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. Instead of @{const corres_rv} as seen in @{thm corresK_split}, we instead
are obligated to show that our function establishes the stateless precondition of the generated
corresK obligation.\<close>


section \<open>Demo\<close>


context begin interpretation Arch .

(* VSpace_R *)


lemma invalidate_asid_entry_corres:
  notes [where pd=pd, corres] =
    load_hw_asid_corres
    invalidate_asid_corres
  notes [corres] =
    invalidate_hw_asid_entry_corres
  shows
  "corres dc (valid_arch_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 (wp load_hw_asid_wp | simp)+
  apply (fastforce simp: pd_at_asid_uniq)
  done


crunch typ_at'[wp]: invalidateASIDEntry, flushSpace "typ_at' T t"
crunch pspace_aligned'[wp]: invalidateASIDEntry "pspace_aligned'"
crunch pspace_distinct'[wp]: invalidateASIDEntry "pspace_distinct'"
crunch ksCurThread[wp]: invalidateASIDEntry, flushSpace "\<lambda>s. P (ksCurThread s)"
crunch obj_at'[wp]: invalidateASIDEntry, flushSpace "obj_at' P p"


lemma delete_asid_corresb:
  notes [where pd=pd, corres] =
    flush_space_corres invalidate_asid_entry_corres

  notes [corres] = corres_gets_asid get_asid_pool_corres_inv'
                   invalidate_asid_entry_corres
                   set_asid_pool_corres gct_corres
                   set_vm_root_corres
  notes [wp] = set_asid_pool_asid_map_unmap[unfolded fun_upd_def] set_asid_pool_vs_lookup_unmap'
               set_asid_pool_arch_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 (* simplification *)
    continue (* liftM rule *)
    continue (* get_asid_pool_corres_inv' *)
    continue (* simplification *)
    continue (* corresK_when *)
    continue (* split *)
    continue (* flush_space_corres *)
    continue (* split *)
    continue (* invalidate_asid_entry_corres *)
    continue (* split *)
    continue (* set_asid_pool_corres *)
    continue (* split *)
    continue (* gct_corres *)
    continue (* simplification *)
    finish (* set_vm_root_corres *)
  apply (wp corres_rv_defer_right | simp add: mask_asid_low_bits_ucast_ucast | fold cur_tcb_def | wps)+
  apply (rule conjI)
  apply (intro impI allI)
  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 (safe; assumption?)
 apply (clarsimp simp add: inv_def mask_asid_low_bits_ucast_ucast)
  apply (rule ext)
  apply clarsimp
  apply (fastforce dest: ucast_ucast_eq)
  apply (simp add: typ_at_to_obj_at_arches)
  apply (clarsimp simp add: obj_at'_def)
  apply (simp add: cur_tcb'_def)
  apply safe
  apply (erule ko_at_weakenE)
  apply (clarsimp simp: graph_of_def)
  apply (fastforce split: if_split_asm)
  apply (frule invs_arch_objs)
  apply (drule (2) valid_arch_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 (op = cap) p s)"
  by (simp add: cte_wp_at_def)

lemma set_vm_root_for_flush_corres:
  notes [corres] = gct_corres getSlotCap_corres
  shows
  "corres (op =)
          (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_arch_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 (* successful goal discharged by corres *)
    finish (* successful terminal goal discharged by corres_once with given rule *)

  apply corres+

  apply (wp get_cap_wp getSlotCap_wp corres_rv_defer_left | wpc| simp)+
  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)
   apply (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 (op =)
          (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_arch_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 corres_rv_defer_left
                      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