| files0[m] = mkfile(m1, md, # links(m, dirs), content0), of[fd] = mkfile(m, mode, m0), err = ESUCCESS, dom of < ino3, m1 < m0 + ino4, afs-cons(dirs, files0), afs-cons(dirs, files), of-cons(of, dirs, files0), of-cons(of, dirs, files), fd ∈ of, m ∈ files0, n ≤ # buf0 ⊦ [choose err0 with ⌊err0⌋ ∨ err0 = ESUCCESS in err := err0; choose bv with true in asynced := bv; dirs1 := dirs; if err = ESUCCESS then afs_write_inode#(mkinode(m, md, false, # links(m, dirs), 0, m0 + ino4); err, dirs, files; asynced); if err ≠ ESUCCESS then ino4 := (m0 ≤ m1 ⊃ m1 - m0;0), err := ESUCCESS; of[fd].pos := m0 + ino4] (dirs1 = dirs → of-cons(of, dirs, files) ∧ dom of < ino3 ∧ afs-cons(dirs, files)), ino4 = 0, n = 0, mode ≠ MODE_W ∧ mode ≠ MODE_RW, m1 % VFS_PAGE_SIZE ≠ 0 ∧ m1 / VFS_PAGE_SIZE ∈ content0, err1 = ESUCCESS ∧ ¬ isdir |
of[fd] = mkfile(m, mode, m0), files0[m] = mkfile(m1, md, # links(m, dirs), content0), err = ESUCCESS, m1 < m0 + ino4, dom of < ino3, afs-cons(dirs, files), afs-cons(dirs, files0), of-cons(of, dirs, files), of-cons(of, dirs, files0), m ∈ files0, fd ∈ of, n ≤ # buf0, ⌊err0⌋ ∨ err0 = ESUCCESS ⊦ [err := err0; choose bv with true in asynced := bv; dirs1 := dirs; if err = ESUCCESS then afs_write_inode#(mkinode(m, md, false, # links(m, dirs), 0, m0 + ino4); err, dirs, files; asynced); if err ≠ ESUCCESS then ino4 := (m0 ≤ m1 ⊃ m1 - m0;0), err := ESUCCESS; of[fd].pos := m0 + ino4] (dirs1 = dirs → of-cons(of, dirs, files) ∧ dom of < ino3 ∧ afs-cons(dirs, files)), ino4 = 0, n = 0, err1 = ESUCCESS ∧ ¬ isdir, m1 % VFS_PAGE_SIZE ≠ 0 ∧ m1 / VFS_PAGE_SIZE ∈ content0, mode ≠ MODE_W ∧ mode ≠ MODE_RW