#
b5cdf470 |
|
13-Jun-2018 |
Gerwin Klein <gerwin.klein@data61.csiro.au> |
globally use session-qualified imports; add Lib session Session-qualified imports will be required for Isabelle2018 and help clarify the structure of sessions in the build tree. This commit mainly adds a new set of sessions for lib/, including a Lib session that includes most theories in lib/ and a few separate sessions for parts that have dependencies beyond CParser or are separate AFP sessions. The group "lib" collects all lib/ sessions. As a consequence, other theories should use lib/ theories by session name, not by path, which in turns means spec and proof sessions should also refer to each other by session name, not path, to avoid duplicate theory errors in theory merges later.
|
#
ead3e6fd |
|
15-Jul-2018 |
Gerwin Klein <gerwin.klein@data61.csiro.au> |
aspec: message_info_to_data is mostly arch independent Factored out msg_label_bits, which is the only architecture specific part.
|
#
f649240c |
|
03-Apr-2018 |
Matthew Brecknell <Matthew.Brecknell@data61.csiro.au> |
x64: CR3 and machine op updates for Meltdown
|
#
a3de401c |
|
03-Apr-2018 |
Matthew Brecknell <Matthew.Brecknell@data61.csiro.au> |
x64: more abstract specs and invariants for ASIDs
|
#
8744fb20 |
|
21-Mar-2018 |
Gerwin Klein <gerwin.klein@data61.csiro.au> |
x64 abstract/machine: introduce and use FPUNullState The FPU state is opaque, and its null state is not necessary an array of zeroes. Instead, the null state is a snapshot taken after initialisation.
|
#
d9c08fc7 |
|
12-Feb-2018 |
Gerwin Klein <gerwin.klein@data61.csiro.au> |
aspec/haskell/machine: refactor user_context interface - remove separate abstract set_/get_register implementation, directly use machine op - make interface aware that user_context does not always need to equal (register => machine_word) - introduce FPU state on x64
|
#
8c549b67 |
|
10-Aug-2017 |
Matthew Brecknell <Matthew.Brecknell@data61.csiro.au> |
x64: remove all trailing whitespace
|
#
ac0a5549 |
|
03-Apr-2017 |
Matthew Brecknell <Matthew.Brecknell@data61.csiro.au> |
x64: Retype_R checking with sorry proofs
|
#
49e12ef7 |
|
20-Mar-2017 |
Joel Beeren <joel.beeren@nicta.com.au> |
x64: change cte_level_bits, obj_bits (Endpoint; Notification) to 5 rather than 4. This is true on all 64-bit platforms as the size of these objects is 4 words (4*8 = 32 = 2^5). However, this breaks the 32-bit ARM proofs that rely on these values being 4 - see jira issue VER-725.
|
#
237fb110 |
|
21-Feb-2017 |
Matthew Brecknell <Matthew.Brecknell@data61.csiro.au> |
x64: fix ArchArch_AI Also includes some corrections to the abstract specification, and minor improvements to some existing proofs.
|
#
3504b119 |
|
18-Jan-2017 |
Matthew Brecknell <Matthew.Brecknell@data61.csiro.au> |
x64: fix X64 after merge, up to ArchVSpace_AI
|
#
5bdcbe53 |
|
09-Jan-2017 |
Matthew Brecknell <Matthew.Brecknell@data61.csiro.au> |
fix ARM build after merge Also: - move some ARM-specific things out of Tcb_AI - port changes from ARM to X64, up to beginning of ArchVSpace_AI
|
#
f2cf12c3 |
|
19-May-2016 |
Joel Beeren <joel.beeren@nicta.com.au> |
x64: updated ASpec for WordSetup arch-split
|
#
1bc374fb |
|
12-May-2016 |
Joel Beeren <joel.beeren@nicta.com.au> |
x64 invs: up to vs_refs_pages
|
#
73b73156 |
|
05-May-2016 |
Joel Beeren <joel.beeren@nicta.com.au> |
x64: add arch_split'd x64 spec with IOMMU stuff
|