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-write-inode | ⊦ pre-write-inode(inode, dirs, files) ↔ valid-wb-inode(inode, dirs, files) | An Axiom |
| pre-lookup | ⊦ pre-lookup(p_ino, dent, dirs, files) ↔ valid-parent-ino(p_ino, dirs, files) | An Axiom |
| pre-create | ⊦ pre-create(p_inode, dent, md, dirs, files) ↔ valid-negdentry(p_inode.ino, dent, dirs, files) ∧ valid-dir-inode(p_inode, dirs, files) | An Axiom |
| pre-unlink | ⊦ pre-unlink(p_inode, c_inode, dent, dirs, files) ↔ valid-dentry(p_inode.ino, dent, dirs, files) ∧ valid-file-inode(c_inode, dirs, files) ∧ valid-dir-inode(p_inode, dirs, files) ∧ c_inode.ino = dent.ino | An Axiom |
| pre-mkdir | ⊦ pre-mkdir(p_inode, dent, md, dirs, files) ↔ valid-negdentry(p_inode.ino, dent, dirs, files) ∧ valid-dir-inode(p_inode, dirs, files) | An Axiom |
| pre-rmdir | ⊦ pre-rmdir(p_inode, c_inode, dent, dirs, files) ↔ dent.ino ≠ ROOT_INO ∧ valid-dentry(p_inode.ino, dent, dirs, files) ∧ dir-empty(dent.ino, dirs, files) ∧ valid-dir-inode(p_inode, dirs, files) ∧ valid-dir-inode(c_inode, dirs, files) ∧ c_inode.ino = dent.ino | An Axiom |
| pre-link | ⊦ pre-link(p_inode, c_inode, old_dent, new_dent, dirs, files) ↔ valid-dentry(old_dent, dirs, files) ∧ valid-negdentry(p_inode.ino, new_dent, dirs, files) ∧ (links(old_dent.ino, dirs) ≠ ∅ ∨ old_dent.ino = ROOT_INO) ∧ valid-dir-inode(p_inode, dirs, files) ∧ valid-file-inode(c_inode, dirs, files) ∧ c_inode.ino = old_dent.ino | An Axiom |
| pre-rename | ⊦ pre-rename(old_parent_inode, old_dent, old_child_inode, new_parent_inode, new_dent, new_child_inode, dirs, files) ↔ ( valid-negdentry(new_parent_inode.ino, new_dent, dirs, files) ∨ valid-dentry(new_parent_inode.ino, new_dent, dirs, files) ∧ valid-wb-inode(new_child_inode, dirs, files) ∧ new_child_inode.ino = new_dent.ino ∧ (valid-file-ino(new_dent.ino, dirs, files) ↔ valid-file-ino(old_dent.ino, dirs, files)) ∧ (valid-dir-ino(new_dent.ino, dirs, files) → new_dent.ino ≠ ROOT_INO ∧ dir-empty(new_dent.ino, dirs, files))) ∧ valid-dentry(old_parent_inode.ino, old_dent, dirs, files) ∧ valid-dir-inode(old_parent_inode, dirs, files) ∧ valid-dir-inode(new_parent_inode, dirs, files) ∧ (new_parent_inode.ino = old_parent_inode.ino → new_parent_inode.meta = old_parent_inode.meta) ∧ valid-wb-inode(old_child_inode, dirs, files) ∧ old_child_inode.ino = old_dent.ino | An Axiom |
| pre-readpage | ⊦ pre-readpage(inode, n, buf, dirs, files) ↔ valid-file-ino(inode.ino, dirs, files) ∧ # buf = VFS_PAGE_SIZE | An Axiom |
| pre-writepage | ⊦ pre-writepage(inode, n, buf, dirs, files) ↔ valid-file-ino(inode.ino, dirs, files) ∧ # buf = VFS_PAGE_SIZE | An Axiom |
| pre-evict | ⊦ pre-evict(inode, dirs, files) ↔ valid-wb-inode(inode, dirs, files) ∧ inode.ino ≠ ROOT_INO | An Axiom |
| pre-readdir | ⊦ pre-readdir(ino, dirs, files) ↔ valid-dir-ino(ino, dirs, files) | An Axiom |
| pre-truncate | ⊦ pre-truncate(inode, n, pageno, buf-opt, dirs, files) ↔ valid-file-inode(inode, dirs, files) ∧ pageno = inode.size / VFS_PAGE_SIZE ∧ (buf-opt.some? → # buf-opt.buf = VFS_PAGE_SIZE) | An Axiom |
| pre-iget | ⊦ pre-iget(ino, dirs, files) ↔ valid-ino(ino, dirs, files) | An Axiom |
| valid-file-inode | ⊦ valid-file-inode(inode, dirs, files) ↔ valid-file-ino(inode.ino, dirs, files) ∧ inode.nlink = files[inode.ino].nlink ∧ inode.nsubdirs = 0 ∧ ¬ inode.directory | An Axiom |
| valid-dir-inode | ⊦ valid-dir-inode(inode, dirs, files) ↔ valid-dir-ino(inode.ino, dirs, files) ∧ inode.nlink = dirs[inode.ino].nlink ∧ inode.size = dirs[inode.ino].size ∧ inode.nsubdirs = dirs[inode.ino].nsubdirs ∧ inode.directory | An Axiom |
| valid-wb-inode | ⊦ valid-wb-inode(inode, dirs, files) ↔ valid-dir-inode(inode, dirs, files) ∨ valid-file-inode(inode, dirs, files) | An Axiom |