| err = err0, ino = ROOT_INO, root.dir?, dom of < ino6, 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)) → [md := md0; ino1 := ino4; ino0 := ino3; 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, ino0 := inode.size; if inode.directory then ino1 := inode.nsubdirs + 2 else ino1 := inode.nlink} else err := EACCESS}] ⟨posix_readmeta#(path, user, root, abs-files(files), abs-of(of); md0, ino4, ino3, err0)⟩ ((psynced → asynced) ∧ md = md0 ∧ ino1 = ino4 ∧ ino0 = ino3 ∧ err = err0) |
root.dir?, dom of < ino6, 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, ino2, 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) ⊦ [md := md0; ino1 := ino4; ino0 := ino3; if err1 = ESUCCESS then choose inode with true in {afs_iget#(ino2, dirs, files, asynced; inode, err1); if err1 = ESUCCESS then if pr(user, inode.meta) then {md := inode.meta, ino0 := inode.size; if inode.directory then ino1 := inode.nsubdirs + 2 else ino1 := inode.nlink} else err1 := EACCESS}] ⟨posix_readmeta#(path, user, root, abs-files(files), abs-of(of); md0, ino4, ino3, err0)⟩ ((psynced → asynced) ∧ md = md0 ∧ ino1 = ino4 ∧ ino0 = ino3 ∧ err1 = err0)