| buf = buf0, err = err0, n = n0, ofh = abs-of(of), root.dir?, dom of < ino, abs(root, ROOT_INO)(dirs), afs-cons(dirs, files), fids-cons(root, abs-files(files), abs-of(of)), of-cons(of, dirs, files), n0 ≤ # buf0, psynced → asynced ⊦ [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 ino1 = of[fd].pos, ino0 = of[fd].pos + n, ino = 0 in if ino1 ≤ inode.size then {let isdir = false in vfs_read_loop#(ino1, ino0, inode, isdir, dirs, files, asynced; buf, ino, err); if ino ≠ 0 then err := ESUCCESS; of[fd].pos := of[fd].pos + ino; n := ino} else n := 0}] ( of-cons(of, dirs, files) ∧ dom of < ino → ⟨posix_read#(fd, user, root, abs-files(files); buf0, n0, err0, ofh)⟩ (ofh = abs-of(of) ∧ (psynced → asynced) ∧ buf = buf0 ∧ n = n0 ∧ err = err0)) |
buf = buf0, err = ESUCCESS, err1 = err0, n = n0, ofh = abs-of(of), root.dir?, dom of < ino, abs(root, ROOT_INO)(dirs), afs-cons(dirs, files), fids-cons(root, abs-files(files), abs-of(of)), of-cons(of, dirs, files), n0 ≤ # buf0, psynced → asynced ⊦ [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 ino1 = of[fd].pos, ino0 = of[fd].pos + n, ino = 0 in if ino1 ≤ inode.size then {let isdir = false in vfs_read_loop#(ino1, ino0, inode, isdir, dirs, files, asynced; buf, ino, err); if ino ≠ 0 then err := ESUCCESS; of[fd].pos := of[fd].pos + ino; n := ino} else n := 0}] ( of-cons(of, dirs, files) ∧ dom of < ino → ⟨posix_read#(fd, user, root, abs-files(files); buf0, n0, err0, ofh)⟩ (ofh = abs-of(of) ∧ (psynced → asynced) ∧ buf = buf0 ∧ n = n0 ∧ err = err0))