| files0[m] = mkfile(m1, md, # links(m, dirs), content0), of[fd] = mkfile(m, mode, m0), buf = buf0, err = ESUCCESS, ino0 = ino, ino1 = m0 + n0, ino2 = m0, inode = mkinode(m, md, false, # links(m, dirs), 0, m1), ¬ isdir, dom of < ino3, afs-cons(dirs, files0), afs-cons(dirs, files), of-cons(of, dirs, files0), of-cons(of, dirs, files), fd ∈ of, m ∈ files0, n0 ≤ # buf0 ⊦ [let pageno = (ino2 + ino0) / VFS_PAGE_SIZE, ino = (ino2 + ino0) % VFS_PAGE_SIZE in let n = min(ino1 - ino2 + ino0, VFS_PAGE_SIZE - ino) in if n ≠ 0 then {vfs_writepage#(inode, pageno, buf, ino0, ino, n, dirs; err, files, asynced); if err = ESUCCESS then ino0 := ino0 + n} else isdir := true] (of-cons(of, dirs, files) ∧ afs-cons(dirs, files)), n0 = 0, mode ≠ MODE_W ∧ mode ≠ MODE_RW, m1 % VFS_PAGE_SIZE ≠ 0 ∧ m1 / VFS_PAGE_SIZE ∈ content0 |
of[fd] = mkfile(m, mode, m0), files0[m] = mkfile(m1, md, # links(m, dirs), content0), buf = buf0, err = ESUCCESS, ino = (ino2 + ino0) % VFS_PAGE_SIZE, ino0 = ino4, ino1 = m0 + n0, ino2 = m0, inode = mkinode(m, md, false, # links(m, dirs), 0, m1), ¬ isdir, pageno = (ino2 + ino0) / VFS_PAGE_SIZE, 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, n0 ≤ # buf0 ⊦ [let n = min(ino1 - ino2 + ino0, VFS_PAGE_SIZE - ino) in if n ≠ 0 then {vfs_writepage#(inode, pageno, buf, ino0, ino, n, dirs; err, files, asynced); if err = ESUCCESS then ino0 := ino0 + n} else isdir := true] (of-cons(of, dirs, files) ∧ afs-cons(dirs, files)), VFS_PAGE_SIZE = 0, n0 = 0, m1 % VFS_PAGE_SIZE ≠ 0 ∧ m1 / VFS_PAGE_SIZE ∈ content0, mode ≠ MODE_W ∧ mode ≠ MODE_RW