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

Heuristic symbolic execution applied rule choose right

And obtained the following new goals

• Proof step 46:

  # buf = VFS_PAGE_SIZE, fo.inodes?, orphans(fs1, ri).inodes?, afs-cons(abs-dirs(fs1, ri), abs-files(fs1, ri)), afs-cons (abs-dirs(fs1, ri), abs-files(fs1, ri)[m, mkfile(fs1[ri[inodekey(m)]].size, fs1[ri[inodekey(m)]].meta, fs1[ri[inodekey(m)]].nlink, abs-content(m, fs1, ri)[pageno, buf])]), 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(fi), ri-inj(ri), ubifs-cons(fs1, ri, orphans(fs1, ri), fi, fo, log0), inodekey(m) ∈ ri, asynced0 → boolvar0 ⊦ ∃ err0. ⌊err0⌋ ∧ ⟨err := err0; asynced0 := ?⟩ ( abs-dirs(fs1, ri) = abs-dirs(fs1[adr1, datanode(datakey(m, pageno), buf)], ri[datakey(m, pageno), adr1]) ∧ abs-files(fs1, ri) = 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, abs-dirs(fs1, ri) = abs-dirs(fs1[adr1, datanode(datakey(m, pageno), buf)], ri[datakey(m, pageno), adr1]) ∧ abs-files(fs1, ri) [m, mkfile(fs1[ri[inodekey(m)]].size, fs1[ri[inodekey(m)]].meta, fs1[ri[inodekey(m)]].nlink, abs-content(m, fs1, ri)[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))

Rule argument

Additional information