| #
c4dc578b |
|
17-Sep-2018 |
Edward Pierzchalski <ed.pierzchalski@data61.csiro.au> |
Fix up proofs after word lemma moves
|
| #
0619a469 |
|
07-Jul-2018 |
Gerwin Klein <gerwin.klein@data61.csiro.au> |
Isabelle2018 x64: CRefine
|
| #
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>")
|
| #
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.
|
| #
33494912 |
|
17-Jan-2018 |
Rafal Kolanski <rafal.kolanski@nicta.com.au> |
x64 crefine: update or sorry broken proofs up to Syscall_C
|
| #
59829524 |
|
15-Oct-2017 |
Joel Beeren <joel.beeren@data61.csiro.au> |
x64: crefine: added StoreWord_C
|