| #
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.
|
| #
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.
|
| #
5b451861 |
|
28-Mar-2018 |
Gerwin Klein <gerwin.klein@data61.csiro.au> |
x64 crefine: Recycle_C sorry free
|
| #
42ad2cba |
|
18-Mar-2018 |
Japheth Lim <Japheth.Lim@data61.csiro.au> |
x64 CRefine: more update for C-parser change to avoid complex call lvals (JIRA VER-881)
Also completes some Ipc_C proofs that were blocked by the C-parser problem.
|
| #
33494912 |
|
17-Jan-2018 |
Rafal Kolanski <rafal.kolanski@nicta.com.au> |
x64 crefine: update or sorry broken proofs up to Syscall_C
|
| #
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.
|
| #
abda36a8 |
|
21-Nov-2017 |
Joel Beeren <joel.beeren@data61.csiro.au> |
x64: crefine: added Recycle_C
|