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: |
|---|---|---|
| read-inv-strong | ⊦ read-inv(n0, n1, inode, buf0, buf1, n, dirs, files) ↔ afs-cons(dirs, files) ∧ # buf0 = # buf1 ∧ inode.ino ∈ files ∧ files[inode.ino].size = inode.size ∧ n0 + n ≤ n1 ∧ n0 + n ≤ inode.size ∧ n1 - n0 ≤ # buf0 ∧ read-inv(n0, n1, buf0, buf1, n, files[inode.ino].content) | An Axiom |
| read-inv | ⊦ read-inv(n0, n1, buf0, buf1, n, content) ↔ ⌜buf1⌝ = ((content.stream from n0) to n) + (⌜buf0⌝ from n) | An Axiom |
| write-inv-strong | ⊦ write-inv(n0, n1, inode, buf, n, dirs, files0, files1) ↔ afs-cons(dirs, files1) ∧ inode.ino ∈ files0 ∧ inode.ino ∈ files1 ∧ files0[inode.ino].size = inode.size ∧ files1[inode.ino].size = files0[inode.ino].size ∧ files1[inode.ino].meta = files0[inode.ino].meta ∧ files1 -- inode.ino = files0 -- inode.ino ∧ n0 + n ≤ n1 ∧ n1 - n0 ≤ # buf ∧ write-inv(n0, n1, buf, n, files0[inode.ino].content, files1[inode.ino].content) | An Axiom |
| write-inv | ⊦ write-inv(n0, n1, buf, n, content0, content1) ↔ content1.stream = (content0.stream to n0) + (⌜buf⌝ to n) + (content0.stream from n0 + n) | An Axiom |
| read-inv-post | ⊦ files[ino] = mkfile(m, md, m1, content) ∧ read-inv(n0, n1, mkinode(ino, md, false, m0, 0, m), buf0, buf1, n, dirs, files) → copy((content.stream to m).buf, n0, buf0, 0, n) = buf1 | A User Theorem |
| read-inv-rec | afs-cons(dirs, files), ino ∈ files, files[ino] = mkfile(n1 + n0 + n, md, m0, content), VFS_PAGE_SIZE = n2 + (n0 + n) % VFS_PAGE_SIZE, n3 + n ≤ # buf0, # buf0 = # buf1 ⊦ read-inv(n0, n3 + n0 + n, buf0, buf1, n, content) → read-inv (n0, n3 + n0 + n, buf0, copy(getpage((n0 + n) / VFS_PAGE_SIZE, content), (n0 + n) % VFS_PAGE_SIZE, buf1, n, min(n3, n2, n1)), min(n3, n2, n1) + n, content) | A User Theorem |
| read-loop-err | err = ESUCCESS ⊦ [vfs_read_loop#(n0, n1, inode, bv, dirs, files, asynced; buf1, n, err)] (⌊err⌋ ∨ err = ESUCCESS) | A User Theorem |
| read-loop-inv | read-inv(n0, n1, inode, buf0, buf1, n, dirs, files) ⊦ [vfs_read_loop#(n0, n1, inode, bv, dirs, files, asynced; buf1, n, err)] read-inv(n0, n1, inode, buf0, buf1, n, dirs, files) | A User Theorem |
| truncate-inv | afs-cons(dirs, files0), files0 = files1, pageno = inode.size / VFS_PAGE_SIZE, buf-opt.none?, inode = getinode(ino, dirs, files0), inode.size = n, inode = inode0, ¬ inode.directory, ino ∈ files0 ⊦ [afs_truncate#(n, pageno; buf-opt, inode, bv, err, dirs, files1, asynced)] ( (err = ESUCCESS ⊃ files1[ino].content.stream from n = σ⊥ ∧ (∀ n0, n1, buf. n1 ≤ # buf → write-inv(n0, n0 + n1, inode, buf, 0, dirs, files1, files1)) ∧ files0 -- ino = files1 -- ino ;⌊err⌋ ) ∧ files0 ~ files1 ∧ inode = inode0) | A User Theorem |
| write-block-inv | write-inv(n0, n1, inode, buf, n, dirs, files0, files1) ⊦ [vfs_write_block#(n0, inode, buf, n1, dirs; n, bv, err, files1, asynced)] write-inv(n0, n1, inode, buf, n, dirs, files0, files1) | A User Theorem |
| write-inode-inv | files1[ino].meta = md, write-inv(n0, n1, mkinode(ino, md, false, m, n0, m0), buf, n, dirs, files0, files1) ⊦ [afs_write_inode#(mkinode(ino, md, false, m, n0, m0 + n); err, dirs, files1; asynced)] [if err = ESUCCESS then files0[ino].size := m0 + n] write-inv(n0, n1, mkinode(ino, md, false, m, n0, files0[ino].size), buf, n, dirs, files0, files1) | A User Theorem |
| write-inv-in0 | ⊦ write-inv(n0, n1, mkinode(ino, md, false, m, m1, m0), buf, n, dirs, files0, files1) → ino ∈ files1 | A User Theorem |
| write-inv-in1 | ⊦ write-inv(n0, n1, mkinode(ino, md, false, m, m1, m0), buf, n, dirs, files0, files1) → ino ∈ files0 | A User Theorem |
| write-inv-ls | ⊦ write-inv(n0, n0 + n1, mkinode(ino, md, false, m, m1, m0), buf, n2, dirs, files0, files1) → n2 ≤ n1 | A User Theorem |
| write-inv-meta | ⊦ files0[ino] = mkfile(m0, md0, n2, content0) ∧ files1[ino] = mkfile(m1, md1, n3, content1) ∧ write-inv(n0, n1, mkinode(ino, md, false, m, n4, m2), buf, n, dirs, files0, files1) → m0 = m1 ∧ md0 = md1 | A User Theorem |
| write-inv-others | ⊦ write-inv(n0, n0 + n1, mkinode(ino, md, false, m, m1, m0), buf, n2, dirs, files0, files1) → (files0 -- ino ≠ files1 -- ino ↔ false) | A User Theorem |
| write-inv-post | ⊦ write-inv(n0, n1, mkinode(ino, md, false, m, m3, m2), buf, n, dirs, files0, files1) ∧ files0[ino] = mkfile(m0, md0, n2, content0) ∧ files1[ino] = mkfile(m1, md1, n3, content1) ∧ content0.stream from m0 = σ⊥ → splice(buf, 0, (content0.stream to m0).buf, n0, n) = (content1.stream to (n ≠ 0 ∧ m0 < n0 + n ⊃ n0 + n;m0)).buf | A User Theorem |
| write-inv-rec | write-inv(n0, n1, mkinode(ino, md, boolvar, m0, m3, m1), buf, n, dirs, files0, files1), files0[ino].content = content0, files1[ino].content = content1, n + m ≤ # buf, m + (n0 + n) % VFS_PAGE_SIZE ≤ VFS_PAGE_SIZE ⊦ write-inv (n0, n1, buf, n + m, content0, content1[(n0 + n) / VFS_PAGE_SIZE, copy(buf, n, getpage((n0 + n) / VFS_PAGE_SIZE, content1), (n0 + n) % VFS_PAGE_SIZE, m)]) | A User Theorem |
| write-inv-stream | files0[ino] = mkfile(m0, md0, n2, content0), files1[ino] = mkfile(m1, md1, n3, content1), write-inv(n0, n1, mkinode(ino, md, false, m, m3, m2), buf, n, dirs, files0, files1) ⊦ content1.stream = (content0.stream to n0) + (⌜buf⌝ to n) + (content0.stream from n0 + n) | A User Theorem |
| write-inv-strong-rec | ino ∈ files1, files1[ino] = mkfile(m2, md0, m3, content), (n0 + n) % VFS_PAGE_SIZE + min(n1 - n0 + n, n2) ≤ VFS_PAGE_SIZE, write-inv(n0, n1, mkinode(ino, md, boolvar, m0, m4, m1), buf, n, dirs, files0, files1) ⊦ write-inv (n0, n1, mkinode(ino, md, boolvar, m0, m4, m1), buf, n + min(n1 - n0 + n, n2), dirs, files0, files1 [ino, mkfile (m2, md0, m3, content[(n0 + n) / VFS_PAGE_SIZE, copy(buf, n, getpage((n0 + n) / VFS_PAGE_SIZE, content), (n0 + n) % VFS_PAGE_SIZE, min(n1 - n0 + n, n2))]) ]) | A User Theorem |
| write-loop-inv | write-inv(n0, n1, inode, buf, n, dirs, files0, files1) ⊦ [vfs_write_loop#(n0, inode, n1, buf, dirs; n, err, files1, asynced)] write-inv(n0, n1, inode, buf, n, dirs, files0, files1) | A User Theorem |
| write-prepost | afs-cons(dirs, files0), of-cons(of0, dirs, files0), files0 = files1, of0 = of1, n0 = n1, n0 ≤ # buf ⊦ [vfs_write#(fd, buf, user; n1, err, of1, dirs, files1, asynced)] [file := of0[fd]] (err = ESUCCESS ⊃ (files1[file.ino].content.stream to files1[file.ino].size).buf = splice(buf, 0, (files0[file.ino].content.stream to files0[file.ino].size).buf, file.pos, n1) ∧ fd ∈ of0 ∧ of1 = of0[fd, file.pos:= (file.pos + n1)] ∧ n1 ≤ n0 ∧ file.ino ∈ files0 ∧ file.ino ∈ files1 ∧ files1[file.ino].meta = files0[file.ino].meta ∧ files1 -- file.ino = files0 -- file.ino ∧ (file.mode = MODE_W ∨ file.mode = MODE_RW) ;files1 ~ files0 ∧ of0 = of1 ∧ (err = EBADFD ∧ (fd ∈ of0 → file.mode ≠ MODE_W ∧ file.mode ≠ MODE_RW) ∨ ⌊err⌋ ) ) | A User Theorem |
| write-prepost-partial | afs-cons(dirs, files0), of-cons(of0, dirs, files0), files0 = files1, of0 = of1, n0 = n1, n0 ≤ # buf, file = of0[fd] ⊦ [vfs_write#(fd, buf, user; n1, err, of1, dirs, files1, asynced)] (err = ESUCCESS ⊃ (files1[file.ino].content.stream to files1[file.ino].size).buf = splice(buf, 0, (files0[file.ino].content.stream to files0[file.ino].size).buf, file.pos, n1) ∧ fd ∈ of0 ∧ of1 = of0[fd, file.pos:= (file.pos + n1)] ∧ n1 ≤ n0 ∧ file.ino ∈ files0 ∧ file.ino ∈ files1 ∧ files1[file.ino].meta = files0[file.ino].meta ∧ files1 -- file.ino = files0 -- file.ino ∧ (file.mode = MODE_W ∨ file.mode = MODE_RW) ;files1 ~ files0 ∧ of0 = of1 ∧ (err = EBADFD ∧ (fd ∈ of0 → file.mode ≠ MODE_W ∧ file.mode ≠ MODE_RW) ∨ ⌊err⌋ ) ) | A User Theorem |
| writepage-afs-cons | afs-cons(dirs, files) ⊦ [vfs_writepage#(inode, n, buf, m, n0, n1, dirs; err, files, asynced)] afs-cons(dirs, files) | A User Theorem |
| writepage-prepost | afs-cons(dirs, files), inode.ino ∈ files, files0 = files, m + n1 ≤ # buf, n0 + n1 ≤ VFS_PAGE_SIZE, ((inode.ino =>mkfile(n2, md, m1, σ) * F))(files) ⊦ [vfs_writepage#(inode, n, buf, m, n0, n1, dirs; err, files, asynced)] ( err = ESUCCESS ∧ ((inode.ino =>mkfile(n2, md, m1, (σ to n * VFS_PAGE_SIZE + n0) + ((⌜buf⌝ from m) to n1) + (σ from n * VFS_PAGE_SIZE + n0 + n1)) * F) )(files) ∨ ⌊err⌋ ∧ files0 = files) | A User Theorem |