..
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
Proof up to Fastpath_C.
2015-12-02 09:07:49 +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
Wait -> Recv: update proofs
2015-11-20 16:02:14 +11:00
PageTableDuplicates.thy
Proof up to Fastpath_C.
2015-12-02 09:07:49 +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