| # buf = VFS_PAGE_SIZE, asynced ↔ asynced3, asynced0 ↔ asynced4, files[m] = mkfile(m0, md0, # links(m, dirs), content), pcache[datakey(m, m2 / VFS_PAGE_SIZE)] = mkpentry(boolvar, buf), buf-opt = some(buf), err = ESUCCESS, inode = mkinode(m, md, false, # links(m, dirs), 0, m2), pageno = m2 / VFS_PAGE_SIZE, afs-cons(dirs, files), dcache-cons(dcache, dirs, files), icache-cons(icache, dirs, files), pcache-cons(pcache, dirs, files), synced(dirs, icache, pcache), m ∈ files, datakey(m, m2 / VFS_PAGE_SIZE) ∈ pcache, asynced2 → synced(files, icache, pcache) ⊦ [abort] ( afs-cons(dirs, files) → ⟪asynced4 := asynced0; if err = ESUCCESS then let asynced = false in {icache_set#(inode, asynced; err, icache); pcache_truncate#(inode.ino, m2, n; err, pcache); if asynced4 then pcache_set#(inode.ino, m2 / VFS_PAGE_SIZE, buf-opt.buf, asynced; err, pcache)}; if ¬ asynced4 ∨ err ≠ ESUCCESS then buf-opt := none⟫ ( icache-cons(icache, dirs, files) ∧ dcache-cons(dcache, dirs, files) ∧ pcache-cons(pcache, dirs, files) ∧ synced(dirs, icache, pcache) ∧ (asynced2 → synced(files, icache, pcache)))), VFS_PAGE_SIZE = 0, pre-truncate(inode, n, pageno, buf-opt, dirs, files) |