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: |
|---|---|---|
| in-icache-overwrite | ⊦ ino ∈ files ⊕ icache ↔ ino ∈ files | An Axiom |
| icache-cons | ⊦ icache-cons(icache, dirs, files) ↔ (∀ ino. ino ∈ icache → icache[ino].inode.ino = ino ∧ (icache[ino].dirty ⊃ valid-file-inode(icache[ino].inode, dirs, files) ;valid-ino(ino, dirs, files) ∧ valid-inode(icache[ino].inode, dirs, files) )) | An Axiom |
| dcache-cons | ⊦ dcache-cons(dcache, dirs, files) ↔ (∀ key. key ∈ dcache → key.dentry? ∧ key.name = dcache[key].name ∧ valid-dentry(key.ino, dcache[key], dirs, files)) | An Axiom |
| pcache-cons | ⊦ pcache-cons(pcache, dirs, files) ↔ (∀ key. key ∈ pcache → key.data? ∧ # pcache[key].page = VFS_PAGE_SIZE ∧ valid-file-ino(key.ino, dirs, files) ∧ (¬ pcache[key].dirty → key.part ∈ files[key.ino].content ∧ pcache[key].page = files[key.ino].content[key.part])) | An Axiom |
| ientry-dirty-cons | ⊦ ientry-dirty-cons(inode, dirs, files) ↔ valid-file-inode(inode, dirs, files) | An Axiom |
| ientry-clean-cons | ⊦ ientry-clean-cons(inode, dirs, files) ↔ valid-ino(inode.ino, dirs, files) ∧ valid-inode(inode, dirs, files) | An Axiom |
| at-icache-overwrite-no-file | ⊦ ino ∈ icache ∧ icache[ino].inode.directory → (files ⊕ icache)[ino] = files[ino] | An Axiom |
| at-icache-overwrite-not-cached | ⊦ ¬ ino ∈ icache → (files ⊕ icache)[ino] = files[ino] | An Axiom |
| at-icache-overwrite | ⊦ ino ∈ icache ∧ ¬ icache[ino].inode.directory → (files ⊕ icache)[ino] = mkfile(icache[ino].inode.size, icache[ino].inode.meta, icache[ino].inode.nlink, files[ino].content) | An Axiom |
| in-pcache-overwrite | ⊦ ino ∈ files ⊕ pcache ↔ ino ∈ files | An Axiom |
| at-pcache-overwrite | ⊦ (files ⊕ pcache)[ino] = mkfile(files[ino].size, files[ino].meta, files[ino].nlink, files[ino].content ⊕ mkcontent(ino, pcache)) | An Axiom |
| at-overwrite-content-old | ⊦ ¬ n ∈ content1 → (content0 ⊕ content1)[n] = content0[n] | An Axiom |
| at-overwrite-content-new | ⊦ n ∈ content1 → (content0 ⊕ content1)[n] = content1[n] | An Axiom |
| in-overwrite-content | ⊦ n ∈ content0 ⊕ content1 ↔ n ∈ content0 ∨ n ∈ content1 | An Axiom |
| at-mkcontent | ⊦ mkcontent(ino, pcache)[n] = pcache[datakey(ino, n)].page | An Axiom |
| in-mkcontent | ⊦ n ∈ mkcontent(ino, pcache) ↔ datakey(ino, n) ∈ pcache | An Axiom |
| synced-files | ⊦ synced(files, icache, pcache) ↔ (∀ ino. ino ∈ files → synced(ino, icache, pcache)) | An Axiom |
| synced-dirs | ⊦ synced(dirs, icache, pcache) ↔ (∀ ino. ino ∈ dirs → synced(ino, icache, pcache)) | An Axiom |
| synced-ino | ⊦ synced(ino, icache, pcache) ↔ (ino ∈ icache → ¬ icache[ino].dirty) ∧ (∀ n. datakey(ino, n) ∈ pcache → ¬ pcache[datakey(ino, n)].dirty) | An Axiom |
| synced-pages | ⊦ synced(ino, m, pcache) ↔ (∀ n. n ≤ m ∧ datakey(ino, n) ∈ pcache → ¬ pcache[datakey(ino, n)].dirty) | An Axiom |
| synced-inode | ⊦ synced(ino, icache) ↔ ino ∈ icache → ¬ icache[ino].dirty | An Axiom |
| overwrite-icache-empty | ⊦ files ⊕ ∅ = files | A User Theorem |
| overwrite-pcache-empty | ⊦ files ⊕ ∅ = files | A User Theorem |
| overwrite-write-inode-clean-dir | ⊦ ino ∈ dirs ∧ ino ∈ icache ∧ icache[ino].inode.directory → (files ⊕ pcache) ⊕ icache = (files ⊕ pcache) ⊕ icache[ino, mkientry(false, icache[ino].inode.meta:= md)] | A User Theorem |
| overwrite-write-inode-clean-file | ⊦ ino ∈ files ∧ ino ∈ icache ∧ ¬ icache[ino].inode.directory → ((files ⊕ pcache) ⊕ icache)[ino, (((files ⊕ pcache) ⊕ icache)[ino].meta:= md).size:= m] = (files[ino, (files[ino].meta:= md).size:= m] ⊕ pcache) ⊕ icache[ino, mkientry(false, (icache[ino].inode.meta:= md).size:= m)] | A User Theorem |
| overwrite-write-inode-dirty | ⊦ ino ∈ files ∧ ino ∈ icache ∧ ¬ icache[ino].inode.directory → ((files ⊕ pcache) ⊕ icache)[ino, (((files ⊕ pcache) ⊕ icache)[ino].meta:= md).size:= m] = (files ⊕ pcache) ⊕ icache[ino, mkientry(true, (icache[ino].inode.meta:= md).size:= m)] | A User Theorem |
| overwrite-write-page-clean | ⊦ ino ∈ files → ((files ⊕ pcache) ⊕ icache)[ino, ((files ⊕ pcache) ⊕ icache)[ino].content:= ((files ⊕ pcache) ⊕ icache)[ino].content[m, buf]] = (files[ino, files[ino].content:= files[ino].content[m, buf]] ⊕ pcache[datakey(ino, m), mkpentry(false, buf)]) ⊕ icache | A User Theorem |
| overwrite-write-page-dirty | ⊦ ino ∈ files → ((files ⊕ pcache) ⊕ icache)[ino, ((files ⊕ pcache) ⊕ icache)[ino].content:= ((files ⊕ pcache) ⊕ icache)[ino].content[m, buf]] = (files ⊕ pcache[datakey(ino, m), mkpentry(true, buf)]) ⊕ icache | A User Theorem |
| pcache-overwrite-read-page | ⊦ ¬ datakey(ino, n) ∈ pcache ∧ ino ∈ files ∧ n ∈ files[ino].content → files ⊕ pcache[datakey(ino, n), mkpentry(false, files[ino].content[n])] = files ⊕ pcache | A User Theorem |
| synced-dirs-add-new-clean-inode | ⊦ ¬ ino ∈ icache → (synced(dirs, icache[ino, mkientry(false, inode)], pcache) ↔ synced(dirs, icache, pcache)) | A User Theorem |
| synced-dirs-add-update-clean-inode | ⊦ ino ∈ icache ∧ ¬ icache[ino].dirty → (synced(dirs, icache[ino, mkientry(false, inode)], pcache) ↔ synced(dirs, icache, pcache)) | A User Theorem |
| synced-dirs-empty | ⊦ synced(dirs, ∅, ∅) | A User Theorem |
| synced-dirs-variant1 | ⊦ synced(dirs, icache, pcache) → (¬ synced(dirs0, icache0, pcache0) ↔ ¬(∀ ino. (ino ∈ dirs → synced(ino, icache, pcache)) → ino ∈ dirs0 → synced(ino, icache0, pcache0))) | A User Theorem |
| synced-files-add-new-clean-inode | ⊦ ¬ ino ∈ icache → (synced(files, icache[ino, mkientry(false, inode)], pcache) ↔ synced(files, icache, pcache)) | A User Theorem |
| synced-files-empty | ⊦ synced(files, ∅, ∅) | A User Theorem |
| synced-files-update-clean-inode | ⊦ ino ∈ icache ∧ ¬ icache[ino].dirty → (synced(files, icache[ino, mkientry(false, inode)], pcache) ↔ synced(files, icache, pcache)) | A User Theorem |
| synced-files-variant1 | ⊦ synced(files, icache, pcache) → (¬ synced(files0, icache0, pcache0) ↔ ¬(∀ ino. (ino ∈ files → synced(ino, icache, pcache)) → ino ∈ files0 → synced(ino, icache0, pcache0))) | A User Theorem |