Proof step 52 from proof fsync-inode-inv (previous step)

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 53:

  files[m1] = mkfile(m5, md1, m6, content0), files[m] = mkfile(m0, md0, # links(m, dirs), content), icache[m] = mkientry(true, mkinode(m1, md, boolvar, m2, m3, m4)), dirs[m1] = mkdir(m7, md2, m8, m9, entries), err = ESUCCESS, err0 = ESUCCESS, inode = mkinode(m1, md, boolvar, m2, m3, m4), inode.directory, afs-cons(dirs, files), afs-cons(dirs[inode.ino, dirs[inode.ino].meta:= inode.meta], files), dcache-cons(dcache, dirs, files), icache-cons(icache, dirs, files), pcache-cons(pcache, dirs, files), pre-write-inode(inode, dirs, files), synced(dirs, icache, pcache), m ∈ files, m ∈ icache, m1 ∈ dirs ∧ m2 = m8 ∧ m4 = m7 ∧ m3 = m9 ∧ boolvar ∨ m1 ∈ files ∧ m2 = m6 ∧ m3 = 0 ∧ ¬ boolvar ⊦ ⟪if err = ESUCCESS then {asynced := false; icache_set_status#(m, asynced; err, icache)}⟫ ( icache-cons(icache, dirs[inode.ino, dirs[inode.ino].meta:= inode.meta], files) ∧ dcache-cons(dcache, dirs[inode.ino, dirs[inode.ino].meta:= inode.meta], files) ∧ pcache-cons(pcache, dirs[inode.ino, dirs[inode.ino].meta:= inode.meta], files) ∧ synced(dirs[inode.ino, dirs[inode.ino].meta:= inode.meta], icache, pcache) ∧ mkinode(m1, md, boolvar, m2, m3, m4).ino ∈ files ∧ mkinode(m1, md, boolvar, m2, m3, m4).nlink = files[mkinode(m1, md, boolvar, m2, m3, m4).ino].nlink ∧ mkinode(m1, md, boolvar, m2, m3, m4).nsubdirs = 0 ∧ ¬ mkinode(m1, md, boolvar, m2, m3, m4).directory)

Rule argument

Additional information