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

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 1606:

  dirs[ino1] = mkdir(m, md, # links(ino1, dirs), m1, entries), dent = negdentry(dent0.name), dent0 = negdentry(str), err = ENOENT, err0 = ESUCCESS, p_ino = ino1, dom of < ino0, afs-cons(dirs, files), ispath(q, ROOT_INO, ino1, dirs, files), of-cons(of, dirs, files), pre-lookup(p_ino, dent0, dirs, files), pw(user, md), px(user, md), px-parent(user, q, ROOT_INO, dirs, files), ino1 ∈ dirs ⊦ ⟪old_dent_inode := p_inode; if err = ESUCCESS then let ino0 = ROOT_INO, dent = negdentry(p.last), p0 = parent(p) in {vfs_walk#(p0, user, dirs, files, asynced; ino0, err); inode := (ino1 ∈ dirs ⊃ mkinode(ino1, md, true, # links(ino1, dirs), m1, m) ;mkinode(ino1, files[ino1].meta, false, files[ino1].nlink, 0, files[ino1].size) ); if err = ESUCCESS then vfs_may_lookup#(ino0, user, dirs, files, asynced; inode, err); if err = ESUCCESS then {afs_lookup#(ino0, dirs, files, asynced; dent, err); if err = ENOENT then vfs_may_create#(ino0, dent, user, dirs, files, asynced; inode, err) else if err = ESUCCESS then vfs_may_delete_check#(ino0, 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 dent0 = new_dent in {old_inode := (ino1 ∈ dirs ⊃ mkinode(ino1, md, true, # links(ino1, dirs), m1, m) ;mkinode(ino1, files[ino1].meta, false, files[ino1].nlink, 0, files[ino1].size) ); afs_rename#(; old_inode, new_inode, old_dent_inode, new_dent_inode, dent, new_dent, err, dirs, files; asynced); if dent0.dentry? then vfs_put_inode#(new_dent_inode, of, asynced; err, dirs, files)}⟫ (of-cons(of, dirs, files) ∧ afs-cons(dirs, files)), p = ε, dent0.name ∈ dirs[p_ino].entries, q + str ' ⊑ p

Rule argument

Additional information