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

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 78:

  # buf = VFS_PAGE_SIZE, asynced ↔ false, files1[m] = mkfile(m0, md, # links(m, dirs), content), files0[m] = mkfile(m0, md, # links(m, dirs), content1), pcache[datakey(m, n)] = mkpentry(true, buf), err = ESUCCESS, ino = m, key = datakey(ino, pageno), pageno = n, n * VFS_PAGE_SIZE < m2, afs-cons(dirs, files0), afs-cons(dirs, files1), afs-cons(dirs, files1[m, mkfile(m0, md, # links(m, dirs), content[n, buf])]), pcache-cons(pcache, dirs, files1), pcache-cons(pcache1, dirs, files0), key ∈ pcache, datakey(m, n) ∈ pcache, m ∈ files1, m ∈ files0, ∀ pageno. (pageno < n ⊃ (pageno ∈ content ↔ pageno ∈ content1 ⊕ mkcontent(m, pcache1)) ∧ content[pageno] = (content1 ⊕ mkcontent(m, pcache1))[pageno] ;(pageno ∈ content ↔ pageno ∈ content1) ∧ content[pageno] = content1[pageno] ), ∀ key. (key ∈ pcache ↔ key ∈ pcache1) ∧ pcache[key].page = pcache1[key].page ∧ (pcache[key].dirty → pcache1[key].dirty) ⊦ pcache-cons(pcache[key, mkpentry(asynced, pcache[key].page)], dirs, files1[m, files1[m].content:= content[n, buf]]) ∧ (∀ key0. (key0 ∈ pcache[key, mkpentry(asynced, pcache[key].page)] ↔ key0 ∈ pcache1) ∧ pcache[key, mkpentry(asynced, pcache[key].page)][key0].page = pcache1[key0].page ∧ (pcache[key, mkpentry(asynced, pcache[key].page)][key0].dirty → pcache1[key0].dirty)) ∧ ( err = ESUCCESS → (∀ pageno. (pageno < n + 1 ⊃ (pageno ∈ content[n, buf] ↔ pageno ∈ content1 ⊕ mkcontent(m, pcache1)) ∧ content[n, buf][pageno] = (content1 ⊕ mkcontent(m, pcache1))[pageno] ;(pageno ∈ content[n, buf] ↔ pageno ∈ content1) ∧ content[n, buf][pageno] = content1[pageno] )))

Rule argument

Additional information