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: |
|---|---|---|
| abs-fnode | ⊦ abs(fnode(fid), ino) = (emp ∧ ⌜ino = fid.ino⌝ ) | An Axiom |
| abs-empty | ⊦ abs(∅, entries) = (⌜entries = ∅⌝ ∧ emp) | An Axiom |
| abs-files-at | ⊦ ino ∈ files → abs-files(files)[⌜ino⌝ ] = mkfile(files[ino].meta, (files[ino].content.stream to files[ino].size).buf) | An Axiom |
| abs-files-in | ⊦ ⌜ino⌝ ∈ abs-files(files) ↔ ino ∈ files | An Axiom |
| abs-of-at | fd ∈ of ⊦ abs-of(of)[fd] = mkfh(⌜of[fd].ino⌝ , of[fd].mode, of[fd].pos) | An Axiom |
| abs-of-in | ⊦ fd ∈ abs-of(of) ↔ fd ∈ of | An Axiom |
| absc-emp | ⊦ abs|(tree, ino, ε, ino0) = (emp ∧ ⌜ino = ino0⌝ ) | An Axiom |
| absc-dnode | ⊦ p ≠ ε → abs|(dnode(md, sdt), ino, p, ino0) = _∃(λ ad. ino => ad * abs|(sdt, ad.entries, p, ino0) ∧ ⌜ad.meta = md⌝ ∧ ⌜ad.size = # ad.entries⌝ ) | An Axiom |
| abs-dnode | ⊦ abs(dnode(md, sdt), ino) = _∃(λ ad. ino => ad * abs(sdt, ad.entries) ∧ ⌜ad.meta = md⌝ ∧ ⌜ad.size = # ad.entries⌝ ) | An Axiom |
| abs-rec | ⊦ ¬ name ∈ sdt → abs(sdt[name, tree], entries) = (⌜name ∈ entries⌝ ∧ abs(tree, entries[name]) * abs(sdt, entries -- name)) | An Axiom |
| absc-entries | ⊦ abs|(sdt, entries, str ' + p, ino0) = (⌜str ∈ entries⌝ ∧ abs|(sdt[str], entries[str], p, ino0) * abs(sdt -- str, entries -- str)) | An Axiom |
| clinks | ⊦ alink ∈ clinks(ps, ino0, dirs, files) ↔ (∃ ino1, p. p ∈ ps ∧ ispath(p, ino0, ino1, dirs, files)) | An Axiom |
| abs-delorphans | ∀ ino. ¬ ino ∈ files ∨ ¬ ino ∈ dirs, ∀ ino. ⌜ino⌝ ∈ tree.fids → ino ∈ files, abs(tree, ROOT_INO)(dirs) ⊦ dirs \ orphans(dirs, files) = dirs | A User Theorem |
| abs-dir-h | ∀ ino. ¬ ino ∈ files ∨ ¬ ino ∈ dirs, ∀ ino. ⌜ino⌝ ∈ tree.fids → ino ∈ files, ((abs(tree, ino) * D))(dirs), ispath(p, ino, ino0, dirs, files) ⊦ tree[p].dir? ↔ ino0 ∈ dirs | A User Theorem |
| abs-dnode-emp | ⊦ abs(dnode(md, ∅), ino) = _∃(λ m, m0. ino => mkdir(0, md, m, m0, ∅)) | A User Theorem |
| abs-files-cong | ⊦ files0 ~ files1 → abs-files(files0) = abs-files(files1) | A User Theorem |
| abs-files-del | ⊦ abs-files(files) -- ⌜ino⌝ = abs-files(files -- ino) | A User Theorem |
| abs-files-emp | ⊦ abs-files(∅) = ∅ | A User Theorem |
| abs-files-new | ⊦ ¬ ino ∈ files ∧ ino ≠ 0 → abs-files(files)[⌜ino⌝ , mkfile(md, mkbuf(0))] = abs-files((files ++ ino)[ino, mkfile(0, md, 1, ∅)]) | A User Theorem |
| abs-files-put | ⊦ ino ∈ files → (abs-files(files)[⌜ino⌝ , f] = abs-files(files[ino, af]) ↔ f.meta = af.meta ∧ f.content = (af.content.stream to af.size).buf) | A User Theorem |
| abs-files-put-nlink | ⊦ ino ∈ files ∧ files[ino] = mkfile(m, md, n0, content) → abs-files(files[ino, mkfile(m, md, n1, content)]) = abs-files(files) | A User Theorem |
| abs-has-rootpath | ⊦ abs(tree, ino0)(dirs) ∧ ino1 ∈ dirs → (∃ p. ispath(p, ino0, ino1, dirs, files)) | A User Theorem |
| abs-has-rootpath-h | ⊦ ((abs(tree, ino0) * {dirs0} ))(dirs) ∧ ino1 ∈ dirs ∧ ¬ ino1 ∈ dirs0 → (∃ p. ispath(p, ino0, ino1, dirs, files)) | A User Theorem |
| abs-is-dnode | ⊦ tree.dir? → abs(tree, ino) = _∃(λ ad. ino => ad * abs(tree.entries, ad.entries) ∧ ⌜ad.meta = tree.meta⌝ ∧ ⌜ad.size = # ad.entries⌝ ) | A User Theorem |
| abs-is-file | ⊦ ¬ ino ∈ dirs → (((abs(tree, ino) * D))(dirs) ↔ tree = fnode(⌜ino⌝ ) ∧ D(dirs)) | A User Theorem |
| abs-meta-h | ∀ ino. ¬ ino ∈ files ∨ ¬ ino ∈ dirs, ∀ ino. ⌜ino⌝ ∈ tree.fids → ino ∈ files, ((abs(tree, ino) * D))(dirs), ispath(p, ino, dirs, files), fs = abs-files(files) ⊦ meta(p, tree, fs) = meta(p, ino, dirs, files) | A User Theorem |
| abs-nlinks-h | ∀ ino. ¬ ino ∈ files ∨ ¬ ino ∈ dirs, ∀ ino. ⌜ino⌝ ∈ tree.fids → ino ∈ files, abs(tree, ino0)(dirs), ino1 ∈ files, ino0 ∈ dirs ⊦ ⌜ino1⌝ ∈ tree.fids ↔ links(ino1, dirs) ≠ ∅ | A User Theorem |
| abs-of-del | ⊦ abs-of(of) -- fd = abs-of(of -- fd) | A User Theorem |
| abs-of-emp | ⊦ abs-of(∅) = ∅ | A User Theorem |
| abs-of-put | ⊦ abs-of(of)[fd, mkfh(⌜ino⌝ , mode, n)] = abs-of(of[fd, mkfile(ino, mode, n)]) | A User Theorem |
| abs-path-h | ∀ ino. ¬ ino ∈ files ∨ ¬ ino ∈ dirs, ∀ ino. ⌜ino⌝ ∈ tree.fids → ino ∈ files, ((abs(tree, ino) * D))(dirs) ⊦ ispath(p, ino, dirs, files) ↔ p ∈ tree | A User Theorem |
| abs-paths-eq | abs(tree, ino0)(dirs), ∀ ino. ¬ ino ∈ files ∨ ¬ ino ∈ dirs, ∀ ino. ⌜ino⌝ ∈ tree.fids → ino ∈ files, ispath(p0, ino0, ino1, dirs, files), ispath(p1, ino0, ino1, dirs, files), ino1 ∈ dirs ⊦ p0 = p1 | A User Theorem |
| abs-tree | ∀ ino. ¬ ino ∈ files ∨ ¬ ino ∈ dirs, ∀ ino. ⌜ino⌝ ∈ tree0.fids → ino ∈ files, ∀ ino. ⌜ino⌝ ∈ tree1.fids → ino ∈ files, ((abs(tree0, ino) * D0))(dirs), ((abs(tree1, ino) * D1))(dirs) ⊦ tree0 = tree1 | A User Theorem |
| abs-unshared-h | ∀ ino. ¬ ino ∈ files ∨ ¬ ino ∈ dirs, ∀ ino. ⌜ino⌝ ∈ tree0.fids → ino ∈ files, ∀ ino. ⌜ino⌝ ∈ tree1.fids → ino ∈ files, ((abs(tree0, ino0) * abs(tree1, ino1) * D))(dirs), ispath(p0, ino0, n0, dirs, files), ispath(p1, ino1, n1, dirs, files), n0 ∈ dirs, n1 ∈ dirs ⊦ n0 ≠ n1 | A User Theorem |
| absc-dnode-one | ⊦ abs|(dnode(md, sdt), ino, str ', ino0) = _∃(λ ad. ino => ad * abs|(sdt, ad.entries, str ', ino0) ∧ ⌜ad.meta = md⌝ ∧ ⌜ad.size = # ad.entries⌝ ) | A User Theorem |
| absc-dnode-rec | ⊦ abs|(dnode(md, sdt), ino, str ' + p, ino0) = _∃(λ ad. ino => ad * abs|(sdt, ad.entries, str ' + p, ino0) ∧ ⌜ad.meta = md⌝ ∧ ⌜ad.size = # ad.entries⌝ ) | A User Theorem |
| absc-drop | ⊦ p ≠ ε ∧ q ⊑ p ∧ parent(p) ∈ tree ∧ tree[parent(p)].dir? → abs|(tree[p, tree0], ino0, q, ino1) = abs|(tree, ino0, q, ino1) | A User Theorem |
| absc-path | ⊦ p ∈ tree ∧ ((abs|(tree, ino, p, ino0) * D))(dirs) ∧ ispath(p, ino, ino1, dirs, files) → ino0 = ino1 | A User Theorem |
| count-entries | ∀ str. str ∈ entries ↔ str ∈ sdt ⊦ # entries = # sdt | A User Theorem |
| counttheshit | ∀ p. p ∈ ps → fpathtolink(p) ∈ ls, ∀ alink. alink ∈ ls → (∃ p. p ∈ ps ∧ fpathtolink(p) = alink), ∀ p, q. p ∈ ps ∧ q ∈ ps ∧ fpathtolink(p) = fpathtolink(q) → p = q ⊦ # ps = # ls ↔ true | A User Theorem |
| entries-any | sdt ≠ ∅ ⊦ ((abs(sdt, sdi) * D))(dirs) ↔ (∃ tree, ino, str, sdi0, sdt0. ¬ str ∈ sdt0 ∧ sdt = sdt0[str, tree] ∧ ¬ str ∈ sdi0 ∧ sdi = sdi0[str, ino] ∧ ((abs(tree, ino) * abs(sdt0, sdi0) * D))(dirs)) | A User Theorem |
| entries-del | ⊦ ((abs(sdt, sdi) * D))(dirs) ∧ ¬ str ∈ sdt → sdi -- str = sdi | A User Theorem |
| entries-dom | ⊦ ((abs(sdt, sdi) * D))(dirs) → (str ∈ sdi ↔ str ∈ sdt) | A User Theorem |
| entries-dom1 | ⊦ str ∈ sdi ∧ ((abs(sdt, sdi) * D))(dirs) → str ∈ sdt | A User Theorem |
| entries-dom2 | ⊦ str ∈ sdt ∧ ((abs(sdt, sdi) * D))(dirs) → str ∈ sdi | A User Theorem |
| entries-empty | ⊦ abs(sdt, ∅) = (⌜sdt = ∅⌝ ∧ emp) | A User Theorem |
| entries-fold | ⊦ ¬ str ∈ sdt ∧ ¬ str ∈ sdi → abs(tree, ino) * abs(sdt, sdi) = abs(sdt[str, tree], sdi[str, ino]) | A User Theorem |
| entries-fold-fnode | ⊦ ¬ str ∈ sdt ∧ ¬ str ∈ sdi → abs(sdt, sdi) = abs(sdt[str, fnode(⌜ino⌝ )], sdi[str, ino]) | A User Theorem |
| entries-fold-p | ⊦ ¬ str ∈ sdt ∧ ¬ str ∈ sdi ∧ ((abs(tree, ino) * abs(sdt, sdi) * D))(dirs) → ((abs(sdt[str, tree], sdi[str, ino]) * D))(dirs) | A User Theorem |
| entries-recdel | ⊦ str ∈ sdt → abs(sdt, sdi) = (⌜str ∈ sdi⌝ ∧ abs(sdt -- str, sdi -- str) * abs(sdt[str], sdi[str])) | A User Theorem |
| entries-unfold | str ∈ sdt ⊦ ((abs(sdt, sdi) * D))(dirs) ↔ (∃ tree, ino, sdi0, sdt0. ¬ str ∈ sdt0 ∧ sdt = sdt0[str, tree] ∧ ¬ str ∈ sdi0 ∧ sdi = sdi0[str, ino] ∧ ((abs(tree, ino) * abs(sdt0, sdi0) * D))(dirs)) | A User Theorem |
| path-fid | ⊦ ispath(p, ino0, ino1, dirs, files) ∧ ino1 ∈ files ∧ ¬ ino1 ∈ dirs ∧ p ∈ tree ∧ ((abs(tree, ino0) * D))(dirs) → tree[p] = fnode(⌜ino1⌝ ) | A User Theorem |
| path-fold | ⊦ ((abs|(tree, ino0, p, ino1) * abs(tree[p], ino1)))(dirs) ∧ p ∈ tree → abs(tree, ino0)(dirs) | A User Theorem |
| path-split-wand | ⊦ p ∈ tree → abs(tree, ino0) = _∃(λ ino1. abs(tree[p], ino1) * (abs(tree[p], ino1) -* abs(tree, ino0))) | A User Theorem |
| path-unfold | ⊦ p ∈ tree → abs(tree, ino0) = _∃(λ ino1. abs|(tree, ino0, p, ino1) * abs(tree[p], ino1)) | A User Theorem |
| path-unfold-wand | ⊦ p ∈ tree → abs|(tree, ino0, p, ino1) ⊆ abs(tree[p], ino1) -* abs(tree, ino0) | A User Theorem |
| tree-fold-dnode | ⊦ ((ino => mkdir(# entries, md, m, m0, entries) * abs(sdt, entries) * D))(dirs) → ((abs(dnode(md, sdt), ino) * D))(dirs) | A User Theorem |