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

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 126:

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

Rule argument

Additional information