Proof step 36 from proof fsync-pages-err (previous step)

Heuristic conditional right split applied rule or split right

And obtained the following new goals

• Proof step 37:

  pcache[datakey(m, n)] = mkpentry(true, buf), err = ESUCCESS, inode = mkinode(m, md, boolvar, m0, m1, m2), pageno = n, n * VFS_PAGE_SIZE < m2, pre-writepage(inode, pageno, buf, dirs, files), datakey(m, n) ∈ pcache, err0 = ESUCCESS ∨ ⌊err0⌋ ⊦ [files[inode.ino].content[pageno] := buf; err := ESUCCESS; asynced := ?; if err = ESUCCESS then afs_check_commit#(dirs, files; err; asynced1); if err = ESUCCESS then {asynced := false; pcache_set_status#(m, n, asynced; err, pcache)}; n := n + 1] (err = ESUCCESS ∨ ⌊err⌋ )

• Proof step 62:

  pcache[datakey(m, n)] = mkpentry(true, buf), err = ESUCCESS, inode = mkinode(m, md, boolvar, m0, m1, m2), pageno = n, n * VFS_PAGE_SIZE < m2, pre-writepage(inode, pageno, buf, dirs, files), datakey(m, n) ∈ pcache, err0 = ESUCCESS ∨ ⌊err0⌋ ⊦ [fail#(; ; err); asynced := ?; if err = ESUCCESS then afs_check_commit#(dirs, files; err; asynced1); if err = ESUCCESS then {asynced := false; pcache_set_status#(m, n, asynced; err, pcache)}; n := n + 1] (err = ESUCCESS ∨ ⌊err⌋ )

Rule argument

Additional information