Proof step 120 from proof refine-unlink (previous step)

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 121:

  dirs[ino1] = mkdir(# entries, md, # links(ino1, dirs), m1, entries), dent = mkdentry(dent0.name, dirs[p_ino].entries[dent0.name]), dent0 = negdentry(str), err = ESUCCESS, p_ino = ino1, root.dir?, root[q].dir?, dom of < ino0, abs(root, ROOT_INO)(dirs), afs-cons(dirs, files), fids-cons(root, abs-files(files), abs-of(of)), 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, dent0.name ∈ dirs[p_ino].entries, psynced → asynced ⊦ [err := ESUCCESS; isdir := false; if err = ESUCCESS then {afs_iget#(dent.ino, dirs, files, asynced; p_inode, err); if err = ESUCCESS then {isdir := p_inode.directory; if isdir then if p_inode.ino = ROOT_INO then err := EACCESS else if p_inode.size ≠ 0 then err := ENOTEMPTY}}; isdir0 := isdir; isdir := false; if isdir ∧ ¬ isdir0 then err := ENOTDIR; if ¬ isdir ∧ isdir0 then err := EISDIR; err1 := err; if err1 = ESUCCESS then afs_check_commit#(dirs, files; err1; asynced); fs := abs-files(files); if err1 = ESUCCESS then {inode := (ino1 ∈ dirs ⊃ mkinode(ino1, md, true, # links(ino1, dirs), m1, # entries) ;mkinode(ino1, files[ino1].meta, false, files[ino1].nlink, 0, files[ino1].size) ); afs_unlink#(; inode, p_inode, dent, err1, dirs, files; asynced); vfs_put_inode#(p_inode, of, asynced; err1, dirs, files)}] ( of-cons(of, dirs, files) ∧ afs-cons(dirs, files) → ⟨posix_unlink#(q + str ', user, abs-of(of); err0, root, fs; psynced)⟩ (fs = abs-files(files) ∧ abs(root, ROOT_INO)(dirs) ∧ (psynced → asynced) ∧ err1 = err0))

Rule argument

Additional information