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

Heuristic conditional right split applied rule if right

And obtained the following new goals

• Proof step 10:

  err = ESUCCESS, files = files1, files0 = files1, n = n1, n0 = n1, of = of1, of0 = of1, afs-cons(dirs, files1), of-cons(of1, dirs, files1), fd ∈ of, n1 ≤ # buf, of[fd].mode ≠ MODE_W → fd ∈ of ⊦ [err := EBADFD; file := of0[fd]] (err = ESUCCESS ⊃ (files[file.ino].content.stream to files[file.ino].size).buf = splice(buf, 0, (files0[file.ino].content.stream to files0[file.ino].size).buf, file.pos, n) ∧ fd ∈ of0 ∧ of = of0[fd, file.pos:= (file.pos + n)] ∧ n ≤ n0 ∧ file.ino ∈ files0 ∧ file.ino ∈ files ∧ files[file.ino].meta = files0[file.ino].meta ∧ files -- file.ino = files0 -- file.ino ∧ (file.mode = MODE_W ∨ file.mode = MODE_RW) ;files ~ files0 ∧ of0 = of ∧ (err = EBADFD ∧ (fd ∈ of → file.mode ≠ MODE_W ∧ file.mode ≠ MODE_RW) ∨ ⌊err⌋ ) ), of[fd].mode = MODE_RW, of[fd].mode = MODE_W

• Proof step 12:

  err = ESUCCESS, files = files1, files0 = files1, n = n1, n0 = n1, of = of1, of0 = of1, afs-cons(dirs, files1), of-cons(of1, dirs, files1), fd ∈ of, n1 ≤ # buf, of[fd].mode ≠ MODE_W → fd ∈ of ⊦ [if n ≠ 0 then choose inode, isdir with true in {afs_iget#(of[fd].ino, dirs, files, asynced; inode, err); if err = ESUCCESS then if inode.directory then err := EISDIR else let ino2 = of[fd].pos, ino1 = of[fd].pos + n, ino0 = 0, pageno = 0, buf-opt = none in {if err = ESUCCESS then pageno := inode.size / VFS_PAGE_SIZE; if err = ESUCCESS then afs_truncate#(inode.size, pageno; buf-opt, inode, isdir, err, dirs, files, asynced); if err = ESUCCESS then vfs_write_loop#(ino2, inode, ino1, buf, dirs; ino0, err, files, asynced); if ino0 ≠ 0 then err := ESUCCESS; if err = ESUCCESS then let ino = inode.size in {n := ino0, ino1 := ino2 + ino0; if ino0 ≠ 0 ∧ ino < ino1 then {inode.size := ino1; afs_check_commit#(dirs, files; err; asynced); if err = ESUCCESS then afs_write_inode#(inode; err, dirs, files; asynced)}; if err ≠ ESUCCESS then n := (ino2 ≤ ino ⊃ ino - ino2;0), err := ESUCCESS; of[fd].pos := ino2 + n}}}; file := of0[fd]] (err = ESUCCESS ⊃ (files[file.ino].content.stream to files[file.ino].size).buf = splice(buf, 0, (files0[file.ino].content.stream to files0[file.ino].size).buf, file.pos, n) ∧ fd ∈ of0 ∧ of = of0[fd, file.pos:= (file.pos + n)] ∧ n ≤ n0 ∧ file.ino ∈ files0 ∧ file.ino ∈ files ∧ files[file.ino].meta = files0[file.ino].meta ∧ files -- file.ino = files0 -- file.ino ∧ (file.mode = MODE_W ∨ file.mode = MODE_RW) ;files ~ files0 ∧ of0 = of ∧ (err = EBADFD ∧ (fd ∈ of → file.mode ≠ MODE_W ∧ file.mode ≠ MODE_RW) ∨ ⌊err⌋ ) ), of[fd].mode ≠ MODE_W ∧ of[fd].mode ≠ MODE_RW

Rule argument

Additional information