| ⟨vfs_put_inode#(getinode(entries0[str], dirs1, files), of, asynced; err3, dirs, files)⟩ (err3 = err2 ∧ dirs = dirs1 ∧ files = files1), # links(entries0[str], dirs0) = m + 1, # entries0 = m0 + 1, dirs0[ino1] = mkdir(m0 + 1, md0, # links(ino1, dirs0), m3, entries0), files0[entries0[str]] = mkfile(m1, md1, m + 1, content0), dirs = dirs1, err0 = err1, err3 = ESUCCESS, files = files0[entries0[str], mkfile(m1, md1, m, content0)], fs = abs-files(files0), ofh = abs-of(of), path = q + str ', root[q].dir?, root.dir?, dom of < ino0, abs(root, ROOT_INO)(dirs0), afs-cons(dirs0, files0), afs-cons(dirs1, files1), fids-cons(root, abs-files(files0), abs-of(of)), ispath(q, ROOT_INO, ino1, dirs0, files0), of-cons(of, dirs0, files0), of-cons(of, dirs1, files1), pw(user, md0), px(user, md0), px-parent(user, q, ROOT_INO, dirs0, files0), str ∈ entries0, ino1 ∈ dirs0, entries0[str] ∈ files0, dirs1 ≡ dirs0[ino1, mkdir(m0, md0, # links(ino1, dirs0), m3, entries0 -- str)], psynced → asynced0, links(ino1, dirs0) ≠ ∅ ∨ ino1 = ROOT_INO ⊦ pre-unlink(path, err2, user, root, fs, ofh) ∧ ⟨err0 := err2; if err0 = ESUCCESS then let fid = root[path].fid in {root := root -- path; if ¬ fid ∈ ofh.fids ∧ ¬ fid ∈ root.fids then fs := fs -- fid}; psynced := ?⟩ (root.dir? ∧ fids-cons(root, fs, abs-of(of)) → fs = abs-files(files1) ∧ abs(root, ROOT_INO)(dirs1) ∧ (psynced → asynced) ∧ err2 = err0), entries0 = ∅, root[q + str '].dir?, entries0[str] ∈ dirs1, entries0[str] ∈ dirs0 |
⟨vfs_put_inode#(getinode(entries0[str], dirs1, files), of, asynced; err3, dirs, files)⟩ (err3 = err2 ∧ dirs = dirs1 ∧ files = files1), # entries0 = m0 + 1, # links(entries0[str], dirs0) = m + 1, files0[entries0[str]] = mkfile(m1, md1, m + 1, content0), dirs0[ino1] = mkdir(m0 + 1, md0, # links(ino1, dirs0), m3, entries0), dirs = dirs1, err3 = ESUCCESS, files = files0[entries0[str], mkfile(m1, md1, m, content0)], fs = abs-files(files0), entries0 ≠ ∅, root.dir?, root[q].dir?, dom of < ino0, abs(root, ROOT_INO)(dirs0), afs-cons(dirs1, files1), afs-cons(dirs0, files0), fids-cons(root, abs-files(files0), abs-of(of)), ispath(q, ROOT_INO, ino1, dirs0, files0), of-cons(of, dirs1, files1), of-cons(of, dirs0, files0), pw(user, md0), px(user, md0), px-parent(user, q, ROOT_INO, dirs0, files0), entries0[str] ∈ files0, ino1 ∈ dirs0, str ∈ entries0, dirs1 ≡ dirs0[ino1, mkdir(m0, md0, # links(ino1, dirs0), m3, entries0 -- str)], ¬ root[q + str '].dir?, ¬ entries0[str] ∈ dirs0, ¬ entries0[str] ∈ dirs1, psynced → asynced0, links(ino1, dirs0) ≠ ∅ ∨ ino1 = ROOT_INO ⊦ pre-unlink(q + str ', err2, user, root, fs, abs-of(of)) ∧ ⟨err0 := err2; if err0 = ESUCCESS then let fid = root[q + str '].fid in {root := root -- (q + str '); if ¬ fid ∈ abs-of(of).fids ∧ ¬ fid ∈ root.fids then fs := fs -- fid}; psynced := ?⟩ (root.dir? ∧ fids-cons(root, fs, abs-of(of)) → fs = abs-files(files1) ∧ abs(root, ROOT_INO)(dirs1) ∧ (psynced → asynced) ∧ err2 = err0)