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-lookup | ⊦ pre-lookup(p_ino, dent, fs, ri, ro) ↔ valid-parent-ino(p_ino, fs, ri, ro) | An Axiom |
| 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) | An Axiom |
| 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 | An Axiom |
| 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) | An Axiom |
| 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 | An Axiom |
| 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 | An Axiom |
| 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) | An Axiom |
| pre-readpage | ⊦ pre-readpage(inode, n, buf, fs, ri) ↔ valid-file-ino(inode.ino, fs, ri) ∧ # buf = VFS_PAGE_SIZE | An Axiom |
| pre-writepage | ⊦ pre-writepage(inode, n, buf, fs, ri) ↔ valid-file-ino(inode.ino, fs, ri) ∧ # buf = VFS_PAGE_SIZE | An Axiom |
| 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) = ∅) | An Axiom |
| pre-readdir | ⊦ pre-readdir(ino, fs, ri) ↔ valid-dir-ino(ino, fs, ri) | An Axiom |
| 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) | An Axiom |
| pre-iget | ⊦ pre-iget(ino, fs, ri) ↔ valid-ino(ino, fs, ri) | An Axiom |
| 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) | An Axiom |
| 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 | An Axiom |
| 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 | An Axiom |
| 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 | An Axiom |
| valid-wb-inode | ⊦ valid-wb-inode(inode, fs, ri) ↔ valid-file-inode(inode, fs, ri) ∨ valid-dir-inode(inode, fs, ri) | An Axiom |
| 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) | An Axiom |
| 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) | An Axiom |
| 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) | An Axiom |
| 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) | An Axiom |