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

Heuristic conditional right split applied rule if right

And obtained the following new goals

• Proof step 36:

  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} or 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⌋ )

• Proof step 72:

  pcache[datakey(m, n)] = mkpentry(true, buf), err = ESUCCESS, inode = mkinode(m, md, boolvar, m0, m1, m2), pageno = n, n * VFS_PAGE_SIZE < m2, datakey(m, n) ∈ pcache, err0 = ESUCCESS ∨ ⌊err0⌋ ⊦ [abort; 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⌋ ), pre-writepage(inode, pageno, buf, dirs, files)

Rule argument

Additional information