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

Heuristic conditional right split applied rule if right

And obtained the following new goals

• Proof step 814:

  # buf-opt0.buf = VFS_PAGE_SIZE, asynced ↔ cache_asynced, asynced0 ↔ asynced5, ((cache_files ⊕ cache_pcache0) ⊕ cache_icache)[m3] = mkfile(m0, md0, # links(m3, cache_dirs), content0), cache_files[m3] = mkfile(m1, md2, # links(m3, cache_dirs), content1), afs_files = (cache_files ⊕ cache_pcache0) ⊕ cache_icache, buf-opt = buf-opt0, buf-opt1 = buf-opt0, cache_dirs0 = cache_dirs, dirs = cache_dirs, err = err0, files = afs_files, inode = inode0, inode0 = mkinode(m3, md1, false, # links(m3, cache_dirs), 0, m2), inode1 = mkinode(m3, md1, false, # links(m3, cache_dirs), 0, m6), n = m6, pageno = m2 / VFS_PAGE_SIZE, buf-opt0.some?, afs-cons(cache_dirs, cache_files), afs-cons(cache_dirs, (cache_files ⊕ cache_pcache0) ⊕ cache_icache), dcache-cons(cache_dcache, cache_dirs, cache_files), icache-cons(cache_icache, cache_dirs, cache_files), pcache-cons(cache_pcache0, cache_dirs, cache_files), pre-truncate(inode, n, pageno, buf-opt, dirs, files), synced(cache_dirs, cache_icache, cache_pcache0), m3 ∈ cache_files, cache_sync → synced(cache_files, cache_icache, cache_pcache0), ∀ key. key ∈ cache_pcache0 → key.data? ⊦ ⟨let old_ino = 0, size = 0 in afs_truncate_internal#(n, pageno; inode, buf-opt, old_ino, size, asynced0, err, dirs, files; asynced)⟩ ( dirs = cache_dirs0 ∧ files = (cache_files[m3, mkfile(m6, md1, # links(m3, cache_dirs0), content1 upto min(m6, m2))] ⊕ truncate(m3, min(m6, m2), cache_pcache0)) ⊕ cache_icache[m3, mkientry(false, mkinode(m3, md1, false, # links(m3, cache_dirs0), 0, m6))] ∧ (asynced ↔ asynced1) ∧ buf-opt1 = buf-opt ∧ inode1 = inode ∧ ¬ asynced0 ∧ ESUCCESS = err), VFS_PAGE_SIZE = 0, m2 ≤ m6 ∧ m2 % VFS_PAGE_SIZE ≠ 0

• Proof step 1241:

  # buf-opt0.buf = VFS_PAGE_SIZE, asynced ↔ cache_asynced, asynced0 ↔ asynced5, ((cache_files ⊕ cache_pcache0) ⊕ cache_icache)[m3] = mkfile(m0, md0, # links(m3, cache_dirs), content0), cache_files[m3] = mkfile(m1, md2, # links(m3, cache_dirs), content1), afs_files = (cache_files ⊕ cache_pcache0) ⊕ cache_icache, buf-opt = buf-opt0, buf-opt1 = buf-opt0, cache_dirs0 = cache_dirs, dirs = cache_dirs, err = err0, files = afs_files, inode = inode0, inode0 = mkinode(m3, md1, false, # links(m3, cache_dirs), 0, m2), inode1 = mkinode(m3, md1, false, # links(m3, cache_dirs), 0, m6), n = m6, pageno = m2 / VFS_PAGE_SIZE, buf-opt0.some?, afs-cons(cache_dirs, cache_files), afs-cons(cache_dirs, (cache_files ⊕ cache_pcache0) ⊕ cache_icache), dcache-cons(cache_dcache, cache_dirs, cache_files), icache-cons(cache_icache, cache_dirs, cache_files), pcache-cons(cache_pcache0, cache_dirs, cache_files), synced(cache_dirs, cache_icache, cache_pcache0), m3 ∈ cache_files, cache_sync → synced(cache_files, cache_icache, cache_pcache0), ∀ key. key ∈ cache_pcache0 → key.data? ⊦ ⟨abort⟩ ( dirs = cache_dirs0 ∧ files = (cache_files[m3, mkfile(m6, md1, # links(m3, cache_dirs0), content1 upto min(m6, m2))] ⊕ truncate(m3, min(m6, m2), cache_pcache0)) ⊕ cache_icache[m3, mkientry(false, mkinode(m3, md1, false, # links(m3, cache_dirs0), 0, m6))] ∧ (asynced ↔ asynced1) ∧ buf-opt1 = buf-opt ∧ inode1 = inode ∧ ¬ asynced0 ∧ ESUCCESS = err), VFS_PAGE_SIZE = 0, pre-truncate(inode, n, pageno, buf-opt, dirs, files), m2 ≤ m6 ∧ m2 % VFS_PAGE_SIZE ≠ 0

Rule argument

Additional information