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: |
|---|---|---|
| create | afs_create#(MD; P_INODE, C_INODE, DENT, ERR, DIRS, FILES; ASYNCED) {if pre-create(P_INODE, DENT, MD, DIRS, FILES) then { {choose INO with ¬ INO ∈ DIRS ∧ ¬ INO ∈ FILES ∧ INO ≠ 0 in afs_create_ino#(P_INODE.ino, MD, INO; DENT, ERR, DIRS, FILES); afs_inode_sync#(P_INODE; DIRS, FILES); P_INODE := getinode(P_INODE.ino, DIRS, FILES); C_INODE := getinode(DENT.ino, DIRS, FILES)} or fail#(; ; ERR); ASYNCED := ?} else abort } | An Axiom |
| truncate | afs_truncate#(N, PAGENO; PBUF-OPT, INODE, MODIFIED, ERR, DIRS, FILES, ASYNCED) {if pre-truncate(INODE, N, PAGENO, PBUF-OPT, DIRS, FILES) then let OFFSET = 0, SIZE = 0 in afs_truncate_internal#(N, PAGENO; INODE, PBUF-OPT, OFFSET, SIZE, MODIFIED, ERR, DIRS, FILES; ASYNCED) else abort } | An Axiom |
| writepage | afs_writepage#(INODE, PAGENO, PBUF, DIRS; ERR, FILES; ASYNCED) {if pre-writepage(INODE, PAGENO, PBUF, DIRS, FILES) then {{FILES[INODE.ino].content[PAGENO] := PBUF; ERR := ESUCCESS} or fail#(; ; ERR); ASYNCED := ?} else abort } | An Axiom |
| readpage | afs_readpage#(INODE, PAGENO, DIRS, FILES, ASYNCED; PBUF, ERR) {if pre-readpage(INODE, PAGENO, PBUF, DIRS, FILES) then { {if PAGENO ∈ FILES[INODE.ino].content then PBUF := FILES[INODE.ino].content[PAGENO] else PBUF := zeropage; ERR := ESUCCESS} or fail#(; ; ERR)} else abort } | An Axiom |
| renam | afs_rename#(; OLD_PARENT_INODE, NEW_PARENT_INODE, OLD_CHILD_INODE, NEW_CHILD_INODE, OLD_DENT, NEW_DENT, ERR, DIRS, FILES; ASYNCED) {if pre-rename(OLD_PARENT_INODE, OLD_DENT, OLD_CHILD_INODE, NEW_PARENT_INODE, NEW_DENT, NEW_CHILD_INODE, DIRS, FILES) then { let OLD_INO = OLD_PARENT_INODE.ino, NEW_INO = NEW_PARENT_INODE.ino, OVERWRITE = NEW_DENT.dentry? in let IDENTITY = OLD_INO = NEW_INO ∧ NEW_DENT = OLD_DENT in {DIRS[OLD_INO].entries := DIRS[OLD_INO].entries -- OLD_DENT.name; if ¬ IDENTITY then {DIRS[OLD_INO].size := DIRS[OLD_INO].size - 1; if OLD_DENT.ino ∈ DIRS then DIRS[OLD_INO].nsubdirs := DIRS[OLD_INO].nsubdirs - 1}; DIRS[NEW_INO].entries[NEW_DENT.name] := OLD_DENT.ino; if OVERWRITE ∧ ¬ IDENTITY then let INO = NEW_DENT.ino in afs_drop_nlink#(INO; DIRS, FILES); if ¬ OVERWRITE then {DIRS[NEW_INO].size := DIRS[NEW_INO].size + 1; if OLD_DENT.ino ∈ DIRS then DIRS[NEW_INO].nsubdirs := DIRS[NEW_INO].nsubdirs + 1}; NEW_DENT := mkdentry(NEW_DENT.name, OLD_DENT.ino); OLD_DENT := negdentry(OLD_DENT.name); afs_inode_sync#(OLD_PARENT_INODE; DIRS, FILES); afs_inode_sync#(NEW_PARENT_INODE; DIRS, FILES); if OVERWRITE then {afs_inode_sync#(NEW_CHILD_INODE; DIRS, FILES); NEW_CHILD_INODE := getinode(NEW_CHILD_INODE.ino, DIRS, FILES)}; OLD_PARENT_INODE := getinode(OLD_PARENT_INODE.ino, DIRS, FILES); NEW_PARENT_INODE := getinode(NEW_PARENT_INODE.ino, DIRS, FILES); ERR := ESUCCESS} or fail#(; ; ERR); ASYNCED := ?} else abort } | An Axiom |
| link | afs_link#(OLD_DENT; P_INODE, C_INODE, NEW_DENT, ERR, DIRS, FILES; ASYNCED) {if pre-link(P_INODE, C_INODE, OLD_DENT, NEW_DENT, DIRS, FILES) then { let P_INO = P_INODE.ino in {DIRS[P_INO].entries[NEW_DENT.name] := OLD_DENT.ino; DIRS[P_INO].size := DIRS[P_INO].size + 1; let INO = OLD_DENT.ino in afs_inc_nlink#(INO; DIRS, FILES); NEW_DENT := mkdentry(NEW_DENT.name, OLD_DENT.ino); afs_inode_sync#(P_INODE; DIRS, FILES); afs_inode_sync#(C_INODE; DIRS, FILES); P_INODE := getinode(P_INODE.ino, DIRS, FILES); C_INODE := getinode(OLD_DENT.ino, DIRS, FILES); ERR := ESUCCESS} or fail#(; ; ERR); ASYNCED := ?} else abort } | An Axiom |
| rmdir | afs_rmdir#(; P_INODE, C_INODE, DENT, ERR, DIRS, FILES; ASYNCED) {if pre-rmdir(P_INODE, C_INODE, DENT, DIRS, FILES) then { let P_INO = P_INODE.ino in {DIRS[P_INO].entries := DIRS[P_INO].entries -- DENT.name; DIRS[P_INO].size := DIRS[P_INO].size - 1; DIRS[P_INO].nsubdirs := DIRS[P_INO].nsubdirs - 1; let INO = DENT.ino in afs_drop_nlink#(INO; DIRS, FILES); DENT := negdentry(DENT.name); afs_inode_sync#(P_INODE; DIRS, FILES); afs_inode_sync#(C_INODE; DIRS, FILES); P_INODE := getinode(P_INODE.ino, DIRS, FILES); C_INODE := getinode(C_INODE.ino, DIRS, FILES); ERR := ESUCCESS} or fail#(; ; ERR); ASYNCED := ?} else abort } | An Axiom |
| mkdir | afs_mkdir#(MD; P_INODE, C_INODE, DENT, ERR, DIRS, FILES; ASYNCED) {if pre-mkdir(P_INODE, DENT, MD, DIRS, FILES) then { {choose INO with ¬ INO ∈ DIRS ∧ ¬ INO ∈ FILES ∧ INO ≠ 0 in afs_mkdir_ino#(P_INODE.ino, MD, INO; DENT, ERR, DIRS); afs_inode_sync#(P_INODE; DIRS, FILES); P_INODE := getinode(P_INODE.ino, DIRS, FILES); C_INODE := getinode(DENT.ino, DIRS, FILES)} or fail#(; ; ERR); ASYNCED := ?} else abort } | An Axiom |
| unlink | afs_unlink#(; P_INODE, C_INODE, DENT, ERR, DIRS, FILES; ASYNCED) {if pre-unlink(P_INODE, C_INODE, DENT, DIRS, FILES) then { let P_INO = P_INODE.ino in {DIRS[P_INO].entries := DIRS[P_INO].entries -- DENT.name; DIRS[P_INO].size := DIRS[P_INO].size - 1; let INO = DENT.ino in afs_drop_nlink#(INO; DIRS, FILES); DENT := negdentry(DENT.name); afs_inode_sync#(P_INODE; DIRS, FILES); afs_inode_sync#(C_INODE; DIRS, FILES); P_INODE := getinode(P_INODE.ino, DIRS, FILES); C_INODE := getinode(C_INODE.ino, DIRS, FILES); ERR := ESUCCESS} or fail#(; ; ERR); ASYNCED := ?} else abort } | An Axiom |
| lookup | afs_lookup#(P_INO, DIRS, FILES, ASYNCED; DENT, ERR) {if pre-lookup(P_INO, DENT, DIRS, FILES) then { if DENT.name ∈ DIRS[P_INO].entries then {DENT := mkdentry(DENT.name, DIRS[P_INO].entries[DENT.name]); ERR := ESUCCESS} else {DENT := negdentry(DENT.name); ERR := ENOENT} or fail#(; ; ERR)} else abort } | An Axiom |
| iget | afs_iget#(INO, DIRS, FILES, ASYNCED; INODE, ERR) {if pre-iget(INO, DIRS, FILES) then {{INODE := getinode(INO, DIRS, FILES); ERR := ESUCCESS} or fail#(; ; ERR)} else abort} | An Axiom |
| evict | afs_evict#(INODE, ASYNCED; ERR, DIRS, FILES) {if pre-evict(INODE, DIRS, FILES) then {ERR := ESUCCESS; let INO = INODE.ino in if INO ∈ DIRS then if DIRS[INO].nlink = 0 then DIRS := DIRS -- INO else if FILES[INO].nlink = 0 then FILES := FILES -- INO} else abort } | An Axiom |
| write_inode | afs_write_inode#(INODE; ERR, DIRS, FILES; ASYNCED) {if pre-write-inode(INODE, DIRS, FILES) then { {if INODE.directory then DIRS[INODE.ino].meta := INODE.meta else {FILES[INODE.ino].meta := INODE.meta; FILES[INODE.ino].size := INODE.size}; ERR := ESUCCESS} or fail#(; ; ERR); ASYNCED := ?} else abort } | An Axiom |
| readdir | afs_readdir#(INODE, DIRS, FILES, ASYNCED; NAMES, ERR) {if pre-readdir(INODE.ino, DIRS, FILES) then {{NAMES := dom DIRS[INODE.ino].entries; ERR := ESUCCESS} or {choose NAMES0 with true in NAMES := NAMES0; fail#(; ; ERR)}} else abort } | An Axiom |
| inc-nlink | afs_inc_nlink#(INO; DIRS, FILES) {if INO ∈ DIRS then DIRS[INO].nlink := DIRS[INO].nlink + 1; if INO ∈ FILES then FILES[INO].nlink := FILES[INO].nlink + 1} | An Axiom |
| drop-nlink | afs_drop_nlink#(INO; DIRS, FILES) {if INO ∈ DIRS then DIRS[INO].nlink := DIRS[INO].nlink - 1; if INO ∈ FILES then FILES[INO].nlink := FILES[INO].nlink - 1} | An Axiom |
| mkdir-ino | afs_mkdir_ino#(P_INO, MD, INO; DENT, ERR, DIRS) {DIRS[P_INO].entries[DENT.name] := INO; DIRS[P_INO].size := DIRS[P_INO].size + 1; DIRS[P_INO].nsubdirs := DIRS[P_INO].nsubdirs + 1; DIRS := DIRS ++ INO; DIRS[INO] := mkdir(0, MD, 1, 0, ∅); DENT := mkdentry(DENT.name, INO); ERR := ESUCCESS } | An Axiom |
| create-ino | afs_create_ino#(P_INO, MD, INO; DENT, ERR, DIRS, FILES) {DIRS[P_INO].entries[DENT.name] := INO; DIRS[P_INO].size := DIRS[P_INO].size + 1; FILES := FILES ++ INO; FILES[INO] := mkfile(0, MD, 1, ∅); DENT := mkdentry(DENT.name, INO); ERR := ESUCCESS } | An Axiom |
| truncate-internal | afs_truncate_internal#(N, PAGENO; INODE, PBUF-OPT, OFFSET, SIZE, MODIFIED, ERR, DIRS, FILES; ASYNCED) { let INO = INODE.ino, CONTENT = FILES[INODE.ino].content, PBUF = ? in {OFFSET := INODE.size % VFS_PAGE_SIZE, SIZE := min(N, INODE.size); MODIFIED := INODE.size ≤ N ∧ OFFSET ≠ 0 ∧ (PAGENO ∈ CONTENT ∨ PBUF-OPT.some?); if MODIFIED then {if PBUF-OPT.some? then PBUF := PBUF-OPT.buf else PBUF := FILES[INO].content[PAGENO]; PBUF := fill(PBUF, zero, OFFSET, VFS_PAGE_SIZE - OFFSET); CONTENT[PAGENO] := PBUF; PBUF-OPT := some(PBUF)}; FILES[INO].content := CONTENT upto SIZE; let NEW_INODE = INODE in {NEW_INODE.size := N; afs_inode_sync#(NEW_INODE; DIRS, FILES)}; INODE := getinode(INODE.ino, DIRS, FILES); ERR := ESUCCESS} or fail#(; ; ERR); ASYNCED := ? } | An Axiom |
| format | afs_format#(N, DOSYNC, SIZE, MD; DIRS; FILES, ASYNCED, ERR) {if SIZE = LEB_SIZE then { {DIRS := ∅, FILES := ∅; DIRS := DIRS ++ ROOT_INO; DIRS[ROOT_INO] := mkdir(0, MD, 0, 0, ∅); ASYNCED := true; ERR := ESUCCESS} or {DIRS := ?, FILES := ?, ASYNCED := ?; fail#(; ; ERR)}} else abort } | An Axiom |
| check-commit | afs_check_commit#(DIRS, FILES; ERR; ASYNCED){fail_or_success#(; ; ERR); choose bv with true in ASYNCED := bv} | An Axiom |
| recovery | afs_recovery#(DOSYNC; DIRS, FILES; ASYNCED, ERR){ASYNCED := true, ERR := ESUCCESS or {DIRS := ?, FILES := ?, ASYNCED := ?; fail#(; ; ERR)}} | An Axiom |
| sync | afs_sync#(DIRS, FILES; ; ASYNCED, ERR){fail_or_success#(; ; ERR); ASYNCED := ERR = ESUCCESS} | An Axiom |
| fsync | afs_fsync#(INODE, ISDATASYNC, DIRS, FILES; ; ASYNCED, ERR) {if valid-file-inode(INODE, DIRS, FILES) then {fail_or_success#(; ; ERR); choose bv with true in ASYNCED := bv} else abort} | An Axiom |
| fsyncdir | afs_fsyncdir#(INODE, ISDATASYNC, DIRS, FILES, ASYNCED; ; ERR){fail_or_success#(; ; ERR)} | An Axiom |
| internal-inode-sync | afs_inode_sync#(INODE; DIRS, FILES) {let INO = INODE.ino in if INO ∈ FILES then {FILES[INO].size := INODE.size; FILES[INO].meta := INODE.meta} else if INO ∈ DIRS then DIRS[INO].meta := INODE.meta } | An Axiom |
| inv-format | old_ino = LEB_SIZE ⊦ ⟪afs_format#(n, asynced, old_ino, md; dirs; files, asynced0, err)⟫ (err = ESUCCESS → asynced0 ∧ afs-cons(dirs, files)) | A Proof Obligation |
| inv-write_inode | afs-cons(dirs, files), pre-write-inode(inode, dirs, files) ⊦ ⟪afs_write_inode#(inode; err, dirs, files; asynced)⟫ afs-cons(dirs, files) | A Proof Obligation |
| inv-iget | afs-cons(dirs, files), pre-iget(ino, dirs, files) ⊦ ⟪afs_iget#(ino, dirs, files, asynced; inode, err)⟫ true | A Proof Obligation |
| inv-truncate | afs-cons(dirs, files), pre-truncate(inode, n, pageno, buf-opt, dirs, files) ⊦ ⟪afs_truncate#(n, pageno; buf-opt, inode, asynced, err, dirs, files, asynced0)⟫ afs-cons(dirs, files) | A Proof Obligation |
| inv-evict | afs-cons(dirs, files), pre-evict(inode, dirs, files) ⊦ ⟪afs_evict#(inode, asynced; err, dirs, files)⟫ afs-cons(dirs, files) | A Proof Obligation |
| inv-readdir | afs-cons(dirs, files), pre-readdir(inode.ino, dirs, files) ⊦ ⟪afs_readdir#(inode, dirs, files, asynced; strings, err)⟫ true | A Proof Obligation |
| inv-writepage | afs-cons(dirs, files), pre-writepage(inode, pageno, buf, dirs, files) ⊦ ⟪afs_writepage#(inode, pageno, buf, dirs; err, files; asynced)⟫ afs-cons(dirs, files) | A Proof Obligation |
| inv-readpage | afs-cons(dirs, files), pre-readpage(inode, pageno, buf, dirs, files) ⊦ ⟪afs_readpage#(inode, pageno, dirs, files, asynced; buf, err)⟫ true | A Proof Obligation |
| inv-renam | afs-cons(dirs, files), pre-rename(old_parent_inode, old_dent, old_child_inode, new_parent_inode, new_dent, new_child_inode, dirs, files) ⊦ ⟪afs_rename#(; old_parent_inode, new_parent_inode, old_child_inode, new_child_inode, old_dent, new_dent, err, dirs, files; asynced)⟫ afs-cons(dirs, files) | A Proof Obligation |
| inv-link | afs-cons(dirs, files), pre-link(p_inode, c_inode, old_dent, new_dent, dirs, files) ⊦ ⟪afs_link#(old_dent; p_inode, c_inode, new_dent, err, dirs, files; asynced)⟫ afs-cons(dirs, files) | A Proof Obligation |
| inv-rmdir | afs-cons(dirs, files), pre-rmdir(p_inode, c_inode, dent, dirs, files) ⊦ ⟪afs_rmdir#(; p_inode, c_inode, dent, err, dirs, files; asynced)⟫ afs-cons(dirs, files) | A Proof Obligation |
| inv-mkdir | afs-cons(dirs, files), pre-mkdir(p_inode, dent, md, dirs, files) ⊦ ⟪afs_mkdir#(md; p_inode, c_inode, dent, err, dirs, files; asynced)⟫ afs-cons(dirs, files) | A Proof Obligation |
| inv-unlink | afs-cons(dirs, files), pre-unlink(p_inode, c_inode, dent, dirs, files) ⊦ ⟪afs_unlink#(; p_inode, c_inode, dent, err, dirs, files; asynced)⟫ afs-cons(dirs, files) | A Proof Obligation |
| inv-create | afs-cons(dirs, files), pre-create(p_inode, dent, md, dirs, files) ⊦ ⟪afs_create#(md; p_inode, c_inode, dent, err, dirs, files; asynced)⟫ afs-cons(dirs, files) | A Proof Obligation |
| inv-lookup | afs-cons(dirs, files), pre-lookup(p_ino, dent, dirs, files) ⊦ ⟪afs_lookup#(p_ino, dirs, files, asynced; dent, err)⟫ true | A Proof Obligation |
| inv-check-commit | afs-cons(dirs, files) ⊦ ⟪afs_check_commit#(dirs, files; err; asynced)⟫ true | A Proof Obligation |
| crash-neutral-write_inode | pre-write-inode(inode, dirs, files), afs-cons(dirs, files), asynced, dirs0 = dirs \ orphans(dirs, files), files0 = files \ orphans(dirs, files) ⊦ ⟨afs_write_inode#(inode; err, dirs, files; asynced)⟩ (asynced ∧ dirs0 = dirs \ orphans(dirs, files) ∧ files0 = files \ orphans(dirs, files)) | A Proof Obligation |
| crash-neutral-iget | pre-iget(ino, dirs, files), afs-cons(dirs, files), asynced, dirs0 = dirs \ orphans(dirs, files), files0 = files \ orphans(dirs, files) ⊦ ⟨afs_iget#(ino, dirs, files, asynced; inode, err)⟩ (asynced ∧ dirs0 = dirs \ orphans(dirs, files) ∧ files0 = files \ orphans(dirs, files)) | A Proof Obligation |
| crash-neutral-truncate | pre-truncate(inode, n, pageno, buf-opt, dirs, files), afs-cons(dirs, files), asynced, dirs0 = dirs \ orphans(dirs, files), files0 = files \ orphans(dirs, files) ⊦ ⟨afs_truncate#(n, pageno; buf-opt, inode, asynced0, err, dirs, files, asynced)⟩ (asynced ∧ dirs0 = dirs \ orphans(dirs, files) ∧ files0 = files \ orphans(dirs, files)) | A Proof Obligation |
| crash-neutral-evict | pre-evict(inode, dirs, files), afs-cons(dirs, files), asynced, dirs0 = dirs \ orphans(dirs, files), files0 = files \ orphans(dirs, files) ⊦ ⟨afs_evict#(inode, asynced; err, dirs, files)⟩ (asynced ∧ dirs0 = dirs \ orphans(dirs, files) ∧ files0 = files \ orphans(dirs, files)) | A Proof Obligation |
| crash-neutral-readdir | pre-readdir(inode.ino, dirs, files), afs-cons(dirs, files), asynced, dirs0 = dirs \ orphans(dirs, files), files0 = files \ orphans(dirs, files) ⊦ ⟨afs_readdir#(inode, dirs, files, asynced; strings, err)⟩ (asynced ∧ dirs0 = dirs \ orphans(dirs, files) ∧ files0 = files \ orphans(dirs, files)) | A Proof Obligation |
| crash-neutral-writepage | pre-writepage(inode, pageno, buf, dirs, files), afs-cons(dirs, files), asynced, dirs0 = dirs \ orphans(dirs, files), files0 = files \ orphans(dirs, files) ⊦ ⟨afs_writepage#(inode, pageno, buf, dirs; err, files; asynced)⟩ (asynced ∧ dirs0 = dirs \ orphans(dirs, files) ∧ files0 = files \ orphans(dirs, files)) | A Proof Obligation |
| crash-neutral-readpage | pre-readpage(inode, pageno, buf, dirs, files), afs-cons(dirs, files), asynced, dirs0 = dirs \ orphans(dirs, files), files0 = files \ orphans(dirs, files) ⊦ ⟨afs_readpage#(inode, pageno, dirs, files, asynced; buf, err)⟩ (asynced ∧ dirs0 = dirs \ orphans(dirs, files) ∧ files0 = files \ orphans(dirs, files)) | A Proof Obligation |
| crash-neutral-renam | pre-rename(old_parent_inode, old_dent, old_child_inode, new_parent_inode, new_dent, new_child_inode, dirs, files), afs-cons(dirs, files), asynced, dirs0 = dirs \ orphans(dirs, files), files0 = files \ orphans(dirs, files) ⊦ ⟨afs_rename#(; old_parent_inode, new_parent_inode, old_child_inode, new_child_inode, old_dent, new_dent, err, dirs, files; asynced)⟩ (asynced ∧ dirs0 = dirs \ orphans(dirs, files) ∧ files0 = files \ orphans(dirs, files)) | A Proof Obligation |
| crash-neutral-link | pre-link(p_inode, c_inode, old_dent, new_dent, dirs, files), afs-cons(dirs, files), asynced, dirs0 = dirs \ orphans(dirs, files), files0 = files \ orphans(dirs, files) ⊦ ⟨afs_link#(old_dent; p_inode, c_inode, new_dent, err, dirs, files; asynced)⟩ (asynced ∧ dirs0 = dirs \ orphans(dirs, files) ∧ files0 = files \ orphans(dirs, files)) | A Proof Obligation |
| crash-neutral-rmdir | pre-rmdir(p_inode, c_inode, dent, dirs, files), afs-cons(dirs, files), asynced, dirs0 = dirs \ orphans(dirs, files), files0 = files \ orphans(dirs, files) ⊦ ⟨afs_rmdir#(; p_inode, c_inode, dent, err, dirs, files; asynced)⟩ (asynced ∧ dirs0 = dirs \ orphans(dirs, files) ∧ files0 = files \ orphans(dirs, files)) | A Proof Obligation |
| crash-neutral-mkdir | pre-mkdir(p_inode, dent, md, dirs, files), afs-cons(dirs, files), asynced, dirs0 = dirs \ orphans(dirs, files), files0 = files \ orphans(dirs, files) ⊦ ⟨afs_mkdir#(md; p_inode, c_inode, dent, err, dirs, files; asynced)⟩ (asynced ∧ dirs0 = dirs \ orphans(dirs, files) ∧ files0 = files \ orphans(dirs, files)) | A Proof Obligation |
| crash-neutral-unlink | pre-unlink(p_inode, c_inode, dent, dirs, files), afs-cons(dirs, files), asynced, dirs0 = dirs \ orphans(dirs, files), files0 = files \ orphans(dirs, files) ⊦ ⟨afs_unlink#(; p_inode, c_inode, dent, err, dirs, files; asynced)⟩ (asynced ∧ dirs0 = dirs \ orphans(dirs, files) ∧ files0 = files \ orphans(dirs, files)) | A Proof Obligation |
| crash-neutral-create | pre-create(p_inode, dent, md, dirs, files), afs-cons(dirs, files), asynced, dirs0 = dirs \ orphans(dirs, files), files0 = files \ orphans(dirs, files) ⊦ ⟨afs_create#(md; p_inode, c_inode, dent, err, dirs, files; asynced)⟩ (asynced ∧ dirs0 = dirs \ orphans(dirs, files) ∧ files0 = files \ orphans(dirs, files)) | A Proof Obligation |
| crash-neutral-lookup | pre-lookup(p_ino, dent, dirs, files), afs-cons(dirs, files), asynced, dirs0 = dirs \ orphans(dirs, files), files0 = files \ orphans(dirs, files) ⊦ ⟨afs_lookup#(p_ino, dirs, files, asynced; dent, err)⟩ (asynced ∧ dirs0 = dirs \ orphans(dirs, files) ∧ files0 = files \ orphans(dirs, files)) | A Proof Obligation |
| crash-neutral-check-commit | afs-cons(dirs, files), asynced, dirs0 = dirs \ orphans(dirs, files), files0 = files \ orphans(dirs, files) ⊦ ⟨afs_check_commit#(dirs, files; err; asynced)⟩ (asynced ∧ dirs0 = dirs \ orphans(dirs, files) ∧ files0 = files \ orphans(dirs, files)) | A Proof Obligation |
| inv-recovery | dirs = dirs0 \ orphans(dirs0, files), files0 = files \ orphans(dirs0, files), asynced, afs-cons(dirs0, files) ⊦ ⟪afs_recovery#(asynced0; dirs, files0; asynced1, err)⟫ (err = ESUCCESS → asynced1 ∧ afs-cons(dirs, files0)) | A Proof Obligation |
| crash-neutral-sync | afs-cons(dirs, files), asynced, dirs0 = dirs \ orphans(dirs, files), files0 = files \ orphans(dirs, files) ⊦ ⟨afs_sync#(dirs, files; ; asynced, err)⟩ (asynced ∧ dirs0 = dirs \ orphans(dirs, files) ∧ files0 = files \ orphans(dirs, files)) | A Proof Obligation |
| inv-sync | afs-cons(dirs, files) ⊦ ⟪afs_sync#(dirs, files; ; asynced, err)⟫ true | A Proof Obligation |
| crash-neutral-recovery | afs-cons(dirs, files), asynced, dirs0 = dirs \ orphans(dirs, files), files0 = files \ orphans(dirs, files) ⊦ ⟨afs_recovery#(asynced0; dirs, files; asynced, err)⟩ (asynced ∧ dirs0 = dirs \ orphans(dirs, files) ∧ files0 = files \ orphans(dirs, files)) | A Proof Obligation |
| crash-neutral-fsync | valid-file-inode(inode, dirs, files), afs-cons(dirs, files), asynced, dirs0 = dirs \ orphans(dirs, files), files0 = files \ orphans(dirs, files) ⊦ ⟨afs_fsync#(inode, asynced0, dirs, files; ; asynced, err)⟩ (asynced ∧ dirs0 = dirs \ orphans(dirs, files) ∧ files0 = files \ orphans(dirs, files)) | A Proof Obligation |
| inv-fsync | afs-cons(dirs, files), valid-file-inode(inode, dirs, files) ⊦ ⟪afs_fsync#(inode, asynced, dirs, files; ; asynced0, err)⟫ true | A Proof Obligation |
| crash-neutral-fsyncdir | afs-cons(dirs, files), asynced, dirs0 = dirs \ orphans(dirs, files), files0 = files \ orphans(dirs, files) ⊦ ⟨afs_fsyncdir#(inode, asynced0, dirs, files, asynced; ; err)⟩ (asynced ∧ dirs0 = dirs \ orphans(dirs, files) ∧ files0 = files \ orphans(dirs, files)) | A Proof Obligation |
| inv-fsyncdir | afs-cons(dirs, files) ⊦ ⟪afs_fsyncdir#(inode, asynced, dirs, files, asynced0; ; err)⟫ true | A Proof Obligation |
| Del-at-entries | ⊦ (entries -- str0)[str] = (str ≠ str0 ⊃ entries[str];(∅)[str]) | A User Theorem |
| Del-size | ⊦ alink ∈ ls → #(ls -- alink) = # ls - 1 | A User Theorem |
| Insert-size | ⊦ ¬ alink ∈ ls → #(ls ++ alink) = # ls + 1 | A User Theorem |
| New-same | ⊦ p_ino ∈ dirs ∧ afs-cons(dirs, files) ∧ ino ≠ 0 ∧ ¬ ino ∈ files ∧ ¬ ino ∈ dirs → ¬ p_ino ∈ (files ++ ino)[ino, af] | A User Theorem |
| afs-cons-create-ino | afs-cons(dirs, files), pre-create(p_inode, dent, md, dirs, files), ¬ ino ∈ dirs, ¬ ino ∈ files, ino ≠ 0 ⊦ ⟪afs_create_ino#(p_inode.ino, md, ino; dent, err, dirs, files)⟫ afs-cons(dirs, files) | A User Theorem |
| afs-cons-inode-sync | afs-cons(dirs, files) ⊦ ⟪afs_inode_sync#(inode; dirs, files)⟫ afs-cons(dirs, files) | A User Theorem |
| afs-cons-mkdir-ino | afs-cons(dirs, files), pre-mkdir(p_inode, dent, md, dirs, files), ¬ ino ∈ dirs, ¬ ino ∈ files, ino ≠ 0 ⊦ ⟪afs_mkdir_ino#(p_inode.ino, md, ino; dent, err, dirs)⟫ afs-cons(dirs, files) | A User Theorem |
| afs-cons-reduce | ⊦ afs-cons(dirs0, files0) → ( afs-cons(dirs1, files1) ↔ (∀ ino, name, n. ROOT_INO ∈ dirs0 ∧ (ino ∈ dirs0 ∧ ino ≠ ROOT_INO ∧ links(ino, dirs0) = ∅ → dir-empty(ino, dirs0, files0)) ∧ ( ino ∈ dirs0 → ¬ ino ∈ files0 ∧ dirs0[ino].nlink = # links(ino, dirs0) ∧ dirs0[ino].nlink ≤ 1 ∧ dirs0[ino].size = # dirs0[ino].entries ∧ dirs0[ino].nsubdirs = # subdirs(ino, dirs0)) ∧ (ino ∈ files0 → ¬ ino ∈ dirs0 ∧ files0[ino].nlink = # links(ino, dirs0)) ∧ (ino ∈ dirs0 ∧ name ∈ dirs0[ino].entries → valid-ino(dirs0[ino].entries[name], dirs0, files0)) ∧ (ino ∈ files0 ∧ n ∈ files0[ino].content → valid-pagesize(ino, n, files0)) → ROOT_INO ∈ dirs1 ∧ (ino ∈ dirs1 ∧ ino ≠ ROOT_INO ∧ links(ino, dirs1) = ∅ → dir-empty(ino, dirs1, files1)) ∧ ( ino ∈ dirs1 → ¬ ino ∈ files1 ∧ dirs1[ino].nlink = # links(ino, dirs1) ∧ dirs1[ino].nlink ≤ 1 ∧ dirs1[ino].size = # dirs1[ino].entries ∧ dirs1[ino].nsubdirs = # subdirs(ino, dirs1)) ∧ (ino ∈ files1 → ¬ ino ∈ dirs1 ∧ files1[ino].nlink = # links(ino, dirs1)) ∧ (ino ∈ dirs1 ∧ name ∈ dirs1[ino].entries → valid-ino(dirs1[ino].entries[name], dirs1, files1)) ∧ (ino ∈ files1 ∧ n ∈ files1[ino].content → valid-pagesize(ino, n, files1)))) | A User Theorem |
| afs-cons-rename-dentry | afs-cons(dirs, files), valid-dentry(old_parent_inode.ino, old_dent, dirs, files), valid-dir-inode(old_parent_inode, dirs, files), valid-dir-inode(new_parent_inode, dirs, files), valid-wb-inode(old_child_inode, dirs, files), old_child_inode.ino = old_dent.ino, valid-dentry(new_parent_inode.ino, new_dent, dirs, files), valid-wb-inode(new_child_inode, dirs, files), new_child_inode.ino = new_dent.ino, new_parent_inode.ino = old_parent_inode.ino → new_parent_inode.meta = old_parent_inode.meta, valid-file-ino(new_dent.ino, dirs, files) ↔ valid-file-ino(old_dent.ino, dirs, files), valid-dir-ino(new_dent.ino, dirs, files) → new_dent.ino ≠ ROOT_INO ∧ dir-empty(new_dent.ino, dirs, files) ⊦ ⟪afs_rename#(; old_parent_inode, new_parent_inode, old_child_inode, new_child_inode, old_dent, new_dent, err, dirs, files; asynced)⟫ afs-cons(dirs, files) | A User Theorem |
| afs-cons-rename-dir-dentry | afs-cons(dirs, files), valid-dentry(old_parent_inode.ino, old_dent, dirs, files), valid-dentry(new_parent_inode.ino, new_dent, dirs, files), valid-dir-inode(old_parent_inode, dirs, files), valid-dir-inode(new_parent_inode, dirs, files), valid-dir-inode(old_child_inode, dirs, files), valid-dir-inode(new_child_inode, dirs, 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, dirs, files) ⊦ ⟪afs_rename#(; old_parent_inode, new_parent_inode, old_child_inode, new_child_inode, old_dent, new_dent, err, dirs, files; asynced)⟫ afs-cons(dirs, files) | A User Theorem |
| afs-cons-rename-dir-negdentry | afs-cons(dirs, files), valid-dentry(old_parent_inode.ino, old_dent, dirs, files), valid-dir-inode(old_parent_inode, dirs, files), valid-dir-inode(new_parent_inode, dirs, files), valid-dir-inode(old_child_inode, dirs, files), old_child_inode.ino = old_dent.ino, new_parent_inode.ino = old_parent_inode.ino → new_parent_inode.meta = old_parent_inode.meta, valid-negdentry(new_parent_inode.ino, new_dent, dirs, files) ⊦ ⟪afs_rename#(; old_parent_inode, new_parent_inode, old_child_inode, new_child_inode, old_dent, new_dent, err, dirs, files; asynced)⟫ afs-cons(dirs, files) | A User Theorem |
| afs-cons-rename-file-dentry | afs-cons(dirs, files), valid-dentry(old_parent_inode.ino, old_dent, dirs, files), valid-dir-inode(old_parent_inode, dirs, files), valid-dir-inode(new_parent_inode, dirs, files), valid-file-inode(old_child_inode, dirs, files), old_child_inode.ino = old_dent.ino, valid-dentry(new_parent_inode.ino, new_dent, dirs, files), valid-file-inode(new_child_inode, dirs, files), new_parent_inode.ino = old_parent_inode.ino → new_parent_inode.meta = old_parent_inode.meta, new_child_inode.ino = new_dent.ino ⊦ ⟪afs_rename#(; old_parent_inode, new_parent_inode, old_child_inode, new_child_inode, old_dent, new_dent, err, dirs, files; asynced)⟫ afs-cons(dirs, files) | A User Theorem |
| afs-cons-rename-file-negdentry | afs-cons(dirs, files), valid-dentry(old_parent_inode.ino, old_dent, dirs, files), valid-dir-inode(old_parent_inode, dirs, files), valid-dir-inode(new_parent_inode, dirs, files), valid-file-inode(old_child_inode, dirs, files), old_child_inode.ino = old_dent.ino, new_parent_inode.ino = old_parent_inode.ino → new_parent_inode.meta = old_parent_inode.meta, valid-negdentry(new_parent_inode.ino, new_dent, dirs, files) ⊦ ⟪afs_rename#(; old_parent_inode, new_parent_inode, old_child_inode, new_child_inode, old_dent, new_dent, err, dirs, files; asynced)⟫ afs-cons(dirs, files) | A User Theorem |
| afs-cons-rename-negdentry | afs-cons(dirs, files), valid-dentry(old_parent_inode.ino, old_dent, dirs, files), valid-dir-inode(old_parent_inode, dirs, files), valid-dir-inode(new_parent_inode, dirs, files), valid-wb-inode(old_child_inode, dirs, files), old_child_inode.ino = old_dent.ino, new_parent_inode.ino = old_parent_inode.ino → new_parent_inode.meta = old_parent_inode.meta, valid-negdentry(new_parent_inode.ino, new_dent, dirs, files) ⊦ ⟪afs_rename#(; old_parent_inode, new_parent_inode, old_child_inode, new_child_inode, old_dent, new_dent, err, dirs, files; asynced)⟫ afs-cons(dirs, files) | A User Theorem |
| inv-crash | dirs = dirs0 \ orphans(dirs0, files) ∧ files0 = files \ orphans(dirs0, files), afs-cons(dirs0, files) ⊦ ⟪skip⟫ ((true → afs-cons(dirs, files0)) ∧ true) | A User Theorem |
| lastlink-move | ⊦ # links(entries0[str0], dirs) = 1 ∧ ino0 ∈ dirs ∧ dirs[ino0] = mkdir(m0, md0, n0, n2, entries0) ∧ ino1 ∈ dirs ∧ dirs[ino1] = mkdir(m1, md1, n1, n3, entries1) ∧ str0 ∈ entries0 ∧ str1 ∈ entries1 → (entries0[str0] = entries1[str1] ↔ str0 = str1 ∧ ino0 = ino1) | A User Theorem |
| lastlink-rename | ⊦ # links(entries[str0], dirs) = 1 ∧ ino ∈ dirs ∧ dirs[ino] = mkdir(m, md, n, n0, entries) ∧ str0 ∈ entries ∧ str1 ∈ entries → (entries[str0] = entries[str1] ↔ str0 = str1) | A User Theorem |