#
6b9d9d24 |
|
09-Jun-2018 |
Gerwin Klein <gerwin.klein@data61.csiro.au> |
Isabelle2018: new "op x" syntax; now is "(x)" (result of "isabelle update_op -m <dir>")
|
#
011e0845 |
|
09-Jun-2018 |
Gerwin Klein <gerwin.klein@data61.csiro.au> |
Isabelle2018: new comment syntax (result of "isabelle update_comments <dirs>")
|
#
2d0baab4 |
|
13-Mar-2018 |
Corey Lewis <corey.lewis@data61.csiro.au> |
Proof update for crunch changes
|
#
51190d18 |
|
26-Feb-2018 |
Gerwin Klein <gerwin.klein@data61.csiro.au> |
ARM bisim: proof update for user_context refactor
|
#
4601f2a1 |
|
06-Feb-2018 |
Joel Beeren <joel.beeren@data61.csiro.au> |
Genericise deletion actions that occur after empty_slot This patch adds a generic "post_cap_deletion" step that is called by finalise_slot. Previous to this, the only caps which had actions required at this stage were IRQHandlerCaps -- it was required that the IRQ bitmap be updated after the cap itself was removed (as the invariants state that for any existing IRQHandlerCap, the corresponding bit in the IRQ bitmap must be set). By genericising this, we add the capacity for new, arch-specific post cap deletion actions to occur in the future.
|
#
2a1beffa |
|
26-Nov-2017 |
Miki Tanaka <miki.tanaka@nicta.com.au> |
arm: update for simple_ko getter/setter
|
#
796887d9 |
|
11-Jul-2017 |
Alejandro Gomez-Londono <alejandro.gomez@nicta.com.au> |
Removes all trailing whitespaces
|
#
7ad3ef3b |
|
13-Mar-2017 |
Miki Tanaka <miki.tanaka@nicta.com.au> |
wp: update the proofs for the new wp/wpc/wpsimp
|
#
b2f2034b |
|
21-Feb-2017 |
Miki Tanaka <miki.tanaka@nicta.com.au> |
Bisim / Access / InfoFlow: updates for Hypervisor stub
|
#
47119bf4 |
|
13-Jan-2017 |
Gerwin Klein <gerwin.klein@nicta.com.au> |
wp_cleanup: update proofs for new wp behaviour 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.
|
#
a4fa4d2b |
|
17-Nov-2016 |
Matthew Brecknell <Matthew.Brecknell@data61.csiro.au> |
Isabelle2016-1: fix some proofs broken by abs_def normalisation Unfolding now automatically converts definitional rules to abs_def normal form before rewriting.
|
#
41d4aa4f |
|
25-Oct-2016 |
Matthew Brecknell <Matthew.Brecknell@data61.csiro.au> |
Isabelle2016-1: update references to renamed constants and facts
|
#
c25817b5 |
|
17-Nov-2016 |
Matthew Brecknell <Matthew.Brecknell@data61.csiro.au> |
trivial: remove some redundant uses of split_if rule
|
#
1289f7bc |
|
09-Nov-2016 |
Alejandro Gomez-Londono <alejandro.gomez@nicta.com.au> |
Updating remaining proofs for tcb_arch reserved_irq and arch_fault changes * 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]
|
#
0e5ffd1e |
|
27-Apr-2016 |
Matthew Brecknell <Matthew.Brecknell@nicta.com.au> |
arch_split: requalify abstract theories
|
#
b8e91541 |
|
25-Apr-2016 |
Matthew Brecknell <Matthew.Brecknell@nicta.com.au> |
arch_split: Bisim checking
|
#
33b5dab6 |
|
08-Feb-2016 |
Gao Xin <xin.gao@nicta.com.au> |
l4v-sabre: proof fix upto InfoFlowC
|
#
ac632c5a |
|
10-Nov-2015 |
Gerwin Klein <gerwin.klein@nicta.com.au> |
Wait -> Recv: update proofs
|
#
457a55a8 |
|
01-Nov-2015 |
Joel Beeren <joel.beeren@nicta.com.au> |
add arch_tcb object to C, rename aep -> ntfn
|
#
d6f7579b |
|
15-Oct-2015 |
Joel Beeren <joel.beeren@nicta.com.au> |
poll: Added new syscall for polling async endpoints (non-blocking wait)
|
#
e6eb9c83 |
|
17-Sep-2015 |
Ramana Kumar <Ramana.Kumar@nicta.com.au> |
aep-binding: finish Bisim with help from Dan
|
#
1ae434b9 |
|
17-Sep-2015 |
Ramana Kumar <Ramana.Kumar@nicta.com.au> |
aep-binding: attempted progress on Bisim, 1 sorry remains assumptions include aep_obj aep = IdleAEP and aep_bound_tcb aep = Some x, which I guess is probably a contradiction, but I don't know how to prove that.
|
#
3372cd32 |
|
15-Jul-2015 |
Joel Beeren <joel.beeren@nicta.com.au> |
SELFOUR-220: When calling handleWait, only delete the TCB's ReplyCap when actually waiting on a synchronous endpoint.
|
#
12fa8686 |
|
16-May-2015 |
Gerwin Klein <gerwin.klein@nicta.com.au> |
fewer warnings
|
#
baa57919 |
|
19-Apr-2015 |
Gerwin Klein <gerwin.klein@nicta.com.au> |
Isabelle2015 update: Bisim
|
#
22af6655 |
|
10-Apr-2015 |
Gerwin Klein <gerwin.klein@nicta.com.au> |
remove even arch calls from separation kernel setup (patch by Simon Winwood)
|
#
0288aeb1 |
|
23-Sep-2014 |
David Greenaway <david.greenaway@nicta.com.au> |
bisim: Isabelle 2014 changes.
|
#
3556bee2 |
|
12-Aug-2014 |
Gerwin Klein <gerwin.klein@nicta.com.au> |
github import of static cap config proofs
|