Proof step 29 from proof inv-readpage (previous step)

Heuristic conditional right split applied rule if right

And obtained the following new goals

• Proof step 30:

  # buf = VFS_PAGE_SIZE, asynced ↔ asynced1, ESUCCESS = ESUCCESS, err = ESUCCESS, 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(dirs, icache, pcache), m ∈ files, pageno ∈ files[inode.ino].content, ESUCCESS = ESUCCESS → pageno ∈ files[inode.ino].content, asynced2 → synced(files, icache, pcache) ⊦ ⟪let asynced = false in {err := ESUCCESS; pcache_set#(m, pageno, files[inode.ino].content[pageno], asynced; err, pcache)}⟫ (pcache-cons(pcache, dirs, files) ∧ synced(dirs, icache, pcache) ∧ (asynced2 → synced(files, icache, pcache))), files[inode.ino].content[pageno] = zeropage, datakey(m, pageno) ∈ pcache

• Proof step 87:

  # buf = VFS_PAGE_SIZE, asynced ↔ asynced1, err = ESUCCESS, 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(dirs, icache, pcache), m ∈ files, pageno ∈ files[inode.ino].content, ESUCCESS = ESUCCESS → pageno ∈ files[inode.ino].content, asynced2 → synced(files, icache, pcache) ⊦ ⟪skip⟫ (pcache-cons(pcache, dirs, files) ∧ synced(dirs, icache, pcache) ∧ (asynced2 → synced(files, icache, pcache))), datakey(m, pageno) ∈ pcache, ESUCCESS = ESUCCESS ∧ files[inode.ino].content[pageno] ≠ zeropage

• Proof step 88:

  # buf = VFS_PAGE_SIZE, asynced ↔ asynced1, ESUCCESS = ESUCCESS, err = ESUCCESS, 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(dirs, icache, pcache), m ∈ files, pageno ∈ files[inode.ino].content, asynced2 → synced(files, icache, pcache) ⊦ datakey(m, pageno) ∈ pcache, pageno ∈ files[inode.ino].content

Rule argument

Additional information