Proof step 22 from proof fsync-pages-overwrite (previous step)

Heuristic conditional right split applied rule if right

And obtained the following new goals

• Proof step 23:

  files[m] = mkfile(m0, md0, # links(m, dirs), content0), files0[m] = mkfile(m0, md0, # links(m, dirs), content), err = ESUCCESS, ino = m, ino0 = m, inode = mkinode(m, md, false, # links(m, dirs), 0, m2), key = datakey(ino0, pageno), pageno = n, pcache[key].dirty, n * VFS_PAGE_SIZE < m2, afs-cons(dirs, files), afs-cons(dirs, files0), pcache-cons(pcache, dirs, files), pcache-cons(pcache1, dirs, files0), m ∈ files, m ∈ files0, key ∈ pcache, ∀ pageno. (pageno < n ⊃ (pageno ∈ content0 ↔ pageno ∈ content ⊕ mkcontent(m, pcache1)) ∧ content0[pageno] = (content ⊕ mkcontent(m, pcache1))[pageno] ;(pageno ∈ content0 ↔ pageno ∈ content) ∧ content0[pageno] = content[pageno] ), ∀ key. (key ∈ pcache ↔ key ∈ pcache1) ∧ pcache[key].page = pcache1[key].page ∧ (pcache[key].dirty → pcache1[key].dirty) ⊦ [let buf = ? in {asynced0 := true; pcache_get#(ino, n, pcache; asynced0, buf, err); if err = ESUCCESS then afs_writepage#(inode, n, buf, dirs; err, files; asynced1); if err = ESUCCESS then afs_check_commit#(dirs, files; err; asynced1); if err = ESUCCESS then {asynced := false; pcache_set_status#(ino, n, asynced; err, pcache)}}; n := n + 1] ( afs-cons(dirs, files) ∧ pcache-cons(pcache, dirs, files) ∧ mkinode(inode.ino, files[inode.ino].meta, false, files[inode.ino].nlink, 0, files[inode.ino].size) = mkinode(inode.ino, files0[inode.ino].meta, false, files0[inode.ino].nlink, 0, files0[inode.ino].size) ∧ ino = inode.ino ∧ inode.ino ∈ files ∧ (∀ key. (key ∈ pcache ↔ key ∈ pcache1) ∧ pcache[key].page = pcache1[key].page ∧ (pcache[key].dirty → pcache1[key].dirty)) ∧ ( err = ESUCCESS → (∀ pageno. (pageno < n ⊃ (pageno ∈ files[inode.ino].content ↔ pageno ∈ files0[inode.ino].content ⊕ mkcontent(inode.ino, pcache1)) ∧ files[inode.ino].content[pageno] = (files0[inode.ino].content ⊕ mkcontent(inode.ino, pcache1))[pageno] ; (pageno ∈ files[inode.ino].content ↔ pageno ∈ files0[inode.ino].content) ∧ files[inode.ino].content[pageno] = files0[inode.ino].content[pageno] ))))

• Proof step 189:

  files[m] = mkfile(m0, md0, # links(m, dirs), content0), files0[m] = mkfile(m0, md0, # links(m, dirs), content), err = ESUCCESS, ino = m, ino0 = m, inode = mkinode(m, md, false, # links(m, dirs), 0, m2), key = datakey(ino0, pageno), pageno = n, n * VFS_PAGE_SIZE < m2, afs-cons(dirs, files), afs-cons(dirs, files0), pcache-cons(pcache, dirs, files), pcache-cons(pcache1, dirs, files0), m ∈ files, m ∈ files0, key ∈ pcache, ∀ pageno. (pageno < n ⊃ (pageno ∈ content0 ↔ pageno ∈ content ⊕ mkcontent(m, pcache1)) ∧ content0[pageno] = (content ⊕ mkcontent(m, pcache1))[pageno] ;(pageno ∈ content0 ↔ pageno ∈ content) ∧ content0[pageno] = content[pageno] ), ∀ key. (key ∈ pcache ↔ key ∈ pcache1) ∧ pcache[key].page = pcache1[key].page ∧ (pcache[key].dirty → pcache1[key].dirty) ⊦ [skip; n := n + 1] ( afs-cons(dirs, files) ∧ pcache-cons(pcache, dirs, files) ∧ mkinode(inode.ino, files[inode.ino].meta, false, files[inode.ino].nlink, 0, files[inode.ino].size) = mkinode(inode.ino, files0[inode.ino].meta, false, files0[inode.ino].nlink, 0, files0[inode.ino].size) ∧ ino = inode.ino ∧ inode.ino ∈ files ∧ (∀ key. (key ∈ pcache ↔ key ∈ pcache1) ∧ pcache[key].page = pcache1[key].page ∧ (pcache[key].dirty → pcache1[key].dirty)) ∧ ( err = ESUCCESS → (∀ pageno. (pageno < n ⊃ (pageno ∈ files[inode.ino].content ↔ pageno ∈ files0[inode.ino].content ⊕ mkcontent(inode.ino, pcache1)) ∧ files[inode.ino].content[pageno] = (files0[inode.ino].content ⊕ mkcontent(inode.ino, pcache1))[pageno] ; (pageno ∈ files[inode.ino].content ↔ pageno ∈ files0[inode.ino].content) ∧ files[inode.ino].content[pageno] = files0[inode.ino].content[pageno] )))), true ∧ pcache[key].dirty

Rule argument

Additional information