6a2692abc6
lib: fix theory includes for arch-splitted WordSetup
2016-05-20 12:31:10 +10:00
80456aa2c7
abstract: reduce syntax ambiguity
2016-05-16 21:11:40 +10:00
322f1023f5
word_lib: adjust theory dependencies
2016-05-16 21:11:40 +10:00
2a6df7a9a3
capDL: remove duplicate wordbits
2016-05-16 21:11:40 +10:00
445efb7c29
lib: closure for Word_Lib and own session
2016-05-16 21:11:40 +10:00
f0faa90f8a
lib/spec/proof/tools: fix word change fallout
2016-05-16 21:11:40 +10:00
7e37215bd2
arch_split: add extend_locale to base import
2016-05-06 18:37:16 +10:00
bb0644beaa
arch_split: merge master
2016-05-06 16:44:43 +10:00
56b226a608
arch_split: CRefine: use requalify instead of shadow
2016-05-06 08:59:33 +10:00
9ceed1eb12
arch_split: fix proofs after removing shadow and unqualify commands and adding fix for crunch. Checks up to DPolicy.
2016-05-04 15:14:41 +10:00
670d1c118d
arch_split: added optional definition override for crunch. Reduced qualification commands to minimal required set.
2016-05-04 15:14:41 +10:00
a2135ca8ce
arch_split: Refine checking, including Orphanage
2016-04-30 16:25:20 +10:00
0c3a12771d
arch_split: merge master
2016-04-28 14:36:43 +10:00
0e5ffd1ea0
arch_split: requalify abstract theories
2016-04-27 18:46:16 +10:00
1d20b393c0
arch_split: replaced sublocale with global_naming
2016-04-27 14:32:38 +10:00
8ab955984f
arch_split: CSpec checking
2016-04-26 13:45:59 +10:00
3191c485d5
arch_split: added ARM_A and ARM_H locales
2016-04-20 17:31:45 +10:00
04362dba27
arch_split: some quick and dirty arch_splitting by selectively interpreting the ARM locale (with FIXMEs)
2016-04-07 17:05:14 +10:00
72337faa7b
arch_split: added namespacing to ExecSpec
2016-04-01 15:17:17 +11:00
144778e8eb
arch_split: avoid caching file_defs in translator to make CONTEXT environment function as expected
2016-04-01 15:09:34 +11:00
d0a29887ff
arch_split: checkpoint for namespacing haskell
2016-04-01 15:09:34 +11:00
f89279e381
arch_split: reworking predicates about arch objects and types
2016-03-24 17:24:14 +11:00
f2cc8d7c0f
arch_split: invariants: progress in ArchADT_AI
2016-03-18 13:08:26 +11:00
7e9b8224ee
Factor out bitfield proof text into Eisbach lib.
...
There's a lot of proof text quoted into the source of the bitfield generator
(../seL4/tools/bitfield_gen.py). Optimising that requires even more complex
proof scripts. Instead of quoting them there, this introduces
lib/BitFieldProofsLib.thy which creates Eisbach methods for discharging some
relevant proof obligations. These can be tweaked without adjusting the
bitfield generator.
This approach could be taken a lot further to simplify the bitfield generator
further.
2016-03-17 15:54:24 +11:00
d7fd88727a
SELFOUR-420: Verification of maxIRQ check in handle_interrupt.
2016-03-17 11:20:52 +11:00
b679b00f97
arch_split: initial attempt at redefining invariants to avoid changing too many proofs
2016-03-04 19:03:45 +11:00
5e2f9a5e7c
arch_split: change caps_of_state to be explicit projection f caps_of_state
2016-03-04 19:03:45 +11:00
b88de8b2e2
arch_split: trivial fixup SpecCheck inconsistency
2016-03-03 16:01:15 +11:00
8042994eec
arch_split: fix namespacing for DSpec and SepTacticsExamples
2016-03-03 14:56:43 +11:00
8cc95bfb8e
arch_split: merge master into arch_split
2016-03-01 11:30:47 +11:00
3144c4d847
Remove time limits from Isabelle ROOT files.
2016-02-29 14:52:37 +11:00
6f6c58168c
SELFOUR-56: Remove diminish rights from IPC
2016-02-24 13:24:10 +11:00
d107cb6758
arch_split: halfway into KHeap_AI
2016-02-22 17:48:52 +11:00
5772559915
regression: bump timeouts further. All timeouts now multiples of 1hr.
2016-02-22 17:38:35 +11:00
84d2889d45
Isabelle2016: merge master into 2016
2016-02-19 16:17:26 +11:00
df8261c121
arch_split: split up Invariants_AI
2016-02-17 16:36:29 +11:00
91b9490d0a
l4v-sabre: regenerate haskell-spec
2016-02-17 11:18:03 +11:00
0d260252ff
l4v-sabre: rebase and fix proofs to infoflow
2016-02-17 11:18:02 +11:00
bc73b112bd
l4v-sabre: change type of irq to be 10 word
2016-02-17 11:18:02 +11:00
50fa257113
rebase and fix problems caused by new machine constants
2016-02-17 11:18:02 +11:00
c45f88745c
l4v-sabre: minor fix on dmo_ackInterrupt and foldME
2016-02-17 11:18:02 +11:00
bee4ba0052
l4v-sabre: fix refine
2016-02-17 11:18:02 +11:00
c1574f1f32
cspec: build: avoid re-entering isabelle via dash-0.5.8
2016-02-17 11:04:20 +11:00
c65e290a8b
Isabelle2016: merge master into 2016
2016-02-16 12:52:24 +11:00
1018d01b6f
arch_split: More namespacing progress and invariant splitting. Checks halfway into Invariants_AI
2016-02-05 17:00:06 +11:00
9718f1bda2
arch_split: progress on namespacing abstract spec
2016-02-05 16:59:18 +11:00
1d0366ac5e
msi: Restructure IOAPIC, MSI interrupts for x86, fix up ARM proofs for new API
2016-02-02 15:57:28 +11:00
253b04f6d9
regression: use CPU instead of real-time timeouts for all tests.
...
Also update and clarify test spec documentation.
2016-02-01 19:51:13 +11:00
b287127924
DRefine and DPolicy finished (includes a small change in ASpec)
2016-01-29 07:11:11 +11:00
0063075ba4
Merge remote-tracking branch 'verification/master' into arch_split
2016-01-28 18:26:53 +11:00
Joel Beeren
Gerwin Klein
Daniel Matichuk
Matthew Brecknell
Thomas Sewell
Sophie Taylor
Japheth Lim
Miki Tanaka
Xin Gao
Gao Xin