3e3baf7b49
arch_split: invariants: split DetSchedAux_AI [VER-602]
2016-07-17 15:20:02 +10:00
0448444776
arch_split: invariants: split Deterministic_AI [VER-600]
2016-07-16 23:02:14 +10:00
138344f90a
arch_split: invariants: split Syscall_AI [VER-571]
2016-07-12 16:50:32 +10:00
ed2f1e1ca3
arch_split: split PDPTEntries_AI, rename as VSpaceEntries_AI [VER-580]
2016-07-12 16:50:32 +10:00
9b342f5ccf
arch_split: invariants: split KernelInit_AI [VER-620]
2016-07-12 16:50:32 +10:00
6b93e4bc81
arch_split: invariants: split BCorres2_AI [VER-577]
2016-07-12 16:50:32 +10:00
ae3644affc
arch_split: invariants: split EmptyFail_AI [VER-576]
2016-07-10 11:33:02 +10:00
6ef4c2d60f
arch_split: invariants: split InterruptAcc_AI [VER-606]
2016-07-09 11:04:22 +10:00
27c5ae792e
arch_split: invariants: split CSpaceInv_AI [VER-604], CSpace_AI [VER-605]
2016-07-09 11:04:22 +10:00
dced98a45d
arch_split: AInvs.thy [VER-581]
2016-07-07 14:13:40 +10:00
eb7f7b1564
arch-split: Tcb_AI.thy done
2016-07-07 13:57:16 +10:00
3ef9d3221c
arch_split: Interrupt_AI [VER-578]
2016-07-05 17:53:53 +10:00
d50e43d717
arch_split: invariants: split CNodeInv_AI [VER-573]
2016-07-04 11:56:53 +10:00
c31ee7a6a9
autocorres-crefine: update CRefine demo to work after AutoCorres refactor
...
Also fixes an AutoCorres bug that surfaced in the demo.
2016-06-30 14:41:55 +10:00
33a7c4becb
merge master into arch_split
2016-06-27 17:19:39 +10:00
b3c809983b
arch_split: invariants: split Ipc_AI [VER-572]
2016-06-27 17:19:11 +10:00
3d7660613a
arch_split: Finalise_AI [VER-568]
2016-06-26 15:26:50 +10:00
2a9ccec08b
autolevity: remove AutoLevity test sessions
2016-06-23 14:02:40 +10:00
92139db60e
autolevity: refine tracing apply everywhere to work via Proof module hooks
...
This avoids doing redundant tactic operations at the top-level and lets
us trace "by" statements easily.
2016-06-23 14:02:40 +10:00
820cf2d366
Arch-split: Untyped.thy done [VER-566]
2016-06-23 12:00:59 +10:00
27607011cd
verification update for seL4 arm_hyp merge to master
2016-06-22 22:28:36 +10:00
238a8061e8
SELFOUR-208: Warn on downgraded write-only mappings
2016-06-21 11:58:40 +10:00
c4a4abfa3d
SELFOUR-511 (trivial verification change)
2016-06-20 21:58:30 +10:00
a70f0138df
isPhysical: add isPhysical check to caps
2016-06-16 16:24:48 +10:00
b9313f6d11
arch_split: invariants: tidied
2016-06-15 10:15:26 +10:00
b172836ff3
ainvs: remove dependency on internal file; mark as unused
2016-06-09 19:27:32 +10:00
1537a8ec4d
arch_split: invariants: split Arch_AI [VER-574]
2016-06-09 14:05:49 +10:00
a1d33dd4db
arch_split: merge master
2016-06-08 21:53:07 +10:00
aceb021f88
arch_split: invariants: split Retype_AI [VER-556]
2016-06-08 10:33:09 +10:00
eb40bef27c
arch_split: IpcCancel_AI [VER-567]
2016-06-02 17:49:05 +10:00
38d77c8a28
CRefine: update AutoCorres demo to work with new data structures
2016-06-02 16:50:03 +10:00
9c608c62dc
arch_split: Schedule_AI [VER-565]
2016-06-02 14:20:06 +10:00
e1ae9e94dd
arch_split: Detype_AI [VER-557]
2016-05-31 15:17:04 +10:00
3e90041831
arch_split: access: fixup locale introduction rule
2016-05-31 15:05:24 +10:00
9f62622532
arch_split: skeleton arch files for AInvs
2016-05-31 15:05:24 +10:00
40570bc4fe
regression: add test to check theory import paths
...
This commit also fixes all bad imports reported by the test script.
Jira issue VER-560
2016-05-27 16:17:13 +10:00
26a7907c95
Merge pull request #43 in SEL4/l4v from ~JALIM/l4v:autocorres-seL4 to master
...
* commit 'ecbb860532b4c576fc4726a805802f16bcf5302c': (29 commits)
autocorres-crefine: specialise corres_no_failI for compatibility with Refine
Add license tags for autocorres-crefine files
crefine: refactor AutoCorresTest a bit
autocorres-crefine: remove local debugging imports
Fix InfoFlowC to accommodate corres_underlying changes.
Fix DRefine to accommodate corres_underlying changes.
autocorres-crefine: experiment with manually translating a function (clzl).
autocorres-crefine: experiment with translating bitfield_gen specs.
autocorres-crefine: start a test case for function calls.
autocorres-crefine: update example proofs to work with no_c_termination, which does not require proving termination for the C spec.
autocorres: add user option "no_c_termination" for previous patch.
Making termination proof optional for AutoCorres.
WIP: autocorres: hacky proof of concept for incremental translation.
autocorres: add some missing WordAbstract rules.
autocorres-crefine: fix some comments in work theory.
autocorres-crefine: prove modifies and (simple) terminates specs.
autocorres-crefine: experiment with generating modifies proofs
autocorres-crefine: run autocorres in kernel_all_substitute locale
autocorres-crefine: update another corres_UL that snuck in before rebasing.
autocorres-crefine: working ccorres for handleYield (modulo some white lies).
...
2016-05-19 01:19:58 +00:00
ecbb860532
autocorres-crefine: specialise corres_no_failI for compatibility with Refine
...
The generic rule is now named corres_no_failI_base.
2016-05-18 15:28:43 +10:00
2f0b484c7c
Add license tags for autocorres-crefine files
2016-05-18 15:10:04 +10:00
36f6ccca4d
crefine: refactor AutoCorresTest a bit
2016-05-17 16:55:47 +10:00
cf0bc1227b
crefine: remove obsolete ML file
2016-05-16 21:11:40 +10:00
dd78d1438c
word_lib: prettify Enumeration.thy
2016-05-16 21:11:40 +10:00
91bd8aebb8
inv-abstract: fewer warnings
2016-05-16 21:11:40 +10:00
2367dff983
word_lib: move out unused HOL_Lemmas
2016-05-16 21:11:40 +10:00
d162d8d01f
word_lib: normalise negative signed words as well.
2016-05-16 21:11:40 +10:00
0ced46820b
manual levity into Word_Lemmas
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
Matthew Brecknell
Alejandro Gomez-Londono
Miki Tanaka
Japheth Lim
Daniel Matichuk
Rafal Kolanski
Joel Beeren
Gerwin Klein