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

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 128:

  dirs[entries0[str]] = mkdir(m, md, # links(entries0[str], dirs), m2, entries), dirs[ino1] = mkdir(m0, md0, # links(ino1, dirs), m3, entries0), dent = negdentry((q0 + str0 ').last), err = ESUCCESS, err0 = ENOENT, err1 = ESUCCESS, inode = getinode(ino, dirs, files), inode0 = mkinode(ino1, md0, true, # links(ino1, dirs), m3, m0), p_inode = getinode(mkdentry(str, entries0[str]).ino, dirs, files), mkdentry(str, entries0[str]).dentry?, dom of < ino2, afs-cons(dirs, files), ispath(q, ROOT_INO, ino1, dirs, files), ispath(q0, ROOT_INO, ino, dirs, files), of-cons(of, dirs, files), pre-iget(ino, dirs, files), pw(user, md0), pw(user, md), px(user, md0), px-parent(user, q, ROOT_INO, dirs, files), px-parent(user, q0, ROOT_INO, dirs, files), str ∈ entries0, ino1 ∈ dirs, entries0[str] ∈ dirs, links(ino1, dirs) ≠ ∅ ∨ ino1 = ROOT_INO ⊦ ⟪new_dent := dent; new_dent_inode := p_inode; if err0 = ESUCCESS then afs_check_commit#(dirs, files; err0; asynced); if err0 = ESUCCESS then let dent = new_dent 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); afs_rename#(; old_inode, inode, old_dent_inode, new_dent_inode, old_dent, new_dent, err0, dirs, files; asynced); if dent.dentry? then vfs_put_inode#(new_dent_inode, of, asynced; err0, dirs, files)}⟫ (of-cons(of, dirs, files) ∧ afs-cons(dirs, files)), q0 + str0 ' = ε, entries0[str] = ROOT_INO, inode.directory, q + str ' ⊑ q0 + str0 '

Rule argument

Additional information