| dirs[ino0] = mkdir(m0, md0, # links(ino0, dirs), m3, entries0), err = ESUCCESS, ino = entries0[str], afs-cons(dirs, files), ispath(q, ROOT_INO, ino0, dirs, files), px(user, md0), str ∈ entries0, ino0 ∈ dirs, q ≠ ε → px(user, parent(q), ROOT_INO, dirs, files), links(ino0, dirs) ≠ ∅ ∨ ino0 = ROOT_INO, ∀ p1, err, p, p_ino, ino, dirs, files, q, user, asynced. # p1 < #(str + p2) → err = ESUCCESS ∧ p = p1 ∧ p_ino = ino ∧ afs-cons(dirs, files) ∧ ispath(q, ROOT_INO, ino, dirs, files) ∧ ino ∈ dirs ∧ (q ≠ ε → px(user, parent(q), ROOT_INO, dirs, files)) → [while p ≠ ε ∧ err = ESUCCESS do {choose inode with true in vfs_may_lookup#(ino, user, dirs, files, asynced; inode, err); if err = ESUCCESS then let dent = negdentry(p.head) in {afs_lookup#(ino, dirs, files, asynced; dent, err); if err = ESUCCESS then {ino := dent.ino; p := p.tail}}}] ( ⌊err⌋ ∨ err = ESUCCESS ∧ ispath(p1, p_ino, ino, dirs, files) ∧ px-parent(user, q + p1, ROOT_INO, dirs, files) ∨ err = ENOENT ∧ ¬ ispath(p1, p_ino, dirs, files) ∨ err = EACCESS ∧ p1 ≠ ε ∧ (∃ p'. p' ⊑ parent(p1) ∧ ispath(p', p_ino, dirs, files) ∧ ¬ px(user, q + p', ROOT_INO, dirs, files))) ⊦ [abort; if err = ESUCCESS then if ¬ inode.directory then err := ENOENT else if ¬ px(user, inode.meta) then err := EACCESS; p := p2; ino := entries0[str]; if err = ESUCCESS then let dent = negdentry(p.head) in {afs_lookup#(ino, dirs, files, asynced; dent, err); if err = ESUCCESS then {ino := dent.ino; p := p.tail}}; while p ≠ ε ∧ err = ESUCCESS do {choose inode with true in vfs_may_lookup#(ino, user, dirs, files, asynced; inode, err); if err = ESUCCESS then let dent = negdentry(p.head) in {afs_lookup#(ino, dirs, files, asynced; dent, err); if err = ESUCCESS then {ino := dent.ino; p := p.tail}}}] ( ⌊err⌋ ∨ err = ESUCCESS ∧ ispath(p2, entries0[str], ino, dirs, files) ∧ px-parent(user, q + str ' + p2, ROOT_INO, dirs, files) ∨ err = ENOENT ∧ ¬ ispath(p2, entries0[str], dirs, files) ∨ err = EACCESS ∧ (∃ p'. p' ⊑ str ' + parent(p2) ∧ ispath(p', ino0, dirs, files) ∧ ¬ px(user, q + p', ROOT_INO, dirs, files))), p2 = ε, pre-iget(ino, dirs, files), ispath(q + str ', ROOT_INO, entries0[str], dirs, files) ∧ entries0[str] ∈ dirs ∧ px(user, q, ROOT_INO, dirs, files) |