[Imprint][Data Privacy Statement][E-Mail]
Back to main index.
View the specification.
View theorem base summary,
View theorem base listing,
the used properties by spec,
the dependency list,
the symbol table,
enrich
posix-permission
,
inode
,
error-class
,
seekflag
with
predicates pre-mkdir : path × metadata × error × user × directory-tree × file-data-store × open-file-handles;
pre-rmdir : path × error × user × directory-tree × file-data-store × open-file-handles;
pre-create : path × metadata × error × user × directory-tree × file-data-store × open-file-handles;
pre-unlink : path × error × user × directory-tree × file-data-store × open-file-handles;
pre-renam : path × path × error × user × directory-tree × file-data-store × open-file-handles;
pre-link : path × path × error × user × directory-tree × file-data-store × open-file-handles;
pre-open : path × file-mode × error × user × directory-tree × file-data-store × open-file-handles;
pre-close : nat × error × user × directory-tree × file-data-store × open-file-handles;
pre-read : nat × nat × error × user × directory-tree × file-data-store × open-file-handles;
pre-write : nat × buffer × nat × error × user × directory-tree × file-data-store × open-file-handles;
pre-seek : nat × nat × seekflag × error × user × directory-tree × file-data-store × open-file-handles;
pre-readmeta : path × error × user × directory-tree × file-data-store × open-file-handles;
pre-writemeta : path × metadata × error × user × directory-tree × file-data-store × open-file-handles;
pre-readdir : path × error × user × directory-tree × file-data-store × open-file-handles;
pre-truncate : path × nat × error × user × directory-tree × file-data-store × open-file-handles;
pre-fsync : path × bool × error × user × directory-tree × file-data-store × open-file-handles;
variables datasyncp : bool;
axioms pre-fsync-esuccess : ⊦ pre-fsync(p, datasyncp, ESUCCESS, user, root, fs, ofh) ↔ p ∈ root ∧ ¬ root[p].dir? ∧ pr(user, p, root, fs);
pre-fsync-eexists : ⊦ ¬ pre-fsync(p, datasyncp, EEXISTS, user, root, fs, ofh);
used for: s;
pre-fsync-enoent : ⊦ pre-fsync(p, datasyncp, ENOENT, user, root, fs, ofh) ↔ ¬ p ∈ root;
used for: s;
pre-fsync-eisdir : ⊦ pre-fsync(p, datasyncp, EISDIR, user, root, fs, ofh) ↔ root[p].dir?;
used for: s;
pre-fsync-enotempty : ⊦ ¬ pre-fsync(p, datasyncp, ENOTEMPTY, user, root, fs, ofh);
used for: s;
pre-fsync-enotdir : ⊦ ¬ pre-fsync(p, datasyncp, ENOTDIR, user, root, fs, ofh);
used for: s;
pre-fsync-ebadfd : ⊦ ¬ pre-fsync(p, datasyncp, EBADFD, user, root, fs, ofh);
used for: s;
pre-fsync-eaccess : ⊦ pre-fsync(p, datasyncp, EACCESS, user, root, fs, ofh) ↔ ¬ pr(user, p, root, fs) ∨ ¬ px(user, parent(p), root, fs);
used for: s;
pre-fsync-elowlevel : ⊦ ⌊err⌋ → pre-fsync(p, datasyncp, err, user, root, fs, ofh);
used for: s;
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);
used for: s;
pre-mkdir-eexists : ⊦ pre-mkdir(p, md, EEXISTS, user, root, fs, ofh) ↔ p ∈ root;
used for: s;
pre-mkdir-enotent : ⊦ pre-mkdir(p, md, ENOENT, user, root, fs, ofh) ↔ ¬ parent(p) ∈ root;
used for: s;
pre-mkdir-eisdir : ⊦ ¬ pre-mkdir(p, md, EISDIR, user, root, fs, ofh);
used for: s;
pre-mkdir-enotempty : ⊦ ¬ pre-mkdir(p, md, ENOTEMPTY, user, root, fs, ofh);
used for: s;
pre-mkdir-enotdir : ⊦ pre-mkdir(p, md, ENOTDIR, user, root, fs, ofh) ↔ ¬ root[parent(p)].dir?;
used for: s;
pre-mkdir-ebadfd : ⊦ ¬ pre-mkdir(p, md, EBADFD, user, root, fs, ofh);
used for: s;
pre-mkdir-eaccess : ⊦ pre-mkdir(p, md, EACCESS, user, root, fs, ofh) ↔ ¬ py(user, parent(p), root, fs);
used for: s;
pre-mkdir-elowlevel : ⊦ ⌊err⌋ → pre-mkdir(p, md, err, user, root, fs, ofh);
used for: s;
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);
used for: s;
pre-rmdir-eexists : ⊦ ¬ pre-rmdir(p, EEXISTS, user, root, fs, ofh);
used for: s;
pre-rmdir-enoent : ⊦ pre-rmdir(p, ENOENT, user, root, fs, ofh) ↔ ¬ p ∈ root;
used for: s;
pre-rmdir-eisdir : ⊦ ¬ pre-rmdir(p, EISDIR, user, root, fs, ofh);
used for: s;
pre-rmdir-enotempty : ⊦ pre-rmdir(p, ENOTEMPTY, user, root, fs, ofh) ↔ root[p].entries ≠ ∅;
used for: s;
pre-rmdir-enotdir : ⊦ pre-rmdir(p, ENOTDIR, user, root, fs, ofh) ↔ ¬ root[parent(p)].dir? ∨ ¬ root[p].dir?;
used for: s;
pre-rmdir-ebadfd : ⊦ ¬ pre-rmdir(p, EBADFD, user, root, fs, ofh);
used for: s;
pre-rmdir-eaccess : ⊦ pre-rmdir(p, EACCESS, user, root, fs, ofh) ↔ p = ε ∨ ¬ py(user, parent(p), root, fs);
used for: s;
pre-rmdir-elowlevel : ⊦ ⌊err⌋ → pre-rmdir(p, err, user, root, fs, ofh);
used for: s;
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);
used for: s;
pre-create-eexists : ⊦ pre-create(p, md, EEXISTS, user, root, fs, ofh) ↔ p ∈ root;
used for: s;
pre-create-enoent : ⊦ pre-create(p, md, ENOENT, user, root, fs, ofh) ↔ ¬ parent(p) ∈ root;
used for: s;
pre-create-eisdir : ⊦ ¬ pre-create(p, md, EISDIR, user, root, fs, ofh);
used for: s;
pre-create-enotempty : ⊦ ¬ pre-create(p, md, ENOTEMPTY, user, root, fs, ofh);
used for: s;
pre-create-enotdir : ⊦ pre-create(p, md, ENOTDIR, user, root, fs, ofh) ↔ ¬ root[parent(p)].dir?;
used for: s;
pre-create-ebadfd : ⊦ ¬ pre-create(p, md, EBADFD, user, root, fs, ofh);
used for: s;
pre-create-eaccess : ⊦ pre-create(p, md, EACCESS, user, root, fs, ofh) ↔ ¬ py(user, parent(p), root, fs);
used for: s;
pre-create-elowlevel : ⊦ ⌊err⌋ → pre-create(p, md, err, user, root, fs, ofh);
used for: s;
pre-unlink-esuccess : ⊦ pre-unlink(p, ESUCCESS, user, root, fs, ofh) ↔ p ≠ ε ∧ p ∈ root ∧ ¬ root[p].dir? ∧ py(user, parent(p), root, fs);
used for: s;
pre-unlink-eexists : ⊦ ¬ pre-unlink(p, EEXISTS, user, root, fs, ofh);
used for: s;
pre-unlink-enoent : ⊦ pre-unlink(p, ENOENT, user, root, fs, ofh) ↔ ¬ p ∈ root;
used for: s;
pre-unlink-eisdir : ⊦ pre-unlink(p, EISDIR, user, root, fs, ofh) ↔ root[p].dir?;
used for: s;
pre-unlink-enotempty : ⊦ ¬ pre-unlink(p, ENOTEMPTY, user, root, fs, ofh);
used for: s;
pre-unlink-enotdir : ⊦ pre-unlink(p, ENOTDIR, user, root, fs, ofh) ↔ ¬ root[parent(p)].dir?;
used for: s;
pre-unlink-ebadfd : ⊦ ¬ pre-unlink(p, EBADFD, user, root, fs, ofh);
used for: s;
pre-unlink-eaccess : ⊦ pre-unlink(p, EACCESS, user, root, fs, ofh) ↔ p = ε ∨ ¬ py(user, parent(p), root, fs);
used for: s;
pre-unlink-elowlevel : ⊦ ⌊err⌋ → pre-unlink(p, err, user, root, fs, ofh);
used for: s;
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));
used for: s;
pre-renam-eexists : ⊦ ¬ pre-renam(p, p', EEXISTS, user, root, fs, ofh);
used for: s;
pre-renam-enoent : ⊦ ¬ pre-renam(p, p', ENOENT, user, root, fs, ofh);
used for: s;
pre-renam-eisdir : ⊦ ¬ pre-renam(p, p', EISDIR, user, root, fs, ofh);
used for: s;
pre-renam-enotempty : ⊦ ¬ pre-renam(p, p', ENOTEMPTY, user, root, fs, ofh);
used for: s;
pre-renam-enotdir : ⊦ ¬ pre-renam(p, p', ENOTDIR, user, root, fs, ofh);
used for: s;
pre-renam-ebadfd : ⊦ ¬ pre-renam(p, p', EBADFD, user, root, fs, ofh);
used for: s;
pre-renam-eaccess : ⊦ ¬ pre-renam(p, p', EACCESS, user, root, fs, ofh);
used for: s;
pre-renam-elowlevel : ⊦ ⌊err⌋ → pre-renam(p, p', err, user, root, fs, ofh);
used for: s;
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);
used for: s;
pre-link-eexists : ⊦ pre-link(p, p', EEXISTS, user, root, fs, ofh) ↔ p' ∈ root;
used for: s;
pre-link-enoent : ⊦ pre-link(p, p', ENOENT, user, root, fs, ofh) ↔ ¬ p ∈ root ∨ ¬ parent(p') ∈ root;
used for: s;
pre-link-eisdir : ⊦ pre-link(p, p', EISDIR, user, root, fs, ofh) ↔ root[p].dir? ∨ root[p'].dir?;
used for: s;
pre-link-enotempty : ⊦ ¬ pre-link(p, p', ENOTEMPTY, user, root, fs, ofh);
used for: s;
pre-link-enotdir : ⊦ pre-link(p, p', ENOTDIR, user, root, fs, ofh) ↔ ¬ root[parent(p)].dir? ∨ ¬ root[parent(p')].dir?;
used for: s;
pre-link-ebadfd : ⊦ ¬ pre-link(p, p', EBADFD, user, root, fs, ofh);
used for: s;
pre-link-eaccess : ⊦ pre-link(p, p', EACCESS, user, root, fs, ofh) ↔ ¬ px(user, parent(p), root, fs) ∨ ¬ py(user, parent(p'), root, fs);
used for: s;
pre-link-elowlevel : ⊦ ⌊err⌋ → pre-link(p, p', err, user, root, fs, ofh);
used for: s;
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));
used for: s;
pre-open-eexists : ⊦ ¬ pre-open(p, mode, EEXISTS, user, root, fs, ofh);
used for: s;
pre-open-enoent : ⊦ pre-open(p, mode, ENOENT, user, root, fs, ofh) ↔ ¬ p ∈ root;
used for: s;
pre-open-eisdir : ⊦ pre-open(p, mode, EISDIR, user, root, fs, ofh) ↔ root[p].dir?;
used for: s;
pre-open-enotempty : ⊦ ¬ pre-open(p, mode, ENOTEMPTY, user, root, fs, ofh);
used for: s;
pre-open-enotdir : ⊦ ¬ pre-open(p, mode, ENOTDIR, user, root, fs, ofh);
used for: s;
pre-open-ebadfd : ⊦ ¬ pre-open(p, mode, EBADFD, user, root, fs, ofh);
used for: s;
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);
used for: s;
pre-open-elowlevel : ⊦ ⌊err⌋ → pre-open(p, mode, err, user, root, fs, ofh);
used for: s;
pre-close-esuccess : ⊦ pre-close(fd, ESUCCESS, user, root, fs, ofh) ↔ fd ∈ ofh;
used for: s;
pre-close-eexists : ⊦ ¬ pre-close(fd, EEXISTS, user, root, fs, ofh);
used for: s;
pre-close-enoent : ⊦ ¬ pre-close(fd, ENOENT, user, root, fs, ofh);
used for: s;
pre-close-eisdir : ⊦ ¬ pre-close(fd, EISDIR, user, root, fs, ofh);
used for: s;
pre-close-enotempty : ⊦ ¬ pre-close(fd, ENOTEMPTY, user, root, fs, ofh);
used for: s;
pre-close-enotdir : ⊦ ¬ pre-close(fd, ENOTDIR, user, root, fs, ofh);
used for: s;
pre-close-ebadfd : ⊦ pre-close(fd, EBADFD, user, root, fs, ofh) ↔ ¬ fd ∈ ofh;
used for: s;
pre-close-eaccess : ⊦ ¬ pre-close(fd, EACCESS, user, root, fs, ofh);
used for: s;
pre-close-elowlevel : ⊦ ⌊err⌋ → pre-close(fd, err, user, root, fs, ofh);
used for: s;
pre-read-esuccess : ⊦ pre-read(fd, n, ESUCCESS, user, root, fs, ofh) ↔ fd ∈ ofh ∧ (ofh[fd].mode = MODE_R ∨ ofh[fd].mode = MODE_RW);
used for: s;
pre-read-eexists : ⊦ ¬ pre-read(fd, n, EEXISTS, user, root, fs, ofh);
used for: s;
pre-read-enoent : ⊦ ¬ pre-read(fd, n, ENOENT, user, root, fs, ofh);
used for: s;
pre-read-eisdir : ⊦ ¬ pre-read(fd, n, EISDIR, user, root, fs, ofh);
used for: s;
pre-read-enotempty : ⊦ ¬ pre-read(fd, n, ENOTEMPTY, user, root, fs, ofh);
used for: s;
pre-read-enotdir : ⊦ ¬ pre-read(fd, n, ENOTDIR, user, root, fs, ofh);
used for: s;
pre-read-ebadfd : ⊦ pre-read(fd, n, EBADFD, user, root, fs, ofh) ↔ ¬ fd ∈ ofh ∨ ofh[fd].mode ≠ MODE_R ∧ ofh[fd].mode ≠ MODE_RW;
used for: s;
pre-read-eaccess : ⊦ ¬ pre-read(fd, n, EACCESS, user, root, fs, ofh);
used for: s;
pre-read-elowlevel : ⊦ ⌊err⌋ → pre-read(fd, n, err, user, root, fs, ofh);
used for: s;
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);
used for: s;
pre-write-eexists : ⊦ ¬ pre-write(fd, buf, n, EEXISTS, user, root, fs, ofh);
used for: s;
pre-write-enoent : ⊦ ¬ pre-write(fd, buf, n, ENOENT, user, root, fs, ofh);
used for: s;
pre-write-eisdir : ⊦ ¬ pre-write(fd, buf, n, EISDIR, user, root, fs, ofh);
used for: s;
pre-write-enotempty : ⊦ ¬ pre-write(fd, buf, n, ENOTEMPTY, user, root, fs, ofh);
used for: s;
pre-write-enotdir : ⊦ ¬ pre-write(fd, buf, n, ENOTDIR, user, root, fs, ofh);
used for: s;
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;
used for: s;
pre-write-eaccess : ⊦ ¬ pre-write(fd, buf, n, EACCESS, user, root, fs, ofh);
used for: s;
pre-write-elowlevel : ⊦ ⌊err⌋ → pre-write(fd, buf, n, err, user, root, fs, ofh);
used for: s;
pre-seek-esuccess : ⊦ pre-seek(fd, n, whence, ESUCCESS, user, root, fs, ofh) ↔ fd ∈ ofh;
used for: s;
pre-seek-eexists : ⊦ ¬ pre-seek(fd, n, whence, EEXISTS, user, root, fs, ofh);
used for: s;
pre-seek-enoent : ⊦ ¬ pre-seek(fd, n, whence, ENOENT, user, root, fs, ofh);
used for: s;
pre-seek-eisdir : ⊦ ¬ pre-seek(fd, n, whence, EISDIR, user, root, fs, ofh);
used for: s;
pre-seek-enotempty : ⊦ ¬ pre-seek(fd, n, whence, ENOTEMPTY, user, root, fs, ofh);
used for: s;
pre-seek-enotdir : ⊦ ¬ pre-seek(fd, n, whence, ENOTDIR, user, root, fs, ofh);
used for: s;
pre-seek-ebadfd : ⊦ pre-seek(fd, n, whence, EBADFD, user, root, fs, ofh) ↔ ¬ fd ∈ ofh;
used for: s;
pre-seek-eaccess : ⊦ ¬ pre-seek(fd, n, whence, EACCESS, user, root, fs, ofh);
used for: s;
pre-seek-elowlevel : ⊦ ⌊err⌋ → pre-seek(fd, n, whence, err, user, root, fs, ofh);
used for: s;
pre-readmeta-esuccess : ⊦ pre-readmeta(p, ESUCCESS, user, root, fs, ofh) ↔ p ∈ root ∧ pr(user, p, root, fs);
used for: s;
pre-readmeta-eexists : ⊦ ¬ pre-readmeta(p, EEXISTS, user, root, fs, ofh);
used for: s;
pre-readmeta-enoent : ⊦ pre-readmeta(p, ENOENT, user, root, fs, ofh) ↔ ¬ p ∈ root;
used for: s;
pre-readmeta-eisdir : ⊦ ¬ pre-readmeta(p, EISDIR, user, root, fs, ofh);
used for: s;
pre-readmeta-enotempty : ⊦ ¬ pre-readmeta(p, ENOTEMPTY, user, root, fs, ofh);
used for: s;
pre-readmeta-enotdir : ⊦ ¬ pre-readmeta(p, ENOTDIR, user, root, fs, ofh);
used for: s;
pre-readmeta-ebadfd : ⊦ ¬ pre-readmeta(p, EBADFD, user, root, fs, ofh);
used for: s;
pre-readmeta-eaccess : ⊦ pre-readmeta(p, EACCESS, user, root, fs, ofh) ↔ ¬ pr(user, p, root, fs);
used for: s;
pre-readmeta-elowlevel : ⊦ ⌊err⌋ → pre-readmeta(p, err, user, root, fs, ofh);
used for: s;
pre-writemeta-esuccess : ⊦ pre-writemeta(p, md, ESUCCESS, user, root, fs, ofh) ↔ p ∈ root ∧ pw(user, p, root, fs);
used for: s;
pre-writemeta-eexists : ⊦ ¬ pre-writemeta(p, md, EEXISTS, user, root, fs, ofh);
used for: s;
pre-writemeta-enoent : ⊦ pre-writemeta(p, md, ENOENT, user, root, fs, ofh) ↔ ¬ p ∈ root;
used for: s;
pre-writemeta-eisdir : ⊦ ¬ pre-writemeta(p, md, EISDIR, user, root, fs, ofh);
used for: s;
pre-writemeta-enotempty : ⊦ ¬ pre-writemeta(p, md, ENOTEMPTY, user, root, fs, ofh);
used for: s;
pre-writemeta-enotdir : ⊦ ¬ pre-writemeta(p, md, ENOTDIR, user, root, fs, ofh);
used for: s;
pre-writemeta-ebadfd : ⊦ ¬ pre-writemeta(p, md, EBADFD, user, root, fs, ofh);
used for: s;
pre-writemeta-eaccess : ⊦ pre-writemeta(p, md, EACCESS, user, root, fs, ofh) ↔ ¬ pw(user, p, root, fs);
used for: s;
pre-writemeta-elowlevel : ⊦ ⌊err⌋ → pre-writemeta(p, md, err, user, root, fs, ofh);
used for: s;
pre-readdir-esuccess : ⊦ pre-readdir(p, ESUCCESS, user, root, fs, ofh) ↔ p ∈ root ∧ root[p].dir? ∧ pr(user, p, root, fs);
used for: s;
pre-readdir-eexists : ⊦ ¬ pre-readdir(p, EEXISTS, user, root, fs, ofh);
used for: s;
pre-readdir-enoent : ⊦ pre-readdir(p, ENOENT, user, root, fs, ofh) ↔ ¬ p ∈ root;
used for: s;
pre-readdir-eisdir : ⊦ ¬ pre-readdir(p, EISDIR, user, root, fs, ofh);
used for: s;
pre-readdir-enotempty : ⊦ ¬ pre-readdir(p, ENOTEMPTY, user, root, fs, ofh);
used for: s;
pre-readdir-enotdir : ⊦ pre-readdir(p, ENOTDIR, user, root, fs, ofh) ↔ ¬ root[p].dir?;
used for: s;
pre-readdir-ebadfd : ⊦ ¬ pre-readdir(p, EBADFD, user, root, fs, ofh);
used for: s;
pre-readdir-eaccess : ⊦ pre-readdir(p, EACCESS, user, root, fs, ofh) ↔ ¬ pr(user, p, root, fs);
used for: s;
pre-readdir-elowlevel : ⊦ ⌊err⌋ → pre-readdir(p, err, user, root, fs, ofh);
used for: s;
pre-truncate-esuccess : ⊦ pre-truncate(p, n, ESUCCESS, user, root, fs, ofh) ↔ p ∈ root ∧ ¬ root[p].dir? ∧ pw(user, p, root, fs);
used for: s;
pre-truncate-eexists : ⊦ ¬ pre-truncate(p, n, EEXISTS, user, root, fs, ofh);
used for: s;
pre-truncate-enoent : ⊦ pre-truncate(p, n, ENOENT, user, root, fs, ofh) ↔ ¬ p ∈ root;
used for: s;
pre-truncate-eisdir : ⊦ pre-truncate(p, n, EISDIR, user, root, fs, ofh) ↔ root[p].dir?;
used for: s;
pre-truncate-enotempty : ⊦ ¬ pre-truncate(p, n, ENOTEMPTY, user, root, fs, ofh);
used for: s;
pre-truncate-enotdir : ⊦ ¬ pre-truncate(p, n, ENOTDIR, user, root, fs, ofh);
used for: s;
pre-truncate-ebadfd : ⊦ ¬ pre-truncate(p, n, EBADFD, user, root, fs, ofh);
used for: s;
pre-truncate-eaccess : ⊦ pre-truncate(p, n, EACCESS, user, root, fs, ofh) ↔ ¬ pw(user, p, root, fs);
used for: s;
pre-truncate-elowlevel : ⊦ ⌊err⌋ → pre-truncate(p, n, err, user, root, fs, ofh);
used for: s;
end enrich