Proof step 42 from proof refine-writepage (previous step)

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 43:

  # buf = VFS_PAGE_SIZE, dirs = abs-dirs(fs1, ri), err = err0, files = abs-files(fs1, ri), inode = mkinode(m, md, boolvar1, m0, m1, m2), orphans(fs1, ri).inodes?, fo.inodes?, afs-cons(abs-dirs(fs1, ri), abs-files(fs1, ri)), file-node-cons(fs1, ri), log-cons(log0, fs1), orphans-cons(fs1, ri, orphans(fs1, ri)), replay-cons-strong(fs1, ri, orphans(fs1, ri), fi, fo, log0), ri-inj(ri), ri-inj(fi), ubifs-cons(fs1, ri, orphans(fs1, ri), fi, fo, log0), inodekey(m) ∈ ri, asynced0 → boolvar0 ⊦ ⟨fail#(; ; err); asynced0 := ?⟩ ( afs-cons(abs-dirs(fs1, ri), files) → abs-dirs(fs1, ri) = abs-dirs(fs1[adr1, datanode(datakey(m, pageno), buf)], ri[datakey(m, pageno), adr1]) ∧ files = abs-files(fs1[adr1, datanode(datakey(m, pageno), buf)], ri[datakey(m, pageno), adr1]) ∧ orphans (abs-dirs(fs1[adr1, datanode(datakey(m, pageno), buf)], ri[datakey(m, pageno), adr1]), abs-files(fs1[adr1, datanode(datakey(m, pageno), buf)], ri[datakey(m, pageno), adr1])) = abs-keys(orphans(fs1, ri)) ∧ (asynced0 → boolvar2) ∧ ESUCCESS = err), fs1[ri[inodekey(m)]].directory, adr1 ∈ fs1, ∃ asynced. afs-cons(abs-dirs(fs1, ri), files[inode.ino, files[inode.ino].content:= files[inode.ino].content[pageno, buf]]) → abs-dirs(fs1, ri) = abs-dirs(fs1[adr1, datanode(datakey(m, pageno), buf)], ri[datakey(m, pageno), adr1]) ∧ files[inode.ino, files[inode.ino].content:= files[inode.ino].content[pageno, buf]] = abs-files(fs1[adr1, datanode(datakey(m, pageno), buf)], ri[datakey(m, pageno), adr1]) ∧ orphans (abs-dirs(fs1[adr1, datanode(datakey(m, pageno), buf)], ri[datakey(m, pageno), adr1]), abs-files(fs1[adr1, datanode(datakey(m, pageno), buf)], ri[datakey(m, pageno), adr1])) = abs-keys(orphans(fs1, ri)) ∧ (asynced → boolvar2) ∧ ESUCCESS = ESUCCESS

Rule argument

Additional information