Proof step 412 from proof inv-write (previous step)

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 413:

  VFS_PAGE_SIZE = n1 + (m0 + ino0) % VFS_PAGE_SIZE, files0[m] = mkfile(m1, md, # links(m, dirs), content0), of[fd] = mkfile(m, mode, m0), files[m] = mkfile(m2, md0, m3, content), buf = copy(buf0, ino0, content[(m0 + ino0) / VFS_PAGE_SIZE], (m0 + ino0) % VFS_PAGE_SIZE, min(m0 + n0 - m0 + ino0, n1)), err = ESUCCESS, inode = mkinode(m, md, false, # links(m, dirs), 0, m1), pageno = (m0 + ino0) / VFS_PAGE_SIZE, dom of < ino3, afs-cons(dirs, files0), afs-cons(dirs, files), of-cons(of, dirs, files0), of-cons(of, dirs, files), pre-writepage(inode, pageno, buf, dirs, files), (m0 + ino0) / VFS_PAGE_SIZE ∈ content, fd ∈ of, m ∈ files0, ino0 ≤ n0, n0 ≤ # buf0, ino0 ≤ # buf0, (m0 + ino0) % VFS_PAGE_SIZE + min(n0 - ino0, n1) ≤ # content[(m0 + ino0) / VFS_PAGE_SIZE], ino0 + min(n0 - ino0, n1) ≤ # buf0, (m0 + ino0) % VFS_PAGE_SIZE + min(m0 + n0 - m0 + ino0, n1) ≤ # content[(m0 + ino0) / VFS_PAGE_SIZE], ino0 + min(m0 + n0 - m0 + ino0, n1) ≤ # buf0, m0 + n0 ≥ m0 + ino0 ⊦ [err := ESUCCESS; asynced := ?; if err = ESUCCESS then ino3 := ino0 + min(m0 + n0 - m0 + ino0, n1)] ( of-cons(of, dirs, files[inode.ino, files[inode.ino].content:= files[inode.ino].content[pageno, buf]]) ∧ afs-cons(dirs, files[inode.ino, files[inode.ino].content:= files[inode.ino].content[pageno, buf]])), VFS_PAGE_SIZE = 0, min(n0 - ino0, n1) = 0, n0 = 0, mode ≠ MODE_W ∧ mode ≠ MODE_RW, m1 % VFS_PAGE_SIZE ≠ 0 ∧ m1 / VFS_PAGE_SIZE ∈ content0

Rule argument

Additional information