Proof step 11 from proof refine-write_inode (previous step)

Heuristic conditional right split applied rule if right

And obtained the following new goals

• Proof step 12:

  afs_dirs = cache_dirs, afs_files = (cache_files ⊕ cache_pcache) ⊕ cache_icache, dirs = cache_dirs, err = err0, files = cache_files, inode = mkinode(m, md, boolvar, m0, m1, m2), afs-cons(cache_dirs, cache_files), afs-cons(cache_dirs, (cache_files ⊕ cache_pcache) ⊕ cache_icache), dcache-cons(cache_dcache, cache_dirs, cache_files), icache-cons(cache_icache, cache_dirs, cache_files), pcache-cons(cache_pcache, cache_dirs, cache_files), pre-write-inode(inode, dirs, files), synced(cache_dirs, cache_icache, cache_pcache), cache_sync → synced(cache_files, cache_icache, cache_pcache), m ∈ cache_dirs ∧ m0 = cache_dirs[m].nlink ∧ m2 = cache_dirs[m].size ∧ m1 = cache_dirs[m].nsubdirs ∧ boolvar ∨ m ∈ cache_files ∧ m0 = ((cache_files ⊕ cache_pcache) ⊕ cache_icache)[m].nlink ∧ m1 = 0 ∧ ¬ boolvar, m ∈ cache_dirs ∧ m0 = cache_dirs[m].nlink ∧ m2 = cache_dirs[m].size ∧ m1 = cache_dirs[m].nsubdirs ∧ boolvar ∨ m ∈ cache_files ∧ m0 = cache_files[m].nlink ∧ m1 = 0 ∧ ¬ boolvar, cache_sync ∨ boolvar ⊦ ⟪ {if inode.directory then dirs[inode.ino].meta := inode.meta else {files[inode.ino].meta := inode.meta; files[inode.ino].size := inode.size}; err := ESUCCESS} or fail#(; ; err); asynced := ?; asynced0 := false; inode0 := mkinode(m, md, boolvar, m0, m1, m2); asynced2 := false; if err = ESUCCESS then icache_get#(inode0.ino, cache_icache; asynced2, inode, err); if err = ESUCCESS ∧ asynced2 then {inode.meta := inode0.meta; if ¬ inode0.directory then inode.size := inode0.size; icache_set#(inode, asynced0; err, cache_icache)} else if asynced0 then err := EFAIL⟫ ⟨afs_write_inode#(mkinode(m, md, boolvar, m0, m1, m2); err0, afs_dirs, afs_files; afs_asynced)⟩ (afs_dirs = dirs ∧ afs_files = (files ⊕ cache_pcache) ⊕ cache_icache ∧ (afs_asynced ↔ asynced) ∧ err = err0)

• Proof step 281:

  afs_dirs = cache_dirs, afs_files = (cache_files ⊕ cache_pcache) ⊕ cache_icache, dirs = cache_dirs, err = err0, files = cache_files, inode = mkinode(m, md, boolvar, m0, m1, m2), afs-cons(cache_dirs, cache_files), afs-cons(cache_dirs, (cache_files ⊕ cache_pcache) ⊕ cache_icache), dcache-cons(cache_dcache, cache_dirs, cache_files), icache-cons(cache_icache, cache_dirs, cache_files), pcache-cons(cache_pcache, cache_dirs, cache_files), synced(cache_dirs, cache_icache, cache_pcache), cache_sync → synced(cache_files, cache_icache, cache_pcache), m ∈ cache_dirs ∧ m0 = cache_dirs[m].nlink ∧ m2 = cache_dirs[m].size ∧ m1 = cache_dirs[m].nsubdirs ∧ boolvar ∨ m ∈ cache_files ∧ m0 = ((cache_files ⊕ cache_pcache) ⊕ cache_icache)[m].nlink ∧ m1 = 0 ∧ ¬ boolvar, m ∈ cache_dirs ∧ m0 = cache_dirs[m].nlink ∧ m2 = cache_dirs[m].size ∧ m1 = cache_dirs[m].nsubdirs ∧ boolvar ∨ m ∈ cache_files ∧ m0 = cache_files[m].nlink ∧ m1 = 0 ∧ ¬ boolvar, cache_sync ∨ boolvar ⊦ ⟪abort; asynced0 := false; inode0 := mkinode(m, md, boolvar, m0, m1, m2); asynced2 := false; if err = ESUCCESS then icache_get#(inode0.ino, cache_icache; asynced2, inode, err); if err = ESUCCESS ∧ asynced2 then {inode.meta := inode0.meta; if ¬ inode0.directory then inode.size := inode0.size; icache_set#(inode, asynced0; err, cache_icache)} else if asynced0 then err := EFAIL⟫ ⟨afs_write_inode#(mkinode(m, md, boolvar, m0, m1, m2); err0, afs_dirs, afs_files; afs_asynced)⟩ (afs_dirs = dirs ∧ afs_files = (files ⊕ cache_pcache) ⊕ cache_icache ∧ (afs_asynced ↔ asynced) ∧ err = err0), pre-write-inode(inode, dirs, files)

Rule argument

Additional information