Proof step 155 from proof inv-unlink (previous step)

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 156:

  files[entries0[str]] = mkfile(m, md1, # links(entries0[str], dirs), content0), dirs[ino1] = mkdir(m0, md0, # links(ino1, dirs), m2, entries0), c_inode = p_inode0, dent = mkdentry(str, entries0[str]), err = ESUCCESS, inode = mkinode(ino1, md0, true, # links(ino1, dirs), m2, m0), p_ino = p_inode.ino, p_inode = inode, p_inode0 = mkinode(entries0[str], md1, false, # links(entries0[str], dirs), 0, m), dom of < ino0, afs-cons(dirs, files), ispath(q, ROOT_INO, ino1, dirs, files), of-cons(of, dirs, files), pre-unlink(p_inode, c_inode, dent, dirs, files), pw(user, md0), px(user, md0), px-parent(user, q, ROOT_INO, dirs, files), ino1 ∈ dirs, entries0[str] ∈ files, str ∈ entries0, dirs[p_ino, dirs[p_ino].entries:= (dirs[p_ino].entries -- dent.name)][p_ino].size ≥ 1, links(ino1, dirs) ≠ ∅ ∨ ino1 = ROOT_INO ⊦ [let ino = dent.ino in {dirs := dirs[p_ino, dirs[p_ino].entries:= (dirs[p_ino].entries -- dent.name)] [p_ino, dirs[p_ino, dirs[p_ino].entries:= (dirs[p_ino].entries -- dent.name)][p_ino] .size:= (dirs[p_ino, dirs[p_ino].entries:= (dirs[p_ino].entries -- dent.name)][p_ino].size - 1) ]; afs_drop_nlink#(ino; dirs, files)}; dent := negdentry(dent.name); afs_inode_sync#(p_inode; dirs, files); afs_inode_sync#(c_inode; dirs, files); p_inode := getinode(p_inode.ino, dirs, files); c_inode := getinode(c_inode.ino, dirs, files); err := ESUCCESS; asynced := ?] (afs-cons(dirs, files) → ⟪vfs_put_inode#(c_inode, of, asynced; err, dirs, files)⟫ (of-cons(of, dirs, files) ∧ afs-cons(dirs, files))), entries0[str] ∈ dirs

Rule argument

Additional information