[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
aubifs-base
,
buffer-option
with
predicates pre-lookup : nat × dentry × node-store × node-index × key-set;
pre-create : inode × dentry × metadata × node-store × node-index × key-set;
pre-unlink : inode × inode × dentry × node-store × node-index × key-set;
pre-mkdir : inode × dentry × metadata × node-store × node-index × key-set;
pre-rmdir : inode × inode × dentry × node-store × node-index × key-set;
pre-link : inode × inode × dentry × dentry × node-store × node-index × key-set;
pre-rename : inode × dentry × inode × inode × dentry × inode × node-store × node-index × key-set;
pre-rename-new-reparent : inode × dentry × inode × inode × dentry × node-store × node-index × key-set;
pre-rename-new-keep-parent : inode × dentry × inode × dentry × node-store × node-index × key-set;
pre-rename-overwrite-reparent : inode × dentry × inode × inode × dentry × inode × node-store × node-index × key-set;
pre-rename-overwrite-keep-parent : inode × dentry × inode × dentry × inode × node-store × node-index × key-set;
pre-readpage : inode × nat × buffer × node-store × node-index;
pre-writepage : inode × nat × buffer × node-store × node-index;
pre-evict : nat × node-store × node-index × key-set;
pre-readdir : nat × node-store × node-index;
pre-truncate : inode × nat × nat × buffer-opt × node-store × node-index × key-set;
pre-iget : nat × node-store × node-index;
pre-write-inode : inode × node-store × node-index × key-set;
valid-inode : inode × node-store × node-index;
valid-file-inode : inode × node-store × node-index;
valid-dir-inode : inode × node-store × node-index;
valid-wb-inode : inode × node-store × node-index;
variables p_ino : nat;
pageno : nat;
p_inode : inode;
c_inode : inode;
new_inode : inode;
old_inode : inode;
new_dent_inode : inode;
old_dent_inode : inode;
old_parent_inode : inode;
old_child_inode : inode;
parent_inode : inode;
new_parent_inode : inode;
new_child_inode : inode;
old_ino : nat;
new_ino : nat;
old_dent : dentry;
new_dent : dentry;
axioms pre-lookup : ⊦ pre-lookup(p_ino, dent, fs, ri, ro) ↔ valid-parent-ino(p_ino, fs, ri, ro);
used for: s, ls;
pre-create
: ⊦ pre-create(p_inode, dent, md, fs, ri, ro) ↔ valid-negdentry(p_inode.ino, dent, fs, ri, ro) ∧ valid-dir-inode(p_inode, fs, ri);
used for: s, ls;
pre-unlink
: ⊦ pre-unlink(p_inode, c_inode, dent, fs, ri, ro)
↔ dent.ino ≠ ROOT_INO ∧ valid-dentry(p_inode.ino, dent, fs, ri, ro) ∧ ¬ inodekey(dent.ino) ∈ ro ∧ fs[ri[inodekey(dent.ino)]].nlink ≠ 0
∧ (fs[ri[inodekey(dent.ino)]].nlink = 1 → links(dent.ino, fs, ri) = {dentrykey(p_inode.ino, dent.name)} )
∧ valid-dir-inode(p_inode, fs, ri) ∧ valid-file-inode(c_inode, fs, ri) ∧ c_inode.ino = dent.ino ∧ p_inode.size ≥ 1;
used for: s, ls;
pre-mkdir : ⊦ pre-mkdir(p_inode, dent, md, fs, ri, ro) ↔ valid-negdentry(p_inode.ino, dent, fs, ri, ro) ∧ valid-dir-inode(p_inode, fs, ri);
used for: s, ls;
pre-rmdir
: ⊦ pre-rmdir(p_inode, c_inode, dent, fs, ri, ro)
↔ dent.ino ≠ ROOT_INO ∧ valid-dentry(p_inode.ino, dent, fs, ri, ro) ∧ fs[ri[inodekey(dent.ino)]].nlink = 1
∧ links(dent.ino, fs, ri) = {dentrykey(p_inode.ino, dent.name)} ∧ dentrykeys(inodekey(dent.ino), ri) = ∅ ∧ ¬ inodekey(dent.ino) ∈ ro
∧ valid-dir-inode(p_inode, fs, ri) ∧ valid-dir-inode(c_inode, fs, ri) ∧ c_inode.ino = dent.ino ∧ p_inode.nsubdirs ≥ 1
∧ p_inode.size ≥ 1;
used for: s, ls;
pre-link
: ⊦ pre-link(p_inode, c_inode, old_dent, new_dent, fs, ri, ro)
↔ (valid-dentry(old_dent, fs, ri, ro) ∧ valid-negdentry(p_inode.ino, new_dent, fs, ri, ro) ∧ ¬ inodekey(old_dent.ino) ∈ ro)
∧ valid-dir-inode(p_inode, fs, ri) ∧ valid-file-inode(c_inode, fs, ri) ∧ c_inode.ino = old_dent.ino;
used for: s, ls;
pre-rename
: ⊦ pre-rename(old_parent_inode, old_dent, old_child_inode, new_parent_inode, new_dent, new_child_inode, fs, ri, ro)
↔ ( valid-negdentry(new_parent_inode.ino, new_dent, fs, ri, ro)
∨ valid-dentry(new_parent_inode.ino, new_dent, fs, ri, ro) ∧ valid-wb-inode(new_child_inode, fs, ri)
∧ new_child_inode.ino = new_dent.ino ∧ (valid-file-ino(new_dent.ino, fs, ri) ↔ valid-file-ino(old_dent.ino, fs, ri))
∧ (valid-dir-ino(new_dent.ino, fs, ri) → new_dent.ino ≠ ROOT_INO ∧ dentrykeys(inodekey(new_dent.ino), ri) = ∅)
∧ new_child_inode.ino ≠ ROOT_INO ∧ new_child_inode.nlink ≠ 0
∧ (new_child_inode.nlink = 1 → links(new_child_inode.ino, fs, ri) = {dentrykey(new_parent_inode.ino, new_dent.name)} ))
∧ valid-dentry(old_parent_inode.ino, old_dent, fs, ri, ro) ∧ valid-dir-inode(new_parent_inode, fs, ri)
∧ valid-dir-inode(old_parent_inode, fs, ri)
∧ (new_parent_inode.ino = old_parent_inode.ino → new_parent_inode.meta = old_parent_inode.meta)
∧ valid-wb-inode(old_child_inode, fs, ri) ∧ old_child_inode.ino = old_dent.ino ∧ old_parent_inode.size ≥ 1
∧ (old_child_inode.directory → old_parent_inode.nsubdirs ≥ 1);
used for: s, ls;
pre-rename-overwrite-reparent
: ⊦ pre-rename-overwrite-reparent(old_parent_inode, old_dent, old_child_inode, new_parent_inode, new_dent, new_child_inode, fs, ri, ro)
↔ valid-dentry(new_parent_inode.ino, new_dent, fs, ri, ro) ∧ valid-wb-inode(new_child_inode, fs, ri)
∧ new_child_inode.ino = new_dent.ino ∧ (valid-file-ino(new_dent.ino, fs, ri) ↔ valid-file-ino(old_dent.ino, fs, ri))
∧ (valid-dir-ino(new_dent.ino, fs, ri) → new_dent.ino ≠ ROOT_INO ∧ dentrykeys(inodekey(new_dent.ino), ri) = ∅)
∧ new_child_inode.ino ≠ ROOT_INO ∧ new_child_inode.nlink ≠ 0
∧ (new_child_inode.nlink = 1 → links(new_child_inode.ino, fs, ri) = {dentrykey(new_parent_inode.ino, new_dent.name)} )
∧ valid-dentry(old_parent_inode.ino, old_dent, fs, ri, ro) ∧ valid-dir-inode(new_parent_inode, fs, ri)
∧ valid-dir-inode(old_parent_inode, fs, ri) ∧ new_parent_inode.ino ≠ old_parent_inode.ino ∧ valid-wb-inode(old_child_inode, fs, ri)
∧ old_child_inode.ino = old_dent.ino ∧ old_parent_inode.size ≥ 1 ∧ (old_child_inode.directory → old_parent_inode.nsubdirs ≥ 1);
used for: s, ls;
pre-rename-overwrite-keep-parent
: ⊦ pre-rename-overwrite-keep-parent(parent_inode, old_dent, old_child_inode, new_dent, new_child_inode, fs, ri, ro)
↔ valid-dentry(parent_inode.ino, new_dent, fs, ri, ro) ∧ valid-wb-inode(new_child_inode, fs, ri) ∧ new_child_inode.ino = new_dent.ino
∧ (valid-file-ino(new_dent.ino, fs, ri) ↔ valid-file-ino(old_dent.ino, fs, ri))
∧ (valid-dir-ino(new_dent.ino, fs, ri) → new_dent.ino ≠ ROOT_INO ∧ dentrykeys(inodekey(new_dent.ino), ri) = ∅)
∧ new_child_inode.ino ≠ ROOT_INO ∧ new_child_inode.nlink ≠ 0
∧ (new_child_inode.nlink = 1 → links(new_child_inode.ino, fs, ri) = {dentrykey(parent_inode.ino, new_dent.name)} )
∧ valid-dentry(parent_inode.ino, old_dent, fs, ri, ro) ∧ valid-dir-inode(parent_inode, fs, ri)
∧ valid-wb-inode(old_child_inode, fs, ri) ∧ old_child_inode.ino = old_dent.ino ∧ parent_inode.size ≥ 1
∧ (old_child_inode.directory → parent_inode.nsubdirs ≥ 1);
used for: s, ls;
pre-rename-new-reparent
: ⊦ pre-rename-new-reparent(old_parent_inode, old_dent, old_child_inode, new_parent_inode, new_dent, fs, ri, ro)
↔ ( valid-negdentry(new_parent_inode.ino, new_dent, fs, ri, ro) ∧ valid-dentry(old_parent_inode.ino, old_dent, fs, ri, ro)
∧ valid-dir-inode(new_parent_inode, fs, ri) ∧ valid-dir-inode(old_parent_inode, fs, ri)
∧ new_parent_inode.ino ≠ old_parent_inode.ino ∧ valid-wb-inode(old_child_inode, fs, ri) ∧ old_child_inode.ino = old_dent.ino)
∧ old_parent_inode.size ≥ 1 ∧ (old_child_inode.directory → old_parent_inode.nsubdirs ≥ 1);
used for: s, ls;
pre-rename-new-keep-parent
: ⊦ pre-rename-new-keep-parent(parent_inode, old_dent, old_child_inode, new_dent, fs, ri, ro)
↔ ( valid-negdentry(parent_inode.ino, new_dent, fs, ri, ro) ∧ valid-dentry(parent_inode.ino, old_dent, fs, ri, ro)
∧ valid-dir-inode(parent_inode, fs, ri) ∧ valid-wb-inode(old_child_inode, fs, ri) ∧ old_child_inode.ino = old_dent.ino)
∧ parent_inode.size ≥ 1 ∧ (old_child_inode.directory → parent_inode.nsubdirs ≥ 1);
used for: s, ls;
pre-readpage : ⊦ pre-readpage(inode, n, buf, fs, ri) ↔ valid-file-ino(inode.ino, fs, ri) ∧ # buf = VFS_PAGE_SIZE;
used for: s, ls;
pre-writepage : ⊦ pre-writepage(inode, n, buf, fs, ri) ↔ valid-file-ino(inode.ino, fs, ri) ∧ # buf = VFS_PAGE_SIZE;
used for: s, ls;
pre-evict
: ⊦ pre-evict(ino, fs, ri, ro)
↔ valid-ino(ino, fs, ri) ∧ ino ≠ ROOT_INO ∧ (∀ ino. inodekey(ino) ∈ ri ∧ inodekey(ino) ∈ ro → dentrykeys(inodekey(ino), ri) = ∅)
∧ (∀ ino. inodekey(ino) ∈ ri ∧ inodekey(ino) ∈ ro → links(ino, fs, ri) = ∅);
used for: s, ls;
pre-readdir : ⊦ pre-readdir(ino, fs, ri) ↔ valid-dir-ino(ino, fs, ri);
used for: s, ls;
pre-truncate
: ⊦ pre-truncate(inode, n, pageno, buf-opt, fs, ri, ro)
↔ valid-file-inode(inode, fs, ri) ∧ (fs[ri[inodekey(inode.ino)]].nlink = 0 ∧ inode.ino ≠ ROOT_INO ↔ inodekey(inode.ino) ∈ ro)
∧ pageno = inode.size / VFS_PAGE_SIZE ∧ (buf-opt.some? → # buf-opt.buf = VFS_PAGE_SIZE);
used for: s, ls;
pre-iget : ⊦ pre-iget(ino, fs, ri) ↔ valid-ino(ino, fs, ri);
used for: s, ls;
pre-write-inode
: ⊦ pre-write-inode(inode, fs, ri, ro)
↔ (valid-file-inode(inode, fs, ri) ∨ valid-dir-inode(inode, fs, ri))
∧ (fs[ri[inodekey(inode.ino)]].nlink = 0 ∧ inode.ino ≠ ROOT_INO ↔ inodekey(inode.ino) ∈ ro);
used for: s, ls;
valid-inode
: ⊦ valid-inode(inode, fs, ri)
↔ valid-ino(inode.ino, fs, ri) ∧ inode.meta = fs[ri[inodekey(inode.ino)]].meta
∧ (inode.directory ↔ fs[ri[inodekey(inode.ino)]].directory) ∧ inode.nlink = fs[ri[inodekey(inode.ino)]].nlink
∧ inode.nsubdirs = fs[ri[inodekey(inode.ino)]].nsubdirs ∧ inode.size = fs[ri[inodekey(inode.ino)]].size;
used for: s, ls;
valid-wb-inode : ⊦ valid-wb-inode(inode, fs, ri) ↔ valid-file-inode(inode, fs, ri) ∨ valid-dir-inode(inode, fs, ri);
used for: s, ls;
valid-file-inode
: ⊦ valid-file-inode(inode, fs, ri)
↔ valid-file-ino(inode.ino, fs, ri) ∧ (inode.directory ↔ fs[ri[inodekey(inode.ino)]].directory)
∧ inode.nlink = fs[ri[inodekey(inode.ino)]].nlink ∧ inode.nsubdirs = fs[ri[inodekey(inode.ino)]].nsubdirs;
used for: s, ls;
valid-dir-inode
: ⊦ valid-dir-inode(inode, fs, ri)
↔ valid-dir-ino(inode.ino, fs, ri) ∧ (inode.directory ↔ fs[ri[inodekey(inode.ino)]].directory)
∧ inode.nlink = fs[ri[inodekey(inode.ino)]].nlink ∧ inode.nsubdirs = fs[ri[inodekey(inode.ino)]].nsubdirs
∧ inode.size = fs[ri[inodekey(inode.ino)]].size;
used for: s, ls;
end enrich