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-gc | orphans-cons(fs, ri, ro), dirs = abs-dirs(fs, ri), files = abs-files(fs, ri), orphans(dirs, files) = abs-keys(ro), asynced → boolvar, afs-cons(dirs, files), ubifs-cons(fs, ri, ro, fi, fo, log), replay-cons-strong(fs, ri, ro, fi, fo, log), file-node-cons(fs, ri), orphans-cons(fs, ri, ro), ri-inj(ri), ri-inj(fi), log-cons(log, fs), ro.inodes?, fo.inodes? ⊦ ⟪aubifs_gc#(fi, ro, fo; ri, fs, log, boolvar)⟫ ⟨asynced := ?⟩ (dirs = abs-dirs(fs, ri) ∧ files = abs-files(fs, ri) ∧ orphans(dirs, files) = abs-keys(ro) ∧ (asynced → boolvar)) | A Proof Obligation |
| initialization | pageno = LEB_SIZE, pageno0 = n ⊦ ⟪aubifs_format#(pageno0, boolvar0, pageno, md; ri, fi, ro, fo, fs, log, boolvar1; err)⟫ ( ( err = ESUCCESS → ⟨afs_format#(n, boolvar0, pageno, md; dirs0; files0, asynced, err0)⟩ ((dirs0 = abs-dirs(fs, ri) ∧ files0 = abs-files(fs, ri) ∧ orphans(dirs0, files0) = abs-keys(ro) ∧ (asynced → boolvar1)) ∧ err = err0)) ∧ ( err ≠ ESUCCESS → (∀ dirs, files, boolvar. ⟨afs_format#(n, boolvar0, pageno, md; dirs0; files0, asynced, err0)⟩ (dirs = dirs0 ∧ files = files0 ∧ (boolvar ↔ asynced) ∧ err = err0)))) | A Proof Obligation |
| refine-lookup | pre-lookup(p_ino, dent, dirs, files), dirs = abs-dirs(fs, ri), files = abs-files(fs, ri), orphans(dirs, files) = abs-keys(ro), asynced → boolvar, afs-cons(dirs, files), ubifs-cons(fs, ri, ro, fi, fo, log), replay-cons-strong(fs, ri, ro, fi, fo, log), file-node-cons(fs, ri), orphans-cons(fs, ri, ro), ri-inj(ri), ri-inj(fi), log-cons(log, fs), ro.inodes?, fo.inodes?, dent = old_dent, err = err0 ⊦ ⟪aubifs_lookup#(p_ino, ri, fi, ro, fo, fs, log, boolvar; dent, err)⟫ ⟨afs_lookup#(p_ino, dirs, files, asynced; old_dent, err0)⟩ ( (dirs = abs-dirs(fs, ri) ∧ files = abs-files(fs, ri) ∧ orphans(dirs, files) = abs-keys(ro) ∧ (asynced → boolvar)) ∧ dent = old_dent ∧ err = err0) | A Proof Obligation |
| refine-create | pre-create(p_inode, dent, md, dirs, files), dirs = abs-dirs(fs, ri), files = abs-files(fs, ri), orphans(dirs, files) = abs-keys(ro), asynced → boolvar, afs-cons(dirs, files), ubifs-cons(fs, ri, ro, fi, fo, log), replay-cons-strong(fs, ri, ro, fi, fo, log), file-node-cons(fs, ri), orphans-cons(fs, ri, ro), ri-inj(ri), ri-inj(fi), log-cons(log, fs), ro.inodes?, fo.inodes?, p_inode = p_inode0, c_inode = p_inode1, dent = old_dent, err = err0 ⊦ ⟪aubifs_create#(md, fi, ro, fo; p_inode, c_inode, dent, err, ri, fs, log, boolvar)⟫ ⟨afs_create#(md; p_inode0, p_inode1, old_dent, err0, dirs, files; asynced)⟩ ( (dirs = abs-dirs(fs, ri) ∧ files = abs-files(fs, ri) ∧ orphans(dirs, files) = abs-keys(ro) ∧ (asynced → boolvar)) ∧ p_inode = p_inode0 ∧ c_inode = p_inode1 ∧ dent = old_dent ∧ err = err0) | A Proof Obligation |
| refine-unlink | pre-unlink(p_inode, c_inode, dent, dirs, files), dirs = abs-dirs(fs, ri), files = abs-files(fs, ri), orphans(dirs, files) = abs-keys(ro), asynced → boolvar, afs-cons(dirs, files), ubifs-cons(fs, ri, ro, fi, fo, log), replay-cons-strong(fs, ri, ro, fi, fo, log), file-node-cons(fs, ri), orphans-cons(fs, ri, ro), ri-inj(ri), ri-inj(fi), log-cons(log, fs), ro.inodes?, fo.inodes?, p_inode = p_inode0, c_inode = p_inode1, dent = old_dent, err = err0 ⊦ ⟪aubifs_unlink#(fi, fo; p_inode, c_inode, dent, err, ri, ro, fs, log, boolvar)⟫ ⟨afs_unlink#(; p_inode0, p_inode1, old_dent, err0, dirs, files; asynced)⟩ ( (dirs = abs-dirs(fs, ri) ∧ files = abs-files(fs, ri) ∧ orphans(dirs, files) = abs-keys(ro) ∧ (asynced → boolvar)) ∧ p_inode = p_inode0 ∧ c_inode = p_inode1 ∧ dent = old_dent ∧ err = err0) | A Proof Obligation |
| refine-mkdir | pre-mkdir(p_inode, dent, md, dirs, files), dirs = abs-dirs(fs, ri), files = abs-files(fs, ri), orphans(dirs, files) = abs-keys(ro), asynced → boolvar, afs-cons(dirs, files), ubifs-cons(fs, ri, ro, fi, fo, log), replay-cons-strong(fs, ri, ro, fi, fo, log), file-node-cons(fs, ri), orphans-cons(fs, ri, ro), ri-inj(ri), ri-inj(fi), log-cons(log, fs), ro.inodes?, fo.inodes?, p_inode = p_inode0, c_inode = p_inode1, dent = old_dent, err = err0 ⊦ ⟪aubifs_mkdir#(md, fi, ro, fo; p_inode, c_inode, dent, err, ri, fs, log, boolvar)⟫ ⟨afs_mkdir#(md; p_inode0, p_inode1, old_dent, err0, dirs, files; asynced)⟩ ( (dirs = abs-dirs(fs, ri) ∧ files = abs-files(fs, ri) ∧ orphans(dirs, files) = abs-keys(ro) ∧ (asynced → boolvar)) ∧ p_inode = p_inode0 ∧ c_inode = p_inode1 ∧ dent = old_dent ∧ err = err0) | A Proof Obligation |
| refine-rmdir | pre-rmdir(p_inode, c_inode, dent, dirs, files), dirs = abs-dirs(fs, ri), files = abs-files(fs, ri), orphans(dirs, files) = abs-keys(ro), asynced → boolvar, afs-cons(dirs, files), ubifs-cons(fs, ri, ro, fi, fo, log), replay-cons-strong(fs, ri, ro, fi, fo, log), file-node-cons(fs, ri), orphans-cons(fs, ri, ro), ri-inj(ri), ri-inj(fi), log-cons(log, fs), ro.inodes?, fo.inodes?, p_inode = p_inode0, c_inode = p_inode1, dent = old_dent, err = err0 ⊦ ⟪aubifs_rmdir#(fi, fo; p_inode, c_inode, dent, err, ri, ro, fs, log, boolvar)⟫ ⟨afs_rmdir#(; p_inode0, p_inode1, old_dent, err0, dirs, files; asynced)⟩ ( (dirs = abs-dirs(fs, ri) ∧ files = abs-files(fs, ri) ∧ orphans(dirs, files) = abs-keys(ro) ∧ (asynced → boolvar)) ∧ p_inode = p_inode0 ∧ c_inode = p_inode1 ∧ dent = old_dent ∧ err = err0) | A Proof Obligation |
| refine-link | pre-link(p_inode, c_inode, old_dent, new_dent, dirs, files), dirs = abs-dirs(fs, ri), files = abs-files(fs, ri), orphans(dirs, files) = abs-keys(ro), asynced → boolvar, afs-cons(dirs, files), ubifs-cons(fs, ri, ro, fi, fo, log), replay-cons-strong(fs, ri, ro, fi, fo, log), file-node-cons(fs, ri), orphans-cons(fs, ri, ro), ri-inj(ri), ri-inj(fi), log-cons(log, fs), ro.inodes?, fo.inodes?, p_inode = p_inode0, c_inode = p_inode1, new_dent = old_dent0, err = err0 ⊦ ⟪aubifs_link#(old_dent, fi, ro, fo; p_inode, c_inode, new_dent, err, ri, fs, log, boolvar)⟫ ⟨afs_link#(old_dent; p_inode0, p_inode1, old_dent0, err0, dirs, files; asynced)⟩ ( (dirs = abs-dirs(fs, ri) ∧ files = abs-files(fs, ri) ∧ orphans(dirs, files) = abs-keys(ro) ∧ (asynced → boolvar)) ∧ 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, dirs, files), dirs = abs-dirs(fs, ri), files = abs-files(fs, ri), orphans(dirs, files) = abs-keys(ro), asynced → boolvar, afs-cons(dirs, files), ubifs-cons(fs, ri, ro, fi, fo, log), replay-cons-strong(fs, ri, ro, fi, fo, log), file-node-cons(fs, ri), orphans-cons(fs, ri, ro), ri-inj(ri), ri-inj(fi), log-cons(log, fs), ro.inodes?, fo.inodes?, 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 ⊦ ⟪aubifs_rename#(fi, fo; old_parent_inode, new_parent_inode, old_child_inode, new_child_inode, old_dent, new_dent, err, ri, ro, fs, log, boolvar)⟫ ⟨afs_rename#(; p_inode, p_inode0, p_inode1, p_inode2, old_dent0, old_dent1, err0, dirs, files; asynced)⟩ ( (dirs = abs-dirs(fs, ri) ∧ files = abs-files(fs, ri) ∧ orphans(dirs, files) = abs-keys(ro) ∧ (asynced → boolvar)) ∧ 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, dirs, files), dirs = abs-dirs(fs, ri), files = abs-files(fs, ri), orphans(dirs, files) = abs-keys(ro), asynced → boolvar, afs-cons(dirs, files), ubifs-cons(fs, ri, ro, fi, fo, log), replay-cons-strong(fs, ri, ro, fi, fo, log), file-node-cons(fs, ri), orphans-cons(fs, ri, ro), ri-inj(ri), ri-inj(fi), log-cons(log, fs), ro.inodes?, fo.inodes?, buf = buf0, err = err0 ⊦ ⟪aubifs_readpage#(inode, pageno, ri, fi, ro, fo, fs, log, boolvar; buf, err)⟫ ⟨afs_readpage#(inode, pageno, dirs, files, asynced; buf0, err0)⟩ ((dirs = abs-dirs(fs, ri) ∧ files = abs-files(fs, ri) ∧ orphans(dirs, files) = abs-keys(ro) ∧ (asynced → boolvar)) ∧ buf = buf0 ∧ err = err0) | A Proof Obligation |
| refine-writepage | pre-writepage(inode, pageno, buf, dirs, files), dirs = abs-dirs(fs, ri), files = abs-files(fs, ri), orphans(dirs, files) = abs-keys(ro), asynced → boolvar, afs-cons(dirs, files), ubifs-cons(fs, ri, ro, fi, fo, log), replay-cons-strong(fs, ri, ro, fi, fo, log), file-node-cons(fs, ri), orphans-cons(fs, ri, ro), ri-inj(ri), ri-inj(fi), log-cons(log, fs), ro.inodes?, fo.inodes?, err = err0 ⊦ ⟪aubifs_writepage#(inode, pageno, buf, fi, ro, fo; err, ri, fs, log, boolvar)⟫ ⟨afs_writepage#(inode, pageno, buf, dirs; err0, files; asynced)⟩ ((dirs = abs-dirs(fs, ri) ∧ files = abs-files(fs, ri) ∧ orphans(dirs, files) = abs-keys(ro) ∧ (asynced → boolvar)) ∧ err = err0) | A Proof Obligation |
| refine-readdir | pre-readdir(inode.ino, dirs, files), dirs = abs-dirs(fs, ri), files = abs-files(fs, ri), orphans(dirs, files) = abs-keys(ro), asynced → boolvar, afs-cons(dirs, files), ubifs-cons(fs, ri, ro, fi, fo, log), replay-cons-strong(fs, ri, ro, fi, fo, log), file-node-cons(fs, ri), orphans-cons(fs, ri, ro), ri-inj(ri), ri-inj(fi), log-cons(log, fs), ro.inodes?, fo.inodes?, strings = strings0, err = err0 ⊦ ⟪aubifs_readdir#(inode, ri, fi, ro, fo, fs, log, boolvar; strings, err)⟫ ⟨afs_readdir#(inode, dirs, files, asynced; strings0, err0)⟩ ( (dirs = abs-dirs(fs, ri) ∧ files = abs-files(fs, ri) ∧ orphans(dirs, files) = abs-keys(ro) ∧ (asynced → boolvar)) ∧ strings = strings0 ∧ err = err0) | A Proof Obligation |
| refine-evict | pre-evict(inode, dirs, files), dirs = abs-dirs(fs, ri), files = abs-files(fs, ri), orphans(dirs, files) = abs-keys(ro), asynced → boolvar, afs-cons(dirs, files), ubifs-cons(fs, ri, ro, fi, fo, log), replay-cons-strong(fs, ri, ro, fi, fo, log), file-node-cons(fs, ri), orphans-cons(fs, ri, ro), ri-inj(ri), ri-inj(fi), log-cons(log, fs), ro.inodes?, fo.inodes?, err = err0 ⊦ ⟪aubifs_evict#(inode, fi, fo, fs, log, boolvar; err, ri, ro)⟫ ⟨afs_evict#(inode, asynced; err0, dirs, files)⟩ ((dirs = abs-dirs(fs, ri) ∧ files = abs-files(fs, ri) ∧ orphans(dirs, files) = abs-keys(ro) ∧ (asynced → boolvar)) ∧ err = err0) | A Proof Obligation |
| refine-truncate | pre-truncate(inode, n, pageno, buf-opt, dirs, files), dirs = abs-dirs(fs, ri), files = abs-files(fs, ri), orphans(dirs, files) = abs-keys(ro), asynced → boolvar, afs-cons(dirs, files), ubifs-cons(fs, ri, ro, fi, fo, log), replay-cons-strong(fs, ri, ro, fi, fo, log), file-node-cons(fs, ri), orphans-cons(fs, ri, ro), ri-inj(ri), ri-inj(fi), log-cons(log, fs), ro.inodes?, fo.inodes?, buf-opt = buf-opt0, inode = p_inode, boolvar0 ↔ boolvar1, err = err0 ⊦ ⟪aubifs_truncate#(n, pageno, fi, ro, fo; buf-opt, inode, boolvar0, err, ri, fs, log, boolvar)⟫ ⟨afs_truncate#(n, pageno; buf-opt0, p_inode, boolvar1, err0, dirs, files, asynced)⟩ ( (dirs = abs-dirs(fs, ri) ∧ files = abs-files(fs, ri) ∧ orphans(dirs, files) = abs-keys(ro) ∧ (asynced → boolvar)) ∧ buf-opt = buf-opt0 ∧ inode = p_inode ∧ (boolvar0 ↔ boolvar1) ∧ err = err0) | A Proof Obligation |
| refine-iget | pre-iget(ino, dirs, files), dirs = abs-dirs(fs, ri), files = abs-files(fs, ri), orphans(dirs, files) = abs-keys(ro), asynced → boolvar, afs-cons(dirs, files), ubifs-cons(fs, ri, ro, fi, fo, log), replay-cons-strong(fs, ri, ro, fi, fo, log), file-node-cons(fs, ri), orphans-cons(fs, ri, ro), ri-inj(ri), ri-inj(fi), log-cons(log, fs), ro.inodes?, fo.inodes?, inode = p_inode, err = err0 ⊦ ⟪aubifs_iget#(ino, ri, fi, ro, fo, fs, log, boolvar; inode, err)⟫ ⟨afs_iget#(ino, dirs, files, asynced; p_inode, err0)⟩ ( (dirs = abs-dirs(fs, ri) ∧ files = abs-files(fs, ri) ∧ orphans(dirs, files) = abs-keys(ro) ∧ (asynced → boolvar)) ∧ inode = p_inode ∧ err = err0) | A Proof Obligation |
| refine-write-inode | pre-write-inode(inode, dirs, files), dirs = abs-dirs(fs, ri), files = abs-files(fs, ri), orphans(dirs, files) = abs-keys(ro), asynced → boolvar, afs-cons(dirs, files), ubifs-cons(fs, ri, ro, fi, fo, log), replay-cons-strong(fs, ri, ro, fi, fo, log), file-node-cons(fs, ri), orphans-cons(fs, ri, ro), ri-inj(ri), ri-inj(fi), log-cons(log, fs), ro.inodes?, fo.inodes?, err = err0 ⊦ ⟪aubifs_write_inode#(inode, fi, ro, fo; err, ri, fs, log, boolvar)⟫ ⟨afs_write_inode#(inode; err0, dirs, files; asynced)⟩ ((dirs = abs-dirs(fs, ri) ∧ files = abs-files(fs, ri) ∧ orphans(dirs, files) = abs-keys(ro) ∧ (asynced → boolvar)) ∧ err = err0) | A Proof Obligation |
| refine-check-commit | dirs = abs-dirs(fs, ri), files = abs-files(fs, ri), orphans(dirs, files) = abs-keys(ro), asynced → boolvar, afs-cons(dirs, files), ubifs-cons(fs, ri, ro, fi, fo, log), replay-cons-strong(fs, ri, ro, fi, fo, log), file-node-cons(fs, ri), orphans-cons(fs, ri, ro), ri-inj(ri), ri-inj(fi), log-cons(log, fs), ro.inodes?, fo.inodes?, err = err0 ⊦ ⟪aubifs_check_commit#(ri, ro; err, fi, fo, fs, log, boolvar)⟫ ⟨afs_check_commit#(dirs, files; err0; asynced)⟩ ((dirs = abs-dirs(fs, ri) ∧ files = abs-files(fs, ri) ∧ orphans(dirs, files) = abs-keys(ro) ∧ (asynced → boolvar)) ∧ err = err0) | A Proof Obligation |
| recovery | fi = fi0, fo = fo0, fs = fs0, log = log0, dirs0 = abs-dirs(fs0, ri), files0 = abs-files(fs0, ri), orphans(dirs0, files0) = abs-keys(ro), boolvar0 → boolvar1, boolvar1, afs-cons(dirs0, files0), ubifs-cons(fs0, ri, ro, fi0, fo0, log0), replay-cons-strong(fs0, ri, ro, fi0, fo0, log0), file-node-cons(fs0, ri), orphans-cons(fs0, ri, ro), ri-inj(ri), ri-inj(fi0), log-cons(log0, fs0), ro.inodes?, fo0.inodes? ⊦ ⟪aubifs_replay#(boolvar2; ri0, fi, ro0, fo, fs, log, boolvar3; err)⟫ ( ( err = ESUCCESS → (∃ dirs, files, asynced. (dirs = dirs0 \ orphans(dirs0, files0) ∧ files = files0 \ orphans(dirs0, files0)) ∧ ⟨afs_recovery#(boolvar2; dirs, files; asynced, err0)⟩ ((dirs = abs-dirs(fs, ri0) ∧ files = abs-files(fs, ri0) ∧ orphans(dirs, files) = abs-keys(ro0) ∧ (asynced → boolvar3)) ∧ err = err0))) ∧ ( err ≠ ESUCCESS → (∀ dirs, files, boolvar. ⟨afs_recovery#(boolvar2; dirs1, files1; asynced0, err0)⟩ (dirs = dirs1 ∧ files = files1 ∧ (boolvar ↔ asynced0) ∧ err = err0)))) | A Proof Obligation |
| refine-sync | dirs = abs-dirs(fs, ri), files = abs-files(fs, ri), orphans(dirs, files) = abs-keys(ro), asynced → boolvar, afs-cons(dirs, files), ubifs-cons(fs, ri, ro, fi, fo, log), replay-cons-strong(fs, ri, ro, fi, fo, log), file-node-cons(fs, ri), orphans-cons(fs, ri, ro), ri-inj(ri), ri-inj(fi), log-cons(log, fs), ro.inodes?, fo.inodes? ⊦ ⟪aubifs_sync#(ri, fi, ro, fo, fs, log; boolvar; err)⟫ ⟨afs_sync#(dirs, files; ; asynced, err0)⟩ ((dirs = abs-dirs(fs, ri) ∧ files = abs-files(fs, ri) ∧ orphans(dirs, files) = abs-keys(ro) ∧ (asynced → boolvar)) ∧ err = err0) | A Proof Obligation |
| refine-fsync | valid-file-inode(inode, dirs, files), dirs = abs-dirs(fs, ri), files = abs-files(fs, ri), orphans(dirs, files) = abs-keys(ro), asynced → boolvar, afs-cons(dirs, files), ubifs-cons(fs, ri, ro, fi, fo, log), replay-cons-strong(fs, ri, ro, fi, fo, log), file-node-cons(fs, ri), orphans-cons(fs, ri, ro), ri-inj(ri), ri-inj(fi), log-cons(log, fs), ro.inodes?, fo.inodes? ⊦ ⟪aubifs_fsync#(inode, boolvar0; ; err)⟫ ⟨afs_fsync#(inode, boolvar0, dirs, files; ; asynced, err0)⟩ ((dirs = abs-dirs(fs, ri) ∧ files = abs-files(fs, ri) ∧ orphans(dirs, files) = abs-keys(ro) ∧ (asynced → boolvar)) ∧ err = err0) | A Proof Obligation |
| refine-fsyncdir | dirs = abs-dirs(fs, ri), files = abs-files(fs, ri), orphans(dirs, files) = abs-keys(ro), asynced → boolvar, afs-cons(dirs, files), ubifs-cons(fs, ri, ro, fi, fo, log), replay-cons-strong(fs, ri, ro, fi, fo, log), file-node-cons(fs, ri), orphans-cons(fs, ri, ro), ri-inj(ri), ri-inj(fi), log-cons(log, fs), ro.inodes?, fo.inodes? ⊦ ⟪aubifs_fsyncdir#(inode, boolvar0; ; err)⟫ ⟨afs_fsyncdir#(inode, boolvar0, dirs, files, asynced; ; err0)⟩ ((dirs = abs-dirs(fs, ri) ∧ files = abs-files(fs, ri) ∧ orphans(dirs, files) = abs-keys(ro) ∧ (asynced → boolvar)) ∧ err = err0) | A Proof Obligation |
| synced | asynced, dirs = abs-dirs(fs, ri), files = abs-files(fs, ri), orphans(dirs, files) = abs-keys(ro), asynced → boolvar, afs-cons(dirs, files), ubifs-cons(fs, ri, ro, fi, fo, log), replay-cons-strong(fs, ri, ro, fi, fo, log), file-node-cons(fs, ri), orphans-cons(fs, ri, ro) ⊦ boolvar | A Proof Obligation |
| eq-preserved-gc | dirs = dirs0, files = files0, asynced ↔ boolvar ⊦ ⟪asynced := ?⟫ (dirs0 = dirs ∧ files0 = files) | A Proof Obligation |
| eq-io-write_inode | ⟨afs_write_inode#(inode; err, dirs, files; asynced)⟩ ((inode = p_inode ∧ err = err0) ∧ dirs = dirs0 ∧ files = files0 ∧ (asynced ↔ boolvar)), dirs = dirs1, files = files1 ⊦ ⟨afs_write_inode#(inode; err, dirs1, files1; boolvar0)⟩ ((inode = p_inode ∧ err = err0) ∧ dirs1 = dirs0 ∧ files1 = files0) | A Proof Obligation |
| eq-io-iget | ⟨afs_iget#(ino, dirs, files, asynced; inode, err)⟩ ((ino = ino0 ∧ inode = p_inode ∧ err = err0) ∧ dirs = dirs0 ∧ files = files0 ∧ (asynced ↔ boolvar)), dirs = dirs1, files = files1 ⊦ ⟨afs_iget#(ino, dirs1, files1, boolvar0; inode, err)⟩ ((ino = ino0 ∧ inode = p_inode ∧ err = err0) ∧ dirs1 = dirs0 ∧ files1 = files0) | A Proof Obligation |
| eq-io-truncate | ⟨afs_truncate#(n, pageno; buf-opt, inode, boolvar, err, dirs, files, asynced)⟩ ( (n = n0 ∧ pageno = pageno0 ∧ buf-opt = buf-opt0 ∧ inode = p_inode ∧ (boolvar ↔ boolvar0) ∧ err = err0) ∧ dirs = dirs0 ∧ files = files0 ∧ (asynced ↔ boolvar1)), dirs = dirs1, files = files1 ⊦ ⟨afs_truncate#(n, pageno; buf-opt, inode, boolvar, err, dirs1, files1, boolvar2)⟩ ((n = n0 ∧ pageno = pageno0 ∧ buf-opt = buf-opt0 ∧ inode = p_inode ∧ (boolvar ↔ boolvar0) ∧ err = err0) ∧ dirs1 = dirs0 ∧ files1 = files0) | A Proof Obligation |
| eq-io-evict | ⟨afs_evict#(inode, asynced; err, dirs, files)⟩ ((inode = p_inode ∧ err = err0) ∧ dirs = dirs0 ∧ files = files0 ∧ (asynced ↔ boolvar)), dirs = dirs1, files = files1 ⊦ ⟨afs_evict#(inode, boolvar0; err, dirs1, files1)⟩ ((inode = p_inode ∧ err = err0) ∧ dirs1 = dirs0 ∧ files1 = files0) | A Proof Obligation |
| eq-io-readdir | ⟨afs_readdir#(inode, dirs, files, asynced; strings, err)⟩ ((inode = p_inode ∧ strings = strings0 ∧ err = err0) ∧ dirs = dirs0 ∧ files = files0 ∧ (asynced ↔ boolvar)), dirs = dirs1, files = files1 ⊦ ⟨afs_readdir#(inode, dirs1, files1, boolvar0; strings, err)⟩ ((inode = p_inode ∧ strings = strings0 ∧ err = err0) ∧ dirs1 = dirs0 ∧ files1 = files0) | A Proof Obligation |
| eq-io-writepage | ⟨afs_writepage#(inode, pageno, buf, dirs; err, files; asynced)⟩ ((inode = p_inode ∧ pageno = pageno0 ∧ buf = buf0 ∧ err = err0) ∧ dirs = dirs0 ∧ files = files0 ∧ (asynced ↔ boolvar)), dirs = dirs1, files = files1 ⊦ ⟨afs_writepage#(inode, pageno, buf, dirs1; err, files1; boolvar0)⟩ ((inode = p_inode ∧ pageno = pageno0 ∧ buf = buf0 ∧ err = err0) ∧ dirs1 = dirs0 ∧ files1 = files0) | A Proof Obligation |
| eq-io-readpage | ⟨afs_readpage#(inode, pageno, dirs, files, asynced; buf, err)⟩ ((inode = p_inode ∧ pageno = pageno0 ∧ buf = buf0 ∧ err = err0) ∧ dirs = dirs0 ∧ files = files0 ∧ (asynced ↔ boolvar)), dirs = dirs1, files = files1 ⊦ ⟨afs_readpage#(inode, pageno, dirs1, files1, boolvar0; buf, err)⟩ ((inode = p_inode ∧ pageno = pageno0 ∧ buf = buf0 ∧ err = err0) ∧ dirs1 = dirs0 ∧ files1 = files0) | A Proof Obligation |
| eq-io-renam | ⟨afs_rename#(; old_parent_inode, new_parent_inode, old_child_inode, new_child_inode, old_dent, new_dent, err, dirs, files; 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) ∧ dirs = dirs0 ∧ files = files0 ∧ (asynced ↔ boolvar)), dirs = dirs1, files = files1 ⊦ ⟨afs_rename#(; old_parent_inode, new_parent_inode, old_child_inode, new_child_inode, old_dent, new_dent, err, dirs1, files1; boolvar0)⟩ ( ( 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) ∧ dirs1 = dirs0 ∧ files1 = files0) | A Proof Obligation |
| eq-io-link | ⟨afs_link#(old_dent; p_inode, c_inode, new_dent, err, dirs, files; asynced)⟩ ( (old_dent = old_dent0 ∧ p_inode = p_inode0 ∧ c_inode = p_inode1 ∧ new_dent = old_dent1 ∧ err = err0) ∧ dirs = dirs0 ∧ files = files0 ∧ (asynced ↔ boolvar)), dirs = dirs1, files = files1 ⊦ ⟨afs_link#(old_dent; p_inode, c_inode, new_dent, err, dirs1, files1; boolvar0)⟩ ((old_dent = old_dent0 ∧ p_inode = p_inode0 ∧ c_inode = p_inode1 ∧ new_dent = old_dent1 ∧ err = err0) ∧ dirs1 = dirs0 ∧ files1 = files0) | A Proof Obligation |
| eq-io-rmdir | ⟨afs_rmdir#(; p_inode, c_inode, dent, err, dirs, files; asynced)⟩ ((p_inode = p_inode0 ∧ c_inode = p_inode1 ∧ dent = old_dent ∧ err = err0) ∧ dirs = dirs0 ∧ files = files0 ∧ (asynced ↔ boolvar)), dirs = dirs1, files = files1 ⊦ ⟨afs_rmdir#(; p_inode, c_inode, dent, err, dirs1, files1; boolvar0)⟩ ((p_inode = p_inode0 ∧ c_inode = p_inode1 ∧ dent = old_dent ∧ err = err0) ∧ dirs1 = dirs0 ∧ files1 = files0) | A Proof Obligation |
| eq-io-mkdir | ⟨afs_mkdir#(md; p_inode, c_inode, dent, err, dirs, files; asynced)⟩ ((md = md0 ∧ p_inode = p_inode0 ∧ c_inode = p_inode1 ∧ dent = old_dent ∧ err = err0) ∧ dirs = dirs0 ∧ files = files0 ∧ (asynced ↔ boolvar)), dirs = dirs1, files = files1 ⊦ ⟨afs_mkdir#(md; p_inode, c_inode, dent, err, dirs1, files1; boolvar0)⟩ ((md = md0 ∧ p_inode = p_inode0 ∧ c_inode = p_inode1 ∧ dent = old_dent ∧ err = err0) ∧ dirs1 = dirs0 ∧ files1 = files0) | A Proof Obligation |
| eq-io-unlink | ⟨afs_unlink#(; p_inode, c_inode, dent, err, dirs, files; asynced)⟩ ((p_inode = p_inode0 ∧ c_inode = p_inode1 ∧ dent = old_dent ∧ err = err0) ∧ dirs = dirs0 ∧ files = files0 ∧ (asynced ↔ boolvar)), dirs = dirs1, files = files1 ⊦ ⟨afs_unlink#(; p_inode, c_inode, dent, err, dirs1, files1; boolvar0)⟩ ((p_inode = p_inode0 ∧ c_inode = p_inode1 ∧ dent = old_dent ∧ err = err0) ∧ dirs1 = dirs0 ∧ files1 = files0) | A Proof Obligation |
| eq-io-create | ⟨afs_create#(md; p_inode, c_inode, dent, err, dirs, files; asynced)⟩ ((md = md0 ∧ p_inode = p_inode0 ∧ c_inode = p_inode1 ∧ dent = old_dent ∧ err = err0) ∧ dirs = dirs0 ∧ files = files0 ∧ (asynced ↔ boolvar)), dirs = dirs1, files = files1 ⊦ ⟨afs_create#(md; p_inode, c_inode, dent, err, dirs1, files1; boolvar0)⟩ ((md = md0 ∧ p_inode = p_inode0 ∧ c_inode = p_inode1 ∧ dent = old_dent ∧ err = err0) ∧ dirs1 = dirs0 ∧ files1 = files0) | A Proof Obligation |
| eq-io-lookup | ⟨afs_lookup#(p_ino, dirs, files, asynced; dent, err)⟩ ((p_ino = pageno ∧ dent = old_dent ∧ err = err0) ∧ dirs = dirs0 ∧ files = files0 ∧ (asynced ↔ boolvar)), dirs = dirs1, files = files1 ⊦ ⟨afs_lookup#(p_ino, dirs1, files1, boolvar0; dent, err)⟩ ((p_ino = pageno ∧ dent = old_dent ∧ err = err0) ∧ dirs1 = dirs0 ∧ files1 = files0) | A Proof Obligation |
| eq-io-fsyncdir | ⟨afs_fsyncdir#(inode, boolvar, dirs, files, asynced; ; err)⟩ ((inode = p_inode ∧ (boolvar ↔ boolvar0) ∧ err = err0) ∧ dirs = dirs0 ∧ files = files0 ∧ (asynced ↔ boolvar1)), dirs = dirs1, files = files1 ⊦ ⟨afs_fsyncdir#(inode, boolvar, dirs1, files1, boolvar2; ; err)⟩ ((inode = p_inode ∧ (boolvar ↔ boolvar0) ∧ err = err0) ∧ dirs1 = dirs0 ∧ files1 = files0) | A Proof Obligation |
| eq-io-fsync | ⟨afs_fsync#(inode, boolvar, dirs, files; ; asynced, err)⟩ ((inode = p_inode ∧ (boolvar ↔ boolvar0) ∧ err = err0) ∧ dirs = dirs0 ∧ files = files0 ∧ (asynced ↔ boolvar1)), dirs = dirs1, files = files1 ⊦ ⟨afs_fsync#(inode, boolvar, dirs1, files1; ; boolvar2, err)⟩ ((inode = p_inode ∧ (boolvar ↔ boolvar0) ∧ err = err0) ∧ dirs1 = dirs0 ∧ files1 = files0) | A Proof Obligation |
| eq-io-sync | ⟨afs_sync#(dirs, files; ; asynced, err)⟩ (err = err0 ∧ dirs = dirs0 ∧ files = files0 ∧ (asynced ↔ boolvar)), dirs = dirs1, files = files1 ⊦ ⟨afs_sync#(dirs1, files1; ; boolvar0, err)⟩ (err = err0 ∧ dirs1 = dirs0 ∧ files1 = files0) | A Proof Obligation |
| eq-io-format | ⟨afs_format#(n, boolvar, pageno, md; dirs; files, asynced, err)⟩ ((n = n0 ∧ (boolvar ↔ boolvar0) ∧ pageno = pageno0 ∧ md = md0 ∧ err = err0) ∧ dirs = dirs0 ∧ files = files0 ∧ (asynced ↔ boolvar1)), dirs = dirs1, files = files1 ⊦ ⟨afs_format#(n, boolvar, pageno, md; dirs1; files1, boolvar2, err)⟩ ((n = n0 ∧ (boolvar ↔ boolvar0) ∧ pageno = pageno0 ∧ md = md0 ∧ err = err0) ∧ dirs1 = dirs0 ∧ files1 = files0) | A Proof Obligation |
| eq-io-check-commit | ⟨afs_check_commit#(dirs, files; err; asynced)⟩ (err = err0 ∧ dirs = dirs0 ∧ files = files0 ∧ (asynced ↔ boolvar)), dirs = dirs1, files = files1 ⊦ ⟨afs_check_commit#(dirs1, files1; err; boolvar0)⟩ (err = err0 ∧ dirs1 = dirs0 ∧ files1 = files0) | A Proof Obligation |
| eq-io-recovery | ⟨afs_recovery#(boolvar; dirs, files; asynced, err)⟩ (((boolvar ↔ boolvar0) ∧ err = err0) ∧ dirs = dirs0 ∧ files = files0 ∧ (asynced ↔ boolvar1)), dirs = dirs1, files = files1 ⊦ ⟨afs_recovery#(boolvar; dirs1, files1; boolvar2, err)⟩ (((boolvar ↔ boolvar0) ∧ err = err0) ∧ dirs1 = dirs0 ∧ files1 = files0) | A Proof Obligation |
| eq-trans | dirs = dirs0, files = files0, dirs0 = dirs1, files0 = files1 ⊦ dirs = dirs1 ∧ files = files1 | A Proof Obligation |
| eq-sym | dirs = dirs0, files = files0 ⊦ dirs0 = dirs ∧ files0 = files | A Proof Obligation |
| eq-refl | ⊦ dirs = dirs ∧ files = files | A Proof Obligation |
| afs-cons-abs-dir-size | ⊦ afs-cons(abs-dirs(fs, ri), abs-files(fs, ri)) ∧ ino ∈ abs-dirs(fs, ri) ∧ abs-dirs(fs, ri)[ino].entries ≠ ∅ → fs[ri[inodekey(ino)]].size ≥ 1 | A User Theorem |
| afs-cons-abs-dir-subdirs | ⊦ afs-cons(abs-dirs(fs, ri), abs-files(fs, ri)) ∧ ino ∈ abs-dirs(fs, ri) ∧ subdirs(ino, abs-dirs(fs, ri)) ≠ ∅ → fs[ri[inodekey(ino)]].nsubdirs ≥ 1 | A User Theorem |
| at-fs | ⊦ fs[adr, nd][adr0] = (adr = adr0 ⊃ nd;fs[adr0]) | A User Theorem |
| at-ri | ⊦ ri[key, adr][key0] = (key = key0 ⊃ adr;ri[key0]) | A User Theorem |
| in-del | ⊦ key ∈ ri -- key0 ↔ key ∈ ri ∧ key ≠ key0 | A User Theorem |
| in-diff | ⊦ key ∈ ri \ ks ↔ key ∈ ri ∧ ¬ key ∈ ks | A User Theorem |
| in-insert | ⊦ str ∈ entries[str0, n] ↔ str0 = str ∨ str ∈ entries | A User Theorem |
| in-insert-ri-cut | ⊦ key ≠ key0 → (key ∈ ri[key0, adr] ↔ key ∈ ri) | A User Theorem |
| in-insert-ri-equiv | ⊦ key ∈ ri[key0, adr] ↔ key = key0 ∨ key ∈ ri | A User Theorem |
| in-ri-data-dentry | ⊦ datakey(ino, n) ∈ ri[dentrykey(ino, str), adr] ↔ datakey(ino, n) ∈ ri | A User Theorem |
| in-ri-data-inode | ⊦ datakey(ino, n) ∈ ri[inodekey(ino), adr] ↔ datakey(ino, n) ∈ ri | A User Theorem |
| in-ri-dentry-data | ⊦ dentrykey(ino, str) ∈ ri[datakey(ino, n), adr] ↔ dentrykey(ino, str) ∈ ri | A User Theorem |
| in-ri-dentry-inode | ⊦ dentrykey(ino, str) ∈ ri[inodekey(ino), adr] ↔ dentrykey(ino, str) ∈ ri | A User Theorem |
| in-ri-inode-data | ⊦ inodekey(ino) ∈ ri[datakey(ino, n), adr] ↔ inodekey(ino) ∈ ri | A User Theorem |
| in-ri-inode-dentry | ⊦ inodekey(ino) ∈ ri[dentrykey(ino, str), adr] ↔ inodekey(ino) ∈ ri | A User Theorem |
| log-cons-2 | ⊦ log-cons(log, fs) ∧ ¬ adr0 ∈ fs ∧ ¬ adr1 ∈ fs ∧ adr0 ≠ adr1 → log-cons(log, fs[adr0, nd0][adr1, nd1]) | A User Theorem |
| mkdir-inj | ⊦ mkdir(n, md, m, n0, entries0) = mkdir(n, md, m, n0, entries1) ↔ entries0 = entries1 | A User Theorem |
| refine-rename-new-keep-parent | old_parent_inode.ino = new_parent_inode.ino, valid-negdentry(new_parent_inode.ino, new_dent, dirs, files), pre-rename(old_inode, old_dent, old_dent_inode, new_inode, new_dent, new_dent_inode, dirs, files), dirs = abs-dirs(fs, ri), files = abs-files(fs, ri), orphans(dirs, files) = abs-keys(ro), boolvar → boolvar0, afs-cons(dirs, files), ubifs-cons(fs, ri, ro, fi, fo, log), orphans-cons(fs, ri, ro), replay-cons-strong(fs, ri, ro, fi, fo, log), file-node-cons(fs, ri), ri-inj(ri), ri-inj(fi), log-cons(log, fs), ro.inodes?, fo.inodes?, old_parent_inode = old_inode, new_parent_inode = new_inode, old_child_inode = old_dent_inode, new_child_inode = new_dent_inode, old_dent = old_dent0, new_dent = old_dent1, err = err0 ⊦ ⟪aubifs_rename_new_keep_parent# (old_child_inode.directory, old_child_inode, fi, ro, fo; old_parent_inode, old_dent, new_dent, err, ri, fs, log, boolvar0); new_parent_inode := old_parent_inode⟫ ⟨afs_rename#(; old_inode, new_inode, old_dent_inode, new_dent_inode, old_dent0, old_dent1, err0, dirs, files; boolvar)⟩ ( (dirs = abs-dirs(fs, ri) ∧ files = abs-files(fs, ri) ∧ orphans(dirs, files) = abs-keys(ro) ∧ (boolvar → boolvar0)) ∧ old_parent_inode = old_inode ∧ new_parent_inode = new_inode ∧ old_child_inode = old_dent_inode ∧ new_child_inode = new_dent_inode ∧ old_dent = old_dent0 ∧ new_dent = old_dent1 ∧ err = err0) | A User Theorem |
| refine-rename-new-reparent | old_parent_inode.ino ≠ new_parent_inode.ino, valid-negdentry(new_parent_inode.ino, new_dent, dirs, files), pre-rename(old_inode, old_dent, old_dent_inode, new_inode, new_dent, new_dent_inode, dirs, files), dirs = abs-dirs(fs, ri), files = abs-files(fs, ri), orphans(dirs, files) = abs-keys(ro), boolvar → boolvar0, afs-cons(dirs, files), ubifs-cons(fs, ri, ro, fi, fo, log), orphans-cons(fs, ri, ro), replay-cons-strong(fs, ri, ro, fi, fo, log), file-node-cons(fs, ri), ri-inj(ri), ri-inj(fi), log-cons(log, fs), ro.inodes?, fo.inodes?, old_parent_inode = old_inode, new_parent_inode = new_inode, old_child_inode = old_dent_inode, new_child_inode = new_dent_inode, old_dent = old_dent0, new_dent = old_dent1, err = err0 ⊦ ⟪aubifs_rename_new_reparent# (old_child_inode.directory, old_child_inode, fi, ro, fo; old_parent_inode, new_parent_inode, old_dent, new_dent, err, ri, fs, log, boolvar0)⟫ ⟨afs_rename#(; old_inode, new_inode, old_dent_inode, new_dent_inode, old_dent0, old_dent1, err0, dirs, files; boolvar)⟩ ( (dirs = abs-dirs(fs, ri) ∧ files = abs-files(fs, ri) ∧ orphans(dirs, files) = abs-keys(ro) ∧ (boolvar → boolvar0)) ∧ old_parent_inode = old_inode ∧ new_parent_inode = new_inode ∧ old_child_inode = old_dent_inode ∧ new_child_inode = new_dent_inode ∧ old_dent = old_dent0 ∧ new_dent = old_dent1 ∧ err = err0) | A User Theorem |
| refine-rename-overwrite-keep-parent | old_parent_inode.ino = new_parent_inode.ino, valid-dentry(new_parent_inode.ino, new_dent, dirs, files), pre-rename(old_inode, old_dent, old_dent_inode, new_inode, new_dent, new_dent_inode, dirs, files), dirs = abs-dirs(fs, ri), files = abs-files(fs, ri), orphans(dirs, files) = abs-keys(ro), boolvar → boolvar0, afs-cons(dirs, files), ubifs-cons(fs, ri, ro, fi, fo, log), orphans-cons(fs, ri, ro), replay-cons-strong(fs, ri, ro, fi, fo, log), file-node-cons(fs, ri), ri-inj(ri), ri-inj(fi), log-cons(log, fs), ro.inodes?, fo.inodes?, old_parent_inode = old_inode, new_parent_inode = new_inode, old_child_inode = old_dent_inode, new_child_inode = new_dent_inode, old_dent = old_dent0, new_dent = old_dent1, err = err0 ⊦ ⟪aubifs_rename_overwrite_keep_parent# (old_child_inode.directory, old_child_inode, fi, fo; old_parent_inode, new_child_inode, old_dent, new_dent, err, ri, ro, fs, log, boolvar0); new_parent_inode := old_parent_inode⟫ ⟨afs_rename#(; old_inode, new_inode, old_dent_inode, new_dent_inode, old_dent0, old_dent1, err0, dirs, files; boolvar)⟩ ( (dirs = abs-dirs(fs, ri) ∧ files = abs-files(fs, ri) ∧ orphans(dirs, files) = abs-keys(ro) ∧ (boolvar → boolvar0)) ∧ old_parent_inode = old_inode ∧ new_parent_inode = new_inode ∧ old_child_inode = old_dent_inode ∧ new_child_inode = new_dent_inode ∧ old_dent = old_dent0 ∧ new_dent = old_dent1 ∧ err = err0) | A User Theorem |
| refine-rename-overwrite-keep-parent-different | old_dent ≠ new_dent, old_parent_inode.ino = new_parent_inode.ino, valid-dentry(new_parent_inode.ino, new_dent, dirs, files), pre-rename(old_inode, old_dent, old_dent_inode, new_inode, new_dent, new_dent_inode, dirs, files), dirs = abs-dirs(fs, ri), files = abs-files(fs, ri), orphans(dirs, files) = abs-keys(ro), boolvar → boolvar0, afs-cons(dirs, files), ubifs-cons(fs, ri, ro, fi, fo, log), orphans-cons(fs, ri, ro), replay-cons-strong(fs, ri, ro, fi, fo, log), file-node-cons(fs, ri), ri-inj(ri), ri-inj(fi), log-cons(log, fs), ro.inodes?, fo.inodes?, old_parent_inode = old_inode, new_parent_inode = new_inode, old_child_inode = old_dent_inode, new_child_inode = new_dent_inode, old_dent = old_dent0, new_dent = old_dent1, err = err0 ⊦ ⟪aubifs_rename_overwrite_keep_parent# (old_child_inode.directory, old_child_inode, fi, fo; old_parent_inode, new_child_inode, old_dent, new_dent, err, ri, ro, fs, log, boolvar0); new_parent_inode := old_parent_inode⟫ ⟨afs_rename#(; old_inode, new_inode, old_dent_inode, new_dent_inode, old_dent0, old_dent1, err0, dirs, files; boolvar)⟩ ( (dirs = abs-dirs(fs, ri) ∧ files = abs-files(fs, ri) ∧ orphans(dirs, files) = abs-keys(ro) ∧ (boolvar → boolvar0)) ∧ old_parent_inode = old_inode ∧ new_parent_inode = new_inode ∧ old_child_inode = old_dent_inode ∧ new_child_inode = new_dent_inode ∧ old_dent = old_dent0 ∧ new_dent = old_dent1 ∧ err = err0) | A User Theorem |
| refine-rename-overwrite-keep-parent-identity | old_dent = new_dent, old_parent_inode.ino = new_parent_inode.ino, valid-dentry(new_parent_inode.ino, new_dent, dirs, files), pre-rename(old_inode, old_dent, old_dent_inode, new_inode, new_dent, new_dent_inode, dirs, files), dirs = abs-dirs(fs, ri), files = abs-files(fs, ri), orphans(dirs, files) = abs-keys(ro), boolvar → boolvar0, afs-cons(dirs, files), ubifs-cons(fs, ri, ro, fi, fo, log), orphans-cons(fs, ri, ro), replay-cons-strong(fs, ri, ro, fi, fo, log), file-node-cons(fs, ri), ri-inj(ri), ri-inj(fi), log-cons(log, fs), ro.inodes?, fo.inodes?, old_parent_inode = old_inode, new_parent_inode = new_inode, old_child_inode = old_dent_inode, new_child_inode = new_dent_inode, old_dent = old_dent0, new_dent = old_dent1, err = err0 ⊦ ⟪aubifs_rename_overwrite_keep_parent# (old_child_inode.directory, old_child_inode, fi, fo; old_parent_inode, new_child_inode, old_dent, new_dent, err, ri, ro, fs, log, boolvar0); new_parent_inode := old_parent_inode⟫ ⟨afs_rename#(; old_inode, new_inode, old_dent_inode, new_dent_inode, old_dent0, old_dent1, err0, dirs, files; boolvar)⟩ ( (dirs = abs-dirs(fs, ri) ∧ files = abs-files(fs, ri) ∧ orphans(dirs, files) = abs-keys(ro) ∧ (boolvar → boolvar0)) ∧ old_parent_inode = old_inode ∧ new_parent_inode = new_inode ∧ old_child_inode = old_dent_inode ∧ new_child_inode = new_dent_inode ∧ old_dent = old_dent0 ∧ new_dent = old_dent1 ∧ err = err0) | A User Theorem |
| refine-rename-overwrite-reparent | old_parent_inode.ino ≠ new_parent_inode.ino, valid-dentry(new_parent_inode.ino, new_dent, dirs, files), pre-rename(old_inode, old_dent, old_dent_inode, new_inode, new_dent, new_dent_inode, dirs, files), dirs = abs-dirs(fs, ri), files = abs-files(fs, ri), orphans(dirs, files) = abs-keys(ro), boolvar → boolvar0, afs-cons(dirs, files), ubifs-cons(fs, ri, ro, fi, fo, log), orphans-cons(fs, ri, ro), replay-cons-strong(fs, ri, ro, fi, fo, log), file-node-cons(fs, ri), ri-inj(ri), ri-inj(fi), log-cons(log, fs), ro.inodes?, fo.inodes?, old_parent_inode = old_inode, new_parent_inode = new_inode, old_child_inode = old_dent_inode, new_child_inode = new_dent_inode, old_dent = old_dent0, new_dent = old_dent1, err = err0 ⊦ ⟪aubifs_rename_overwrite_reparent# (old_child_inode.directory, old_child_inode, fi, fo ; old_parent_inode, new_parent_inode, new_child_inode, old_dent, new_dent, err, ri, ro, fs, log, boolvar0)⟫ ⟨afs_rename#(; old_inode, new_inode, old_dent_inode, new_dent_inode, old_dent0, old_dent1, err0, dirs, files; boolvar)⟩ ( (dirs = abs-dirs(fs, ri) ∧ files = abs-files(fs, ri) ∧ orphans(dirs, files) = abs-keys(ro) ∧ (boolvar → boolvar0)) ∧ old_parent_inode = old_inode ∧ new_parent_inode = new_inode ∧ old_child_inode = old_dent_inode ∧ new_child_inode = new_dent_inode ∧ old_dent = old_dent0 ∧ new_dent = old_dent1 ∧ err = err0) | A User Theorem |
| refine-rename-overwrite-reparent-dir | old_parent_inode.ino ≠ new_parent_inode.ino, new_dent_inode.directory, valid-dentry(new_parent_inode.ino, new_dent, dirs, files), pre-rename(old_inode, old_dent, old_dent_inode, new_inode, new_dent, new_dent_inode, dirs, files), dirs = abs-dirs(fs, ri), files = abs-files(fs, ri), orphans(dirs, files) = abs-keys(ro), boolvar → boolvar0, afs-cons(dirs, files), ubifs-cons(fs, ri, ro, fi, fo, log), orphans-cons(fs, ri, ro), replay-cons-strong(fs, ri, ro, fi, fo, log), file-node-cons(fs, ri), ri-inj(ri), ri-inj(fi), log-cons(log, fs), ro.inodes?, fo.inodes?, old_parent_inode = old_inode, new_parent_inode = new_inode, old_child_inode = old_dent_inode, new_child_inode = new_dent_inode, old_dent = old_dent0, new_dent = old_dent1, err = err0 ⊦ ⟪aubifs_rename_overwrite_reparent# (old_child_inode.directory, old_child_inode, fi, fo ; old_parent_inode, new_parent_inode, new_child_inode, old_dent, new_dent, err, ri, ro, fs, log, boolvar0)⟫ ⟨afs_rename#(; old_inode, new_inode, old_dent_inode, new_dent_inode, old_dent0, old_dent1, err0, dirs, files; boolvar)⟩ ( (dirs = abs-dirs(fs, ri) ∧ files = abs-files(fs, ri) ∧ orphans(dirs, files) = abs-keys(ro) ∧ (boolvar → boolvar0)) ∧ old_parent_inode = old_inode ∧ new_parent_inode = new_inode ∧ old_child_inode = old_dent_inode ∧ new_child_inode = new_dent_inode ∧ old_dent = old_dent0 ∧ new_dent = old_dent1 ∧ err = err0) | A User Theorem |
| refine-rename-overwrite-reparent-file | old_parent_inode.ino ≠ new_parent_inode.ino, ¬ new_dent_inode.directory, valid-dentry(new_parent_inode.ino, new_dent, dirs, files), pre-rename(old_inode, old_dent, old_dent_inode, new_inode, new_dent, new_dent_inode, dirs, files), dirs = abs-dirs(fs, ri), files = abs-files(fs, ri), orphans(dirs, files) = abs-keys(ro), boolvar → boolvar0, afs-cons(dirs, files), ubifs-cons(fs, ri, ro, fi, fo, log), orphans-cons(fs, ri, ro), replay-cons-strong(fs, ri, ro, fi, fo, log), file-node-cons(fs, ri), ri-inj(ri), ri-inj(fi), log-cons(log, fs), ro.inodes?, fo.inodes?, old_parent_inode = old_inode, new_parent_inode = new_inode, old_child_inode = old_dent_inode, new_child_inode = new_dent_inode, old_dent = old_dent0, new_dent = old_dent1, err = err0 ⊦ ⟪aubifs_rename_overwrite_reparent# (old_child_inode.directory, old_child_inode, fi, fo ; old_parent_inode, new_parent_inode, new_child_inode, old_dent, new_dent, err, ri, ro, fs, log, boolvar0)⟫ ⟨afs_rename#(; old_inode, new_inode, old_dent_inode, new_dent_inode, old_dent0, old_dent1, err0, dirs, files; boolvar)⟩ ( (dirs = abs-dirs(fs, ri) ∧ files = abs-files(fs, ri) ∧ orphans(dirs, files) = abs-keys(ro) ∧ (boolvar → boolvar0)) ∧ old_parent_inode = old_inode ∧ new_parent_inode = new_inode ∧ old_child_inode = old_dent_inode ∧ new_child_inode = new_dent_inode ∧ old_dent = old_dent0 ∧ new_dent = old_dent1 ∧ err = err0) | A User Theorem |
| rename-precond-abs | ⊦ dirs = abs-dirs(fs, ri) ∧ files = abs-files(fs, ri) ∧ orphans(dirs, files) = abs-keys(ro) ∧ afs-cons(dirs, files) ∧ ro.inodes? ∧ file-node-cons(fs, ri) ∧ log-cons(log, fs) ∧ replay-cons-strong(fs, ri, ro, fi, fo, log) ∧ ri-inj(ri) ∧ ri-inj(fi) ∧ ubifs-cons(fs, ri, ro, fi, fo, log) ∧ pre-rename(old_parent_inode, old_dent, old_child_inode, new_parent_inode, new_dent, new_child_inode, dirs, files) → pre-rename(old_parent_inode, old_dent, old_child_inode, new_parent_inode, new_dent, new_child_inode, fs, ri, ro) | A User Theorem |
| ubifs-cons-pagesize | key.data? ⊦ key ∈ ri ∧ ubifs-cons(fs, ri, ro, fi, fo, log) → # fs[ri[key]].data = VFS_PAGE_SIZE | A User Theorem |
| valid-parent-ino-precond | ⊦ afs-cons(abs-dirs(fs, ri), abs-files(fs, ri)) ∧ fs[ri[inodekey(m)]].directory ∧ inodekey(m) ∈ ri ∧ fo.inodes? ∧ ro.inodes? ∧ log-cons(log, fs) ∧ ri-inj(fi) ∧ ri-inj(ri) ∧ replay-cons-strong(fs, ri, ro, fi, fo, log) ∧ ubifs-cons(fs, ri, ro, fi, fo, log) ∧ abs-keys(ro) = abs-keys(orphans(fs, ri)) ∧ (links(m, abs-dirs(fs, ri)) ≠ ∅ ∨ m = ROOT_INO) → valid-parent-ino(m, fs, ri, ro) | A User Theorem |