| ⟨afs_truncate#(m2, m2 / VFS_PAGE_SIZE; buf-opt, inode, isdir, err2, dirs1, files1, asynced)⟩ (buf-opt = buf-opt0 ∧ inode = inode0 ∧ (isdir ↔ isdir0) ∧ err2 = ESUCCESS ∧ dirs1 = dirs0 ∧ files1 = files0 ∧ (asynced ↔ asynced0)), files1 -- m = files0 -- m, files0[m] = mkfile(m2, md0, # links(m, dirs1), content), of1[fd] = mkfile(m, mode, m0), files1[m] = mkfile(m2, md0, # links(m, dirs1), content0), buf-opt = none, err2 = ESUCCESS, content.stream from m2 = σ⊥, ino2 = of1[fd].pos, inode = mkinode(m, md0, false, # links(m, dirs1), 0, m2), inode0 = mkinode(m, md0, false, # links(m, dirs1), 0, m2), n = ino, content0.stream to m2 = content.stream to m2, m2 < m0 + ino, afs-cons(dirs1, files1), of-cons(of1, dirs1, files1), write-inv(m0, m0 + n1, mkinode(m, md0, false, # links(m, dirs1), 0, m2), buf, ino, dirs0, files0, files), write-inv(m0, m0 + n1, mkinode(m, md0, false, # links(m, dirs1), 0, m2), buf, 0, dirs0, files0, files0), files1 ~ files0, fd ∈ of1, m ∈ files1, m ∈ files, n1 ≤ # buf, (ino2 ≤ m2 ⊃ m2 ≥ ino2;true), ⌊err0⌋ ∨ err0 = ESUCCESS, err1 = ESUCCESS ∨ ⌊err1⌋ ⊦ [of := of1[fd, of1[fd].pos:= (ino2 + (ino2 ≤ m2 ⊃ m2 - ino2;0))]] (ESUCCESS = ESUCCESS ⊃ (files[m].content.stream to files[m].size).buf = splice(buf, 0, (content0.stream to m2).buf, m0, (ino2 ≤ m2 ⊃ m2 - ino2;0)) ∧ of = of1[fd, of1[fd].pos:= (m0 + (ino2 ≤ m2 ⊃ m2 - ino2;0))] ∧ (ino2 ≤ m2 ⊃ m2 - ino2;0) ≤ n1 ∧ m ∈ files ∧ files[m].meta = md0 ∧ files -- m = files1 -- m ∧ (mode = MODE_W ∨ mode = MODE_RW) ;files ~ files1 ∧ of1 = of ∧ (ESUCCESS = EBADFD ∧ (fd ∈ of → of[fd].mode ≠ MODE_W ∧ of[fd].mode ≠ MODE_RW) ∨ ⌊ESUCCESS⌋ ) ), err0 = ESUCCESS, ino = 0, n1 = 0, mode ≠ MODE_W ∧ mode ≠ MODE_RW |
⟨afs_truncate#(m2, m2 / VFS_PAGE_SIZE; buf-opt, inode, isdir, err2, dirs1, files1, asynced)⟩ (buf-opt = buf-opt0 ∧ inode = inode0 ∧ (isdir ↔ isdir0) ∧ err2 = ESUCCESS ∧ dirs1 = dirs0 ∧ files1 = files0 ∧ (asynced ↔ asynced0)), files1 -- m = files0 -- m, files1[m] = mkfile(m2, md0, # links(m, dirs1), content0), of1[fd] = mkfile(m, mode, m0), files0[m] = mkfile(m2, md0, # links(m, dirs1), content), buf-opt = none, err2 = ESUCCESS, content.stream from m2 = σ⊥, ino2 = of1[fd].pos, inode = mkinode(m, md0, false, # links(m, dirs1), 0, m2), inode0 = mkinode(m, md0, false, # links(m, dirs1), 0, m2), n = ino, content0.stream to m2 = content.stream to m2, m2 < m0 + ino, afs-cons(dirs1, files1), of-cons(of1, dirs1, files1), write-inv(m0, m0 + n1, mkinode(m, md0, false, # links(m, dirs1), 0, m2), buf, 0, dirs0, files0, files0), write-inv(m0, m0 + n1, mkinode(m, md0, false, # links(m, dirs1), 0, m2), buf, ino, dirs0, files0, files), files1 ~ files0, m ∈ files, m ∈ files1, fd ∈ of1, n1 ≤ # buf, (ino2 ≤ m2 ⊃ m2 ≥ ino2;true), err1 = ESUCCESS ∨ ⌊err1⌋ , ⌊err0⌋ ∨ err0 = ESUCCESS ⊦ err0 = ESUCCESS, ino = 0, n1 = 0, (ESUCCESS = ESUCCESS ⊃ (files[m].content.stream to files[m].size).buf = splice(buf, 0, (content0.stream to m2).buf, m0, (ino2 ≤ m2 ⊃ m2 - ino2;0)) ∧ of1[fd, of1[fd].pos:= (ino2 + (ino2 ≤ m2 ⊃ m2 - ino2;0))] = of1[fd, of1[fd].pos:= (m0 + (ino2 ≤ m2 ⊃ m2 - ino2;0))] ∧ (ino2 ≤ m2 ⊃ m2 - ino2;0) ≤ n1 ∧ m ∈ files ∧ files[m].meta = md0 ∧ files -- m = files1 -- m ∧ (mode = MODE_W ∨ mode = MODE_RW) ; files ~ files1 ∧ of1 = of1[fd, of1[fd].pos:= (ino2 + (ino2 ≤ m2 ⊃ m2 - ino2;0))] ∧ ( ESUCCESS = EBADFD ∧ ( fd ∈ of1[fd, of1[fd].pos:= (ino2 + (ino2 ≤ m2 ⊃ m2 - ino2;0))] → of1[fd, of1[fd].pos:= (ino2 + (ino2 ≤ m2 ⊃ m2 - ino2;0))][fd].mode ≠ MODE_W ∧ of1[fd, of1[fd].pos:= (ino2 + (ino2 ≤ m2 ⊃ m2 - ino2;0))][fd].mode ≠ MODE_RW) ∨ ⌊ESUCCESS⌋ ) ), mode ≠ MODE_W ∧ mode ≠ MODE_RW