Proof step 1409 from proof refine-truncate-buff-none-uncached (previous step)

Heuristic conditional right split applied rule if right

And obtained the following new goals

• Proof step 1410:

  cache_files[m3] = mkfile(m1, md2, # links(m3, cache_dirs), content1), ((cache_files ⊕ cache_pcache0) ⊕ cache_icache)[m3] = mkfile(m0, md0, # links(m3, cache_dirs), content0), afs_files = ((cache_files ⊕ cache_pcache0) ⊕ cache_icache)[m3, mkfile(m0, md0, # links(m3, cache_dirs), content0 upto min(m6, m2))], cache_dirs0 = cache_dirs, dirs = cache_dirs, files = afs_files, ino = inode.ino, inode = mkinode(m3, md1, false, # links(m3, cache_dirs), 0, m6), 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), ino ∈ dirs, m3 ∈ cache_files, cache_sync → synced(cache_files, cache_icache, cache_pcache0), ∀ key. key ∈ cache_pcache0 → key.data? ⊦ ⟨dirs[ino].meta := inode.meta; inode := (m3 ∈ dirs ⊃ mkinode(m3, dirs[m3].meta, true, dirs[m3].nlink, dirs[m3].nsubdirs, dirs[m3].size) ;mkinode(m3, files[m3].meta, false, files[m3].nlink, 0, files[m3].size) ); err := ESUCCESS; 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 ∧ mkinode(m3, md1, false, # links(m3, cache_dirs0), 0, m6) = inode ∧ ESUCCESS = err), ino ∈ files, datakey(m3, m2 / VFS_PAGE_SIZE) ∈ cache_pcache0, m2 ≤ m6 ∧ m2 % VFS_PAGE_SIZE ≠ 0 ∧ m2 / VFS_PAGE_SIZE ∈ content0, m2 ≤ m6 ∧ m2 % VFS_PAGE_SIZE ≠ 0 ∧ m2 / VFS_PAGE_SIZE ∈ content1

• Proof step 1414:

  cache_files[m3] = mkfile(m1, md2, # links(m3, cache_dirs), content1), ((cache_files ⊕ cache_pcache0) ⊕ cache_icache)[m3] = mkfile(m0, md0, # links(m3, cache_dirs), content0), afs_files = ((cache_files ⊕ cache_pcache0) ⊕ cache_icache)[m3, mkfile(m0, md0, # links(m3, cache_dirs), content0 upto min(m6, m2))], cache_dirs0 = cache_dirs, dirs = cache_dirs, files = afs_files, ino = inode.ino, inode = mkinode(m3, md1, false, # links(m3, cache_dirs), 0, m6), 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? ⊦ ⟨skip; inode := (m3 ∈ dirs ⊃ mkinode(m3, dirs[m3].meta, true, dirs[m3].nlink, dirs[m3].nsubdirs, dirs[m3].size) ;mkinode(m3, files[m3].meta, false, files[m3].nlink, 0, files[m3].size) ); err := ESUCCESS; 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 ∧ mkinode(m3, md1, false, # links(m3, cache_dirs0), 0, m6) = inode ∧ ESUCCESS = err), ino ∈ files, datakey(m3, m2 / VFS_PAGE_SIZE) ∈ cache_pcache0, ino ∈ dirs, m2 ≤ m6 ∧ m2 % VFS_PAGE_SIZE ≠ 0 ∧ m2 / VFS_PAGE_SIZE ∈ content0, m2 ≤ m6 ∧ m2 % VFS_PAGE_SIZE ≠ 0 ∧ m2 / VFS_PAGE_SIZE ∈ content1

Rule argument

Additional information