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

Heuristic symbolic execution applied rule let right

And obtained the following new goals

• Proof step 8:

  dent = negdentry(p3.last), ino = ROOT_INO, p = p1, p0 = parent(p3), p3 = p2, dom of < ino0, afs-cons(dirs, files), of-cons(of, dirs, files) ⊦ ⟪vfs_walk#(p0, user, dirs, files, asynced; ino, err); if err = ESUCCESS then let isrename = true in vfs_may_delete#(ino, isrename, user, dirs, files, asynced; inode, dent, p_inode, isdir, err); old_inode := inode; old_dent := dent; old_dent_inode := p_inode; if err = ESUCCESS then let ino = ROOT_INO, dent = negdentry(p.last), p0 = parent(p) in {vfs_walk#(p0, user, dirs, files, asynced; ino, err); if err = ESUCCESS then vfs_may_lookup#(ino, user, dirs, files, asynced; inode, err); if err = ESUCCESS then {afs_lookup#(ino, dirs, files, asynced; dent, err); if err = ENOENT then vfs_may_create#(ino, dent, user, dirs, files, asynced; inode, err) else if err = ESUCCESS then vfs_may_delete_check#(ino, user, dirs, files, asynced; inode, isdir, dent, p_inode, err)}; new_inode := inode; new_dent := dent; new_dent_inode := p_inode}; if err = ESUCCESS then afs_check_commit#(dirs, files; err; asynced); if err = ESUCCESS then let dent = new_dent in {afs_rename#(; old_inode, new_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)), p = ε, p3 = ε, p3 ⊑ p

• Proof step 1661:

  p = p1, p0 = p2, dom of < ino, afs-cons(dirs, files), of-cons(of, dirs, files) ⊦ p = ε, p0 = ε, p0 ⊑ p, p0 ≠ ε ∧ p0 ≠ ε

Rule argument

Additional information