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

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 54:

  # buf = VFS_PAGE_SIZE, pcache[datakey(m, n)] = mkpentry(true, buf), files0[m] = mkfile(m1, md1, # links(m, dirs), content1), files1[m] = mkfile(m1, md1, # links(m, dirs), content0), err = ESUCCESS, files = files1[inode.ino, files1[inode.ino].content:= files1[inode.ino].content[pageno, buf]], inode = mkinode(m, md, false, # links(m, dirs), 0, m2), pageno = n, n * VFS_PAGE_SIZE < m2, afs-cons(dirs, files1), afs-cons(dirs, files0), pcache-cons(pcache1, dirs, files0), pcache-cons(pcache, dirs, files1), m ∈ files0, m ∈ files1, datakey(m, n) ∈ pcache, ∀ key. (key ∈ pcache ↔ key ∈ pcache1) ∧ pcache[key].page = pcache1[key].page ∧ (pcache[key].dirty → pcache1[key].dirty), ∀ pageno. (pageno < n ⊃ (pageno ∈ content0 ↔ pageno ∈ content1 ⊕ mkcontent(m, pcache1)) ∧ content0[pageno] = (content1 ⊕ mkcontent(m, pcache1))[pageno] ;(pageno ∈ content0 ↔ pageno ∈ content1) ∧ content0[pageno] = content1[pageno] ) ⊦ [err := ESUCCESS; asynced := ?] ( afs-cons(dirs, files) → [if err = ESUCCESS then afs_check_commit#(dirs, files; err; asynced1); ino := m; if err = ESUCCESS then {asynced := false; pcache_set_status#(ino, n, asynced; err, pcache)}; n := n + 1] ( pcache-cons(pcache, dirs, files) ∧ mkinode(m, files[m].meta, false, files[m].nlink, 0, files[m].size) = mkinode(m, md1, false, # links(m, dirs), 0, m1) ∧ ino = m ∧ m ∈ 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[m].content ↔ pageno ∈ content1 ⊕ mkcontent(m, pcache1)) ∧ files[m].content[pageno] = (content1 ⊕ mkcontent(m, pcache1))[pageno] ;(pageno ∈ files[m].content ↔ pageno ∈ content1) ∧ files[m].content[pageno] = content1[pageno] )))))

Rule argument

Additional information