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

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 231:

  asynced ↔ asynced3, ¬ asynced3, err = ESUCCESS, err0 = ESUCCESS, ino = m, inode = inode1, afs-cons(dirs, files), afs-cons(dirs, files[m, (files[m].meta:= md).size:= m2]), dcache-cons(dcache, dirs, files), icache-cons(icache, dirs, files), pcache-cons(pcache, dirs, files), synced(files, icache, pcache), synced(dirs, icache, pcache), ino ∈ icache, m ∈ files ⊦ ⟪icache_set#((icache[ino].inode.meta:= md).size:= m2, false; err, icache)⟫ ( icache-cons(icache, dirs, files[m, (files[m].meta:= md).size:= m2]) ∧ dcache-cons(dcache, dirs, files[m, (files[m].meta:= md).size:= m2]) ∧ pcache-cons(pcache, dirs, files[m, (files[m].meta:= md).size:= m2]) ∧ synced(dirs, icache, pcache) ∧ synced(files[m, (files[m].meta:= md).size:= m2], icache, pcache))

Rule argument

Additional information