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

Heuristic symbolic execution applied rule skip right

And obtained the following new goals

• Proof step 191:

  isdir1 ↔ true, isdir ↔ true, isdir0 ↔ isdir, dirs[entries0[str]] = mkdir(m, md, # links(entries0[str], dirs), m2, entries), dirs[ino1] = mkdir(m0, md0, # links(ino1, dirs), m3, entries0), dirs[ino] = mkdir(m1, md1, # links(ino, dirs), m5, entries1), dent = mkdentry(str0, entries1[str0]), err = EACCESS, err0 = ESUCCESS, err1 = ESUCCESS, inode = getinode(ino, dirs, files), inode0 = mkinode(ino, md1, true, # links(ino, dirs), m5, m1), p_inode = mkinode(entries0[str], md, true, # links(entries0[str], dirs), m2, m), 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), pw(user, md0), pw(user, md), px(user, md1), px(user, md0), px-parent(user, q, ROOT_INO, dirs, files), px-parent(user, q0, ROOT_INO, dirs, files), str0 ∈ entries1, ino ∈ dirs, ino1 ∈ dirs, entries0[str] ∈ dirs, str ∈ entries0, links(ino1, dirs) ≠ ∅ ∨ ino1 = ROOT_INO, links(ino, dirs) ≠ ∅ ∨ ino = ROOT_INO, ¬ px(user, inode.meta) ∨ ¬ pw(user, inode.meta) ⊦ ⟪if ¬ isdir1 ∧ isdir0 then err := EISDIR; 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 {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, 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)), entries0[str] = ROOT_INO, q + str ' ⊑ q0 + str0 '

Rule argument

Additional information