Proof step 105 from proof refine-link (previous step)

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 106:

  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, err2 = ESUCCESS, 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) ), 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), px(user, md), px-parent(user, q, ROOT_INO, dirs, files), ino1 ∈ dirs, dent0.name ∈ dirs[p_ino].entries, psynced → asynced ⊦ [if err = ESUCCESS then afs_iget#(dent.ino, dirs, files, asynced; inode, err); if err = ESUCCESS ∧ inode.directory then err := EISDIR; c_inode := inode; old_dent := dent; err1 := err; if err1 = ESUCCESS then let ino = ROOT_INO, dent = negdentry(path'.last), path = parent(path') in {vfs_walk#(path, user, dirs, files, asynced; ino, err1); if err1 = ESUCCESS then vfs_may_create#(ino, dent, user, dirs, files, asynced; inode, err1); new_inode := inode, new_dent := dent}; if err1 = ESUCCESS then afs_check_commit#(dirs, files; err1; asynced); fs := abs-files(files); if err1 = ESUCCESS then afs_link#(old_dent; new_inode, c_inode, new_dent, err1, dirs, files; asynced)] ( of-cons(of, dirs, files) ∧ afs-cons(dirs, files) → ⟨posix_link#(q + str ', path', user, fs, abs-of(of); err0, root; psynced)⟩ (fs = abs-files(files) ∧ abs(root, ROOT_INO)(dirs) ∧ (psynced → asynced) ∧ err1 = err0)), path' = ε

Rule argument

Additional information