| #
011e0845 |
|
09-Jun-2018 |
Gerwin Klein <gerwin.klein@data61.csiro.au> |
Isabelle2018: new comment syntax
(result of "isabelle update_comments <dirs>")
|
| #
c3900139 |
|
21-Apr-2018 |
Matthew Brecknell <Matthew.Brecknell@data61.csiro.au> |
x64 crefine: prove several lemmas in Retype_C
To prove that retyping a TCB establishes the state relation for TCBs,
it is necessary to prove that the C FPU null state is always equal to
the Haskell FPU null state. This commit therefore includes some
machinery for maintaining the state relation for the FPU null state,
and repairs many proofs.
|
| #
f649240c |
|
03-Apr-2018 |
Matthew Brecknell <Matthew.Brecknell@data61.csiro.au> |
x64: CR3 and machine op updates for Meltdown
|
| #
2a3639c6 |
|
29-Mar-2018 |
Gerwin Klein <gerwin.klein@data61.csiro.au> |
x64 crefine: Schedule_C sorry free
|
| #
e38bcf6b |
|
20-Mar-2018 |
Japheth Lim <Japheth.Lim@data61.csiro.au> |
x64 CRefine: proof repairs after wp changes
|
| #
53553ea2 |
|
17-Jan-2018 |
Rafal Kolanski <rafal.kolanski@nicta.com.au> |
x64 crefine: update scheduler bitmap lemmas
Applied the changes from invert-fastpath on ARM_HYP to available X64
files, updated relevant proofs to 64-bit, reduced IpcCancel sorries to
sign_extend only, reduced Schedule to one sorry.
|
| #
1fc3536a |
|
06-Nov-2017 |
Joel Beeren <joel.beeren@data61.csiro.au> |
x64: crefine: added Schedule_C
|