This is a listing of all goals defined over the current specification. Axioms are marked yellow, proved theorems green and unproved theorems blue. Click on individual names to get more information on the proof.
| Name: | Sequent: | Type: |
|---|---|---|
| pre-truncate-esuccess | ⊦ pre-truncate(p, n, ESUCCESS, user, root, fs, ofh) ↔ p ∈ root ∧ ¬ root[p].dir? ∧ pw(user, p, root, fs) | An Axiom |
| pre-readdir-esuccess | ⊦ pre-readdir(p, ESUCCESS, user, root, fs, ofh) ↔ p ∈ root ∧ root[p].dir? ∧ pr(user, p, root, fs) | An Axiom |
| pre-writemeta-esuccess | ⊦ pre-writemeta(p, md, ESUCCESS, user, root, fs, ofh) ↔ p ∈ root ∧ pw(user, p, root, fs) | An Axiom |
| pre-readmeta-esuccess | ⊦ pre-readmeta(p, ESUCCESS, user, root, fs, ofh) ↔ p ∈ root ∧ pr(user, p, root, fs) | An Axiom |
| pre-seek-esuccess | ⊦ pre-seek(fd, n, whence, ESUCCESS, user, root, fs, ofh) ↔ fd ∈ ofh | An Axiom |
| pre-write-esuccess | ⊦ pre-write(fd, buf, n, ESUCCESS, user, root, fs, ofh) ↔ fd ∈ ofh ∧ (ofh[fd].mode = MODE_W ∨ ofh[fd].mode = MODE_RW) | An Axiom |
| pre-read-esuccess | ⊦ pre-read(fd, n, ESUCCESS, user, root, fs, ofh) ↔ fd ∈ ofh ∧ (ofh[fd].mode = MODE_R ∨ ofh[fd].mode = MODE_RW) | An Axiom |
| pre-close-esuccess | ⊦ pre-close(fd, ESUCCESS, user, root, fs, ofh) ↔ fd ∈ ofh | An Axiom |
| pre-open-esuccess | ⊦ pre-open(p, mode, ESUCCESS, user, root, fs, ofh) ↔ p ∈ root ∧ ¬ root[p].dir? ∧ (mode = MODE_R ∨ mode = MODE_RW → pr(user, p, root, fs)) ∧ (mode = MODE_W ∨ mode = MODE_RW → pw(user, p, root, fs)) | An Axiom |
| pre-link-esuccess | ⊦ pre-link(p, p', ESUCCESS, user, root, fs, ofh) ↔ p ∈ root ∧ ¬ root[p].dir? ∧ ¬ p' ∈ root ∧ parent(p') ∈ root ∧ root[parent(p')].dir? ∧ px(user, parent(p), root, fs) ∧ py(user, parent(p'), root, fs) | An Axiom |
| pre-renam-esuccess | ⊦ pre-renam(p, p', ESUCCESS, user, root, fs, ofh) ↔ p' ≠ ε ∧ p ∈ root ∧ ¬ p ⊑ p' ∧ parent(p') ∈ root ∧ root[parent(p')].dir? ∧ (p' ∈ root → (root[p].dir? ↔ root[p'].dir?)) ∧ (p' ∈ root ∧ root[p'].dir? → root[p'].entries = ∅) ∧ py(user, parent(p), root, fs) ∧ py(user, parent(p'), root, fs) ∧ (root[p].dir? → pw(user, p, root, fs)) | An Axiom |
| pre-unlink-esuccess | ⊦ pre-unlink(p, ESUCCESS, user, root, fs, ofh) ↔ p ≠ ε ∧ p ∈ root ∧ ¬ root[p].dir? ∧ py(user, parent(p), root, fs) | An Axiom |
| pre-create-esuccess | ⊦ pre-create(p, md, ESUCCESS, user, root, fs, ofh) ↔ ¬ p ∈ root ∧ parent(p) ∈ root ∧ root[parent(p)].dir? ∧ py(user, parent(p), root, fs) | An Axiom |
| pre-rmdir-esuccess | ⊦ pre-rmdir(p, ESUCCESS, user, root, fs, ofh) ↔ p ≠ ε ∧ p ∈ root ∧ root[p].dir? ∧ root[p].entries = ∅ ∧ py(user, parent(p), root, fs) | An Axiom |
| pre-mkdir-elowlevel | ⊦ ⌊err⌋ → pre-mkdir(p, md, err, user, root, fs, ofh) | An Axiom |
| pre-mkdir-eaccess | ⊦ pre-mkdir(p, md, EACCESS, user, root, fs, ofh) ↔ ¬ py(user, parent(p), root, fs) | An Axiom |
| pre-mkdir-ebadfd | ⊦ ¬ pre-mkdir(p, md, EBADFD, user, root, fs, ofh) | An Axiom |
| pre-mkdir-enotdir | ⊦ pre-mkdir(p, md, ENOTDIR, user, root, fs, ofh) ↔ ¬ root[parent(p)].dir? | An Axiom |
| pre-mkdir-enotempty | ⊦ ¬ pre-mkdir(p, md, ENOTEMPTY, user, root, fs, ofh) | An Axiom |
| pre-mkdir-eisdir | ⊦ ¬ pre-mkdir(p, md, EISDIR, user, root, fs, ofh) | An Axiom |
| pre-mkdir-enotent | ⊦ pre-mkdir(p, md, ENOENT, user, root, fs, ofh) ↔ ¬ parent(p) ∈ root | An Axiom |
| pre-mkdir-eexists | ⊦ pre-mkdir(p, md, EEXISTS, user, root, fs, ofh) ↔ p ∈ root | An Axiom |
| pre-mkdir-esuccess | ⊦ pre-mkdir(p, md, ESUCCESS, user, root, fs, ofh) ↔ ¬ p ∈ root ∧ parent(p) ∈ root ∧ root[parent(p)].dir? ∧ py(user, parent(p), root, fs) | An Axiom |
| pre-truncate-elowlevel | ⊦ ⌊err⌋ → pre-truncate(p, n, err, user, root, fs, ofh) | An Axiom |
| pre-truncate-eaccess | ⊦ pre-truncate(p, n, EACCESS, user, root, fs, ofh) ↔ ¬ pw(user, p, root, fs) | An Axiom |
| pre-truncate-ebadfd | ⊦ ¬ pre-truncate(p, n, EBADFD, user, root, fs, ofh) | An Axiom |
| pre-truncate-enotdir | ⊦ ¬ pre-truncate(p, n, ENOTDIR, user, root, fs, ofh) | An Axiom |
| pre-truncate-enotempty | ⊦ ¬ pre-truncate(p, n, ENOTEMPTY, user, root, fs, ofh) | An Axiom |
| pre-truncate-eisdir | ⊦ pre-truncate(p, n, EISDIR, user, root, fs, ofh) ↔ root[p].dir? | An Axiom |
| pre-truncate-enoent | ⊦ pre-truncate(p, n, ENOENT, user, root, fs, ofh) ↔ ¬ p ∈ root | An Axiom |
| pre-truncate-eexists | ⊦ ¬ pre-truncate(p, n, EEXISTS, user, root, fs, ofh) | An Axiom |
| pre-readdir-elowlevel | ⊦ ⌊err⌋ → pre-readdir(p, err, user, root, fs, ofh) | An Axiom |
| pre-readdir-eaccess | ⊦ pre-readdir(p, EACCESS, user, root, fs, ofh) ↔ ¬ pr(user, p, root, fs) | An Axiom |
| pre-readdir-ebadfd | ⊦ ¬ pre-readdir(p, EBADFD, user, root, fs, ofh) | An Axiom |
| pre-readdir-enotdir | ⊦ pre-readdir(p, ENOTDIR, user, root, fs, ofh) ↔ ¬ root[p].dir? | An Axiom |
| pre-readdir-enotempty | ⊦ ¬ pre-readdir(p, ENOTEMPTY, user, root, fs, ofh) | An Axiom |
| pre-readdir-eisdir | ⊦ ¬ pre-readdir(p, EISDIR, user, root, fs, ofh) | An Axiom |
| pre-readdir-enoent | ⊦ pre-readdir(p, ENOENT, user, root, fs, ofh) ↔ ¬ p ∈ root | An Axiom |
| pre-readdir-eexists | ⊦ ¬ pre-readdir(p, EEXISTS, user, root, fs, ofh) | An Axiom |
| pre-writemeta-elowlevel | ⊦ ⌊err⌋ → pre-writemeta(p, md, err, user, root, fs, ofh) | An Axiom |
| pre-writemeta-eaccess | ⊦ pre-writemeta(p, md, EACCESS, user, root, fs, ofh) ↔ ¬ pw(user, p, root, fs) | An Axiom |
| pre-writemeta-ebadfd | ⊦ ¬ pre-writemeta(p, md, EBADFD, user, root, fs, ofh) | An Axiom |
| pre-writemeta-enotdir | ⊦ ¬ pre-writemeta(p, md, ENOTDIR, user, root, fs, ofh) | An Axiom |
| pre-writemeta-enotempty | ⊦ ¬ pre-writemeta(p, md, ENOTEMPTY, user, root, fs, ofh) | An Axiom |
| pre-writemeta-eisdir | ⊦ ¬ pre-writemeta(p, md, EISDIR, user, root, fs, ofh) | An Axiom |
| pre-writemeta-enoent | ⊦ pre-writemeta(p, md, ENOENT, user, root, fs, ofh) ↔ ¬ p ∈ root | An Axiom |
| pre-writemeta-eexists | ⊦ ¬ pre-writemeta(p, md, EEXISTS, user, root, fs, ofh) | An Axiom |
| pre-readmeta-elowlevel | ⊦ ⌊err⌋ → pre-readmeta(p, err, user, root, fs, ofh) | An Axiom |
| pre-readmeta-eaccess | ⊦ pre-readmeta(p, EACCESS, user, root, fs, ofh) ↔ ¬ pr(user, p, root, fs) | An Axiom |
| pre-readmeta-ebadfd | ⊦ ¬ pre-readmeta(p, EBADFD, user, root, fs, ofh) | An Axiom |
| pre-readmeta-enotdir | ⊦ ¬ pre-readmeta(p, ENOTDIR, user, root, fs, ofh) | An Axiom |
| pre-readmeta-enotempty | ⊦ ¬ pre-readmeta(p, ENOTEMPTY, user, root, fs, ofh) | An Axiom |
| pre-readmeta-eisdir | ⊦ ¬ pre-readmeta(p, EISDIR, user, root, fs, ofh) | An Axiom |
| pre-readmeta-enoent | ⊦ pre-readmeta(p, ENOENT, user, root, fs, ofh) ↔ ¬ p ∈ root | An Axiom |
| pre-readmeta-eexists | ⊦ ¬ pre-readmeta(p, EEXISTS, user, root, fs, ofh) | An Axiom |
| pre-seek-elowlevel | ⊦ ⌊err⌋ → pre-seek(fd, n, whence, err, user, root, fs, ofh) | An Axiom |
| pre-seek-eaccess | ⊦ ¬ pre-seek(fd, n, whence, EACCESS, user, root, fs, ofh) | An Axiom |
| pre-seek-ebadfd | ⊦ pre-seek(fd, n, whence, EBADFD, user, root, fs, ofh) ↔ ¬ fd ∈ ofh | An Axiom |
| pre-seek-enotdir | ⊦ ¬ pre-seek(fd, n, whence, ENOTDIR, user, root, fs, ofh) | An Axiom |
| pre-seek-enotempty | ⊦ ¬ pre-seek(fd, n, whence, ENOTEMPTY, user, root, fs, ofh) | An Axiom |
| pre-seek-eisdir | ⊦ ¬ pre-seek(fd, n, whence, EISDIR, user, root, fs, ofh) | An Axiom |
| pre-seek-enoent | ⊦ ¬ pre-seek(fd, n, whence, ENOENT, user, root, fs, ofh) | An Axiom |
| pre-seek-eexists | ⊦ ¬ pre-seek(fd, n, whence, EEXISTS, user, root, fs, ofh) | An Axiom |
| pre-write-elowlevel | ⊦ ⌊err⌋ → pre-write(fd, buf, n, err, user, root, fs, ofh) | An Axiom |
| pre-write-eaccess | ⊦ ¬ pre-write(fd, buf, n, EACCESS, user, root, fs, ofh) | An Axiom |
| pre-write-ebadfd | ⊦ pre-write(fd, buf, n, EBADFD, user, root, fs, ofh) ↔ ¬ fd ∈ ofh ∨ ofh[fd].mode ≠ MODE_W ∧ ofh[fd].mode ≠ MODE_RW | An Axiom |
| pre-write-enotdir | ⊦ ¬ pre-write(fd, buf, n, ENOTDIR, user, root, fs, ofh) | An Axiom |
| pre-write-enotempty | ⊦ ¬ pre-write(fd, buf, n, ENOTEMPTY, user, root, fs, ofh) | An Axiom |
| pre-write-eisdir | ⊦ ¬ pre-write(fd, buf, n, EISDIR, user, root, fs, ofh) | An Axiom |
| pre-write-enoent | ⊦ ¬ pre-write(fd, buf, n, ENOENT, user, root, fs, ofh) | An Axiom |
| pre-write-eexists | ⊦ ¬ pre-write(fd, buf, n, EEXISTS, user, root, fs, ofh) | An Axiom |
| pre-read-elowlevel | ⊦ ⌊err⌋ → pre-read(fd, n, err, user, root, fs, ofh) | An Axiom |
| pre-read-eaccess | ⊦ ¬ pre-read(fd, n, EACCESS, user, root, fs, ofh) | An Axiom |
| pre-read-ebadfd | ⊦ pre-read(fd, n, EBADFD, user, root, fs, ofh) ↔ ¬ fd ∈ ofh ∨ ofh[fd].mode ≠ MODE_R ∧ ofh[fd].mode ≠ MODE_RW | An Axiom |
| pre-read-enotdir | ⊦ ¬ pre-read(fd, n, ENOTDIR, user, root, fs, ofh) | An Axiom |
| pre-read-enotempty | ⊦ ¬ pre-read(fd, n, ENOTEMPTY, user, root, fs, ofh) | An Axiom |
| pre-read-eisdir | ⊦ ¬ pre-read(fd, n, EISDIR, user, root, fs, ofh) | An Axiom |
| pre-read-enoent | ⊦ ¬ pre-read(fd, n, ENOENT, user, root, fs, ofh) | An Axiom |
| pre-read-eexists | ⊦ ¬ pre-read(fd, n, EEXISTS, user, root, fs, ofh) | An Axiom |
| pre-close-elowlevel | ⊦ ⌊err⌋ → pre-close(fd, err, user, root, fs, ofh) | An Axiom |
| pre-close-eaccess | ⊦ ¬ pre-close(fd, EACCESS, user, root, fs, ofh) | An Axiom |
| pre-close-ebadfd | ⊦ pre-close(fd, EBADFD, user, root, fs, ofh) ↔ ¬ fd ∈ ofh | An Axiom |
| pre-close-enotdir | ⊦ ¬ pre-close(fd, ENOTDIR, user, root, fs, ofh) | An Axiom |
| pre-close-enotempty | ⊦ ¬ pre-close(fd, ENOTEMPTY, user, root, fs, ofh) | An Axiom |
| pre-close-eisdir | ⊦ ¬ pre-close(fd, EISDIR, user, root, fs, ofh) | An Axiom |
| pre-close-enoent | ⊦ ¬ pre-close(fd, ENOENT, user, root, fs, ofh) | An Axiom |
| pre-close-eexists | ⊦ ¬ pre-close(fd, EEXISTS, user, root, fs, ofh) | An Axiom |
| pre-open-elowlevel | ⊦ ⌊err⌋ → pre-open(p, mode, err, user, root, fs, ofh) | An Axiom |
| pre-open-eaccess | ⊦ pre-open(p, mode, EACCESS, user, root, fs, ofh) ↔ (mode = MODE_R ∨ mode = MODE_RW) ∧ ¬ pr(user, p, root, fs) ∨ (mode = MODE_W ∨ mode = MODE_RW) ∧ ¬ pw(user, p, root, fs) ∨ ¬ px(user, parent(p), root, fs) | An Axiom |
| pre-open-ebadfd | ⊦ ¬ pre-open(p, mode, EBADFD, user, root, fs, ofh) | An Axiom |
| pre-open-enotdir | ⊦ ¬ pre-open(p, mode, ENOTDIR, user, root, fs, ofh) | An Axiom |
| pre-open-enotempty | ⊦ ¬ pre-open(p, mode, ENOTEMPTY, user, root, fs, ofh) | An Axiom |
| pre-open-eisdir | ⊦ pre-open(p, mode, EISDIR, user, root, fs, ofh) ↔ root[p].dir? | An Axiom |
| pre-open-enoent | ⊦ pre-open(p, mode, ENOENT, user, root, fs, ofh) ↔ ¬ p ∈ root | An Axiom |
| pre-open-eexists | ⊦ ¬ pre-open(p, mode, EEXISTS, user, root, fs, ofh) | An Axiom |
| pre-link-elowlevel | ⊦ ⌊err⌋ → pre-link(p, p', err, user, root, fs, ofh) | An Axiom |
| pre-link-eaccess | ⊦ pre-link(p, p', EACCESS, user, root, fs, ofh) ↔ ¬ px(user, parent(p), root, fs) ∨ ¬ py(user, parent(p'), root, fs) | An Axiom |
| pre-link-ebadfd | ⊦ ¬ pre-link(p, p', EBADFD, user, root, fs, ofh) | An Axiom |
| pre-link-enotdir | ⊦ pre-link(p, p', ENOTDIR, user, root, fs, ofh) ↔ ¬ root[parent(p)].dir? ∨ ¬ root[parent(p')].dir? | An Axiom |
| pre-link-enotempty | ⊦ ¬ pre-link(p, p', ENOTEMPTY, user, root, fs, ofh) | An Axiom |
| pre-link-eisdir | ⊦ pre-link(p, p', EISDIR, user, root, fs, ofh) ↔ root[p].dir? ∨ root[p'].dir? | An Axiom |
| pre-link-enoent | ⊦ pre-link(p, p', ENOENT, user, root, fs, ofh) ↔ ¬ p ∈ root ∨ ¬ parent(p') ∈ root | An Axiom |
| pre-link-eexists | ⊦ pre-link(p, p', EEXISTS, user, root, fs, ofh) ↔ p' ∈ root | An Axiom |
| pre-renam-elowlevel | ⊦ ⌊err⌋ → pre-renam(p, p', err, user, root, fs, ofh) | An Axiom |
| pre-renam-eaccess | ⊦ ¬ pre-renam(p, p', EACCESS, user, root, fs, ofh) | An Axiom |
| pre-renam-ebadfd | ⊦ ¬ pre-renam(p, p', EBADFD, user, root, fs, ofh) | An Axiom |
| pre-renam-enotdir | ⊦ ¬ pre-renam(p, p', ENOTDIR, user, root, fs, ofh) | An Axiom |
| pre-renam-enotempty | ⊦ ¬ pre-renam(p, p', ENOTEMPTY, user, root, fs, ofh) | An Axiom |
| pre-renam-eisdir | ⊦ ¬ pre-renam(p, p', EISDIR, user, root, fs, ofh) | An Axiom |
| pre-renam-enoent | ⊦ ¬ pre-renam(p, p', ENOENT, user, root, fs, ofh) | An Axiom |
| pre-renam-eexists | ⊦ ¬ pre-renam(p, p', EEXISTS, user, root, fs, ofh) | An Axiom |
| pre-unlink-elowlevel | ⊦ ⌊err⌋ → pre-unlink(p, err, user, root, fs, ofh) | An Axiom |
| pre-unlink-eaccess | ⊦ pre-unlink(p, EACCESS, user, root, fs, ofh) ↔ p = ε ∨ ¬ py(user, parent(p), root, fs) | An Axiom |
| pre-unlink-ebadfd | ⊦ ¬ pre-unlink(p, EBADFD, user, root, fs, ofh) | An Axiom |
| pre-unlink-enotdir | ⊦ pre-unlink(p, ENOTDIR, user, root, fs, ofh) ↔ ¬ root[parent(p)].dir? | An Axiom |
| pre-unlink-enotempty | ⊦ ¬ pre-unlink(p, ENOTEMPTY, user, root, fs, ofh) | An Axiom |
| pre-unlink-eisdir | ⊦ pre-unlink(p, EISDIR, user, root, fs, ofh) ↔ root[p].dir? | An Axiom |
| pre-unlink-enoent | ⊦ pre-unlink(p, ENOENT, user, root, fs, ofh) ↔ ¬ p ∈ root | An Axiom |
| pre-unlink-eexists | ⊦ ¬ pre-unlink(p, EEXISTS, user, root, fs, ofh) | An Axiom |
| pre-create-elowlevel | ⊦ ⌊err⌋ → pre-create(p, md, err, user, root, fs, ofh) | An Axiom |
| pre-create-eaccess | ⊦ pre-create(p, md, EACCESS, user, root, fs, ofh) ↔ ¬ py(user, parent(p), root, fs) | An Axiom |
| pre-create-ebadfd | ⊦ ¬ pre-create(p, md, EBADFD, user, root, fs, ofh) | An Axiom |
| pre-create-enotdir | ⊦ pre-create(p, md, ENOTDIR, user, root, fs, ofh) ↔ ¬ root[parent(p)].dir? | An Axiom |
| pre-create-enotempty | ⊦ ¬ pre-create(p, md, ENOTEMPTY, user, root, fs, ofh) | An Axiom |
| pre-create-eisdir | ⊦ ¬ pre-create(p, md, EISDIR, user, root, fs, ofh) | An Axiom |
| pre-create-enoent | ⊦ pre-create(p, md, ENOENT, user, root, fs, ofh) ↔ ¬ parent(p) ∈ root | An Axiom |
| pre-create-eexists | ⊦ pre-create(p, md, EEXISTS, user, root, fs, ofh) ↔ p ∈ root | An Axiom |
| pre-rmdir-elowlevel | ⊦ ⌊err⌋ → pre-rmdir(p, err, user, root, fs, ofh) | An Axiom |
| pre-rmdir-eaccess | ⊦ pre-rmdir(p, EACCESS, user, root, fs, ofh) ↔ p = ε ∨ ¬ py(user, parent(p), root, fs) | An Axiom |
| pre-rmdir-ebadfd | ⊦ ¬ pre-rmdir(p, EBADFD, user, root, fs, ofh) | An Axiom |
| pre-rmdir-enotdir | ⊦ pre-rmdir(p, ENOTDIR, user, root, fs, ofh) ↔ ¬ root[parent(p)].dir? ∨ ¬ root[p].dir? | An Axiom |
| pre-rmdir-enotempty | ⊦ pre-rmdir(p, ENOTEMPTY, user, root, fs, ofh) ↔ root[p].entries ≠ ∅ | An Axiom |
| pre-rmdir-eisdir | ⊦ ¬ pre-rmdir(p, EISDIR, user, root, fs, ofh) | An Axiom |
| pre-rmdir-enoent | ⊦ pre-rmdir(p, ENOENT, user, root, fs, ofh) ↔ ¬ p ∈ root | An Axiom |
| pre-rmdir-eexists | ⊦ ¬ pre-rmdir(p, EEXISTS, user, root, fs, ofh) | An Axiom |
| pre-fsync-elowlevel | ⊦ ⌊err⌋ → pre-fsync(p, datasyncp, err, user, root, fs, ofh) | An Axiom |
| pre-fsync-eaccess | ⊦ pre-fsync(p, datasyncp, EACCESS, user, root, fs, ofh) ↔ ¬ pr(user, p, root, fs) ∨ ¬ px(user, parent(p), root, fs) | An Axiom |
| pre-fsync-ebadfd | ⊦ ¬ pre-fsync(p, datasyncp, EBADFD, user, root, fs, ofh) | An Axiom |
| pre-fsync-enotdir | ⊦ ¬ pre-fsync(p, datasyncp, ENOTDIR, user, root, fs, ofh) | An Axiom |
| pre-fsync-enotempty | ⊦ ¬ pre-fsync(p, datasyncp, ENOTEMPTY, user, root, fs, ofh) | An Axiom |
| pre-fsync-eisdir | ⊦ pre-fsync(p, datasyncp, EISDIR, user, root, fs, ofh) ↔ root[p].dir? | An Axiom |
| pre-fsync-enoent | ⊦ pre-fsync(p, datasyncp, ENOENT, user, root, fs, ofh) ↔ ¬ p ∈ root | An Axiom |
| pre-fsync-eexists | ⊦ ¬ pre-fsync(p, datasyncp, EEXISTS, user, root, fs, ofh) | An Axiom |
| pre-fsync-esuccess | ⊦ pre-fsync(p, datasyncp, ESUCCESS, user, root, fs, ofh) ↔ p ∈ root ∧ ¬ root[p].dir? ∧ pr(user, p, root, fs) | An Axiom |
| pre-close-efail | ⊦ pre-close(fd, EFAIL, user, root, fs, ofh) | A User Theorem |
| pre-create-efail | ⊦ pre-create(p, md, EFAIL, user, root, fs, ofh) | A User Theorem |
| pre-link-efail | ⊦ pre-link(p, p', EFAIL, user, root, fs, ofh) | A User Theorem |
| pre-mkdir-efail | ⊦ pre-mkdir(p, md, EFAIL, user, root, fs, ofh) | A User Theorem |
| pre-open-efail | ⊦ pre-open(p, mode, EFAIL, user, root, fs, ofh) | A User Theorem |
| pre-read-efail | ⊦ pre-read(fd, n, EFAIL, user, root, fs, ofh) | A User Theorem |
| pre-readdir-efail | ⊦ pre-readdir(p, EFAIL, user, root, fs, ofh) | A User Theorem |
| pre-readmeta-efail | ⊦ pre-readmeta(p, EFAIL, user, root, fs, ofh) | A User Theorem |
| pre-renam-efail | ⊦ pre-renam(p, p', EFAIL, user, root, fs, ofh) | A User Theorem |
| pre-rmdir-efail | ⊦ pre-rmdir(p, EFAIL, user, root, fs, ofh) | A User Theorem |
| pre-seek-efail | ⊦ pre-seek(fd, n, whence, EFAIL, user, root, fs, ofh) | A User Theorem |
| pre-truncate-efail | ⊦ pre-truncate(p, n, EFAIL, user, root, fs, ofh) | A User Theorem |
| pre-unlink-efail | ⊦ pre-unlink(p, EFAIL, user, root, fs, ofh) | A User Theorem |
| pre-write-efail | ⊦ pre-write(fd, buf, n, EFAIL, user, root, fs, ofh) | A User Theorem |
| pre-writemeta-efail | ⊦ pre-writemeta(p, md, EFAIL, user, root, fs, ofh) | A User Theorem |