Currently this just modifies the rule but not any of the proofs that use
it. The old version is kept for now but should be removed once all of
the proofs are updated.
Signed-off-by: Corey Lewis <Corey.Lewis@data61.csiro.au>
This updates the proofs for a change in the C code. The IRQ control
syscall now returns an error whenever the IRQ parameter is not a valid
IRQ value. Previously, the syscall threw away some higher-order bits
before checking for IRQ validity.
Incidentally, the C now only uses the name `irq` for variables of type
`irq_t`, and `irq_w` for variables of type `word_t`. This avoids trouble
with c-parser name mangling.
The things that usually go wrong:
- wp fall through: add +, e.g.
apply (wp select_wp) -> apply (wp select_wp)+
- precondition: you can remove most hoare_pre, but wpc still needs it, and
sometimes the wp instance relies on being able to fit a rule to the
current non-schematic precondition. In that case, use "including no_pre"
to switch off the automatic hoare_pre application.
- very rarely there is a schematic postcondition that interferes with the
new trivial cleanup rules, because the rest of the script assumes some
specific state afterwards (shouldn't happen in a reasonable proof, but
not all proofs are reasonable..). In that case, (wp_once ...)+ should
emulate the old behaviour precisely.
* tcb_context rephrasing to (tcb_context o tcb_arch) and respectively
for set operations
* unfolding of reserved_irq for trivially solving most lemmas
* Changes to the inductive definition of integrity_obj to account for
tcb_arch and tcb_context new location
* Changes to the tcb examples in ExampleSystem to include tcb_arch
* Rephrasing of domain_sep_inv to accommodate the ReservedIRQ case
* Mostly rephrasing of tcb_context to (some form of) (tcb_context o tcb_arch)
* Trivial unfolding of handle_reserved_irq for hoare rules
* Examples in Example_Valid_State.thy were updated
* Nothing remarkable, mostly rephrasing of tcb_context and ReservedIRQ
handling
* Fun fact, some proofs are now shorter
tags: [VER-623][SELFOUR-413]
This commit should at least remove merge conflict markers, and the idea
is that at least refine, crefine, drefine, and infoflow (with sorrys)
build. Subsequent commits may be required to fix build issues that I
have not picked up.
Corey Lewis
Corey Lewis
Gerwin Klein
Mitchell Buckley
Thomas Sewell
Matthew Brecknell
Alejandro Gomez-Londono
Gerwin Klein
Matthew Brecknell
Sophie Taylor
Gao Xin
Joel Beeren
Miki Tanaka
Thomas Sewell
Ramana Kumar
David Greenaway