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: |
|---|---|---|
| refine-check-commit | afs_dirs = cache_dirs, afs_files = (cache_files ⊕ cache_pcache) ⊕ cache_icache, afs_asynced ↔ cache_asynced, afs-cons(afs_dirs, afs_files), icache-cons(cache_icache, cache_dirs, cache_files), dcache-cons(cache_dcache, cache_dirs, cache_files), pcache-cons(cache_pcache, cache_dirs, cache_files), synced(cache_dirs, cache_icache, cache_pcache), cache_sync → synced(cache_files, cache_icache, cache_pcache), afs-cons(cache_dirs, cache_files), err = err0 ⊦ ⟪cache_check_commit#(cache_dirs, cache_files; err, cache_asynced)⟫ ⟨afs_check_commit#(afs_dirs, afs_files; err0; afs_asynced)⟩ ((afs_dirs = cache_dirs ∧ afs_files = (cache_files ⊕ cache_pcache) ⊕ cache_icache ∧ (afs_asynced ↔ cache_asynced)) ∧ err = err0) | A Proof Obligation |
| initialization | size = LEB_SIZE ⊦ ⟪cache_format#(n, asynced0, size, md; cache_dirs, cache_files, cache_asynced, cache_icache, cache_dcache, cache_pcache; cache_sync, err)⟫ ( ( err = ESUCCESS → ⟨afs_format#(n, asynced0, size, md; afs_dirs; afs_files, afs_asynced, err0)⟩ ((afs_dirs = cache_dirs ∧ afs_files = (cache_files ⊕ cache_pcache) ⊕ cache_icache ∧ (afs_asynced ↔ cache_asynced)) ∧ err = err0)) ∧ ( err ≠ ESUCCESS → (∀ dirs, files, asynced. ⟨afs_format#(n, asynced0, size, md; afs_dirs; afs_files, afs_asynced, err0)⟩ (dirs = afs_dirs ∧ files = afs_files ∧ (asynced ↔ afs_asynced) ∧ err = err0)))) | A Proof Obligation |
| refine-sync | afs_dirs = cache_dirs, afs_files = (cache_files ⊕ cache_pcache) ⊕ cache_icache, afs_asynced ↔ cache_asynced, afs-cons(afs_dirs, afs_files), icache-cons(cache_icache, cache_dirs, cache_files), dcache-cons(cache_dcache, cache_dirs, cache_files), pcache-cons(cache_pcache, cache_dirs, cache_files), synced(cache_dirs, cache_icache, cache_pcache), cache_sync → synced(cache_files, cache_icache, cache_pcache), afs-cons(cache_dirs, cache_files) ⊦ ⟪cache_sync#(cache_dirs, cache_files; cache_asynced; err)⟫ ⟨afs_sync#(afs_dirs, afs_files; ; afs_asynced, err0)⟩ ((afs_dirs = cache_dirs ∧ afs_files = (cache_files ⊕ cache_pcache) ⊕ cache_icache ∧ (afs_asynced ↔ cache_asynced)) ∧ err = err0) | A Proof Obligation |
| refine-lookup | pre-lookup(p_ino, dent, afs_dirs, afs_files), afs_dirs = cache_dirs, afs_files = (cache_files ⊕ cache_pcache) ⊕ cache_icache, afs_asynced ↔ cache_asynced, afs-cons(afs_dirs, afs_files), icache-cons(cache_icache, cache_dirs, cache_files), dcache-cons(cache_dcache, cache_dirs, cache_files), pcache-cons(cache_pcache, cache_dirs, cache_files), synced(cache_dirs, cache_icache, cache_pcache), cache_sync → synced(cache_files, cache_icache, cache_pcache), afs-cons(cache_dirs, cache_files), dent = dent0, err = err0 ⊦ ⟪cache_lookup#(p_ino, cache_dirs, cache_files, cache_asynced; dent, err, cache_dcache)⟫ ⟨afs_lookup#(p_ino, afs_dirs, afs_files, afs_asynced; dent0, err0)⟩ ((afs_dirs = cache_dirs ∧ afs_files = (cache_files ⊕ cache_pcache) ⊕ cache_icache ∧ (afs_asynced ↔ cache_asynced)) ∧ dent = dent0 ∧ err = err0) | A Proof Obligation |
| refine-create | pre-create(p_inode, dent, md, afs_dirs, afs_files), afs_dirs = cache_dirs, afs_files = (cache_files ⊕ cache_pcache) ⊕ cache_icache, afs_asynced ↔ cache_asynced, afs-cons(afs_dirs, afs_files), icache-cons(cache_icache, cache_dirs, cache_files), dcache-cons(cache_dcache, cache_dirs, cache_files), pcache-cons(cache_pcache, cache_dirs, cache_files), synced(cache_dirs, cache_icache, cache_pcache), cache_sync → synced(cache_files, cache_icache, cache_pcache), afs-cons(cache_dirs, cache_files), p_inode = p_inode0, c_inode = p_inode1, dent = dent0, err = err0 ⊦ ⟪cache_create#(md; p_inode, c_inode, dent, err, cache_dirs, cache_files, cache_icache, cache_dcache, cache_asynced)⟫ ⟨afs_create#(md; p_inode0, p_inode1, dent0, err0, afs_dirs, afs_files; afs_asynced)⟩ ( (afs_dirs = cache_dirs ∧ afs_files = (cache_files ⊕ cache_pcache) ⊕ cache_icache ∧ (afs_asynced ↔ cache_asynced)) ∧ p_inode = p_inode0 ∧ c_inode = p_inode1 ∧ dent = dent0 ∧ err = err0) | A Proof Obligation |
| refine-unlink | pre-unlink(p_inode, c_inode, dent, afs_dirs, afs_files), afs_dirs = cache_dirs, afs_files = (cache_files ⊕ cache_pcache) ⊕ cache_icache, afs_asynced ↔ cache_asynced, afs-cons(afs_dirs, afs_files), icache-cons(cache_icache, cache_dirs, cache_files), dcache-cons(cache_dcache, cache_dirs, cache_files), pcache-cons(cache_pcache, cache_dirs, cache_files), synced(cache_dirs, cache_icache, cache_pcache), cache_sync → synced(cache_files, cache_icache, cache_pcache), afs-cons(cache_dirs, cache_files), p_inode = p_inode0, c_inode = p_inode1, dent = dent0, err = err0 ⊦ ⟪cache_unlink#(; p_inode, c_inode, dent, err, cache_dirs, cache_files, cache_icache, cache_dcache, cache_asynced)⟫ ⟨afs_unlink#(; p_inode0, p_inode1, dent0, err0, afs_dirs, afs_files; afs_asynced)⟩ ( (afs_dirs = cache_dirs ∧ afs_files = (cache_files ⊕ cache_pcache) ⊕ cache_icache ∧ (afs_asynced ↔ cache_asynced)) ∧ p_inode = p_inode0 ∧ c_inode = p_inode1 ∧ dent = dent0 ∧ err = err0) | A Proof Obligation |
| refine-mkdir | pre-mkdir(p_inode, dent, md, afs_dirs, afs_files), afs_dirs = cache_dirs, afs_files = (cache_files ⊕ cache_pcache) ⊕ cache_icache, afs_asynced ↔ cache_asynced, afs-cons(afs_dirs, afs_files), icache-cons(cache_icache, cache_dirs, cache_files), dcache-cons(cache_dcache, cache_dirs, cache_files), pcache-cons(cache_pcache, cache_dirs, cache_files), synced(cache_dirs, cache_icache, cache_pcache), cache_sync → synced(cache_files, cache_icache, cache_pcache), afs-cons(cache_dirs, cache_files), p_inode = p_inode0, c_inode = p_inode1, dent = dent0, err = err0 ⊦ ⟪cache_mkdir#(md; p_inode, c_inode, dent, err, cache_dirs, cache_files, cache_icache, cache_dcache, cache_asynced)⟫ ⟨afs_mkdir#(md; p_inode0, p_inode1, dent0, err0, afs_dirs, afs_files; afs_asynced)⟩ ( (afs_dirs = cache_dirs ∧ afs_files = (cache_files ⊕ cache_pcache) ⊕ cache_icache ∧ (afs_asynced ↔ cache_asynced)) ∧ p_inode = p_inode0 ∧ c_inode = p_inode1 ∧ dent = dent0 ∧ err = err0) | A Proof Obligation |
| refine-rmdir | pre-rmdir(p_inode, c_inode, dent, afs_dirs, afs_files), afs_dirs = cache_dirs, afs_files = (cache_files ⊕ cache_pcache) ⊕ cache_icache, afs_asynced ↔ cache_asynced, afs-cons(afs_dirs, afs_files), icache-cons(cache_icache, cache_dirs, cache_files), dcache-cons(cache_dcache, cache_dirs, cache_files), pcache-cons(cache_pcache, cache_dirs, cache_files), synced(cache_dirs, cache_icache, cache_pcache), cache_sync → synced(cache_files, cache_icache, cache_pcache), afs-cons(cache_dirs, cache_files), p_inode = p_inode0, c_inode = p_inode1, dent = dent0, err = err0 ⊦ ⟪cache_rmdir#(; p_inode, c_inode, dent, err, cache_dirs, cache_files, cache_icache, cache_dcache, cache_asynced)⟫ ⟨afs_rmdir#(; p_inode0, p_inode1, dent0, err0, afs_dirs, afs_files; afs_asynced)⟩ ( (afs_dirs = cache_dirs ∧ afs_files = (cache_files ⊕ cache_pcache) ⊕ cache_icache ∧ (afs_asynced ↔ cache_asynced)) ∧ p_inode = p_inode0 ∧ c_inode = p_inode1 ∧ dent = dent0 ∧ err = err0) | A Proof Obligation |
| refine-link | pre-link(p_inode, c_inode, old_dent, new_dent, afs_dirs, afs_files), afs_dirs = cache_dirs, afs_files = (cache_files ⊕ cache_pcache) ⊕ cache_icache, afs_asynced ↔ cache_asynced, afs-cons(afs_dirs, afs_files), icache-cons(cache_icache, cache_dirs, cache_files), dcache-cons(cache_dcache, cache_dirs, cache_files), pcache-cons(cache_pcache, cache_dirs, cache_files), synced(cache_dirs, cache_icache, cache_pcache), cache_sync → synced(cache_files, cache_icache, cache_pcache), afs-cons(cache_dirs, cache_files), p_inode = p_inode0, c_inode = p_inode1, new_dent = old_dent0, err = err0 ⊦ ⟪cache_link#(old_dent; p_inode, c_inode, new_dent, err, cache_dirs, cache_files, cache_icache, cache_dcache, cache_asynced)⟫ ⟨afs_link#(old_dent; p_inode0, p_inode1, old_dent0, err0, afs_dirs, afs_files; afs_asynced)⟩ ( (afs_dirs = cache_dirs ∧ afs_files = (cache_files ⊕ cache_pcache) ⊕ cache_icache ∧ (afs_asynced ↔ cache_asynced)) ∧ p_inode = p_inode0 ∧ c_inode = p_inode1 ∧ new_dent = old_dent0 ∧ err = err0) | A Proof Obligation |
| refine-renam | pre-rename(old_parent_inode, old_dent, old_child_inode, new_parent_inode, new_dent, new_child_inode, afs_dirs, afs_files), afs_dirs = cache_dirs, afs_files = (cache_files ⊕ cache_pcache) ⊕ cache_icache, afs_asynced ↔ cache_asynced, afs-cons(afs_dirs, afs_files), icache-cons(cache_icache, cache_dirs, cache_files), dcache-cons(cache_dcache, cache_dirs, cache_files), pcache-cons(cache_pcache, cache_dirs, cache_files), synced(cache_dirs, cache_icache, cache_pcache), cache_sync → synced(cache_files, cache_icache, cache_pcache), afs-cons(cache_dirs, cache_files), old_parent_inode = p_inode, new_parent_inode = p_inode0, old_child_inode = p_inode1, new_child_inode = p_inode2, old_dent = old_dent0, new_dent = old_dent1, err = err0 ⊦ ⟪cache_rename# (; old_parent_inode, new_parent_inode, old_child_inode, new_child_inode, old_dent, new_dent, err, cache_dirs, cache_files, cache_icache, cache_dcache, cache_asynced)⟫ ⟨afs_rename#(; p_inode, p_inode0, p_inode1, p_inode2, old_dent0, old_dent1, err0, afs_dirs, afs_files; afs_asynced)⟩ ( (afs_dirs = cache_dirs ∧ afs_files = (cache_files ⊕ cache_pcache) ⊕ cache_icache ∧ (afs_asynced ↔ cache_asynced)) ∧ old_parent_inode = p_inode ∧ new_parent_inode = p_inode0 ∧ old_child_inode = p_inode1 ∧ new_child_inode = p_inode2 ∧ old_dent = old_dent0 ∧ new_dent = old_dent1 ∧ err = err0) | A Proof Obligation |
| refine-readpage | pre-readpage(inode, pageno, buf, afs_dirs, afs_files), afs_dirs = cache_dirs, afs_files = (cache_files ⊕ cache_pcache) ⊕ cache_icache, afs_asynced ↔ cache_asynced, afs-cons(afs_dirs, afs_files), icache-cons(cache_icache, cache_dirs, cache_files), dcache-cons(cache_dcache, cache_dirs, cache_files), pcache-cons(cache_pcache, cache_dirs, cache_files), synced(cache_dirs, cache_icache, cache_pcache), cache_sync → synced(cache_files, cache_icache, cache_pcache), afs-cons(cache_dirs, cache_files), buf = buf0, err = err0 ⊦ ⟪cache_readpage#(inode, pageno, cache_dirs, cache_files, cache_asynced; buf, err, cache_pcache)⟫ ⟨afs_readpage#(inode, pageno, afs_dirs, afs_files, afs_asynced; buf0, err0)⟩ ((afs_dirs = cache_dirs ∧ afs_files = (cache_files ⊕ cache_pcache) ⊕ cache_icache ∧ (afs_asynced ↔ cache_asynced)) ∧ buf = buf0 ∧ err = err0) | A Proof Obligation |
| refine-writepage | pre-writepage(inode, pageno, buf, afs_dirs, afs_files), afs_dirs = cache_dirs, afs_files = (cache_files ⊕ cache_pcache) ⊕ cache_icache, afs_asynced ↔ cache_asynced, afs-cons(afs_dirs, afs_files), icache-cons(cache_icache, cache_dirs, cache_files), dcache-cons(cache_dcache, cache_dirs, cache_files), pcache-cons(cache_pcache, cache_dirs, cache_files), synced(cache_dirs, cache_icache, cache_pcache), cache_sync → synced(cache_files, cache_icache, cache_pcache), afs-cons(cache_dirs, cache_files), err = err0 ⊦ ⟪cache_writepage#(inode, pageno, buf, cache_sync, cache_dirs; err, cache_files, cache_pcache, cache_asynced)⟫ ⟨afs_writepage#(inode, pageno, buf, afs_dirs; err0, afs_files; afs_asynced)⟩ ((afs_dirs = cache_dirs ∧ afs_files = (cache_files ⊕ cache_pcache) ⊕ cache_icache ∧ (afs_asynced ↔ cache_asynced)) ∧ err = err0) | A Proof Obligation |
| refine-readdir | pre-readdir(inode.ino, afs_dirs, afs_files), afs_dirs = cache_dirs, afs_files = (cache_files ⊕ cache_pcache) ⊕ cache_icache, afs_asynced ↔ cache_asynced, afs-cons(afs_dirs, afs_files), icache-cons(cache_icache, cache_dirs, cache_files), dcache-cons(cache_dcache, cache_dirs, cache_files), pcache-cons(cache_pcache, cache_dirs, cache_files), synced(cache_dirs, cache_icache, cache_pcache), cache_sync → synced(cache_files, cache_icache, cache_pcache), afs-cons(cache_dirs, cache_files), strings = strings0, err = err0 ⊦ ⟪cache_readdir#(inode, cache_dirs, cache_files, cache_asynced; strings, err)⟫ ⟨afs_readdir#(inode, afs_dirs, afs_files, afs_asynced; strings0, err0)⟩ ( (afs_dirs = cache_dirs ∧ afs_files = (cache_files ⊕ cache_pcache) ⊕ cache_icache ∧ (afs_asynced ↔ cache_asynced)) ∧ strings = strings0 ∧ err = err0) | A Proof Obligation |
| refine-evict | pre-evict(inode, afs_dirs, afs_files), afs_dirs = cache_dirs, afs_files = (cache_files ⊕ cache_pcache) ⊕ cache_icache, afs_asynced ↔ cache_asynced, afs-cons(afs_dirs, afs_files), icache-cons(cache_icache, cache_dirs, cache_files), dcache-cons(cache_dcache, cache_dirs, cache_files), pcache-cons(cache_pcache, cache_dirs, cache_files), synced(cache_dirs, cache_icache, cache_pcache), cache_sync → synced(cache_files, cache_icache, cache_pcache), afs-cons(cache_dirs, cache_files), err = err0 ⊦ ⟪cache_evict#(inode, cache_asynced; err, cache_dirs, cache_files, cache_icache, cache_pcache)⟫ ⟨afs_evict#(inode, afs_asynced; err0, afs_dirs, afs_files)⟩ ((afs_dirs = cache_dirs ∧ afs_files = (cache_files ⊕ cache_pcache) ⊕ cache_icache ∧ (afs_asynced ↔ cache_asynced)) ∧ err = err0) | A Proof Obligation |
| refine-truncate | pre-truncate(inode, n, pageno, buf-opt, afs_dirs, afs_files), afs_dirs = cache_dirs, afs_files = (cache_files ⊕ cache_pcache) ⊕ cache_icache, afs_asynced ↔ cache_asynced, afs-cons(afs_dirs, afs_files), icache-cons(cache_icache, cache_dirs, cache_files), dcache-cons(cache_dcache, cache_dirs, cache_files), pcache-cons(cache_pcache, cache_dirs, cache_files), synced(cache_dirs, cache_icache, cache_pcache), cache_sync → synced(cache_files, cache_icache, cache_pcache), afs-cons(cache_dirs, cache_files), buf-opt = buf-opt0, inode = inode0, asynced ↔ asynced0, err = err0 ⊦ ⟪cache_truncate#(n, pageno; buf-opt, inode, asynced, err, cache_dirs, cache_files, cache_asynced, cache_icache, cache_pcache)⟫ ⟨afs_truncate#(n, pageno; buf-opt0, inode0, asynced0, err0, afs_dirs, afs_files, afs_asynced)⟩ ( (afs_dirs = cache_dirs ∧ afs_files = (cache_files ⊕ cache_pcache) ⊕ cache_icache ∧ (afs_asynced ↔ cache_asynced)) ∧ buf-opt = buf-opt0 ∧ inode = inode0 ∧ (asynced ↔ asynced0) ∧ err = err0) | A Proof Obligation |
| refine-iget | pre-iget(ino, afs_dirs, afs_files), afs_dirs = cache_dirs, afs_files = (cache_files ⊕ cache_pcache) ⊕ cache_icache, afs_asynced ↔ cache_asynced, afs-cons(afs_dirs, afs_files), icache-cons(cache_icache, cache_dirs, cache_files), dcache-cons(cache_dcache, cache_dirs, cache_files), pcache-cons(cache_pcache, cache_dirs, cache_files), synced(cache_dirs, cache_icache, cache_pcache), cache_sync → synced(cache_files, cache_icache, cache_pcache), afs-cons(cache_dirs, cache_files), inode = inode0, err = err0 ⊦ ⟪cache_iget#(ino, cache_dirs, cache_files, cache_asynced; inode, err, cache_icache)⟫ ⟨afs_iget#(ino, afs_dirs, afs_files, afs_asynced; inode0, err0)⟩ ( (afs_dirs = cache_dirs ∧ afs_files = (cache_files ⊕ cache_pcache) ⊕ cache_icache ∧ (afs_asynced ↔ cache_asynced)) ∧ inode = inode0 ∧ err = err0) | A Proof Obligation |
| refine-write_inode | pre-write-inode(inode, afs_dirs, afs_files), afs_dirs = cache_dirs, afs_files = (cache_files ⊕ cache_pcache) ⊕ cache_icache, afs_asynced ↔ cache_asynced, afs-cons(afs_dirs, afs_files), icache-cons(cache_icache, cache_dirs, cache_files), dcache-cons(cache_dcache, cache_dirs, cache_files), pcache-cons(cache_pcache, cache_dirs, cache_files), synced(cache_dirs, cache_icache, cache_pcache), cache_sync → synced(cache_files, cache_icache, cache_pcache), afs-cons(cache_dirs, cache_files), err = err0 ⊦ ⟪cache_write_inode#(inode, cache_sync; err, cache_dirs, cache_files, cache_icache, cache_asynced)⟫ ⟨afs_write_inode#(inode; err0, afs_dirs, afs_files; afs_asynced)⟩ ((afs_dirs = cache_dirs ∧ afs_files = (cache_files ⊕ cache_pcache) ⊕ cache_icache ∧ (afs_asynced ↔ cache_asynced)) ∧ err = err0) | A Proof Obligation |
| recovery | cache_dirs = cache_dirs0 \ orphans(cache_dirs0, cache_files0), cache_files = cache_files0 \ orphans(cache_dirs0, cache_files0), afs_dirs0 = cache_dirs0, afs_files0 = (cache_files0 ⊕ cache_pcache0) ⊕ cache_icache0, afs_asynced0 ↔ cache_asynced0, cache_asynced0, afs-cons(afs_dirs0, afs_files0), icache-cons(cache_icache0, cache_dirs0, cache_files0), dcache-cons(cache_dcache0, cache_dirs0, cache_files0), pcache-cons(cache_pcache0, cache_dirs0, cache_files0), synced(cache_dirs0, cache_icache0, cache_pcache0), cache_sync0 → synced(cache_files0, cache_icache0, cache_pcache0), afs-cons(cache_dirs0, cache_files0) ⊦ ⟪cache_recovery#(asynced0; cache_dirs, cache_files, cache_asynced, cache_icache, cache_dcache, cache_pcache; cache_sync, err)⟫ ( ( err = ESUCCESS → (∃ afs_dirs, afs_files, afs_asynced. (afs_dirs = afs_dirs0 \ orphans(afs_dirs0, afs_files0) ∧ afs_files = afs_files0 \ orphans(afs_dirs0, afs_files0)) ∧ ⟨afs_recovery#(asynced0; afs_dirs, afs_files; afs_asynced, err0)⟩ ((afs_dirs = cache_dirs ∧ afs_files = (cache_files ⊕ cache_pcache) ⊕ cache_icache ∧ (afs_asynced ↔ cache_asynced)) ∧ err = err0))) ∧ ( err ≠ ESUCCESS → (∀ dirs, files, asynced. ⟨afs_recovery#(asynced0; afs_dirs, afs_files; afs_asynced, err0)⟩ (dirs = afs_dirs ∧ files = afs_files ∧ (asynced ↔ afs_asynced) ∧ err = err0)))) | A Proof Obligation |
| refine-fsync | valid-file-inode(inode, afs_dirs, afs_files), afs_dirs = cache_dirs, afs_files = (cache_files ⊕ cache_pcache) ⊕ cache_icache, afs_asynced ↔ cache_asynced, afs-cons(afs_dirs, afs_files), icache-cons(cache_icache, cache_dirs, cache_files), dcache-cons(cache_dcache, cache_dirs, cache_files), pcache-cons(cache_pcache, cache_dirs, cache_files), synced(cache_dirs, cache_icache, cache_pcache), cache_sync → synced(cache_files, cache_icache, cache_pcache), afs-cons(cache_dirs, cache_files) ⊦ ⟪cache_fsync#(inode, asynced, cache_sync; cache_dirs, cache_files, cache_icache, cache_pcache, cache_asynced; err)⟫ ⟨afs_fsync#(inode, asynced, afs_dirs, afs_files; ; afs_asynced, err0)⟩ ((afs_dirs = cache_dirs ∧ afs_files = (cache_files ⊕ cache_pcache) ⊕ cache_icache ∧ (afs_asynced ↔ cache_asynced)) ∧ err = err0) | A Proof Obligation |
| refine-fsyncdir | afs_dirs = cache_dirs, afs_files = (cache_files ⊕ cache_pcache) ⊕ cache_icache, afs_asynced ↔ cache_asynced, afs-cons(afs_dirs, afs_files), icache-cons(cache_icache, cache_dirs, cache_files), dcache-cons(cache_dcache, cache_dirs, cache_files), pcache-cons(cache_pcache, cache_dirs, cache_files), synced(cache_dirs, cache_icache, cache_pcache), cache_sync → synced(cache_files, cache_icache, cache_pcache), afs-cons(cache_dirs, cache_files) ⊦ ⟪cache_fsyncdir#(inode, asynced, cache_dirs, cache_files, cache_asynced; ; err)⟫ ⟨afs_fsyncdir#(inode, asynced, afs_dirs, afs_files, afs_asynced; ; err0)⟩ ((afs_dirs = cache_dirs ∧ afs_files = (cache_files ⊕ cache_pcache) ⊕ cache_icache ∧ (afs_asynced ↔ cache_asynced)) ∧ err = err0) | A Proof Obligation |
| synced | afs_asynced, afs_dirs = cache_dirs, afs_files = (cache_files ⊕ cache_pcache) ⊕ cache_icache, afs_asynced ↔ cache_asynced, afs-cons(afs_dirs, afs_files), icache-cons(cache_icache, cache_dirs, cache_files), dcache-cons(cache_dcache, cache_dirs, cache_files), pcache-cons(cache_pcache, cache_dirs, cache_files), synced(cache_dirs, cache_icache, cache_pcache), cache_sync → synced(cache_files, cache_icache, cache_pcache) ⊦ cache_asynced | A Proof Obligation |
| refine-rename-dir-dentry | icache-cons(cache_icache, cache_dirs, cache_files), dcache-cons(cache_dcache, cache_dirs, cache_files), pcache-cons(cache_pcache, cache_dirs, cache_files), afs-cons(cache_dirs, cache_files), afs-cons(afs_dirs, afs_files), synced(cache_dirs, cache_icache, cache_pcache), cache_sync → synced(cache_files, cache_icache, cache_pcache), valid-dentry(old_parent_inode.ino, old_dent, afs_dirs, afs_files), valid-dentry(new_parent_inode.ino, new_dent, afs_dirs, afs_files), valid-dir-inode(old_parent_inode, afs_dirs, afs_files), valid-dir-inode(new_parent_inode, afs_dirs, afs_files), valid-dir-inode(old_child_inode, afs_dirs, afs_files), valid-dir-inode(new_child_inode, afs_dirs, afs_files), old_child_inode.ino = old_dent.ino, new_child_inode.ino = new_dent.ino, new_parent_inode.ino = old_parent_inode.ino → new_parent_inode.meta = old_parent_inode.meta, new_dent.ino ≠ ROOT_INO ∧ dir-empty(new_dent.ino, afs_dirs, afs_files), afs_dirs = cache_dirs, afs_files = (cache_files ⊕ cache_pcache) ⊕ cache_icache, afs_asynced ↔ cache_asynced, old_parent_inode = old_parent_inode0, new_parent_inode = new_parent_inode0, old_child_inode = old_child_inode0, new_child_inode = new_child_inode0, old_dent = old_dent0, new_dent = new_dent0, err = err0 ⊦ ⟪cache_rename# (; old_parent_inode, new_parent_inode, old_child_inode, new_child_inode, old_dent, new_dent, err, cache_dirs, cache_files, cache_icache, cache_dcache, cache_asynced)⟫ ⟨afs_rename# (; old_parent_inode0, new_parent_inode0, old_child_inode0, new_child_inode0, old_dent0, new_dent0, err0, afs_dirs, afs_files; afs_asynced)⟩ ( old_parent_inode = old_parent_inode0 ∧ new_parent_inode = new_parent_inode0 ∧ old_child_inode = old_child_inode0 ∧ new_child_inode = new_child_inode0 ∧ old_dent = old_dent0 ∧ new_dent = new_dent0 ∧ err = err0 ∧ afs_dirs = cache_dirs ∧ afs_files = (cache_files ⊕ cache_pcache) ⊕ cache_icache ∧ (afs_asynced ↔ cache_asynced)) | A User Theorem |
| refine-rename-dir-negdentry | icache-cons(cache_icache, cache_dirs, cache_files), dcache-cons(cache_dcache, cache_dirs, cache_files), pcache-cons(cache_pcache, cache_dirs, cache_files), afs-cons(cache_dirs, cache_files), afs-cons(afs_dirs, afs_files), synced(cache_dirs, cache_icache, cache_pcache), cache_sync → synced(cache_files, cache_icache, cache_pcache), valid-dentry(old_parent_inode.ino, old_dent, afs_dirs, afs_files), valid-negdentry(new_parent_inode.ino, new_dent, afs_dirs, afs_files), valid-dir-inode(old_parent_inode, afs_dirs, afs_files), valid-dir-inode(new_parent_inode, afs_dirs, afs_files), valid-dir-inode(old_child_inode, afs_dirs, afs_files), old_child_inode.ino = old_dent.ino, new_parent_inode.ino = old_parent_inode.ino → new_parent_inode.meta = old_parent_inode.meta, afs_dirs = cache_dirs, afs_files = (cache_files ⊕ cache_pcache) ⊕ cache_icache, afs_asynced ↔ cache_asynced, old_parent_inode = old_parent_inode0, new_parent_inode = new_parent_inode0, old_child_inode = old_child_inode0, new_child_inode = new_child_inode0, old_dent = old_dent0, new_dent = new_dent0, err = err0 ⊦ ⟪cache_rename# (; old_parent_inode, new_parent_inode, old_child_inode, new_child_inode, old_dent, new_dent, err, cache_dirs, cache_files, cache_icache, cache_dcache, cache_asynced)⟫ ⟨afs_rename# (; old_parent_inode0, new_parent_inode0, old_child_inode0, new_child_inode0, old_dent0, new_dent0, err0, afs_dirs, afs_files; afs_asynced)⟩ ( old_parent_inode = old_parent_inode0 ∧ new_parent_inode = new_parent_inode0 ∧ old_child_inode = old_child_inode0 ∧ new_child_inode = new_child_inode0 ∧ old_dent = old_dent0 ∧ new_dent = new_dent0 ∧ err = err0 ∧ afs_dirs = cache_dirs ∧ afs_files = (cache_files ⊕ cache_pcache) ⊕ cache_icache ∧ (afs_asynced ↔ cache_asynced)) | A User Theorem |
| refine-rename-file-dentry | icache-cons(cache_icache, cache_dirs, cache_files), dcache-cons(cache_dcache, cache_dirs, cache_files), pcache-cons(cache_pcache, cache_dirs, cache_files), afs-cons(cache_dirs, cache_files), afs-cons(afs_dirs, afs_files), synced(cache_dirs, cache_icache, cache_pcache), cache_sync → synced(cache_files, cache_icache, cache_pcache), valid-dentry(old_parent_inode.ino, old_dent, afs_dirs, afs_files), valid-dentry(new_parent_inode.ino, new_dent, afs_dirs, afs_files), valid-dir-inode(old_parent_inode, afs_dirs, afs_files), valid-dir-inode(new_parent_inode, afs_dirs, afs_files), valid-file-inode(old_child_inode, afs_dirs, afs_files), valid-file-inode(new_child_inode, afs_dirs, afs_files), old_child_inode.ino = old_dent.ino, new_child_inode.ino = new_dent.ino, new_parent_inode.ino = old_parent_inode.ino → new_parent_inode.meta = old_parent_inode.meta, afs_dirs = cache_dirs, afs_files = (cache_files ⊕ cache_pcache) ⊕ cache_icache, afs_asynced ↔ cache_asynced, old_parent_inode = old_parent_inode0, new_parent_inode = new_parent_inode0, old_child_inode = old_child_inode0, new_child_inode = new_child_inode0, old_dent = old_dent0, new_dent = new_dent0, err = err0 ⊦ ⟪cache_rename# (; old_parent_inode, new_parent_inode, old_child_inode, new_child_inode, old_dent, new_dent, err, cache_dirs, cache_files, cache_icache, cache_dcache, cache_asynced)⟫ ⟨afs_rename# (; old_parent_inode0, new_parent_inode0, old_child_inode0, new_child_inode0, old_dent0, new_dent0, err0, afs_dirs, afs_files; afs_asynced)⟩ ( old_parent_inode = old_parent_inode0 ∧ new_parent_inode = new_parent_inode0 ∧ old_child_inode = old_child_inode0 ∧ new_child_inode = new_child_inode0 ∧ old_dent = old_dent0 ∧ new_dent = new_dent0 ∧ err = err0 ∧ afs_dirs = cache_dirs ∧ afs_files = (cache_files ⊕ cache_pcache) ⊕ cache_icache ∧ (afs_asynced ↔ cache_asynced)) | A User Theorem |
| refine-rename-file-negdentry | icache-cons(cache_icache, cache_dirs, cache_files), dcache-cons(cache_dcache, cache_dirs, cache_files), pcache-cons(cache_pcache, cache_dirs, cache_files), afs-cons(cache_dirs, cache_files), afs-cons(afs_dirs, afs_files), synced(cache_dirs, cache_icache, cache_pcache), cache_sync → synced(cache_files, cache_icache, cache_pcache), valid-dentry(old_parent_inode.ino, old_dent, afs_dirs, afs_files), valid-negdentry(new_parent_inode.ino, new_dent, afs_dirs, afs_files), valid-dir-inode(old_parent_inode, afs_dirs, afs_files), valid-dir-inode(new_parent_inode, afs_dirs, afs_files), valid-file-inode(old_child_inode, afs_dirs, afs_files), old_child_inode.ino = old_dent.ino, new_parent_inode.ino = old_parent_inode.ino → new_parent_inode.meta = old_parent_inode.meta, afs_dirs = cache_dirs, afs_files = (cache_files ⊕ cache_pcache) ⊕ cache_icache, afs_asynced ↔ cache_asynced, old_parent_inode = old_parent_inode0, new_parent_inode = new_parent_inode0, old_child_inode = old_child_inode0, new_child_inode = new_child_inode0, old_dent = old_dent0, new_dent = new_dent0, err = err0 ⊦ ⟪cache_rename# (; old_parent_inode, new_parent_inode, old_child_inode, new_child_inode, old_dent, new_dent, err, cache_dirs, cache_files, cache_icache, cache_dcache, cache_asynced)⟫ ⟨afs_rename# (; old_parent_inode0, new_parent_inode0, old_child_inode0, new_child_inode0, old_dent0, new_dent0, err0, afs_dirs, afs_files; afs_asynced)⟩ ( old_parent_inode = old_parent_inode0 ∧ new_parent_inode = new_parent_inode0 ∧ old_child_inode = old_child_inode0 ∧ new_child_inode = new_child_inode0 ∧ old_dent = old_dent0 ∧ new_dent = new_dent0 ∧ err = err0 ∧ afs_dirs = cache_dirs ∧ afs_files = (cache_files ⊕ cache_pcache) ⊕ cache_icache ∧ (afs_asynced ↔ cache_asynced)) | A User Theorem |
| refine-truncate-buff-none-cached | valid-file-inode(inode, afs_dirs, afs_files), pageno = inode.size / VFS_PAGE_SIZE, buf-opt.none?, datakey(inode.ino, pageno) ∈ cache_pcache, afs_dirs = cache_dirs, afs_files = (cache_files ⊕ cache_pcache) ⊕ cache_icache, afs_asynced ↔ cache_asynced, afs-cons(afs_dirs, afs_files), icache-cons(cache_icache, cache_dirs, cache_files), dcache-cons(cache_dcache, cache_dirs, cache_files), pcache-cons(cache_pcache, cache_dirs, cache_files), synced(cache_dirs, cache_icache, cache_pcache), cache_sync → synced(cache_files, cache_icache, cache_pcache), afs-cons(cache_dirs, cache_files), buf-opt = buf-opt0, inode = inode0, asynced ↔ asynced0, err = err0 ⊦ ⟪cache_truncate#(n, pageno; buf-opt, inode, asynced, err, cache_dirs, cache_files, cache_asynced, cache_icache, cache_pcache)⟫ ⟨afs_truncate#(n, pageno; buf-opt0, inode0, asynced0, err0, afs_dirs, afs_files, afs_asynced)⟩ ( (afs_dirs = cache_dirs ∧ afs_files = (cache_files ⊕ cache_pcache) ⊕ cache_icache ∧ (afs_asynced ↔ cache_asynced)) ∧ buf-opt = buf-opt0 ∧ inode = inode0 ∧ (asynced ↔ asynced0) ∧ err = err0) | A User Theorem |
| refine-truncate-buff-none-uncached | valid-file-inode(inode, afs_dirs, afs_files), pageno = inode.size / VFS_PAGE_SIZE, buf-opt.none?, ¬ datakey(inode.ino, pageno) ∈ cache_pcache, afs_dirs = cache_dirs, afs_files = (cache_files ⊕ cache_pcache) ⊕ cache_icache, afs_asynced ↔ cache_asynced, afs-cons(afs_dirs, afs_files), icache-cons(cache_icache, cache_dirs, cache_files), dcache-cons(cache_dcache, cache_dirs, cache_files), pcache-cons(cache_pcache, cache_dirs, cache_files), synced(cache_dirs, cache_icache, cache_pcache), cache_sync → synced(cache_files, cache_icache, cache_pcache), afs-cons(cache_dirs, cache_files), buf-opt = buf-opt0, inode = inode0, asynced ↔ asynced0, err = err0 ⊦ ⟪cache_truncate#(n, pageno; buf-opt, inode, asynced, err, cache_dirs, cache_files, cache_asynced, cache_icache, cache_pcache)⟫ ⟨afs_truncate#(n, pageno; buf-opt0, inode0, asynced0, err0, afs_dirs, afs_files, afs_asynced)⟩ ( (afs_dirs = cache_dirs ∧ afs_files = (cache_files ⊕ cache_pcache) ⊕ cache_icache ∧ (afs_asynced ↔ cache_asynced)) ∧ buf-opt = buf-opt0 ∧ inode = inode0 ∧ (asynced ↔ asynced0) ∧ err = err0) | A User Theorem |
| refine-truncate-buff-some | valid-file-inode(inode, afs_dirs, afs_files), pageno = inode.size / VFS_PAGE_SIZE, buf-opt.some?, # buf-opt.buf = VFS_PAGE_SIZE, afs_dirs = cache_dirs, afs_files = (cache_files ⊕ cache_pcache) ⊕ cache_icache, afs_asynced ↔ cache_asynced, afs-cons(afs_dirs, afs_files), icache-cons(cache_icache, cache_dirs, cache_files), dcache-cons(cache_dcache, cache_dirs, cache_files), pcache-cons(cache_pcache, cache_dirs, cache_files), synced(cache_dirs, cache_icache, cache_pcache), cache_sync → synced(cache_files, cache_icache, cache_pcache), afs-cons(cache_dirs, cache_files), buf-opt = buf-opt0, inode = inode0, asynced ↔ asynced0, err = err0 ⊦ ⟪cache_truncate#(n, pageno; buf-opt, inode, asynced, err, cache_dirs, cache_files, cache_asynced, cache_icache, cache_pcache)⟫ ⟨afs_truncate#(n, pageno; buf-opt0, inode0, asynced0, err0, afs_dirs, afs_files, afs_asynced)⟩ ( (afs_dirs = cache_dirs ∧ afs_files = (cache_files ⊕ cache_pcache) ⊕ cache_icache ∧ (afs_asynced ↔ cache_asynced)) ∧ buf-opt = buf-opt0 ∧ inode = inode0 ∧ (asynced ↔ asynced0) ∧ err = err0) | A User Theorem |