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

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 41:

  ⟨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, ino0 = 0, ino2 = of1[fd].pos, 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, fd ∈ of1, m ∈ files1, 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⌋ ) ⊦ [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}] (err0 = ESUCCESS ⊃ (files0[m].content.stream to files0[m].size).buf = splice(buf, 0, (content0.stream to m1).buf, m0, n) ∧ of = of1[fd, of1[fd].pos:= (m0 + n)] ∧ n ≤ n1 ∧ m ∈ files0 ∧ files0[m].meta = md ∧ files0 -- m = files1 -- m ∧ (mode = MODE_W ∨ mode = MODE_RW) ;files0 ~ files1 ∧ of1 = of ∧ (err0 = EBADFD ∧ (fd ∈ of → of[fd].mode ≠ MODE_W ∧ of[fd].mode ≠ MODE_RW) ∨ ⌊err0⌋ ) ), n1 = 0, mode ≠ MODE_W ∧ mode ≠ MODE_RW

Rule argument

Additional information