| err = err0, ino = ROOT_INO, root.dir?, dom of < ino0, abs(root, ROOT_INO)(dirs), afs-cons(dirs, files), fids-cons(root, abs-files(files), abs-of(of)), of-cons(of, dirs, files), psynced → asynced ⊦ ∀ ino, err. ⌊err⌋ ∨ err = ESUCCESS ∧ ispath(path, ROOT_INO, ino, dirs, files) ∧ px-parent(user, path, ROOT_INO, dirs, files) ∨ err = ENOENT ∧ ¬ ispath(path, ROOT_INO, dirs, files) ∨ err = EACCESS ∧ path ≠ ε ∧ (∃ p'. p' ⊑ parent(path) ∧ ispath(p', ROOT_INO, dirs, files) ∧ ¬ px(user, p', ROOT_INO, dirs, files)) → [strings := strings0; if err = ESUCCESS then {mode := MODE_R; isdir := true; 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; strings, err)}}] ⟨posix_readdir#(path, user, root, abs-files(files), abs-of(of); strings0, err0)⟩ ((psynced → asynced) ∧ strings = strings0 ∧ err = err0) |
root.dir?, dom of < ino0, abs(root, ROOT_INO)(dirs), afs-cons(dirs, files), fids-cons(root, abs-files(files), abs-of(of)), of-cons(of, dirs, files), psynced → asynced, ⌊err1⌋ ∨ err1 = ESUCCESS ∧ ispath(path, ROOT_INO, ino1, dirs, files) ∧ px-parent(user, path, ROOT_INO, dirs, files) ∨ err1 = ENOENT ∧ ¬ ispath(path, ROOT_INO, dirs, files) ∨ err1 = EACCESS ∧ path ≠ ε ∧ p' ⊑ parent(path) ∧ ispath(p', ROOT_INO, dirs, files) ∧ ¬ px(user, p', ROOT_INO, dirs, files) ⊦ [strings := strings0; if err1 = ESUCCESS then {mode := MODE_R; isdir := true; choose inode with true in {vfs_may_open#(ino1, isdir, mode, user, dirs, files, asynced; inode, err1); if err1 = ESUCCESS then afs_readdir#(inode, dirs, files, asynced; strings, err1)}}] ⟨posix_readdir#(path, user, root, abs-files(files), abs-of(of); strings0, err0)⟩ ((psynced → asynced) ∧ strings = strings0 ∧ err1 = err0)