Proof step 122 from proof refine-truncate-buff-none-cached (previous step)

Heuristic symbolic execution applied rule or right

And obtained the following new goals

• Proof step 123:

  # buf0 = VFS_PAGE_SIZE, VFS_PAGE_SIZE = n0 + m2 % VFS_PAGE_SIZE, cache_pcache0[datakey(m3, m2 / VFS_PAGE_SIZE)] = mkpentry(boolvar, buf0), 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, buf-opt = none, cache_dirs0 = cache_dirs, dirs = cache_dirs, files = afs_files, inode = mkinode(m3, md, false, # links(m3, cache_dirs), 0, m2), n = m, old_ino = 0, pageno = m2 / VFS_PAGE_SIZE, size = 0, 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, datakey(m3, m2 / VFS_PAGE_SIZE) ∈ cache_pcache0, m2 ≤ m, cache_sync → synced(cache_files, cache_icache, cache_pcache0), ∀ key. key ∈ cache_pcache0 → key.data? ⊦ ⟨fail#(; ; err); asynced := ?⟩ ( dirs = cache_dirs0 ∧ files = ( cache_files [m3, mkfile(m, md, # links(m3, cache_dirs0), content1[m2 / VFS_PAGE_SIZE, fill(buf0, zero, m2 % VFS_PAGE_SIZE, n0)] upto m2) ] ⊕ truncate(m3, m2, cache_pcache0)[datakey(m3, m2 / VFS_PAGE_SIZE), mkpentry(false, fill(buf0, zero, m2 % VFS_PAGE_SIZE, n0))]) ⊕ cache_icache[m3, mkientry(false, mkinode(m3, md, false, # links(m3, cache_dirs0), 0, m))] ∧ ¬ asynced ∧ some(fill(buf0, zero, m2 % VFS_PAGE_SIZE, n0)) = buf-opt ∧ (m3 ∈ cache_dirs0 ⊃ mkinode(m3, cache_dirs0[m3].meta, true, cache_dirs0[m3].nlink, cache_dirs0[m3].nsubdirs, cache_dirs0[m3].size) ;mkinode(m3, md, false, # links(m3, cache_dirs0), 0, m) ) = inode ∧ asynced0 ∧ ESUCCESS = err), ⟨let ino = inode.ino, content = files[inode.ino].content, buf = ? in {old_ino := inode.size % VFS_PAGE_SIZE, size := min(n, inode.size); asynced0 := inode.size ≤ n ∧ old_ino ≠ 0 ∧ (pageno ∈ content ∨ buf-opt.some?); if asynced0 then {if buf-opt.some? then buf := buf-opt.buf else buf := files[ino].content[pageno]; buf := fill(buf, zero, old_ino, VFS_PAGE_SIZE - old_ino); content[pageno] := buf; buf-opt := some(buf)}; files[ino].content := content upto size; let new_inode = inode in {new_inode.size := n; afs_inode_sync#(new_inode; dirs, files)}; inode := getinode(inode.ino, dirs, files); err := ESUCCESS}; asynced := ?⟩ ( dirs = cache_dirs0 ∧ files = ( cache_files [m3, mkfile(m, md, # links(m3, cache_dirs0), content1[m2 / VFS_PAGE_SIZE, fill(buf0, zero, m2 % VFS_PAGE_SIZE, n0)] upto m2) ] ⊕ truncate(m3, m2, cache_pcache0)[datakey(m3, m2 / VFS_PAGE_SIZE), mkpentry(false, fill(buf0, zero, m2 % VFS_PAGE_SIZE, n0))]) ⊕ cache_icache[m3, mkientry(false, mkinode(m3, md, false, # links(m3, cache_dirs0), 0, m))] ∧ ¬ asynced ∧ some(fill(buf0, zero, m2 % VFS_PAGE_SIZE, n0)) = buf-opt ∧ (m3 ∈ cache_dirs0 ⊃ mkinode(m3, cache_dirs0[m3].meta, true, cache_dirs0[m3].nlink, cache_dirs0[m3].nsubdirs, cache_dirs0[m3].size) ;mkinode(m3, md, false, # links(m3, cache_dirs0), 0, m) ) = inode ∧ asynced0 ∧ ESUCCESS = err), m2 % VFS_PAGE_SIZE = 0, VFS_PAGE_SIZE = 0

Rule argument

Additional information