Proof step 53 from proof fsync-pages-inv (previous step)

Heuristic conditional right split applied rule or split right

And obtained the following new goals

• Proof step 54:

  # buf = VFS_PAGE_SIZE, pcache[datakey(m, n0)] = mkpentry(true, buf), files0[m] = mkfile(m1, md0, # links(m, dirs), content), files[m] = mkfile(m0, md1, # links(m, dirs), content0), err = ESUCCESS, inode = mkinode(m, md, false, # links(m, dirs), 0, m2), pageno = n0, n0 * VFS_PAGE_SIZE < m2, afs-cons(dirs, files0), afs-cons(dirs, files), dcache-cons(dcache, dirs, files), dcache-cons(dcache, dirs, files0), icache-cons(icache, dirs, files), icache-cons(icache, dirs, files0), pcache-cons(pcache, dirs, files), pcache-cons(pcache0, dirs, files0), synced(dirs, icache, pcache), synced(dirs, icache, pcache0), datakey(m, n0) ∈ pcache, m ∈ files, m ∈ files0 ⊦ [files[inode.ino].content[pageno] := buf; err := ESUCCESS; asynced := ?] ( afs-cons(dirs, files) → ⟪if err = ESUCCESS then afs_check_commit#(dirs, files; err; asynced1); n := n0; if err = ESUCCESS then {asynced := false; pcache_set_status#(m, n, asynced; err, pcache)}; n := n + 1⟫ ( icache-cons(icache, dirs, files) ∧ dcache-cons(dcache, dirs, files) ∧ pcache-cons(pcache, dirs, files) ∧ synced(dirs, icache, pcache) ∧ m ∈ files ∧ # links(m, dirs) = files[m].nlink ∧ (m2 + VFS_PAGE_SIZE - n * VFS_PAGE_SIZE) + n0 * VFS_PAGE_SIZE < m2 + VFS_PAGE_SIZE))

• Proof step 312:

  # buf = VFS_PAGE_SIZE, pcache[datakey(m, n0)] = mkpentry(true, buf), files0[m] = mkfile(m1, md0, # links(m, dirs), content), files[m] = mkfile(m0, md1, # links(m, dirs), content0), err = ESUCCESS, inode = mkinode(m, md, false, # links(m, dirs), 0, m2), pageno = n0, n0 * VFS_PAGE_SIZE < m2, afs-cons(dirs, files0), afs-cons(dirs, files), dcache-cons(dcache, dirs, files), dcache-cons(dcache, dirs, files0), icache-cons(icache, dirs, files), icache-cons(icache, dirs, files0), pcache-cons(pcache, dirs, files), pcache-cons(pcache0, dirs, files0), synced(dirs, icache, pcache), synced(dirs, icache, pcache0), datakey(m, n0) ∈ pcache, m ∈ files, m ∈ files0 ⊦ [fail#(; ; err); asynced := ?] ( afs-cons(dirs, files) → ⟪if err = ESUCCESS then afs_check_commit#(dirs, files; err; asynced1); n := n0; if err = ESUCCESS then {asynced := false; pcache_set_status#(m, n, asynced; err, pcache)}; n := n + 1⟫ ( icache-cons(icache, dirs, files) ∧ dcache-cons(dcache, dirs, files) ∧ pcache-cons(pcache, dirs, files) ∧ synced(dirs, icache, pcache) ∧ m ∈ files ∧ # links(m, dirs) = files[m].nlink ∧ (m2 + VFS_PAGE_SIZE - n * VFS_PAGE_SIZE) + n0 * VFS_PAGE_SIZE < m2 + VFS_PAGE_SIZE))

Rule argument

Additional information