| #
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>")
|
| #
cf1052e3 |
|
27-May-2018 |
Michael Sproul <michael.sproul@data61.csiro.au> |
x64: crefine: prove prepareThreadDelete_ccorres (VER-837)
|
| #
f68aa385 |
|
27-May-2018 |
Joel Beeren <joel.beeren@data61.csiro.au> |
x64: crefine: almost finished decodeX86PortInvocation_ccorres
|
| #
4fedfb5e |
|
06-May-2018 |
Michael Sproul <michael.sproul@data61.csiro.au> |
x64: crefine: clear remaining sorry in Interrupt_C (VER-879)
|
| #
58f74efb |
|
10-Apr-2018 |
Matthew Brecknell <Matthew.Brecknell@data61.csiro.au> |
x64: clear some sorries in VSpace_C
|
| #
f649240c |
|
03-Apr-2018 |
Matthew Brecknell <Matthew.Brecknell@data61.csiro.au> |
x64: CR3 and machine op updates for Meltdown
|
| #
87f6ad3f |
|
15-Mar-2018 |
Michael Sproul <michael.sproul@data61.csiro.au> |
x64: crefine: prove unmapPage_ccorres
This required the addition of a new assumption in Machine_C about
invalidateTranslationSingleASID
|
| #
55b5f165 |
|
04-Oct-2017 |
Joel Beeren <joel.beeren@data61.csiro.au> |
x64: crefine: added getFaultAddr_ccorres to machine assumptions
|
| #
c80d51bf |
|
27-Sep-2017 |
Joel Beeren <joel.beeren@data61.csiro.au> |
x64: crefine: added Machine_C
|