Proof step 49 from proof write-term (previous step)

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 50:

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

Rule argument

Additional information