Proof step 90 from proof write-prepost (previous step)

User applied rule if right

And obtained the following new goals

• Proof step 91:

  ⟨afs_truncate#(m2, m2 / VFS_PAGE_SIZE; buf-opt, inode1, isdir, err0, dirs1, files1, asynced)⟩ (buf-opt = buf-opt0 ∧ inode1 = inode0 ∧ (isdir ↔ isdir0) ∧ err0 = 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, dirs = dirs0, err = err0, err0 = ESUCCESS, content.stream from m2 = σ⊥, inode = mkinode(m, md0, false, # links(m, dirs1), 0, of1[fd].pos + ino), inode0 = mkinode(m, md0, false, # links(m, dirs1), 0, m2), inode1 = mkinode(m, md0, false, # links(m, dirs1), 0, m2), content0.stream to m2 = content.stream to m2, m2 < m0 + ino, afs-cons(dirs1, files1), of-cons(of1, dirs1, files1), pre-write-inode(inode, dirs, files), 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, fd ∈ of1, m ∈ files, m ∈ files1, n1 ≤ # buf, err1 = ESUCCESS ∨ ⌊err1⌋ ⊦ [ {if inode.directory then dirs[inode.ino].meta := inode.meta else {files[inode.ino].meta := inode.meta; files[inode.ino].size := inode.size}; err := ESUCCESS} or fail#(; ; err); asynced := ?; ino2 := of1[fd].pos; n := ino; err0 := err; if err0 ≠ ESUCCESS then n := (ino2 ≤ m2 ⊃ m2 - ino2;0), err0 := ESUCCESS; of := of1[fd, of1[fd].pos:= (ino2 + n)]; file := of1[fd]] (err0 = 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 ∧ (err0 = EBADFD ∧ (fd ∈ of → file.mode ≠ MODE_W ∧ file.mode ≠ MODE_RW) ∨ ⌊err0⌋ ) ), ino = 0, n1 = 0, mode ≠ MODE_W ∧ mode ≠ MODE_RW

• Proof step 187:

  ⟨afs_truncate#(m2, m2 / VFS_PAGE_SIZE; buf-opt, inode1, isdir, err0, dirs1, files1, asynced)⟩ (buf-opt = buf-opt0 ∧ inode1 = inode0 ∧ (isdir ↔ isdir0) ∧ err0 = 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, dirs = dirs0, err = err0, err0 = ESUCCESS, content.stream from m2 = σ⊥, inode = mkinode(m, md0, false, # links(m, dirs1), 0, of1[fd].pos + ino), inode0 = mkinode(m, md0, false, # links(m, dirs1), 0, m2), inode1 = mkinode(m, md0, false, # links(m, dirs1), 0, m2), 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, fd ∈ of1, m ∈ files, m ∈ files1, n1 ≤ # buf, err1 = ESUCCESS ∨ ⌊err1⌋ ⊦ [abort; ino2 := of1[fd].pos; n := ino; err0 := err; if err0 ≠ ESUCCESS then n := (ino2 ≤ m2 ⊃ m2 - ino2;0), err0 := ESUCCESS; of := of1[fd, of1[fd].pos:= (ino2 + n)]; file := of1[fd]] (err0 = 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 ∧ (err0 = EBADFD ∧ (fd ∈ of → file.mode ≠ MODE_W ∧ file.mode ≠ MODE_RW) ∨ ⌊err0⌋ ) ), ino = 0, n1 = 0, pre-write-inode(inode, dirs, files), mode ≠ MODE_W ∧ mode ≠ MODE_RW

Rule argument

Additional information