| dirs0[ino3] = mkdir(# entries, md1, # links(ino3, dirs0), m4, entries), entries0[str] = entries[str], dirs0[ino1] = mkdir(# entries0, md0, # links(ino1, dirs0), m2, entries0), files0[entries[str]] = mkfile(m0, md2, # links(entries[str], dirs0), content0), dirs0[ino2] = mkdir(# entries1, md, # links(ino2, dirs0), m3, entries1), err0 = err2, fs = abs-files(files0), ofh = abs-of(of), path = q + str ', path' = q0 + str0 ', root[q0].dir?, root[q].dir?, root.dir?, dom of < ino0, abs(root, ROOT_INO)(dirs0), afs-cons(dirs0, files0), afs-cons(dirs, files0[entries[str], mkfile(m0, md2, # links(entries[str], dirs0) + 1, content0)]), fids-cons(root, abs-files(files0), abs-of(of)), ispath(q, ROOT_INO, ino1, dirs0, files0), ispath(q0, ROOT_INO, ino2, dirs0, files0), of-cons(of, dirs, files0[entries[str], mkfile(m0, md2, # links(entries[str], dirs0) + 1, content0)]), of-cons(of, dirs0, files0), pw(user, md), px(user, md), px(user, md0), px-parent(user, q, ROOT_INO, dirs0, files0), px-parent(user, q0, ROOT_INO, dirs0, files0), str ∈ entries, ino3 ∈ dirs0, ino2 ∈ dirs0, ino1 ∈ dirs0, str ∈ entries0, entries[str] ∈ files0, dirs ≡ dirs0[ino2, mkdir(# entries1 + 1, md, # links(ino2, dirs0), m3, entries1[str0, entries[str]])], psynced → asynced0, links(ino1, dirs0) ≠ ∅ ∨ ino1 = ROOT_INO, links(ino3, dirs0) ≠ ∅ ∨ ino3 = ROOT_INO ⊦ ∃ err. pre-link(path, path', err, user, root, fs, ofh) ∧ ⟨err0 := err; if err0 = ESUCCESS then let fid = root[path].fid in root[path'] := fnode(fid); psynced := ?⟩ ( abs-files(files0) = abs-files (files0[entries[str], mkfile(m0, md2, # links(entries[str], dirs0) + 1, content0)] [entries0[str], mkfile(m0, md2, # links(entries[str], dirs0) + 1, content0) ]) ∧ abs(root, ROOT_INO)(dirs) ∧ (psynced → asynced) ∧ ESUCCESS = err0), # links(ino2, dirs0) = 0, ino2 = ROOT_INO, links(ino2, dirs0) = ∅, root[q + str '].dir?, str0 ∈ entries1, entries[str] ∈ dirs0, entries[str] ∈ dirs, ino2 ∈ dirs |
dirs0[ino2] = mkdir(# entries1, md, # links(ino2, dirs0), m3, entries1), files0[entries[str]] = mkfile(m0, md2, # links(entries[str], dirs0), content0), dirs0[ino1] = mkdir(# entries0, md0, # links(ino1, dirs0), m2, entries0), entries0[str] = entries[str], dirs0[ino3] = mkdir(# entries, md1, # links(ino3, dirs0), m4, entries), # links(ino2, dirs0) ≠ 0, ino2 ≠ ROOT_INO, links(ino2, dirs0) ≠ ∅, root.dir?, root[q].dir?, root[q0].dir?, dom of < ino0, abs(root, ROOT_INO)(dirs0), afs-cons(dirs, files0[entries[str], mkfile(m0, md2, # links(entries[str], dirs0) + 1, content0)]), afs-cons(dirs0, files0), fids-cons(root, abs-files(files0), abs-of(of)), ispath(q0, ROOT_INO, ino2, dirs0, files0), ispath(q, ROOT_INO, ino1, dirs0, files0), of-cons(of, dirs0, files0), of-cons(of, dirs, files0[entries[str], mkfile(m0, md2, # links(entries[str], dirs0) + 1, content0)]), pw(user, md), px(user, md0), px(user, md), px-parent(user, q0, ROOT_INO, dirs0, files0), px-parent(user, q, ROOT_INO, dirs0, files0), entries[str] ∈ files0, str ∈ entries0, ino1 ∈ dirs0, ino2 ∈ dirs0, ino3 ∈ dirs0, str ∈ entries, dirs ≡ dirs0[ino2, mkdir(# entries1 + 1, md, # links(ino2, dirs0), m3, entries1[str0, entries[str]])], ¬ root[q + str '].dir?, ¬ ino2 ∈ dirs, ¬ entries[str] ∈ dirs, ¬ entries[str] ∈ dirs0, ¬ str0 ∈ entries1, psynced → asynced0, links(ino3, dirs0) ≠ ∅ ∨ ino3 = ROOT_INO, links(ino1, dirs0) ≠ ∅ ∨ ino1 = ROOT_INO ⊦ ∃ err. pre-link(q + str ', q0 + str0 ', err, user, root, abs-files(files0), abs-of(of)) ∧ ⟨err0 := err; if err0 = ESUCCESS then let fid = root[q + str '].fid in root[q0 + str0 '] := fnode(fid); psynced := ?⟩ ( abs-files(files0) = abs-files (files0[entries[str], mkfile(m0, md2, # links(entries[str], dirs0) + 1, content0)] [entries0[str], mkfile(m0, md2, # links(entries[str], dirs0) + 1, content0) ]) ∧ abs(root, ROOT_INO)(dirs) ∧ (psynced → asynced) ∧ ESUCCESS = err0)