| root[path].dir? ↔ ino2 ∈ dirs, err0 = err2, fs = abs-files(files), ino = ino3, ino0 = ino4, ino1 = ino4, ino5 = ino3, md = md0, md1 = md0, ofh = abs-of(of), root.dir?, dom of < ino6, abs(root, ROOT_INO)(dirs), afs-cons(dirs, files), fids-cons(root, abs-files(files), abs-of(of)), ispath(path, ROOT_INO, ino2, dirs, files), of-cons(of, dirs, files), px-parent(user, path, ROOT_INO, dirs, files), ⌊err1⌋ , psynced → asynced, ino2 ∈ dirs ∨ ino2 ∈ files ⊦ ∃ err. pre-readmeta(path, err, user, root, fs, ofh) ∧ ⟨err0 := err; if err0 = ESUCCESS then if root[path].dir? then md := root[path].meta, ino0 := # root[path].subdirs + 2, ino := # root[path].entries else let fid = root[path].fid in md := fs[fid].meta, ino0 := count(fid, root.fids), ino := # fs[fid].content⟩ ((psynced → asynced) ∧ md1 = md ∧ ino1 = ino0 ∧ ino5 = ino ∧ err1 = err0) |
root[path].dir? ↔ ino2 ∈ dirs, ino = ino3, ino0 = ino4, md = md0, root.dir?, dom of < ino6, abs(root, ROOT_INO)(dirs), afs-cons(dirs, files), fids-cons(root, abs-files(files), abs-of(of)), ispath(path, ROOT_INO, ino2, dirs, files), of-cons(of, dirs, files), px-parent(user, path, ROOT_INO, dirs, files), ⌊err1⌋ , psynced → asynced, ino2 ∈ dirs ∨ ino2 ∈ files ⊦ ∃ err. pre-readmeta(path, err, user, root, abs-files(files), abs-of(of)) ∧ ⟨err0 := err; if err0 = ESUCCESS then if ino2 ∈ dirs then md := root[path].meta, ino0 := # root[path].subdirs + 2, ino := # root[path].entries else let fid = root[path].fid in md := abs-files(files)[fid].meta, ino0 := count(fid, root.fids), ino := # abs-files(files)[fid].content⟩ ((psynced → asynced) ∧ md0 = md ∧ ino4 = ino0 ∧ ino3 = ino ∧ err1 = err0)