| #
c4dc578b |
|
17-Sep-2018 |
Edward Pierzchalski <ed.pierzchalski@data61.csiro.au> |
Fix up proofs after word lemma moves
|
| #
d7574020 |
|
20-Sep-2018 |
Edward Pierzchalski <ed.pierzchalski@data61.csiro.au> |
Remove pure word lemmas from proof/*
Removes redundant lemmas after moving them up to Word_Lib.
|
| #
8173a37c |
|
13-Aug-2018 |
Mitchell Buckley <mitchell.buckley@data61.csiro.au> |
Updated specs and proofs for SELFOUR-1491: control IRQ triggering on ARM.
|
| #
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
|
| #
2d0baab4 |
|
13-Mar-2018 |
Corey Lewis <corey.lewis@data61.csiro.au> |
Proof update for crunch changes
|
| #
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.
|
| #
2f540e80 |
|
17-Dec-2017 |
Matthew Brecknell <Matthew.Brecknell@data61.csiro.au> |
add constant definitions for bounds on untyped object sizes
|
| #
3cb118fe |
|
28-Aug-2017 |
Matthew Brecknell <Matthew.Brecknell@data61.csiro.au> |
Isabelle2017: update Refine for RC0
|
| #
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.
|
| #
42401684 |
|
02-Aug-2017 |
Joel Beeren <joel.beeren@nicta.com.au> |
refine: integrate all architectures
|
| #
c72bece0 |
|
18-Jul-2017 |
Daniel Matichuk <daniel.matichuk@data61.csiro.au> |
fix ARM Refine for newest corres method after ARM_HYP rebase
VER-737
|
| #
196e2e2e |
|
12-Apr-2017 |
Daniel Matichuk <daniel.matichuk@data61.csiro.au> |
fix corres proofs for corres method
Fixing the fact that ex_abs is slightly rephrased
VER-737
|
| #
796887d9 |
|
11-Jul-2017 |
Alejandro Gomez-Londono <alejandro.gomez@nicta.com.au> |
Removes all trailing whitespaces
|
| #
b7670996 |
|
17-May-2017 |
Alejandro Gomez-Londono <alejandro.gomez@data61.csiro.au> |
arm refine: Updating theories for ainvs changes
|
| #
7657681f |
|
29-Jan-2017 |
Rafal Kolanski <rafal.kolanski@nicta.com.au> |
move refine/* to refine/ARM/*, parametrise over $L4V_ARCH
|