Proof step 17 from proof inv-writepage (previous step)

Heuristic conditional right split applied rule or split right

And obtained the following new goals

• Proof step 18:

  # buf = VFS_PAGE_SIZE, inode = mkinode(m, md, boolvar, m0, m1, m2), afs-cons(dirs, files), dcache-cons(dcache, dirs, files), icache-cons(icache, dirs, files), pcache-cons(pcache, dirs, files), synced(files, icache, pcache), synced(dirs, icache, pcache), m ∈ files ⊦ [files[inode.ino].content[pageno] := buf; err := ESUCCESS; asynced := ?] ( afs-cons(dirs, files) → ⟪asynced2 := false; if err = ESUCCESS then pcache_set#(m, pageno, buf, asynced2; err, pcache)⟫ ( icache-cons(icache, dirs, files) ∧ dcache-cons(dcache, dirs, files) ∧ pcache-cons(pcache, dirs, files) ∧ synced(dirs, icache, pcache) ∧ synced(files, icache, pcache)))

• Proof step 137:

  # buf = VFS_PAGE_SIZE, inode = mkinode(m, md, boolvar, m0, m1, m2), afs-cons(dirs, files), dcache-cons(dcache, dirs, files), icache-cons(icache, dirs, files), pcache-cons(pcache, dirs, files), synced(files, icache, pcache), synced(dirs, icache, pcache), m ∈ files ⊦ [fail#(; ; err); asynced := ?] ( afs-cons(dirs, files) → ⟪asynced2 := false; if err = ESUCCESS then pcache_set#(m, pageno, buf, asynced2; err, pcache)⟫ ( icache-cons(icache, dirs, files) ∧ dcache-cons(dcache, dirs, files) ∧ pcache-cons(pcache, dirs, files) ∧ synced(dirs, icache, pcache) ∧ synced(files, icache, pcache)))

Rule argument

Additional information