adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity
lh-l4v/proof/refine
History
Thomas Sewell 043a69c81b Fix Orphanage from array changes, refactor. 
Some generalisation is done in finaliseSlot_invs'' to avoid
duplicating it in Orphanage and PageTableDuplicates.

Finally cleanup in haskell translation.
 		2015-12-02 09:15:32 +11:00
..
ADT_H.thy add arch_tcb object to C, rename aep -> ntfn 2015-11-20 16:02:13 +11:00
ArchAcc_R.thy Proof up to Fastpath_C. 2015-12-02 09:07:49 +11:00
Arch_R.thy Proof up to Fastpath_C. 2015-12-02 09:07:49 +11:00
Bits_R.thy add arch_tcb object to C, rename aep -> ntfn 2015-11-20 16:02:13 +11:00
BuildRefineCache.thy Import release snapshot. 2014-07-14 21:32:44 +02:00
CNodeInv_R.thy Fix Orphanage from array changes, refactor. 2015-12-02 09:15:32 +11:00
CSpace1_R.thy Proof up to Fastpath_C. 2015-12-02 09:07:49 +11:00
CSpace_I.thy WIP on handling array assertions. Up to Retype_C. 2015-12-02 09:06:06 +11:00
CSpace_R.thy Proof up to Fastpath_C. 2015-12-02 09:07:49 +11:00
Cache.thy Import release snapshot. 2014-07-14 21:32:44 +02:00
Corres.thy Import release snapshot. 2014-07-14 21:32:44 +02:00
Detype_R.thy WIP on handling array assertions. Up to Retype_C. 2015-12-02 09:06:06 +11:00
EmptyFail.thy WIP on handling array assertions. Up to Retype_C. 2015-12-02 09:06:06 +11:00
EmptyFail_H.thy Proof up to Fastpath_C. 2015-12-02 09:07:49 +11:00
Finalise_R.thy add arch_tcb object to C, rename aep -> ntfn 2015-11-20 16:02:13 +11:00
IncKernelInit.thy Import release snapshot. 2014-07-14 21:32:44 +02:00
Include.thy Import release snapshot. 2014-07-14 21:32:44 +02:00
InitLemmas.thy 2015 update for Refine 2015-05-12 17:17:31 +02:00
InterruptAcc_R.thy add arch_tcb object to C, rename aep -> ntfn 2015-11-20 16:02:13 +11:00
Interrupt_R.thy add arch_tcb object to C, rename aep -> ntfn 2015-11-20 16:02:13 +11:00
Invariants_H.thy Proof up to Fastpath_C. 2015-12-02 09:07:49 +11:00
Invocations_R.thy Import release snapshot. 2014-07-14 21:32:44 +02:00
IpcCancel_R.thy Fixes for merge/rebase with mainline. 2015-12-02 09:15:26 +11:00
Ipc_R.thy WIP on handling array assertions. Up to Retype_C. 2015-12-02 09:06:06 +11:00
KHeap_R.thy add arch_tcb object to C, rename aep -> ntfn 2015-11-20 16:02:13 +11:00
KernelInit_R.thy abstract Haskell init parameters into constants 2014-11-06 18:48:36 +11:00
LevityCatch.thy add arch_tcb object to C, rename aep -> ntfn 2015-11-20 16:02:13 +11:00
Machine_R.thy 2015 update for Refine 2015-05-12 17:17:31 +02:00
Orphanage.thy Fix Orphanage from array changes, refactor. 2015-12-02 09:15:32 +11:00
PageTableDuplicates.thy Fix Orphanage from array changes, refactor. 2015-12-02 09:15:32 +11:00
RAB_FN.thy Finally done with array assertions. 2015-12-02 09:08:27 +11:00
README.md misc: Proofing and formatting of README.md files. 2014-07-28 13:15:48 +10:00
Refine.thy Merge branch 'master' into aep-merge 2015-09-10 17:06:45 +10:00
Retype_R.thy add arch_tcb object to C, rename aep -> ntfn 2015-11-20 16:02:13 +11:00
Schedule_R.thy add arch_tcb object to C, rename aep -> ntfn 2015-11-20 16:02:13 +11:00
StateRelation.thy add arch_tcb object to C, rename aep -> ntfn 2015-11-20 16:02:13 +11:00
SubMonad_R.thy 2015 update for Refine 2015-05-12 17:17:31 +02:00
Syscall_R.thy WIP on handling array assertions. Up to Retype_C. 2015-12-02 09:06:06 +11:00
TcbAcc_R.thy add arch_tcb object to C, rename aep -> ntfn 2015-11-20 16:02:13 +11:00
Tcb_R.thy Wait -> Recv: update proofs 2015-11-20 16:02:14 +11:00
Untyped_R.thy Proof up to Fastpath_C. 2015-12-02 09:07:49 +11:00
VSpace_R.thy WIP on handling array assertions. Up to Retype_C. 2015-12-02 09:06:06 +11:00

README.md

Design Spec Refinement Proof

This proof establishes that seL4's design specification is a formal refinement (i.e. a correct implementation) of its abstract specification. This proof also interweaves the definition and proofs of the global invariant for the design specification, and builds on the Abstract Spec Invariant Proof. It is described in the TPHOLS '08 paper.

Building

To build from the l4v/ directory, run:

./isabelle/bin/isabelle build -d . -v -b Refine

Important Theories

The top-level theory where the refinement statement is established over the entire kernel is Refine; the state-relation that relates the state-spaces of the two specifications is defined in StateRelation and the basic correspondence property proved over each kernel function is defined in Corres.