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: |
|---|---|---|
| getbyte | ⊦ getbyte(m, content) = getpage(m / VFS_PAGE_SIZE, content)[m % VFS_PAGE_SIZE] | An Axiom |
| getpage | ⊦ getpage(n, content) = (n ∈ content ⊃ content[n];zeropage) | An Axiom |
| stream | ⊦ content.stream = ⌜λ n. getbyte(n, content)⌝ | An Axiom |
| files-iso | ⊦ files0 ~ files1 ↔ (∀ ino. (ino ∈ files0 ↔ ino ∈ files1) ∧ ( ino ∈ files0 → files0[ino].size = files1[ino].size ∧ files0[ino].meta = files1[ino].meta ∧ files0[ino].nlink = files1[ino].nlink ∧ files0[ino].content.stream to files0[ino].size = files1[ino].content.stream to files1[ino].size)) | An Axiom |
| afs-cons-getpage-size | ⊦ afs-cons(dirs, files) ∧ ino ∈ files ∧ files[ino] = mkfile(m, md, m0, content) → # getpage(n, content) = VFS_PAGE_SIZE | A User Theorem |
| at-content-stream | ⊦ n ∈ content ∧ # content[n] = VFS_PAGE_SIZE → ⌜content[n]⌝ = (content.stream from n * VFS_PAGE_SIZE) to VFS_PAGE_SIZE | A User Theorem |
| buf-stream-eq | ⌜# buf⌝ = # σ ⊦ buf = σ.buf ↔ ⌜buf⌝ = σ | A User Theorem |
| bufs-eq | ⊦ ¬ # σ < ⌜n⌝ ∧ ¬ # σ < ⌜m⌝ → ((σ to n).buf = (σ to m).buf ↔ n = m) | A User Theorem |
| content-read | ⊦ # getpage(n, content) = VFS_PAGE_SIZE → ⌜getpage(n, content)⌝ = (content.stream from n * VFS_PAGE_SIZE) to VFS_PAGE_SIZE | A User Theorem |
| content-trunc | ⊦ n = n0 * VFS_PAGE_SIZE + n1 ∧ n1 ≠ 0 ∧ n1 < VFS_PAGE_SIZE → (content upto n).stream = (content.stream to (n0 + 1) * VFS_PAGE_SIZE) + σ⊥ | A User Theorem |
| content-trunc-exact | ⊦ n = n0 * VFS_PAGE_SIZE → (content upto n).stream = (content.stream to n0 * VFS_PAGE_SIZE) + σ⊥ | A User Theorem |
| content-write | ⊦ # buf = VFS_PAGE_SIZE → content[n, buf].stream = (content.stream to n * VFS_PAGE_SIZE) + ⌜buf⌝ + (content.stream from (n + 1) * VFS_PAGE_SIZE) | A User Theorem |
| copy-stream-append | ⊦ n0 + m ≤ # buf0 ∧ n1 + m ≤ # buf1 → ⌜copy(buf0, n0, buf1, n1, m)⌝ = (⌜buf1⌝ to n1) + ((⌜buf0⌝ from n0) to m) + ((⌜buf1⌝ from n1 + m) to (# buf1 - n1 + m)) | A User Theorem |
| emptytream-dist-to | ⊦ (σ⊥ to n) + σ⊥ to m = σ⊥ to m | A User Theorem |
| emtpystream-merge-to | ⊦ (σ⊥ to n) + (σ⊥ to m) = σ⊥ to n + m | A User Theorem |
| fill-stream-append | ⊦ n + m = # buf → ⌜fill(buf, zero, n, m)⌝ = (⌜buf⌝ to n) + (σ⊥ to m) | A User Theorem |
| getbyte-drop-lower | ⊦ n < m * VFS_PAGE_SIZE → getbyte(n, content[m, buf]) = getbyte(n, content) | A User Theorem |
| getbyte-drop-upper | ⊦ (m + 1) * VFS_PAGE_SIZE ≤ n → getbyte(n, content[m, buf]) = getbyte(n, content) | A User Theorem |
| iso-refl | ⊦ files ~ files | A User Theorem |
| iso-sym | ⊦ files0 ~ files1 → files1 ~ files0 | A User Theorem |
| iso-trans | ⊦ files0 ~ files1 ∧ files1 ~ files2 → files0 ~ files2 | A User Theorem |
| iso-unfold | ⊦ ino ∈ files0 ∨ ino ∈ files1 → ( files0 ~ files1 ↔ files0 ~ files1 ∧ files0[ino].size = files1[ino].size ∧ files0[ino].meta = files1[ino].meta ∧ files0[ino].nlink = files1[ino].nlink ∧ files0[ino].content.stream to files0[ino].size = files1[ino].content.stream to files1[ino].size) | A User Theorem |
| stream-at | ⊦ content.stream[n] = getbyte(n, content) | A User Theorem |
| stream-empty | ⊦ ∅.stream = σ⊥ | A User Theorem |
| stream-size | ⊦ # content.stream = ∞ | A User Theorem |
| stream-size-from | ⊦ #(content.stream from n) = ∞ | A User Theorem |
| stream-split-lastpage | ⊦ ¬ m ∈ content → content.stream to m * VFS_PAGE_SIZE + VFS_PAGE_SIZE = (content.stream to m * VFS_PAGE_SIZE) + (σ⊥ to VFS_PAGE_SIZE) | A User Theorem |
| stream-split-partial-lastpage | ⊦ ¬ m ∈ content ∧ n < VFS_PAGE_SIZE → content.stream to m * VFS_PAGE_SIZE + n = (content.stream to m * VFS_PAGE_SIZE) + (σ⊥ to n) | A User Theorem |
| stream-upto | ⊦ (content upto n).stream to n = content.stream to n | A User Theorem |
| upto-stream | ⊦ (content upto m).stream to m = content.stream to m | A User Theorem |
| zeropage-mod-pagesize | ⊦ (zeropage)[n % VFS_PAGE_SIZE] = zero | A User Theorem |
| zerostream-size | ⊦ # σ⊥ = ∞ | A User Theorem |