| #
a424d55e |
|
09-Mar-2020 |
Gerwin Klein <gerwin.klein@data61.csiro.au> |
licenses: convert license tags to SPDX
|
| #
c34840d0 |
|
05-Jun-2019 |
Gerwin Klein <gerwin.klein@data61.csiro.au> |
global: isabelle update_cartouches
|
| #
16346084 |
|
03-Apr-2018 |
Joel Beeren <joel.beeren@data61.csiro.au> |
arm: ioportcontrol: Fixes after adding IOPortControlCaps to x64
|
| #
3dafec7d |
|
25-Jan-2017 |
Joel Beeren <Joel.Beeren@nicta.com.au> |
backport changes to ARM proofs from X64 work in progress
- replace ARM-specific constants and types with aliases which can be
instantiated separately for each architecture.
- expand lib with lemmas used in X64 proofs.
- simplify some proofs.
Also-by: Matthew Brecknell <Matthew.Brecknell@data61.csiro.au>
|
| #
c1782fc1 |
|
11-Jan-2017 |
Matthew Brecknell <Matthew.Brecknell@data61.csiro.au> |
x64: fix ARM build after merge
|
| #
25a63548 |
|
12-Dec-2016 |
Joel Beeren <joel.beeren@nicta.com.au> |
AInvs: remove references to arch specific stuff in Ipc_AI
|
| #
2553371a |
|
06-Nov-2016 |
Joel Beeren <joel.beeren@nicta.com.au> |
SELFOUR-64: Remove general Recycle operation
This removes the RecycleCap CNodeInvocation, whilst
retaining recycle behaviour for Endpoints -- now renamed
CNodeCancelBadgedSends.
|
| #
5e16ec56 |
|
10-Feb-2016 |
Joel Beeren <joel.beeren@nicta.com.au> |
SELFOUR-421: first attempt at abstract spec
|
| #
7a5f569a |
|
22-Aug-2016 |
Matthew Brecknell <Matthew.Brecknell@data61.csiro.au> |
x64 invariants: extract word-len-specific parts of update_cap_data (CSpace_A)
|
| #
1d20b393 |
|
26-Apr-2016 |
Daniel Matichuk <daniel.matichuk@nicta.com.au> |
arch_split: replaced sublocale with global_naming
|
| #
3191c485 |
|
20-Apr-2016 |
Daniel Matichuk <daniel.matichuk@nicta.com.au> |
arch_split: added ARM_A and ARM_H locales
|
| #
9718f1bd |
|
04-Feb-2016 |
Daniel Matichuk <daniel.matichuk@nicta.com.au> |
arch_split: progress on namespacing abstract spec
|
| #
fad2c6aa |
|
11-Jan-2016 |
Daniel Matichuk <daniel.matichuk@nicta.com.au> |
paramatrised abstract and haskell specs over L4V_ARCH
Haskell translator was modified to support multiple translations
of the haskell, with different build parameters.
|