Proof step 12 from proof refine-truncate-buff-some (previous step)

Heuristic symbolic execution applied rule skip right

And obtained the following new goals

• Proof step 13:

  # buf-opt0.buf = VFS_PAGE_SIZE, asynced ↔ asynced5, afs_asynced ↔ cache_asynced, asynced3 ↔ cache_asynced, asynced4 ↔ asynced, asynced2 ↔ buf-opt.some?, asynced1 ↔ false, asynced0 ↔ false, ((cache_files ⊕ cache_pcache) ⊕ cache_icache)[m] = mkfile(m0, md0, m1, content), afs_dirs = cache_dirs, afs_files = (cache_files ⊕ cache_pcache) ⊕ cache_icache, buf-opt = buf-opt0, dirs = cache_dirs, err = ESUCCESS, err1 = err0, files = cache_files, icache = cache_icache, ino = inode.ino, inode = mkinode(m, md, false, m1, 0, m2), pageno = m2 / VFS_PAGE_SIZE, pcache = cache_pcache, size = inode.size, buf-opt0.some?, 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-truncate(inode, n, pageno, buf-opt, dirs, files), synced(cache_dirs, cache_icache, cache_pcache), m ∈ cache_files, cache_sync → synced(cache_files, cache_icache, cache_pcache) ⊦ ⟪if err = ESUCCESS then afs_truncate#(n, pageno; buf-opt, inode, asynced4, err, dirs, files, asynced3); if err = ESUCCESS then let asynced = false in {icache_set#(inode, asynced; err, icache); pcache_truncate#(inode.ino, size, n; err, pcache); if asynced4 then pcache_set#(inode.ino, pageno, buf-opt.buf, asynced; err, pcache)}; if (¬ asynced4 ∨ err ≠ ESUCCESS) ∧ ¬ asynced2 then buf-opt := none⟫ ⟨inode0 := mkinode(m, md, false, m1, 0, m2); afs_truncate#(n, m2 / VFS_PAGE_SIZE; buf-opt0, inode0, asynced5, err0, afs_dirs, afs_files, afs_asynced)⟩ ( afs_dirs = dirs ∧ afs_files = (files ⊕ pcache) ⊕ icache ∧ (afs_asynced ↔ asynced3) ∧ buf-opt = buf-opt0 ∧ inode = inode0 ∧ (asynced4 ↔ asynced5) ∧ err = err0), VFS_PAGE_SIZE = 0

Rule argument

Additional information