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

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 54:

  of[fd] = mkfile(m, mode, m0), files[m] = mkfile(m1, md, # links(m, dirs), content0), buf-opt = none, content = files[inode.ino].content, dirs1 = dirs, err = ESUCCESS, ino = inode.ino, ino0 = min(n, inode.size), ino1 = inode.size % VFS_PAGE_SIZE, ino2 = 0, ino5 = 0, ino6 = ino2, ino7 = ino5, inode = mkinode(m, md, false, # links(m, dirs), 0, m1), n = m1, new_inode = inode, pageno = m1 / VFS_PAGE_SIZE, dom of < ino3, afs-cons(dirs, files), of-cons(of, dirs, files), pageno ∈ files[ino].content, m ∈ files, fd ∈ of, inode.size ≤ n, n0 ≤ # buf0, ino1 + (VFS_PAGE_SIZE - ino1) ≤ # files[ino].content[pageno], VFS_PAGE_SIZE ≥ ino1, pageno ∈ content ∨ buf-opt.some? ⊦ [files0 := files[ino, files[ino].content:= (content[pageno, fill(files[ino].content[pageno], zero, ino1, VFS_PAGE_SIZE - ino1)] upto ino0)]; afs_inode_sync#(new_inode.size:= n; dirs, files0); inode := getinode(inode.ino, dirs, files0); err := ESUCCESS; asynced := ?; ino4 := 0; if err = ESUCCESS then vfs_write_loop#(m0, inode, m0 + n0, buf0, dirs; ino4, err, files0, asynced); if ino4 ≠ 0 then err := ESUCCESS; if err = ESUCCESS then let ino = inode.size in {n0 := ino4, ino1 := m0 + ino4; if ino4 ≠ 0 ∧ ino < ino1 then {inode.size := ino1; afs_check_commit#(dirs, files0; err; asynced); if err = ESUCCESS then afs_write_inode#(inode; err, dirs, files0; asynced)}; if err ≠ ESUCCESS then n0 := (m0 ≤ ino ⊃ ino - m0;0), err := ESUCCESS; of[fd].pos := m0 + n0}] (dirs1 = dirs → of-cons(of, dirs, files0) ∧ dom of < ino3 ∧ afs-cons(dirs, files0)), VFS_PAGE_SIZE = 0, ino1 = 0, n0 = 0, mode ≠ MODE_W ∧ mode ≠ MODE_RW

Rule argument

Additional information