Proof step 613 from proof inv-renam (previous step)

Heuristic symbolic execution applied rule skip right

And obtained the following new goals

• Proof step 614:

  dirs[ino] = mkdir(m1, md1, # links(ino, dirs), m5, entries1), dirs[ino1] = mkdir(m0, md0, # links(ino1, dirs), m3, entries0), dirs[entries0[str]] = mkdir(m, md, # links(entries0[str], dirs), m2, entries), err = EACCESS, err0 = ENOENT, err1 = ESUCCESS, inode = getinode(ino, dirs, files), inode0 = mkinode(ino, md1, true, # links(ino, dirs), m5, m1), mkdentry(str, entries0[str]).dentry?, dom of < ino2, afs-cons(dirs, files), ispath(q0, ROOT_INO, ino, dirs, files), ispath(q, ROOT_INO, ino1, dirs, files), of-cons(of, dirs, files), pw(user, md), pw(user, md0), px(user, md0), px(user, md1), px-parent(user, q0, ROOT_INO, dirs, files), px-parent(user, q, ROOT_INO, dirs, files), entries0[str] ∈ dirs, ino1 ∈ dirs, ino ∈ dirs, str ∈ entries0, ¬ px(user, inode.meta) ∨ ¬ pw(user, inode.meta), links(ino, dirs) ≠ ∅ ∨ ino = ROOT_INO, links(ino1, dirs) ≠ ∅ ∨ ino1 = ROOT_INO ⊦ ⟪if err = ESUCCESS then let dent = negdentry(str0) in {old_inode := (ino1 ∈ dirs ⊃ mkinode(ino1, md0, true, # links(ino1, dirs), m3, m0) ;mkinode(ino1, files[ino1].meta, false, files[ino1].nlink, 0, files[ino1].size) ); old_dent := mkdentry(str, entries0[str]); old_dent_inode := getinode(mkdentry(str, entries0[str]).ino, dirs, files); new_dent := negdentry(str0); new_dent_inode := getinode(mkdentry(str, entries0[str]).ino, dirs, files); afs_rename#(; old_inode, inode, old_dent_inode, new_dent_inode, old_dent, new_dent, err, dirs, files; asynced); if dent.dentry? then vfs_put_inode#(new_dent_inode, of, asynced; err, dirs, files)}⟫ (of-cons(of, dirs, files) ∧ afs-cons(dirs, files)), entries0[str] = ROOT_INO, str0 ∈ entries1, q + str ' ⊑ q0 + str0 '

Rule argument

Additional information