Proof step 20 from proof inv-write_inode (previous step)

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 21:

  err = ESUCCESS, inode = mkinode(m, md, boolvar, m0, m1, m2), inode.directory, afs-cons(dirs[inode.ino, dirs[inode.ino].meta:= inode.meta], files), afs-cons(dirs, 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), asynced2 → synced(files, icache, pcache), m ∈ dirs ∧ m0 = dirs[m].nlink ∧ m2 = dirs[m].size ∧ m1 = dirs[m].nsubdirs ∧ boolvar ∨ m ∈ files ∧ m0 = files[m].nlink ∧ m1 = 0 ∧ ¬ boolvar, asynced2 ∨ boolvar ⊦ ⟪asynced0 := false; inode0 := mkinode(m, md, boolvar, m0, m1, m2); asynced3 := false; if err = ESUCCESS then icache_get#(inode0.ino, icache; asynced3, inode1, err); if err = ESUCCESS ∧ asynced3 then {inode1.meta := inode0.meta; if ¬ inode0.directory then inode1.size := inode0.size; icache_set#(inode1, asynced0; err, icache)} else if asynced0 then err := EFAIL⟫ ( 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) ∧ (asynced2 → synced(files, icache, pcache)))

Rule argument

Additional information