#
c4dc578b |
|
17-Sep-2018 |
Edward Pierzchalski <ed.pierzchalski@data61.csiro.au> |
Fix up proofs after word lemma moves
|
#
590b83ce |
|
23-Jun-2018 |
Gerwin Klein <gerwin.klein@data61.csiro.au> |
Isabelle2018 arm: AInvs
|
#
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>")
|
#
a3de401c |
|
03-Apr-2018 |
Matthew Brecknell <Matthew.Brecknell@data61.csiro.au> |
x64: more abstract specs and invariants for ASIDs
|
#
0f38e200 |
|
25-Feb-2018 |
Thomas Sewell <Thomas.Sewell@data61.csiro.au> |
Many proof repairs.
|
#
652cbb96 |
|
14-Mar-2018 |
Thomas Sewell <Thomas.Sewell@data61.csiro.au> |
Initial proof updates for combinator changes.
|
#
6d8e9170 |
|
19-Jul-2017 |
Miki Tanaka <miki.tanaka@nicta.com.au> |
Remove valid_arch_objs now that we have valid_vspace_objs to express validiy of vspace objects, we do not need valid_arch_objs: we have valid_objs to state the validity of non-vspace arch objects.
|
#
fb9de60c |
|
25-May-2017 |
Alejandro Gomez-Londono <alejandro.gomez@data61.csiro.au> |
arm ainvs: Update for create_mapping_entries changes
|
#
702bfecd |
|
17-May-2017 |
Joel Beeren <joel.beeren@nicta.com.au> |
ainvs: reintroduce second_level_tables all over the place, update generic Arch_AI and various ArchArch_AI's to match
|
#
237fb110 |
|
21-Feb-2017 |
Matthew Brecknell <Matthew.Brecknell@data61.csiro.au> |
x64: fix ArchArch_AI Also includes some corrections to the abstract specification, and minor improvements to some existing proofs.
|
#
c54cbb38 |
|
15-Feb-2017 |
Matthew Brecknell <Matthew.Brecknell@data61.csiro.au> |
x64: remove arch-specific detail that crept back into Untyped_AI
|
#
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.
|
#
511c6b2d |
|
03-Nov-2016 |
Matthew Brecknell <Matthew.Brecknell@data61.csiro.au> |
Isabelle2016-1: rename free variables to avoid capture
|
#
41d4aa4f |
|
25-Oct-2016 |
Matthew Brecknell <Matthew.Brecknell@data61.csiro.au> |
Isabelle2016-1: update references to renamed constants and facts
|
#
a96346e3 |
|
26-May-2016 |
Thomas Sewell <Thomas.Sewell@nicta.com.au> |
SELFOUR-444: Finished InfoFlow and DRefine.
|
#
63888fa9 |
|
16-May-2016 |
Thomas Sewell <Thomas.Sewell@nicta.com.au> |
SELFOUR-444: AInvs proven for preemptible retype.
|
#
8d4a8eb2 |
|
21-Sep-2016 |
Xin,Gao <xin.gao@nicta.com.au> |
SELFOUR-421: fix coding style
|
#
1013e959 |
|
30-Jul-2016 |
Matthew Brecknell <Matthew.Brecknell@data61.csiro.au> |
arch_split: give some vspace concepts more generic names In particular rename "pd" to "vspace", when the pd represents an address space.
|
#
1537a8ec |
|
08-Jun-2016 |
Matthew Brecknell <Matthew.Brecknell@nicta.com.au> |
arch_split: invariants: split Arch_AI [VER-574]
|
#
9f626225 |
|
10-May-2016 |
Daniel Matichuk <daniel.matichuk@nicta.com.au> |
arch_split: skeleton arch files for AInvs
|