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: |
|---|---|---|
| write-loop | vfs_write_loop#(START, INODE, END, BUF, DIRS; TOTAL, ERR, FILES, ASYNCED) {let DONE = false in while ERR = ESUCCESS ∧ ¬ DONE do vfs_write_block#(START, INODE, BUF, END, DIRS; TOTAL, DONE, ERR, FILES, ASYNCED)} | An Axiom |
| readdir | vfs_readdir#(PATH, USER, DIRS, FILES, ASYNCED; NAMES, ERR) {let INO = ROOT_INO, ISDIR = true, MODE = MODE_R in {vfs_walk#(PATH, USER, DIRS, FILES, ASYNCED; INO, ERR); if ERR = ESUCCESS then choose INODE with true in {vfs_may_open#(INO, ISDIR, MODE, USER, DIRS, FILES, ASYNCED; INODE, ERR); if ERR = ESUCCESS then afs_readdir#(INODE, DIRS, FILES, ASYNCED; NAMES, ERR)}} } | An Axiom |
| writemeta | vfs_writemeta#(PATH, MD, USER; ERR, DIRS, FILES, ASYNCED) {let INO = ROOT_INO in {vfs_walk#(PATH, USER, DIRS, FILES, ASYNCED; INO, ERR); if ERR = ESUCCESS then choose INODE with true in {afs_iget#(INO, DIRS, FILES, ASYNCED; INODE, ERR); if ERR = ESUCCESS then if pw(USER, INODE.meta) then {INODE.meta := MD; afs_check_commit#(DIRS, FILES; ERR; ASYNCED); if ERR = ESUCCESS then afs_write_inode#(INODE; ERR, DIRS, FILES; ASYNCED)} else ERR := EACCESS}} } | An Axiom |
| seek | vfs_seek#(FD, WHENCE, USER, DIRS, FILES, ASYNCED; N, ERR, OF) {ERR := ESUCCESS; if ¬ FD ∈ OF then ERR := EBADFD else {if WHENCE = SEEK_CUR then N := OF[FD].pos + N else if WHENCE = SEEK_END then choose INODE with true in {afs_iget#(OF[FD].ino, DIRS, FILES, ASYNCED; INODE, ERR); if ERR = ESUCCESS then N := INODE.size + N}; if ERR = ESUCCESS then OF[FD].pos := N} } | An Axiom |
| write | vfs_write#(FD, BUF, USER; N, ERR, OF, DIRS, FILES, ASYNCED) {if N ≤ # BUF then {ERR := ESUCCESS; if ¬ FD ∈ OF then ERR := EBADFD else if OF[FD].mode ≠ MODE_W ∧ OF[FD].mode ≠ MODE_RW then ERR := EBADFD else if N ≠ 0 then choose INODE, MODIFIED with true in {afs_iget#(OF[FD].ino, DIRS, FILES, ASYNCED; INODE, ERR); if ERR = ESUCCESS then if INODE.directory then ERR := EISDIR else let START = OF[FD].pos, END = OF[FD].pos + N, TOTAL = 0, PAGENO = 0, PBUF-OPT = none in {if ERR = ESUCCESS then PAGENO := INODE.size / VFS_PAGE_SIZE; if ERR = ESUCCESS then afs_truncate#(INODE.size, PAGENO; PBUF-OPT, INODE, MODIFIED, ERR, DIRS, FILES, ASYNCED); if ERR = ESUCCESS then vfs_write_loop#(START, INODE, END, BUF, DIRS; TOTAL, ERR, FILES, ASYNCED); if TOTAL ≠ 0 then ERR := ESUCCESS; if ERR = ESUCCESS then let SIZE = INODE.size in {N := TOTAL, END := START + TOTAL; if TOTAL ≠ 0 ∧ SIZE < END then {INODE.size := END; afs_check_commit#(DIRS, FILES; ERR; ASYNCED); if ERR = ESUCCESS then afs_write_inode#(INODE; ERR, DIRS, FILES; ASYNCED)}; if ERR ≠ ESUCCESS then N := (START ≤ SIZE ⊃ SIZE - START;0), ERR := ESUCCESS; OF[FD].pos := START + N}}}} else abort } | An Axiom |
| read | vfs_read#(FD, USER, DIRS, FILES, ASYNCED; BUF, N, ERR, OF) {if N ≤ # BUF then {ERR := ESUCCESS; if ¬ FD ∈ OF then ERR := EBADFD else if OF[FD].mode ≠ MODE_R ∧ OF[FD].mode ≠ MODE_RW then ERR := EBADFD else choose INODE with true in {afs_iget#(OF[FD].ino, DIRS, FILES, ASYNCED; INODE, ERR); if ERR = ESUCCESS then if INODE.directory then ERR := EISDIR else let START = OF[FD].pos, END = OF[FD].pos + N, TOTAL = 0 in if START ≤ INODE.size then {let DONE = false in vfs_read_loop#(START, END, INODE, DONE, DIRS, FILES, ASYNCED; BUF, TOTAL, ERR); if TOTAL ≠ 0 then ERR := ESUCCESS; OF[FD].pos := OF[FD].pos + TOTAL; N := TOTAL} else N := 0}} else abort } | An Axiom |
| close | vfs_close#(FD, USER, ASYNCED; ERR, OF, DIRS, FILES) {ERR := ESUCCESS; if ¬ FD ∈ OF then ERR := EBADFD else let DEL_INO = OF[FD].ino in choose DEL_INODE with true in {afs_iget#(DEL_INO, DIRS, FILES, ASYNCED; DEL_INODE, ERR); if ERR = ESUCCESS then {OF := OF -- FD; vfs_put_inode#(DEL_INODE, OF, ASYNCED; ERR, DIRS, FILES)}} } | An Axiom |
| open | vfs_open#(PATH, MODE, USER, DIRS, FILES, ASYNCED; FD, ERR, OF, MAXINO) {let INO = ROOT_INO, INODE = ? in {vfs_walk#(PATH, USER, DIRS, FILES, ASYNCED; INO, ERR); if ERR = ESUCCESS then let ISDIR = false in vfs_may_open#(INO, ISDIR, MODE, USER, DIRS, FILES, ASYNCED; INODE, ERR); if ERR = ESUCCESS then {OF[MAXINO] := mkfile(INO, MODE, 0); FD := MAXINO; MAXINO := MAXINO + 1}} } | An Axiom |
| link | vfs_link#(PATH, PATH', USER; ERR, DIRS, FILES, ASYNCED) {choose OLD_DENT, NEW_DENT, INODE, NEW_INODE, C_INODE with true in if PATH = ε ∨ PATH' = ε then ERR := EISDIR else {let INO = ROOT_INO, DENT = negdentry(PATH.last), PATH = parent(PATH) in {vfs_walk#(PATH, USER, DIRS, FILES, ASYNCED; INO, ERR); if ERR = ESUCCESS then vfs_may_link#(INO, USER, DIRS, FILES, ASYNCED; INODE, DENT, ERR); C_INODE := INODE; OLD_DENT := DENT}; if ERR = ESUCCESS then let INO = ROOT_INO, DENT = negdentry(PATH'.last), PATH = parent(PATH') in {vfs_walk#(PATH, USER, DIRS, FILES, ASYNCED; INO, ERR); if ERR = ESUCCESS then vfs_may_create#(INO, DENT, USER, DIRS, FILES, ASYNCED; INODE, ERR); NEW_INODE := INODE, NEW_DENT := DENT}; if ERR = ESUCCESS then afs_check_commit#(DIRS, FILES; ERR; ASYNCED); if ERR = ESUCCESS then afs_link#(OLD_DENT; NEW_INODE, C_INODE, NEW_DENT, ERR, DIRS, FILES; ASYNCED)} } | An Axiom |
| renam | vfs_rename#(PATH, PATH', USER, OF; ERR, DIRS, FILES, ASYNCED) {choose OLD_DENT, NEW_DENT, ISDIR, INODE, OLD_INODE, NEW_INODE, DEL_INODE, OLD_DENT_INODE, NEW_DENT_INODE with true in if PATH = ε ∨ PATH' = ε ∨ PATH ⊑ PATH' then ERR := EACCESS else {let INO = ROOT_INO, DENT = negdentry(PATH.last), PATH = parent(PATH) in {vfs_walk#(PATH, USER, DIRS, FILES, ASYNCED; INO, ERR); if ERR = ESUCCESS then let ISRENAME = true in vfs_may_delete#(INO, ISRENAME, USER, DIRS, FILES, ASYNCED; INODE, DENT, DEL_INODE, ISDIR, ERR); OLD_INODE := INODE; OLD_DENT := DENT; OLD_DENT_INODE := DEL_INODE}; if ERR = ESUCCESS then let INO = ROOT_INO, DENT = negdentry(PATH'.last), PATH = parent(PATH') in {vfs_walk#(PATH, USER, DIRS, FILES, ASYNCED; INO, ERR); if ERR = ESUCCESS then vfs_may_lookup#(INO, USER, DIRS, FILES, ASYNCED; INODE, ERR); if ERR = ESUCCESS then {afs_lookup#(INO, DIRS, FILES, ASYNCED; DENT, ERR); if ERR = ENOENT then vfs_may_create#(INO, DENT, USER, DIRS, FILES, ASYNCED; INODE, ERR) else if ERR = ESUCCESS then vfs_may_delete_check#(INO, USER, DIRS, FILES, ASYNCED; INODE, ISDIR, DENT, DEL_INODE, ERR)}; NEW_INODE := INODE; NEW_DENT := DENT; NEW_DENT_INODE := DEL_INODE}; if ERR = ESUCCESS then afs_check_commit#(DIRS, FILES; ERR; ASYNCED); if ERR = ESUCCESS then let DENT = NEW_DENT in {afs_rename#(; OLD_INODE, NEW_INODE, OLD_DENT_INODE, NEW_DENT_INODE, OLD_DENT, NEW_DENT, ERR, DIRS, FILES; ASYNCED); if DENT.dentry? then vfs_put_inode#(NEW_DENT_INODE, OF, ASYNCED; ERR, DIRS, FILES)}} } | An Axiom |
| unlink | vfs_unlink#(PATH, USER, OF; ERR, DIRS, FILES, ASYNCED) {if PATH = ε then ERR := EACCESS else let INO = ROOT_INO, DENT = negdentry(PATH.last), PATH = parent(PATH), ISDIR = false, INODE = ?, DEL_INODE = ? in {vfs_walk#(PATH, USER, DIRS, FILES, ASYNCED; INO, ERR); if ERR = ESUCCESS then vfs_may_delete_check#(INO, USER, DIRS, FILES, ASYNCED; INODE, ISDIR, DENT, DEL_INODE, ERR); if ERR = ESUCCESS then afs_check_commit#(DIRS, FILES; ERR; ASYNCED); if ERR = ESUCCESS then {afs_unlink#(; INODE, DEL_INODE, DENT, ERR, DIRS, FILES; ASYNCED); vfs_put_inode#(DEL_INODE, OF, ASYNCED; ERR, DIRS, FILES)}} } | An Axiom |
| create | vfs_create#(PATH, MD, USER; ERR, DIRS, FILES, ASYNCED) {if PATH = ε then ERR := EEXISTS else let INO = ROOT_INO, DENT = negdentry(PATH.last), PATH = parent(PATH), INODE = ?, C_INODE = ? in {vfs_walk#(PATH, USER, DIRS, FILES, ASYNCED; INO, ERR); if ERR = ESUCCESS then vfs_may_create#(INO, DENT, USER, DIRS, FILES, ASYNCED; INODE, ERR); if ERR = ESUCCESS then afs_check_commit#(DIRS, FILES; ERR; ASYNCED); if ERR = ESUCCESS then afs_create#(MD; INODE, C_INODE, DENT, ERR, DIRS, FILES; ASYNCED)} } | An Axiom |
| rmdir | vfs_rmdir#(PATH, USER, OF; ERR, DIRS, FILES, ASYNCED) {if PATH = ε then ERR := EACCESS else let INO = ROOT_INO, DENT = negdentry(PATH.last), PATH = parent(PATH), ISDIR = true, INODE = ?, DEL_INODE = ? in {vfs_walk#(PATH, USER, DIRS, FILES, ASYNCED; INO, ERR); if ERR = ESUCCESS then vfs_may_delete_check#(INO, USER, DIRS, FILES, ASYNCED; INODE, ISDIR, DENT, DEL_INODE, ERR); if ERR = ESUCCESS then afs_check_commit#(DIRS, FILES; ERR; ASYNCED); if ERR = ESUCCESS then {afs_rmdir#(; INODE, DEL_INODE, DENT, ERR, DIRS, FILES; ASYNCED); vfs_put_inode#(DEL_INODE, OF, ASYNCED; ERR, DIRS, FILES)}} } | An Axiom |
| mkdir | vfs_mkdir#(PATH, MD, USER; ERR, DIRS, FILES, ASYNCED) {if PATH = ε then ERR := EEXISTS else let INO = ROOT_INO, DENT = negdentry(PATH.last), PATH = parent(PATH), INODE = ?, C_INODE = ? in {vfs_walk#(PATH, USER, DIRS, FILES, ASYNCED; INO, ERR); if ERR = ESUCCESS then vfs_may_create#(INO, DENT, USER, DIRS, FILES, ASYNCED; INODE, ERR); if ERR = ESUCCESS then afs_check_commit#(DIRS, FILES; ERR; ASYNCED); if ERR = ESUCCESS then afs_mkdir#(MD; INODE, C_INODE, DENT, ERR, DIRS, FILES; ASYNCED)} } | An Axiom |
| walk | vfs_walk#(PATH, USER, DIRS, FILES, ASYNCED; INO, ERR) {ERR := ESUCCESS; let PATH = PATH in while PATH ≠ ε ∧ ERR = ESUCCESS do {choose INODE with true in vfs_may_lookup#(INO, USER, DIRS, FILES, ASYNCED; INODE, ERR); if ERR = ESUCCESS then let DENT = negdentry(PATH.head) in {afs_lookup#(INO, DIRS, FILES, ASYNCED; DENT, ERR); if ERR = ESUCCESS then {INO := DENT.ino; PATH := PATH.tail}}} } | An Axiom |
| truncate | vfs_truncate#(PATH, N, USER; ERR, DIRS, FILES, ASYNCED) {let INO = ROOT_INO, MODE = MODE_W, PAGENO = 0, PBUF-OPT = none, INODE = ?, MODIFIED = ? in {vfs_walk#(PATH, USER, DIRS, FILES, ASYNCED; INO, ERR); if ERR = ESUCCESS then let ISDIR = false in vfs_may_open#(INO, ISDIR, MODE, USER, DIRS, FILES, ASYNCED; INODE, ERR); if ERR = ESUCCESS then afs_check_commit#(DIRS, FILES; ERR; ASYNCED); if ERR = ESUCCESS then PAGENO := INODE.size / VFS_PAGE_SIZE; if ERR = ESUCCESS then afs_truncate#(N, PAGENO; PBUF-OPT, INODE, MODIFIED, ERR, DIRS, FILES, ASYNCED)} } | An Axiom |
| may-lookup | vfs_may_lookup#(INO, USER, DIRS, FILES, ASYNCED; INODE, ERR) {afs_iget#(INO, DIRS, FILES, ASYNCED; INODE, ERR); if ERR = ESUCCESS then if ¬ INODE.directory then ERR := ENOENT else if ¬ px(USER, INODE.meta) then ERR := EACCESS } | An Axiom |
| may-create | vfs_may_create#(INO, DENT, USER, DIRS, FILES, ASYNCED; INODE, ERR) {afs_iget#(INO, DIRS, FILES, ASYNCED; INODE, ERR); if ERR = ESUCCESS then if ¬ INODE.directory then ERR := ENOTDIR else if ¬ px(USER, INODE.meta) ∨ ¬ pw(USER, INODE.meta) then ERR := EACCESS else {afs_lookup#(INO, DIRS, FILES, ASYNCED; DENT, ERR); if ERR = ESUCCESS then ERR := EEXISTS else if ERR = ENOENT then ERR := ESUCCESS} } | An Axiom |
| read-loop | vfs_read_loop#(START, END, INODE, DONE, DIRS, FILES, ASYNCED; BUF, TOTAL, ERR) {while ERR = ESUCCESS ∧ ¬ DONE do vfs_read_block#(START, END, INODE, DIRS, FILES, ASYNCED; BUF, TOTAL, DONE, ERR)} | An Axiom |
| write-block | vfs_write_block#(START, INODE, BUF, END, DIRS; TOTAL, DONE, ERR, FILES, ASYNCED) {let PAGENO = (START + TOTAL) / VFS_PAGE_SIZE, OFFSET = (START + TOTAL) % VFS_PAGE_SIZE in let N = min(END - START + TOTAL, VFS_PAGE_SIZE - OFFSET) in if N ≠ 0 then {vfs_writepage#(INODE, PAGENO, BUF, TOTAL, OFFSET, N, DIRS; ERR, FILES, ASYNCED); if ERR = ESUCCESS then TOTAL := TOTAL + N} else DONE := true } | An Axiom |
| read-block | vfs_read_block#(START, END, INODE, DIRS, FILES, ASYNCED; BUF, TOTAL, DONE, ERR) {let PAGENO = (START + TOTAL) / VFS_PAGE_SIZE, OFFSET = (START + TOTAL) % VFS_PAGE_SIZE, PBUF = mkbuf(VFS_PAGE_SIZE) in let N = min(END - START + TOTAL, VFS_PAGE_SIZE - OFFSET, INODE.size - START + TOTAL) in if N ≠ 0 then {afs_readpage#(INODE, PAGENO, DIRS, FILES, ASYNCED; PBUF, ERR); if ERR = ESUCCESS then {BUF := copy(PBUF, OFFSET, BUF, TOTAL, N); TOTAL := TOTAL + N}} else DONE := true } | An Axiom |
| may-open | vfs_may_open#(INO, ISDIR, MODE, USER, DIRS, FILES, ASYNCED; INODE, ERR) {afs_iget#(INO, DIRS, FILES, ASYNCED; INODE, ERR); if ERR = ESUCCESS then if ¬(INODE.directory ↔ ISDIR) then ERR := (INODE.directory ⊃ EISDIR;ENOTDIR) else if (MODE = MODE_R ∨ MODE = MODE_RW) ∧ ¬ pr(USER, INODE.meta) ∨ (MODE = MODE_W ∨ MODE = MODE_RW) ∧ ¬ pw(USER, INODE.meta) then ERR := EACCESS } | An Axiom |
| may-delete | vfs_may_delete#(INO, ISRENAME, USER, DIRS, FILES, ASYNCED; INODE, DENT, DENT_INODE, ISDIR, ERR) {afs_iget#(INO, DIRS, FILES, ASYNCED; INODE, ERR); if ERR = ESUCCESS then if ¬ INODE.directory then ERR := ENOTDIR else if ¬ px(USER, INODE.meta) ∨ ¬ pw(USER, INODE.meta) then ERR := EACCESS else {afs_lookup#(INO, DIRS, FILES, ASYNCED; DENT, ERR); if ERR = ESUCCESS then {afs_iget#(DENT.ino, DIRS, FILES, ASYNCED; DENT_INODE, ERR); if ERR = ESUCCESS then {ISDIR := DENT_INODE.directory; if ISDIR then if DENT_INODE.ino = ROOT_INO then ERR := EACCESS else if ISRENAME ∧ ¬ pw(USER, DENT_INODE.meta) then ERR := EACCESS else if ¬ ISRENAME ∧ DENT_INODE.size ≠ 0 then ERR := ENOTEMPTY}}} } | An Axiom |
| readmeta | vfs_readmeta#(PATH, USER, DIRS, FILES, ASYNCED; MD, NLINK, SIZE, ERR) {let INO = ROOT_INO in {vfs_walk#(PATH, USER, DIRS, FILES, ASYNCED; INO, ERR); if ERR = ESUCCESS then choose INODE with true in {afs_iget#(INO, DIRS, FILES, ASYNCED; INODE, ERR); if ERR = ESUCCESS then if pr(USER, INODE.meta) then {MD := INODE.meta, SIZE := INODE.size; if INODE.directory then NLINK := INODE.nsubdirs + 2 else NLINK := INODE.nlink} else ERR := EACCESS}} } | An Axiom |
| may-delete-check | vfs_may_delete_check#(INO, USER, DIRS, FILES, ASYNCED; INODE, ISDIR, DENT, DENT_INODE, ERR) {let ISDIR0 = ISDIR, ISRENAME = false in {vfs_may_delete#(INO, ISRENAME, USER, DIRS, FILES, ASYNCED; INODE, DENT, DENT_INODE, ISDIR, ERR); if ISDIR0 ∧ ¬ ISDIR then ERR := ENOTDIR; if ¬ ISDIR0 ∧ ISDIR then ERR := EISDIR} } | An Axiom |
| put-inode | vfs_put_inode#(DEL_INODE, OF, ASYNCED; ERR, DIRS, FILES) {if ERR = ESUCCESS ∧ ¬ is-open(DEL_INODE.ino, OF) then afs_evict#(DEL_INODE, ASYNCED; ERR, DIRS, FILES)} | An Axiom |
| may-link | vfs_may_link#(INO, USER, DIRS, FILES, ASYNCED; INODE, DENT, ERR) {afs_iget#(INO, DIRS, FILES, ASYNCED; INODE, ERR); if ERR = ESUCCESS then if ¬ INODE.directory then ERR := ENOTDIR else if ¬ px(USER, INODE.meta) then ERR := EACCESS else {afs_lookup#(INO, DIRS, FILES, ASYNCED; DENT, ERR); if ERR = ESUCCESS then afs_iget#(DENT.ino, DIRS, FILES, ASYNCED; INODE, ERR); if ERR = ESUCCESS ∧ INODE.directory then ERR := EISDIR} } | An Axiom |
| write-page | vfs_writepage#(INODE, PAGENO, BUF, TOTAL, OFFSET, N, DIRS; ERR, FILES, ASYNCED) {let PBUF = mkbuf(VFS_PAGE_SIZE) in {afs_readpage#(INODE, PAGENO, DIRS, FILES, ASYNCED; PBUF, ERR); if ERR = ESUCCESS then afs_check_commit#(DIRS, FILES; ERR; ASYNCED); if ERR = ESUCCESS then {PBUF := copy(BUF, TOTAL, PBUF, OFFSET, N); afs_writepage#(INODE, PAGENO, PBUF, DIRS; ERR, FILES; ASYNCED)}} } | An Axiom |
| format | vfs_format#(N, DOSYNC, SIZE, MD; DIRS, FILES, ASYNCED; OF, MAXINO, ERR) {if SIZE = LEB_SIZE then {OF := ∅; MAXINO := 0; afs_format#(N, DOSYNC, SIZE, MD; DIRS; FILES, ASYNCED, ERR)} else abort} | An Axiom |
| recover | vfs_recover#(DOSYNC; DIRS, FILES, ASYNCED; OF, MAXINO, ERR){OF := ∅; MAXINO := 0; afs_recovery#(DOSYNC; DIRS, FILES; ASYNCED, ERR)} | An Axiom |
| sync | vfs_sync#(DIRS, FILES; ASYNCED; ERR){afs_sync#(DIRS, FILES; ; ASYNCED, ERR)} | An Axiom |
| fsync | vfs_fsync#(PATH, ISDATASYNC, USER, DIRS, FILES; ASYNCED; ERR) {let INO = ROOT_INO, MODE = MODE_R, INODE = ? in {ERR := ESUCCESS; vfs_walk#(PATH, USER, DIRS, FILES, ASYNCED; INO, ERR); if ERR = ESUCCESS then let ISDIR = false in vfs_may_open#(INO, ISDIR, MODE, USER, DIRS, FILES, ASYNCED; INODE, ERR); if ERR = ESUCCESS then afs_fsync#(INODE, ISDATASYNC, DIRS, FILES; ; ASYNCED, ERR); if ERR = ESUCCESS then afs_sync#(DIRS, FILES; ; ASYNCED, ERR)} } | An Axiom |
| fsyncdir | vfs_fsyncdir#(PATH, ISDATASYNC, USER, DIRS, FILES; ASYNCED; ERR) {let INO = ROOT_INO, MODE = MODE_R, NAMES = ∅, ISDIR = true, INODE = ?, C_INODE = ? in {ERR := ESUCCESS; vfs_walk#(PATH, USER, DIRS, FILES, ASYNCED; INO, ERR); if ERR = ESUCCESS then vfs_may_open#(INO, ISDIR, MODE, USER, DIRS, FILES, ASYNCED; INODE, ERR); if ERR = ESUCCESS then afs_readdir#(INODE, DIRS, FILES, ASYNCED; NAMES, ERR); while NAMES ≠ ∅ ∧ ERR = ESUCCESS do choose NAME with NAME ∈ NAMES in {let DENT = negdentry(NAME) in {afs_lookup#(INODE.ino, DIRS, FILES, ASYNCED; DENT, ERR); if ERR = ESUCCESS then afs_iget#(DENT.ino, DIRS, FILES, ASYNCED; C_INODE, ERR)}; if ERR = ESUCCESS then if C_INODE.directory then let PATH' = PATH + NAME in vfs_fsyncdir#(PATH', ISDATASYNC, USER, DIRS, FILES; ASYNCED; ERR) else afs_fsync#(C_INODE, ISDATASYNC, DIRS, FILES; ; ASYNCED, ERR); NAMES := NAMES -- NAME}; if ERR = ESUCCESS then afs_sync#(DIRS, FILES; ; ASYNCED, ERR)} } | An Axiom |
| inv-format | ino = LEB_SIZE ⊦ ⟪vfs_format#(n, isdir, ino, md; dirs, files, asynced; of, ino0, err)⟫ (err = ESUCCESS → asynced ∧ of-cons(of, dirs, files) ∧ dom of < ino0 ∧ afs-cons(dirs, files)) | A Proof Obligation |
| inv-write | of-cons(of, dirs, files), dom of < ino, afs-cons(dirs, files), n ≤ # buf ⊦ ⟪vfs_write#(fd, buf, user; n, err, of, dirs, files, asynced)⟫ (of-cons(of, dirs, files) ∧ dom of < ino ∧ afs-cons(dirs, files)) | A Proof Obligation |
| inv-read | of-cons(of, dirs, files), dom of < ino, afs-cons(dirs, files), n ≤ # buf ⊦ ⟪vfs_read#(fd, user, dirs, files, asynced; buf, n, err, of)⟫ (of-cons(of, dirs, files) ∧ dom of < ino) | A Proof Obligation |
| inv-readdir | of-cons(of, dirs, files), afs-cons(dirs, files) ⊦ ⟪vfs_readdir#(p, user, dirs, files, asynced; strings, err)⟫ true | A Proof Obligation |
| inv-readmeta | of-cons(of, dirs, files), afs-cons(dirs, files) ⊦ ⟪vfs_readmeta#(p, user, dirs, files, asynced; md, ino, ino0, err)⟫ true | A Proof Obligation |
| inv-seek | of-cons(of, dirs, files), dom of < ino, afs-cons(dirs, files) ⊦ ⟪vfs_seek#(fd, whence, user, dirs, files, asynced; n, err, of)⟫ (of-cons(of, dirs, files) ∧ dom of < ino) | A Proof Obligation |
| inv-truncate | of-cons(of, dirs, files), afs-cons(dirs, files) ⊦ ⟪vfs_truncate#(p, n, user; err, dirs, files, asynced)⟫ (of-cons(of, dirs, files) ∧ afs-cons(dirs, files)) | A Proof Obligation |
| inv-close | of-cons(of, dirs, files), dom of < ino, afs-cons(dirs, files) ⊦ ⟪vfs_close#(fd, user, asynced; err, of, dirs, files)⟫ (of-cons(of, dirs, files) ∧ dom of < ino ∧ afs-cons(dirs, files)) | A Proof Obligation |
| inv-open | of-cons(of, dirs, files), dom of < ino, afs-cons(dirs, files) ⊦ ⟪vfs_open#(p, mode, user, dirs, files, asynced; fd, err, of, ino)⟫ (of-cons(of, dirs, files) ∧ dom of < ino) | A Proof Obligation |
| inv-link | of-cons(of, dirs, files), afs-cons(dirs, files) ⊦ ⟪vfs_link#(p, p0, user; err, dirs, files, asynced)⟫ (of-cons(of, dirs, files) ∧ afs-cons(dirs, files)) | A Proof Obligation |
| inv-renam | of-cons(of, dirs, files), dom of < ino, afs-cons(dirs, files) ⊦ ⟪vfs_rename#(p, p0, user, of; err, dirs, files, asynced)⟫ (of-cons(of, dirs, files) ∧ afs-cons(dirs, files)) | A Proof Obligation |
| inv-unlink | of-cons(of, dirs, files), dom of < ino, afs-cons(dirs, files) ⊦ ⟪vfs_unlink#(p, user, of; err, dirs, files, asynced)⟫ (of-cons(of, dirs, files) ∧ afs-cons(dirs, files)) | A Proof Obligation |
| inv-rmdir | of-cons(of, dirs, files), dom of < ino, afs-cons(dirs, files) ⊦ ⟪vfs_rmdir#(p, user, of; err, dirs, files, asynced)⟫ (of-cons(of, dirs, files) ∧ afs-cons(dirs, files)) | A Proof Obligation |
| inv-mkdir | of-cons(of, dirs, files), afs-cons(dirs, files) ⊦ ⟪vfs_mkdir#(p, md, user; err, dirs, files, asynced)⟫ (of-cons(of, dirs, files) ∧ afs-cons(dirs, files)) | A Proof Obligation |
| inv-create | of-cons(of, dirs, files), afs-cons(dirs, files) ⊦ ⟪vfs_create#(p, md, user; err, dirs, files, asynced)⟫ (of-cons(of, dirs, files) ∧ afs-cons(dirs, files)) | A Proof Obligation |
| inv-recover | dirs = dirs0 \ orphans(dirs0, files), files0 = files \ orphans(dirs0, files), isdir, of-cons(of, dirs0, files), dom of < ino, afs-cons(dirs0, files) ⊦ ⟪vfs_recover#(isdir0; dirs, files0, asynced; of0, ino0, err)⟫ (err = ESUCCESS → asynced ∧ of-cons(of0, dirs, files0) ∧ dom of0 < ino0 ∧ afs-cons(dirs, files0)) | A Proof Obligation |
| inv-writemeta | of-cons(of, dirs, files), afs-cons(dirs, files) ⊦ ⟪vfs_writemeta#(p, md, user; err, dirs, files, asynced)⟫ (of-cons(of, dirs, files) ∧ afs-cons(dirs, files)) | A Proof Obligation |
| inv-sync | of-cons(of, dirs, files), afs-cons(dirs, files) ⊦ ⟪vfs_sync#(dirs, files; asynced; err)⟫ true | A Proof Obligation |
| inv-fsync | of-cons(of, dirs, files), afs-cons(dirs, files) ⊦ ⟪vfs_fsync#(p, isdir, user, dirs, files; asynced; err)⟫ true | A Proof Obligation |
| inv-fsyncdir | of-cons(of, dirs, files), afs-cons(dirs, files) ⊦ ⟪vfs_fsyncdir#(p, isdir, user, dirs, files; asynced; err)⟫ (⌊err⌋ ∨ err = ESUCCESS) | A Proof Obligation |
| inv-put-inode | afs-cons(dirs, files), of-cons(of, dirs, files), ¬ is-open(inode.ino, of) → pre-evict(inode, dirs, files) ⊦ ⟪vfs_put_inode#(inode, of, asynced; err, dirs, files)⟫ (afs-cons(dirs, files) ∧ of-cons(of, dirs, files)) | A User Theorem |
| of-cons-reduce | ⊦ of-cons(of0, dirs0, files0) → (of-cons(of1, dirs1, files1) ↔ (∀ n. (n ∈ of0 → of0[n].ino ∈ files0) → n ∈ of1 → of1[n].ino ∈ files1)) | A User Theorem |
| px-last | ⊦ px(user, parent(p), ino, dirs, files) → (px(user, p, ino, dirs, files) ↔ px(user, meta(p, ino, dirs, files))) | A User Theorem |
| read-loop-term | n0 + n ≤ n1, inode.ino ∈ files, n0 + n ≤ inode.size, n1 - n0 ≤ # buf, afs-cons(dirs, files) ⊦ ⟪vfs_read_loop#(n0, n1, inode, bv, dirs, files, asynced; buf, n, err)⟫ true | A User Theorem |
| valid-content-reduce | ⊦ valid-content(files0) → ( valid-content(files1) ↔ (∀ ino, n. (ino ∈ files0 ∧ n ∈ files0[ino].content → n * VFS_PAGE_SIZE < files0[ino].size) → ino ∈ files1 ∧ n ∈ files1[ino].content → n * VFS_PAGE_SIZE < files1[ino].size)) | A User Theorem |
| walk-prepost | ino = ROOT_INO, afs-cons(dirs, files) ⊦ ⟪vfs_walk#(p, user, dirs, files, asynced; ino, err)⟫ ( ⌊err⌋ ∨ err = ESUCCESS ∧ ispath(p, ROOT_INO, ino, dirs, files) ∧ px-parent(user, p, ROOT_INO, dirs, files) ∨ err = ENOENT ∧ ¬ ispath(p, ROOT_INO, dirs, files) ∨ err = EACCESS ∧ p ≠ ε ∧ (∃ p'. p' ⊑ parent(p) ∧ ispath(p', ROOT_INO, dirs, files) ∧ ¬ px(user, p', ROOT_INO, dirs, files))) | A User Theorem |
| walk-prepost-h | p_ino ∈ dirs, p_ino = ino, afs-cons(dirs, files), ispath(q, ROOT_INO, p_ino, dirs, files), q ≠ ε → px(user, parent(q), ROOT_INO, dirs, files) ⊦ [vfs_walk#(p, user, dirs, files, asynced; ino, err)] ( ⌊err⌋ ∨ err = ESUCCESS ∧ ispath(p, p_ino, ino, dirs, files) ∧ px-parent(user, q + p, ROOT_INO, dirs, files) ∨ err = ENOENT ∧ ¬ ispath(p, p_ino, dirs, files) ∨ err = EACCESS ∧ p ≠ ε ∧ (∃ p'. p' ⊑ parent(p) ∧ ispath(p', p_ino, dirs, files) ∧ ¬ px(user, q + p', ROOT_INO, dirs, files))) | A User Theorem |
| walk-prepost-parent | ino = ROOT_INO, afs-cons(dirs, files), p ≠ ε ⊦ ⟪vfs_walk#(parent(p), user, dirs, files, asynced; ino, err)⟫ ∃ q, str. p = q + str ∧ ( ⌊err⌋ ∨ err = ESUCCESS ∧ ispath(q, ROOT_INO, ino, dirs, files) ∧ px-parent(user, q, ROOT_INO, dirs, files) ∨ err = ENOENT ∧ ¬ ispath(q, ROOT_INO, dirs, files) ∨ err = EACCESS ∧ (∃ p'. p' ⊑ q ∧ ispath(p', ROOT_INO, dirs, files) ∧ ¬ px(user, p', ROOT_INO, dirs, files))) | A User Theorem |
| walk-term | ino ∈ dirs, links(ino, dirs) ≠ ∅ ∨ ino = ROOT_INO, afs-cons(dirs, files) ⊦ ⟪vfs_walk#(p, user, dirs, files, asynced; ino, err)⟫ true | A User Theorem |
| write-loop-0 | files0 = files1 ⊦ [vfs_write_loop#(n0, inode, n1, buf, dirs; n, err, files0, asynced)] (n = 0 → files0 = files1) | A User Theorem |
| write-loop-err | err = ESUCCESS ⊦ [vfs_write_loop#(n0, inode, n1, buf, dirs; n, err, files, asynced)] (err = ESUCCESS ∨ ⌊err⌋ ) | A User Theorem |
| write-loop-term | n0 + n ≤ n1, valid-file-inode(inode, dirs, files), n1 - n0 ≤ # buf, afs-cons(dirs, files) ⊦ ⟪vfs_write_loop#(n0, inode, n1, buf, dirs; n, err, files, asynced)⟫ valid-file-inode(inode, dirs, files) | A User Theorem |
| write-term | of-cons(of, dirs, files), afs-cons(dirs, files), dirs0 = dirs, n ≤ # buf ⊦ ⟪vfs_write#(fd, buf, user; n, err, of, dirs, files, asynced)⟫ (dirs0 = dirs) | A User Theorem |