A lemma (entry) may depend on lemmas (entries) below its position, but never on lemmas
above its position. This means the list is a topological order of the dependency graph.
An entry 'all subs proved' means that all used lemmas are (transitively) proved.
| Name: | Status: | Subs proved? | Used: |
|---|
| crash-neutral-recover | proved | all subs proved
| recover,
|
| inv-enter-readonly | proved | all subs proved
| enter-readonly,
|
| crash-neutral-enter-readonly | proved | all subs proved
| enter-readonly,
|
| inv-is-readonly | proved | all subs proved
| is-readonly,
|
| crash-neutral-is-readonly | proved | all subs proved
| is-readonly,
|
| inv-destroy-buf | proved | all subs proved
| destroy-buf,
|
| crash-neutral-destroy-buf | proved | all subs proved
| destroy-buf,
|
| inv-get-page-size | proved | all subs proved
| get-page-size,
|
| inv-get-leb-size | proved | all subs proved
| get-leb-size,
|
| crash-neutral-get-page-size | proved | all subs proved
| get-page-size,
|
| crash-neutral-get-leb-size | proved | all subs proved
| get-leb-size,
|
| inv-move-buf | proved | all subs proved
| fwd-buffered-mapped,
move-buf,
|
| crash-neutral-move-buf | proved | all subs proved
| fwd-buffered-mapped,
move-buf,
|
| inv-commit | proved | all subs proved
| commit,
|
| inv-requires-commit | proved | all subs proved
| requires-commit,
|
| crash-neutral-commit | proved | all subs proved
| commit,
|
| crash-neutral-requires-commit | proved | all subs proved
| requires-commit,
|
| inv-add-log-leb | proved | all subs proved
| add-log-leb,
|
| crash-neutral-add-log-leb | proved | all subs proved
| add-log-leb,
|
| inv-get-volume-size | proved | all subs proved
| get-volume-size,
|
| crash-neutral-get-volume-size | proved | all subs proved
| get-volume-size,
|
| crash-neutral-write-buf | proved | all subs proved
| fwd-buffered-mapped,
write-buf,
|
| crash-neutral-read-buf | proved | all subs proved
| read-buf,
|
| crash-neutral-remap | proved | all subs proved
| remap,
|
| crash-neutral-unmap | proved | all subs proved
| unmap,
|
| inv-recover | proved | all subs proved
| recover,
|
| inv-write-buf | proved | all subs proved
| fwd-buffered-mapped,
write-buf,
|
| inv-read-buf | proved | all subs proved
| read-buf,
|
| inv-remap | proved | all subs proved
| remap,
|
| inv-unmap | proved | all subs proved
| unmap,
|
| crash-neutral-get-buf | proved | all subs proved
| get-buf,
|
| inv-get-buf | proved | all subs proved
| get-buf,
|
| synced-unmap | proved | all subs proved
| unmap,
|
| synced-remap | proved | all subs proved
| remap,
|
| synced-add-log-leb | proved | all subs proved
| add-log-leb,
|
| synced-commit | proved | all subs proved
| commit,
|
| synced-write-buf | proved | all subs proved
| write-buf,
fwd-buffered-mapped,
|
| inv-format | proved | all subs proved
| format,
|
| enter-readonly | axiom | | |
| is-readonly | axiom | | |
| destroy-buf | axiom | | |
| get-page-size | axiom | | |
| get-leb-size | axiom | | |
| move-buf | axiom | | |
| requires-commit | axiom | | |
| get-volume-size | axiom | | |
| recover | axiom | | |
| read-buf | axiom | | |
| get-buf | axiom | | |
| unmap | axiom | | |
| remap | axiom | | |
| add-log-leb | axiom | | |
| commit | axiom | | |
| fwd-buffered-mapped | proved | all subs proved
| |
| write-buf | axiom | | |
| format | axiom | | |