| #
c4dc578b |
|
17-Sep-2018 |
Edward Pierzchalski <ed.pierzchalski@data61.csiro.au> |
Fix up proofs after word lemma moves
|
| #
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>")
|
| #
011e0845 |
|
09-Jun-2018 |
Gerwin Klein <gerwin.klein@data61.csiro.au> |
Isabelle2018: new comment syntax
(result of "isabelle update_comments <dirs>")
|
| #
5ce7ed47 |
|
03-Jul-2018 |
Joel Beeren <joel.beeren@data61.csiro.au> |
x64: crefine: add SetTLSBase invocation to x64 CRefine
|
| #
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.
|
| #
82474647 |
|
09-Mar-2018 |
Gerwin Klein <gerwin.klein@data61.csiro.au> |
x64 crefine: FPU updates
|
| #
3fb9903e |
|
25-Feb-2018 |
Japheth Lim <Japheth.Lim@data61.csiro.au> |
x64: crefine: update for C-parser change to avoid complex call lvals (JIRA VER-881)
|
| #
c2797809 |
|
26-Feb-2018 |
Michael Sproul <michael.sproul@data61.csiro.au> |
x64: crefine: fix confused deputy problem when setting priorities
|
| #
511d2e36 |
|
19-Feb-2018 |
Matthew Brecknell <Matthew.Brecknell@data61.csiro.au> |
x64: update proofs for new ccorres_rewrite
|
| #
9141e3c1 |
|
01-Feb-2018 |
Joel Beeren <joel.beeren@data61.csiro.au> |
x64: crefine: move lemma from Tcb_C to SR_lemmas_C, and more canonical_address lemmas to SR_Lemmas
|
| #
bcac2c84 |
|
01-Feb-2018 |
Matthew Brecknell <Matthew.Brecknell@data61.csiro.au> |
x64: clear some sorry proofs from CSpace_C
Also update some Haskell and abstract specs relating to IO ports.
|
| #
b072714c |
|
31-Jan-2018 |
Joel Beeren <joel.beeren@data61.csiro.au> |
x64: crefine: move pspace_canonical' lemmas to refine
|
| #
5d425337 |
|
29-Jan-2018 |
Joel Beeren <joel.beeren@data61.csiro.au> |
x64: crefine: cleared sorries in Tcb_C
|
| #
74a4be7a |
|
24-Jan-2018 |
Joel Beeren <joel.beeren@data61.csiro.au> |
x64: crefine: cleared non sign extend sorries in Tcb_C
|
| #
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.
|
| #
c858e6b7 |
|
11-Jan-2018 |
Joel Beeren <joel.beeren@data61.csiro.au> |
x64: crefine: cleared sorry in checkCapAt_ccorres
|
| #
5ccbe606 |
|
06-Nov-2017 |
Joel Beeren <joel.beeren@data61.csiro.au> |
x64: crefine: added Tcb_C
|