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: |
|---|
| inv-map | proved | all subs proved
| inv-write,
map,
lf-vtbl-info,
|
| inv-write | proved | all subs proved
| lf-valid-wl-bad,
inv-change,
prepost-io-write-data,
lf-used-info,
lf-used-valid-peb,
lf-valid-wl-not-erroneous,
lf-mapped-info,
lf-mapped-valid-peb,
ubi-io-inv-fwd,
prepost-write-multiple,
write,
lf-vtbl-info,
|
| prepost-write-multiple | proved | all subs proved
| prepost-write-once,
write-multiple,
ls-array-append-length0,
lf-vtbl-info,
|
| prepost-write-once | proved | all subs proved
| ubi-io-inv-fillcount0,
wl-put-peb,
next-sqnum,
ubi-io-inv-fwd,
lf-valid-wl-not-erroneous,
lf-valid-wl-free-emptyvidhdr,
lf-valid-vtbl-neq-free,
prepost-get-peb,
write-once,
ls-array-append-length0,
lf-vtbl-info,
|
| inv-change | proved | all subs proved
| prepost-atomic-leb-change,
ubi-io-inv-fwd,
lf-valid-wl-not-erroneous,
lf-valid-wl-free-emptyvidhdr,
lf-valid-vtbl-neq-free,
prepost-get-peb,
change,
lf-vtbl-info,
|
| inv-sync-device | proved | all subs proved
| inv-erase-all,
sync-device,
lf-vtbl-info,
|
| inv-erase | proved | all subs proved
| inv-erase-all,
inv-unmap,
erase,
lf-vtbl-info,
|
| inv-recover | proved | all subs proved
| lf-valid-wl-bad,
lf-used-valid-peb,
lf-valid-vtbl-neq-erasing,
lf-mapped-info,
lf-mapped-valid-peb,
lf-used-info,
prepost-fix-ecs,
prepost-init-vols-mappings,
lf-valid-wl-not-erroneous,
prepost-init-vols-sizes,
ubi-io-inv-fwd,
lf-valid-recs-sqns-vidhdr,
lf-valid-recs-notin-eraseq,
prepost-scan-all,
recover,
lf-vtbl-info,
|
| inv-create-volume | proved | all subs proved
| prepost-atomic-leb-change,
ubi-io-inv-fwd,
lf-valid-wl-not-erroneous,
lf-valid-wl-free-emptyvidhdr,
lf-valid-vtbl-neq-free,
prepost-get-peb,
inv-erase-all,
create-volume,
lf-vtbl-info,
|
| inv-wl-worker | proved | all subs proved
| ls-datasize-wear-level,
lf-valid-wl-bad,
prepost-erase-worker-helper,
lf-mapped-info,
lf-mapped-valid-peb,
prepost-atomic-leb-change,
lf-used-info,
lf-used-valid-peb,
ubi-io-inv-fwd,
lf-valid-wl-not-erroneous,
lf-valid-wl-free-emptyvidhdr,
lf-valid-vtbl-neq-free,
prepost-get-pebs-for-wl,
wl-worker,
lf-vtbl-info,
|
| prepost-scan-all | proved | all subs proved
| lf-valid-eraseq-stronger-notin-recs,
ls-max,
lf-valid-recs-max,
lf-valid-recs-valid-peb,
lf-valid-recs-in-apebs,
lf-valid-recs-sqns-vidhdr,
lf-valid-recs-notin-eraseq,
ubi-io-inv-fwd,
nat-sum-leq,
scan-all,
|
| inv-erase-all | proved | all subs proved
| prepost-erase-worker-helper,
erase-all,
lf-vtbl-info,
|
| prepost-get-peb | proved | all subs proved
| ubi-io-inv-fwd,
lf-valid-wl-not-erroneous,
lf-valid-wl-free-emptyvidhdr,
lf-valid-vtbl-neq-free,
prepost-wl-free-max-below,
prepost-erase-worker-helper,
prepost-wl-get-free-min,
wl-get-peb,
lf-vtbl-info,
|
| prepost-atomic-leb-change | proved | all subs proved
| ubi-io-inv-fillcount0,
ls-datasize-empbuf-append-lower,
lf-mapped-info,
lf-mapped-valid-peb,
lf-used-info,
lf-used-valid-peb,
ls-valid-global-sqn-vtbl,
wl-put-peb,
ls-subarray-datasize,
ls-array-append-length0,
ls-datasize-zero,
next-sqnum,
atomic-leb-change,
ubi-io-inv-fwd,
lf-valid-wl-not-erroneous,
lf-valid-wl-free-emptyvidhdr,
lf-valid-vtbl-neq-free,
lf-vtbl-info,
|
| inv-erase-worker | proved | all subs proved
| prepost-erase-worker-helper,
erase-worker,
lf-vtbl-info,
|
| lf-valid-recs-max | proved | all subs proved
| lf-valid-recs-valid-peb,
lf-valid-recs-in-apebs,
lf-valid-recs-sqns-vidhdr,
|
| ls-datasize-empbuf-append-lower | proved | all subs proved
| ls-datasize-zero,
|
| prepost-io-write-data | proved | all subs proved
| ls-array-append-length0,
lf-used-info,
lf-used-valid-peb,
ubi-io-inv-fwd,
lf-valid-wl-not-erroneous,
lf-vtbl-info,
|
| inv-unmap | proved | all subs proved
| lf-used-valid-peb,
lf-valid-wl-not-erroneous,
wl-put-peb,
lf-used-info,
lf-mapped-info,
lf-mapped-valid-peb,
unmap,
lf-vtbl-info,
|
| prepost-init-vols-mappings | proved | all subs proved
| lf-used-info,
ls-max,
lf-used-valid-peb,
lf-valid-wl-not-erroneous,
lf-valid-recs-notin-eraseq,
init-vols,
lf-vtbl-info,
|
| prepost-get-pebs-for-wl | proved | all subs proved
| prepost-wl-get-used-min,
lf-valid-vtbl-neq-free,
prepost-wl-free-max-below,
prepost-wl-get-free-min,
get-pebs-for-wl,
lf-vtbl-info,
|
| ls-datasize-wear-level | proved | all subs proved
| nat-sum-leq,
ls-datasize-zero,
|
| prepost-erase-worker-helper | proved | all subs proved
| ubi-io-inv-fwd,
lf-valid-wl-not-erroneous,
lf-valid-wl-bad,
erase-worker-helper,
lf-valid-vtbl-neq-erasing,
lf-valid-eraseq-middle-wlar,
lf-vtbl-info,
|
| ubi-is-max-unique | proved | all subs proved
| lf-vtbl-info,
|
| inv-read | proved | all subs proved
| lf-valid-wl-bad,
lf-used-valid-peb,
ubi-io-inv-fwd,
lf-valid-wl-not-erroneous,
lf-used-info,
lf-mapped-info,
lf-mapped-valid-peb,
read,
lf-vtbl-info,
|
| inv-get-volume-size | proved | all subs proved
| get-volume-size,
lf-vtbl-info,
|
| lf-valid-eraseq-stronger-notin-recs | proved | all subs proved
| lf-used-info,
|
| prepost-wl-get-used-min | proved | all subs proved
| get-used-min,
|
| prepost-wl-get-free-min | proved | all subs proved
| get-free-min,
|
| prepost-wl-free-max-below | proved | all subs proved
| find-max-below,
|
| ls-subarray-datasize | proved | all subs proved
| subbarray-alignup-datasize-empty,
ls-array-append-length0,
nat-sum-leq,
|
| ubi-io-inv-fillcount0 | proved | all subs proved
| ubi-io-inv-fwd,
|
| ls-datasize-zero | proved | all subs proved
| ls-array-append-length0,
|
| lf-valid-recs-valid-peb | proved | all subs proved
| lf-valid-recs-in-apebs,
|
| prepost-init-vols-sizes | proved | all subs proved
| init-vols-sizes,
|
| prepost-fix-ecs | proved | all subs proved
| fix-ecs,
|
| lf-valid-wl-free-emptyvidhdr | proved | all subs proved
| ubi-io-inv-fwd,
lf-valid-wl-not-erroneous,
|
| lf-mapped-valid-peb | proved | all subs proved
| lf-mapped-info,
|
| lf-valid-wl-bad | proved | all subs proved
| lf-valid-wl-not-erroneous,
|
| lf-vtbl-info | proved | all subs proved
| lf-used-info,
|
| valid-peb-write-valid-peb | proved | all subs proved
| ls-array-append-length0,
ubi-io-inv-fwd,
|
| inv-get-page-size | proved | all subs proved
| get-page-size,
|
| inv-get-leb-size | proved | all subs proved
| get-leb-size,
|
| inv-format | proved | all subs proved
| ubi-io-inv-fwd,
nat-sum-leq,
format,
|
| write-once | axiom | | |
| write-multiple | axiom | | |
| get-used-min | axiom | | |
| get-free-min | axiom | | |
| find-max-below | axiom | | |
| scan-all | axiom | | |
| init-vols-sizes | axiom | | |
| init-vols | axiom | | |
| ls-max | proved | all subs proved
| |
| get-pebs-for-wl | axiom | | |
| wl-get-peb | axiom | | |
| fix-ecs | axiom | | |
| lf-valid-eraseq-middle-wlar | proved | all subs proved
| |
| erase-worker-helper | axiom | | |
| atomic-leb-change | axiom | | |
| next-sqnum | axiom | | |
| ls-valid-global-sqn-vtbl | proved | all subs proved
| |
| subbarray-alignup-datasize-empty | proved | all subs proved
| |
| ls-array-append-length0 | proved | all subs proved
| |
| lf-valid-recs-in-apebs | proved | all subs proved
| |
| erase-all | axiom | | |
| get-page-size | axiom | | |
| get-leb-size | axiom | | |
| sync-device | axiom | | |
| read | axiom | | |
| write | axiom | | |
| unmap | axiom | | |
| wl-put-peb | axiom | | |
| erase | axiom | | |
| map | axiom | | |
| change | axiom | | |
| recover | axiom | | |
| lf-valid-recs-notin-eraseq | proved | all subs proved
| |
| lf-valid-recs-sqns-vidhdr | proved | all subs proved
| |
| lf-valid-vtbl-neq-erasing | proved | all subs proved
| |
| format | axiom | | |
| nat-sum-leq | proved | all subs proved
| |
| get-volume-size | axiom | | |
| create-volume | axiom | | |
| wl-worker | axiom | | |
| lf-valid-vtbl-neq-free | proved | all subs proved
| |
| lf-valid-wl-not-erroneous | proved | all subs proved
| |
| ubi-io-inv-fwd | proved | all subs proved
| |
| lf-used-valid-peb | proved | all subs proved
| |
| lf-used-info | proved | all subs proved
| |
| lf-mapped-info | proved | all subs proved
| |
| erase-worker | axiom | | |