| pcache[datakey(m, n)] = mkpentry(true, buf0), buf = pcache[datakey(m, n)].page, err = ESUCCESS, inode = mkinode(m, md, boolvar, m0, m1, m2), pageno = n, n * VFS_PAGE_SIZE < m2, datakey(m, n) ∈ pcache, ∀ ino. ino ≠ m ∧ ino ∈ files0 → mkfile(files[ino].size, files[ino].meta, files[ino].nlink, files[ino].content ⊕ mkcontent(ino, pcache)) = mkfile(files0[ino].size, files0[ino].meta, files0[ino].nlink, files0[ino].content ⊕ mkcontent(ino, pcache0)) ∧ ino ∈ files ⊦ [abort; if err = ESUCCESS then afs_check_commit#(dirs, files; err; asynced1); if err = ESUCCESS then {asynced := false; pcache_set_status#(m, n, asynced; err, pcache)}; n := n + 1] ∀ ino. ino ≠ m ∧ ino ∈ files0 → mkfile(files[ino].size, files[ino].meta, files[ino].nlink, files[ino].content ⊕ mkcontent(ino, pcache)) = mkfile(files0[ino].size, files0[ino].meta, files0[ino].nlink, files0[ino].content ⊕ mkcontent(ino, pcache0)) ∧ ino ∈ files, pre-writepage(inode, pageno, buf, dirs, files) |