7623c07355
autocorres: Delete obsolete README file.
2014-07-25 11:35:13 +10:00
b304df74ca
autocorres: Create basic README.md file.
2014-07-25 11:34:28 +10:00
1421b09366
Even more cleanup of drefine.
2014-07-25 11:23:24 +10:00
c060f715db
Add a top-level file for the capDL API proofs.
2014-07-24 19:56:24 +10:00
283b54b351
comment to explain different do_user_op function in infoflow ADT
2014-07-24 14:53:57 +10:00
b57c8ca1e4
README.md for tools/
2014-07-24 13:58:16 +10:00
93375ba96d
Initial README.md files for proof/
2014-07-24 13:31:57 +10:00
30947b3e3f
add links to README.md
2014-07-24 10:49:32 +10:00
ffb0d165f6
Some more cleanup of drefine.
2014-07-23 15:29:20 +10:00
add3ea9cd5
sys-init: Show the separation algebra for capDL is a cancellative separation algebra.
...
* The separation algebra for capDL is also a cancellative separation algebra.
* The arrows are strictly_exact, meaning they describe only a single heap.
* Since we have a cancellative separation algebra, this means the arrows are also precise.
2014-07-23 15:20:52 +10:00
4326d30cdc
the other README files for spec/
2014-07-22 19:11:43 -04:00
fc4200f845
README files for spec/
2014-07-22 19:10:10 -04:00
0fa0a14f7d
filled in README
2014-07-22 18:35:05 -04:00
154da63715
remove old levity and taint-mode comments
2014-07-22 18:10:28 +02:00
50dda7708c
comment cleanup
2014-07-22 18:10:20 +02:00
acf0abe16a
Cleanup of a number of definitions of the separation algebra for capDL.
...
* The definitions of the separation "arrows" is slightly nicer and more consistent.
- We have a nicer correspondence between sep_map_c and sep_map_s.
- sep_map_irq now specifies exactly what the IRQ table contains
(that it *only* has one entry, not that it contains at least that entry).
- Nicer LaTeX output for the arrows.
* A number of minor renaming of constants and types.
- cdl_component => cdl_component_id
- sep_entity => cdl_component
- state_sep_projection => sep_state_projection
- obj_to_sep_state => object_to_sep_state
* Removed a few unused lemmas.
2014-07-22 14:37:37 +10:00
36588c4359
Minor cleanup of proofs in the Take/Grant security model.
2014-07-22 14:36:53 +10:00
798e891f1f
allow ROOT path customisation from outside l4v/
2014-07-21 17:18:43 +02:00
1273b8aac8
fix haskell version generation
2014-07-21 11:18:14 +02:00
f37be4295d
less disconcerting warning messages..
2014-07-21 11:17:34 +02:00
cd9ff69ffb
update ROOTS file
2014-07-19 16:11:34 +02:00
7cd9594a0c
Retire old dft package; resurrect Haskell manual.
...
Text is still out of date, but the document builds.
Added out-of-date warning text.
2014-07-19 15:55:06 +02:00
ebf2c21831
removed ancient arch tags
2014-07-19 10:48:49 +02:00
b081233283
Sync Haskell code with C
2014-07-18 18:04:45 +02:00
c5e926fcab
add getpaddr changes to haskell (by Joel Beeren)
2014-07-18 17:46:59 +02:00
a6d4ed8151
Merge branch 'getpaddr-merge'
2014-07-18 17:31:09 +02:00
9d9a325032
Updates for getpaddr system call (by Joel Beeren)
2014-07-18 17:21:34 +02:00
4d2a2c317b
renamed LICENSE file to match up with headers.
2014-07-18 16:48:55 +02:00
d52d8ad148
Fix previous commit.
2014-07-19 00:04:21 +10:00
07b85fe034
Move some more lemmas into lib.
2014-07-18 17:23:07 +10:00
d13c27e220
Release snapshot
2014-07-18 05:03:59 +10:00
84595f4233
release cleanup
2014-07-17 18:22:50 +02:00
2a03e81df4
Import release snapshot.
2014-07-14 21:32:44 +02:00
David Greenaway
Corey Lewis
Andrew Boyton
Toby Murray
Gerwin Klein
TrusthworthySystems