adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity
lh-l4v/proof/refine
History
Thomas Sewell 9a1ec71a2d Refactor of crunch. 
Substantial adjustments to crunch. Main user changes are:
  - 'lift' and 'unfold' mechanisms replaced by more general 'rule'.
  - some more 'ignores' standardised.
  - crunch has a more principled overall design:
    + discover crunch rule
      * provided or by definition extraction
    + recurse according to rule
    + prove goal based on rule, recursive discoveries, standard tactic
      * wp/simp adjustments tweak tactic
 		2016-08-24 15:53:53 +10:00
..
ADT_H.thy word_lib: adjust theory dependencies 2016-05-16 21:11:40 +10:00
ArchAcc_R.thy arch_split: give some vspace concepts more generic names 2016-08-03 14:46:48 +10:00
Arch_R.thy arch_split: invariants: tidied 2016-06-15 10:15:26 +10:00
Bits_R.thy Refactor of crunch. 2016-08-24 15:53:53 +10:00
BuildRefineCache.thy Import release snapshot. 2014-07-14 21:32:44 +02:00
CNodeInv_R.thy Refactor of crunch. 2016-08-24 15:53:53 +10:00
CSpace1_R.thy autocorres-crefine: specialise corres_no_failI for compatibility with Refine 2016-05-18 15:28:43 +10:00
CSpace_I.thy arch_split: Refine checking up to end of Finalise_R 2016-04-28 17:16:49 +10:00
CSpace_R.thy Refactor of crunch. 2016-08-24 15:53:53 +10:00
Cache.thy Import release snapshot. 2014-07-14 21:32:44 +02:00
Corres.thy autocorres-crefine: add pre-no-fail flag to corres. Updated AI+Refine. 2016-01-22 15:08:14 +11:00
Detype_R.thy Merge pull request #43 in SEL4/l4v from ~JALIM/l4v:autocorres-seL4 to master 2016-05-19 01:19:58 +00:00
EmptyFail.thy arch_split: replaced sublocale with global_naming 2016-04-27 14:32:38 +10:00
EmptyFail_H.thy arch_split: InfoFlowC checking 2016-05-06 13:15:37 +10:00
Finalise_R.thy Refactor of crunch. 2016-08-24 15:53:53 +10:00
IncKernelInit.thy Import release snapshot. 2014-07-14 21:32:44 +02:00
Include.thy repair ARM proofs up to Refine after factoring out architecture 2016-01-13 12:02:12 +11:00
InitLemmas.thy 2015 update for Refine 2015-05-12 17:17:31 +02:00
InterruptAcc_R.thy arch_split: Refine checking up to end of Finalise_R 2016-04-28 17:16:49 +10:00
Interrupt_R.thy 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
Invariants_H.thy word_lib: adjust theory dependencies 2016-05-16 21:11:40 +10:00
Invocations_R.thy arch_split: replaced sublocale with global_naming 2016-04-27 14:32:38 +10:00
IpcCancel_R.thy autocorres-crefine: specialise corres_no_failI for compatibility with Refine 2016-05-18 15:28:43 +10:00
Ipc_R.thy Refactor of crunch. 2016-08-24 15:53:53 +10:00
KHeap_R.thy autocorres-crefine: specialise corres_no_failI for compatibility with Refine 2016-05-18 15:28:43 +10:00
KernelInit_R.thy abstract Haskell init parameters into constants 2014-11-06 18:48:36 +11:00
LevityCatch.thy arch_split: replaced sublocale with global_naming 2016-04-27 14:32:38 +10:00
Machine_R.thy arch_split: replaced sublocale with global_naming 2016-04-27 14:32:38 +10:00
Orphanage.thy word_lib: adjust theory dependencies 2016-05-16 21:11:40 +10:00
PageTableDuplicates.thy lib/spec/proof/tools: fix word change fallout 2016-05-16 21:11:40 +10:00
RAB_FN.thy trivial: fixups including some licence headers 2016-05-09 13:27:15 +10:00
README.md misc: Proofing and formatting of README.md files. 2014-07-28 13:15:48 +10:00
Refine.thy Merge pull request #43 in SEL4/l4v from ~JALIM/l4v:autocorres-seL4 to master 2016-05-19 01:19:58 +00:00
Retype_R.thy word_lib: adjust theory dependencies 2016-05-16 21:11:40 +10:00
Schedule_R.thy Merge pull request #43 in SEL4/l4v from ~JALIM/l4v:autocorres-seL4 to master 2016-05-19 01:19:58 +00:00
StateRelation.thy arch_split: Refine checking up to end of Finalise_R 2016-04-28 17:16:49 +10:00
SubMonad_R.thy Merge branch 'master' of ssh://bitbucket.keg.ertos.in.nicta.com.au:7999/SEL4/l4v into autocorres-seL4 2016-05-11 15:08:22 +10:00
Syscall_R.thy Refactor of crunch. 2016-08-24 15:53:53 +10:00
TcbAcc_R.thy autocorres-crefine: specialise corres_no_failI for compatibility with Refine 2016-05-18 15:28:43 +10:00
Tcb_R.thy Refactor of crunch. 2016-08-24 15:53:53 +10:00
Untyped_R.thy Refactor of crunch. 2016-08-24 15:53:53 +10:00
VSpace_R.thy arch_split: give some vspace concepts more generic names 2016-08-03 14:46:48 +10: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.