Proof step 427 from proof inv-rename-dir-dentry (previous step)

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 428:

  dirs0[entries0[str0]] = mkdir(m3, md3, # links(entries0[str0], dirs0), m6, ∅), dirs0[m] = mkdir(m1, md1, # links(m, dirs0), m4, entries0), dirs = dirs0[m, mkdir(m1, md2, # links(m, dirs0), m4, entries0)], ino = inode.ino, inode = mkinode(entries0[str0], md, true, # links(entries0[str0], dirs0), m6, m3), afs-cons(dirs0, files), dcache-cons(dcache, dirs0, files), icache-cons(icache, dirs0, files), pcache-cons(pcache, dirs0, files), synced(dirs0, icache, pcache), m ∈ dirs0, str0 ∈ entries0, entries0[str0] ∈ dirs0, ino ∈ dirs, asynced2 → synced(files, icache, pcache), links(m, dirs0) ≠ ∅ ∨ m = ROOT_INO ⊦ [new_child_inode := (entries0[str0] ∈ dirs[ino, dirs[ino].meta:= inode.meta] ⊃ mkinode (entries0[str0], dirs[ino, dirs[ino].meta:= inode.meta][entries0[str0]].meta, true, dirs[ino, dirs[ino].meta:= inode.meta][entries0[str0]].nlink, dirs[ino, dirs[ino].meta:= inode.meta][entries0[str0]].nsubdirs, dirs[ino, dirs[ino].meta:= inode.meta][entries0[str0]].size) ;mkinode(entries0[str0], files[entries0[str0]].meta, false, files[entries0[str0]].nlink, 0, files[entries0[str0]].size) ); old_parent_inode := (m ∈ dirs[ino, dirs[ino].meta:= inode.meta] ⊃ mkinode (m, dirs[ino, dirs[ino].meta:= inode.meta][m].meta, true, dirs[ino, dirs[ino].meta:= inode.meta][m].nlink, dirs[ino, dirs[ino].meta:= inode.meta][m].nsubdirs, dirs[ino, dirs[ino].meta:= inode.meta][m].size) ;mkinode(m, files[m].meta, false, files[m].nlink, 0, files[m].size) ); new_parent_inode := (m ∈ dirs[ino, dirs[ino].meta:= inode.meta] ⊃ mkinode (m, dirs[ino, dirs[ino].meta:= inode.meta][m].meta, true, dirs[ino, dirs[ino].meta:= inode.meta][m].nlink, dirs[ino, dirs[ino].meta:= inode.meta][m].nsubdirs, dirs[ino, dirs[ino].meta:= inode.meta][m].size) ;mkinode(m, files[m].meta, false, files[m].nlink, 0, files[m].size) ); err := ESUCCESS; asynced := ?] ( afs-cons(dirs[ino, dirs[ino].meta:= inode.meta], files) → ⟪if err = ESUCCESS then let asynced = false in {icache_set#(old_parent_inode, asynced; err, icache); icache_set#(new_parent_inode, asynced; err, icache); if true then icache_set#(new_child_inode, asynced; err, icache); dcache_delete#(old_parent_inode.ino, mkdentry(str0, entries0[str0]).name; err, dcache); dcache_set# (new_parent_inode.ino, mkdentry(mkdentry(str0, entries0[str0]).name, mkdentry(str0, entries0[str0]).ino).name, mkdentry(mkdentry(str0, entries0[str0]).name, mkdentry(str0, entries0[str0]).ino) ; err, dcache)}⟫ ( icache-cons(icache, dirs[ino, dirs[ino].meta:= inode.meta], files) ∧ dcache-cons(dcache, dirs[ino, dirs[ino].meta:= inode.meta], files) ∧ pcache-cons(pcache, dirs[ino, dirs[ino].meta:= inode.meta], files) ∧ synced(dirs[ino, dirs[ino].meta:= inode.meta], icache, pcache) ∧ (asynced2 → synced(files, icache, pcache)))), entries0[str0] = ROOT_INO, ino ∈ files

Rule argument

Additional information