Proof step 152 from proof refine-mkdir (previous step)

Heuristic symbolic execution applied rule let right

And obtained the following new goals

• Proof step 153:

  dirs0[ino1] = mkdir(# entries0, md1, # links(ino1, dirs0), m1, entries0), files0 = files, ino = inode.ino, inode = mkinode(ino1, md1, true, # links(ino1, dirs0), m1, # entries0), ((ino2 => mkdir(0, md, 1, 0, ∅) * (λ dirs1. dirs3 = dirs1)))(dirs), root[q].dir?, root.dir?, dom of < ino0, abs(root, ROOT_INO)(dirs0), afs-cons(dirs0, files), fids-cons(root, abs-files(files), abs-of(of)), ispath(q, ROOT_INO, ino1, dirs0, files), of-cons(of, dirs0, files), pw(user, md1), px(user, md1), px-parent(user, q, ROOT_INO, dirs0, files), ino1 ∈ dirs0, ino2 ∈ dirs4, dirs3 ≡ dirs0[ino1, mkdir(# entries0 + 1, md1, # links(ino1, dirs0), m1 + 1, entries0[str, ino2])], dirs4 ≡ dirs3 ++ ino2, dirs ≡ dirs4[ino2, mkdir(0, md, 1, 0, ∅)], psynced → asynced0, links(ino1, dirs0) ≠ ∅ ∨ ino1 = ROOT_INO ⊦ [if ino ∈ files then {files[ino].size := inode.size; files[ino].meta := inode.meta} else if ino ∈ dirs then dirs[ino].meta := inode.meta; inode := (ino1 ∈ dirs ⊃ mkinode(ino1, dirs[ino1].meta, true, dirs[ino1].nlink, dirs[ino1].nsubdirs, dirs[ino1].size) ;mkinode(ino1, files[ino1].meta, false, files[ino1].nlink, 0, files[ino1].size) ); c_inode := getinode(mkdentry(str, ino2).ino, dirs, files); asynced := ?] ( of-cons(of, dirs, files) ∧ afs-cons(dirs, files) → ⟨posix_mkdir#(q + str ', md, user, abs-files(files0), abs-of(of); err2, root; psynced)⟩ (abs-files(files0) = abs-files(files) ∧ abs(root, ROOT_INO)(dirs) ∧ (psynced → asynced) ∧ ESUCCESS = err2)), str ∈ entries0, ino2 ∈ files, ino2 ∈ dirs0, ino2 ∈ dirs3

Rule argument

Additional information