Proof step 210 from proof refine-rmdir (previous step)

Heuristic symbolic execution applied rule skip right

And obtained the following new goals

• Proof step 211:

  # entries0 = m + 1, dirs0[entries0[str]] = mkdir(0, md, # links(entries0[str], dirs0), m3, ∅), dirs0[ino1] = mkdir(m + 1, md2, # links(ino1, dirs0), m2, entries0), root[q + str '] = dnode(md1, ∅), fs = abs-files(files), ino = mkdentry(str, entries0[str]).ino, mkdentry(str, entries0[str]).dentry?, root.dir?, root[q].dir?, dom of < ino0, abs(root, ROOT_INO)(dirs0), afs-cons(dirs0, files), fids-cons(root, abs-files(files), abs-of(of)), ispath(q, ROOT_INO, ino1, dirs0, files), of-cons(of, dirs0, files), pw(user, md2), px(user, md2), px-parent(user, q, ROOT_INO, dirs0, files), str ∈ entries0, ino1 ∈ dirs0, entries0[str] ∈ dirs0, ino ∈ dirs1, dirs1 ≡ dirs0[ino1, mkdir(m, md2, # links(ino1, dirs0), m2 - 1, entries0 -- str)], dirs ≡ dirs1[ino, dirs1[ino].nlink:= (dirs1[ino].nlink - 1)], 1 ≤ m2, dirs1[ino].nlink ≥ 1, psynced → asynced0, links(ino1, dirs0) ≠ ∅ ∨ ino1 = ROOT_INO ⊦ [dent := negdentry(mkdentry(str, entries0[str]).name); afs_inode_sync#(mkinode(ino1, md2, true, # links(ino1, dirs0), m2, m + 1); dirs, files); afs_inode_sync#(mkinode(entries0[str], md, true, # links(entries0[str], dirs0), m3, 0); dirs, files); inode := (ino1 ∈ dirs ⊃ mkinode(ino1, dirs[ino1].meta, true, dirs[ino1].nlink, dirs[ino1].nsubdirs, dirs[ino1].size) ;mkinode(ino1, files[ino1].meta, false, files[ino1].nlink, 0, files[ino1].size) ); c_inode := getinode(entries0[str], dirs, files); err := ESUCCESS; asynced := ?; vfs_put_inode#(c_inode, of, asynced; err, dirs, files)] ( of-cons(of, dirs, files) ∧ afs-cons(dirs, files) → ⟨posix_rmdir#(q + str ', user, fs, abs-of(of); err1, root; psynced)⟩ (fs = abs-files(files) ∧ abs(root, ROOT_INO)(dirs) ∧ (psynced → asynced) ∧ err = err1)), entries0 = ∅, m2 = 0

Rule argument

Additional information