This also moves ex_abs_underlying from Corres_Method.thy to
ExtraCorres.thy and adds a variant of corres_underlying_split
Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
At the point we call set_asid_pool, the pool we are writing is out
of date, because invalidate_asid_entry will have changed it. This
commit adds another read operation after invalidate_asid_entry to
perform a write that is similarly atomic as the corresponding C code.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
set_asid_pool_empty and delete_asid_empty_table_pt aren't used on
RISCV64 (despite being proved and declared [wp]). Hopefully these won't
be needed on AARCH64.
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
On HYP platforms with projections it's sometimes useful to be able to
grab the `arch_valid_obj` formulation for specific arch types like page
tables before the simplifier breaks them apart for you.
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
For AARCH64 showing that valid_vspace_objs is preserved over a retype
operation via the retype_region_proofs_invs locale, it is not sufficient
to only know valid_vspace_objs. Since this locale already assumes invs,
use invs, which implies the other requirements for AARCH64.
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
During deployment of these tactics, two problems appeared:
* monadic_rewrite_single_pass
* would try to step after the action completed, which sometimes worked,
yielding unpredictable results
* finalise was called on monadic_rewrite goals generated by action,
which was fine with the `solves <wpsimp>` default, but yielded
unpredictable results with user-supplied finalise methods
* monadic_rewrite_symb_exec
* did not schematise the precondition before attempting to apply the
rule, resulting in lack of progress when it was expected;
this now yields an extra subgoal in rare obvious-precondition
cases, but is more user-friendly in the general case
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
In single-pass methods and symb_exec* methods, the finalise method
argument is optional, defaulting to solves<wpsimp> which is good enough
for most side-conditions and many WP goals.
`monadic_rewrite_symb_exec_l/r_known` methods internally supply the
instantiated theorem variable name, allowing specifying the
instantiation directly:
`monadic_rewrite_symb_exec_l cte_cap`
Symbolic execution removes no-name eta terms so that the actual variable
name in the monad is used, reducing need for rename_tac.
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
`_symb_exec` rules now assume `monadic_rewrite` statement first, to allow
chaining and automation, by deferring WP goals to later
`_symb_exec_*_known*`: better use of invariance of executed statement
renamed `monadic_rewrite_rule` to `monadic_rewrite_l_method`, added
equivalent for RHS
renamed `monadic_rewrite_simple` to `monadic_rewrite_l`, and changed
action argument into a supplied rule (expected single-fire usage), and
added equivalent for RHS
renamed `lhs`->`l` and `rhs`->`r`
renamed `monadic_rewrite_pre_imp_refl` -> `_eq`
added: generic rules for rewriting under corres_underlying
* `monadic_rewrite_corres_l_generic`
* `monadic_rewrite_corres_r_generic`
added: `monadic_rewrite_if_r_True/False`
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
Overhauled symbolic execution lemmas, improved genericity:
* monadic_rewrite_symb_exec_l' and r' are now main lemmas
* _F/_nF variants for LHS, E/nE variants for RHS
* non-apostrophied versions combine the above
* same for drop/known lemmas
Consolidated monadic_rewrite and corres lemmas:
* old monadic_rewrite_corres was never used except when rotated, so
monadic_rewrite_corres2 -> monadic_rewrite_corres
* monadic_rewrite_corres' unused and not needed -> removed
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
The standard form for a hoare triple showing the function is
state-invariant is `f {| P |}`, and that's what we crunch in later
proofs.
Using this form allows `[OF whatever_inv]` to instantiate, while using
the `f {|(=) s|}` form does not.
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
Isabelle allows preservation of variable names across rules if the name
associated with a DeBruijn index matches. All forms of monadic symbolic
execution lemmas should therefore use some form of:
`f >== \<lambda>rv. g rv` and refer to `\<All>rv. some_prop_of rv` in
the assumptions, to expose the bound names in the proof, avoiding
unnecessary `rename_tac`.
The following lemmas have been renamed after multiple discussions:
* `monadic_rewrite_imp` -> `monadic_rewrite_guard_imp` (to match [c]corres)
* `monadic_rewrite_weaken` -> `monadic_rewrite_weaken_flags`
(people expected "weaken" rules to weaken the precondition, not flags)
* `monadic_rewrite_weaken2` -> `monadic_rewrite_weaken_flags'`
(same reason)
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
Using named constructor arguments added to the datatype package allows
removal of the old way of writing them out explicitly.
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
The theory Value_Types is used without Value_Types_Test in the
AutoCorres release, which makes the @{file ..} antiquotation fail.
Including Value_Types_Test in the dependencies of Value_Types to
include it in the release doesn't work, because that would be a
circular dependency.
So to avoid manually enumerating release files, we make this a pure
@{text ..} antiquotation instead.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Michael McInerney
Corey Lewis
Gerwin Klein
Rafal Kolanski