| files1[m] = mkfile(m1, md, # links(m, dirs), content0), of1[fd] = mkfile(m, mode, m0), buf-opt = none, err = ESUCCESS, files = files1, inode = mkinode(m, md, false, # links(m, dirs), 0, m1), m2 = # links(m, dirs), n1 ≠ 0, afs-cons(dirs, files1), of-cons(of1, dirs, files1), fd ∈ of1, m ∈ files1, n1 ≤ # buf ⊦ [afs_truncate#(m1, m1 / VFS_PAGE_SIZE; buf-opt, inode, isdir, err, dirs, files, asynced)] ( (err = ESUCCESS ⊃ files[m].content.stream from m1 = σ⊥ ∧ (∀ n0, n1, buf. n1 ≤ # buf → write-inv(n0, n0 + n1, mkinode(m, md, false, m2, 0, m1), buf, 0, dirs, files, files)) ∧ files1 -- m = files -- m ;⌊err⌋ ) ∧ files1 ~ files ∧ inode = mkinode(m, md, false, m2, 0, m1) → [ino2 := of1[fd].pos; ino0 := 0; if err = ESUCCESS then vfs_write_loop#(ino2, inode, of1[fd].pos + n1, buf, dirs; ino0, err, files, asynced); if ino0 ≠ 0 then err := ESUCCESS; of := of1; n := n1; if err = ESUCCESS then let ino = inode.size in {n := ino0, ino1 := ino2 + ino0; if ino0 ≠ 0 ∧ ino < ino1 then {inode.size := ino1; afs_check_commit#(dirs, files; err; asynced); if err = ESUCCESS then afs_write_inode#(inode; err, dirs, files; asynced)}; if err ≠ ESUCCESS then n := (ino2 ≤ ino ⊃ ino - ino2;0), err := ESUCCESS; of[fd].pos := ino2 + n}; file := of1[fd]] (err = ESUCCESS ⊃ (files[file.ino].content.stream to files[file.ino].size).buf = splice(buf, 0, (files1[file.ino].content.stream to files1[file.ino].size).buf, file.pos, n) ∧ of = of1[fd, file.pos:= (file.pos + n)] ∧ n ≤ n1 ∧ file.ino ∈ files1 ∧ file.ino ∈ files ∧ files[file.ino].meta = files1[file.ino].meta ∧ files -- file.ino = files1 -- file.ino ∧ (file.mode = MODE_W ∨ file.mode = MODE_RW) ;files ~ files1 ∧ of1 = of ∧ (err = EBADFD ∧ (fd ∈ of → file.mode ≠ MODE_W ∧ file.mode ≠ MODE_RW) ∨ ⌊err⌋ ) )), mode ≠ MODE_W ∧ mode ≠ MODE_RW |
⟨afs_truncate#(m1, m1 / VFS_PAGE_SIZE; buf-opt, inode, isdir, err, dirs, files, asynced)⟩ (buf-opt = buf-opt0 ∧ inode = inode0 ∧ (isdir ↔ isdir0) ∧ err = err0 ∧ dirs = dirs0 ∧ files = files0 ∧ (asynced ↔ asynced0)), of1[fd] = mkfile(m, mode, m0), files1[m] = mkfile(m1, md, # links(m, dirs), content0), buf-opt = none, err = ESUCCESS, files = files1, inode = mkinode(m, md, false, # links(m, dirs), 0, m1), inode0 = mkinode(m, md, false, m2, 0, m1), m2 = # links(m, dirs), afs-cons(dirs, files1), of-cons(of1, dirs, files1), files1 ~ files0, m ∈ files1, fd ∈ of1, n1 ≤ # buf, (err0 = ESUCCESS ⊃ files0[m].content.stream from m1 = σ⊥ ∧ (∀ n0, n1, buf. n1 ≤ # buf → write-inv(n0, n0 + n1, mkinode(m, md, false, m2, 0, m1), buf, 0, dirs0, files0, files0)) ∧ files1 -- m = files0 -- m ;⌊err0⌋ ) ⊦ [ino2 := of1[fd].pos; ino0 := 0; if err0 = ESUCCESS then vfs_write_loop#(ino2, inode0, of1[fd].pos + n1, buf, dirs0; ino0, err0, files0, asynced0); if ino0 ≠ 0 then err0 := ESUCCESS; of := of1; n := n1; if err0 = ESUCCESS then let ino = inode0.size in {n := ino0, ino1 := ino2 + ino0; if ino0 ≠ 0 ∧ ino < ino1 then {inode0.size := ino1; afs_check_commit#(dirs0, files0; err0; asynced0); if err0 = ESUCCESS then afs_write_inode#(inode0; err0, dirs0, files0; asynced0)}; if err0 ≠ ESUCCESS then n := (ino2 ≤ ino ⊃ ino - ino2;0), err0 := ESUCCESS; of[fd].pos := ino2 + n}; file := of1[fd]] (err0 = ESUCCESS ⊃ (files0[file.ino].content.stream to files0[file.ino].size).buf = splice(buf, 0, (files1[file.ino].content.stream to files1[file.ino].size).buf, file.pos, n) ∧ of = of1[fd, file.pos:= (file.pos + n)] ∧ n ≤ n1 ∧ file.ino ∈ files1 ∧ file.ino ∈ files0 ∧ files0[file.ino].meta = files1[file.ino].meta ∧ files0 -- file.ino = files1 -- file.ino ∧ (file.mode = MODE_W ∨ file.mode = MODE_RW) ;files0 ~ files1 ∧ of1 = of ∧ (err0 = EBADFD ∧ (fd ∈ of → file.mode ≠ MODE_W ∧ file.mode ≠ MODE_RW) ∨ ⌊err0⌋ ) ), n1 = 0, mode ≠ MODE_W ∧ mode ≠ MODE_RW