Proof step 116 from proof write-prepost-partial (previous step)

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 117:

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

Rule argument

Additional information