Proof step 53 from proof inv-truncate-buff-none-uncached (previous step)

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 54:

  asynced0 ↔ inode.size ≤ n ∧ old_ino ≠ 0 ∧ (pageno ∈ content ∨ buf-opt.some?), files[m] = mkfile(m1, md1, # links(m, dirs), content0), asynced0, buf-opt = none, content = files[inode.ino].content, err = ESUCCESS, ino = inode.ino, inode = mkinode(m, md, false, # links(m, dirs), 0, m2), old_ino = inode.size % VFS_PAGE_SIZE, old_ino0 = 0, pageno = m2 / VFS_PAGE_SIZE, size = min(n, inode.size), size0 = 0, afs-cons(dirs, files), dcache-cons(dcache, dirs, files), icache-cons(icache, dirs, files), pcache-cons(pcache, dirs, files), synced(dirs, icache, pcache), pageno ∈ files[ino].content, m ∈ files, old_ino + (VFS_PAGE_SIZE - old_ino) ≤ # files[ino].content[pageno], VFS_PAGE_SIZE ≥ old_ino, asynced2 → synced(files, icache, pcache) ⊦ [buf-opt := some(fill(files[ino].content[pageno], zero, old_ino, VFS_PAGE_SIZE - old_ino)); files0 := files[ino, files[ino].content:= (content[pageno, fill(files[ino].content[pageno], zero, old_ino, VFS_PAGE_SIZE - old_ino)] upto size)]; let new_inode = inode in {new_inode.size := n; afs_inode_sync#(new_inode; dirs, files0)}; inode := getinode(inode.ino, dirs, files0); err := ESUCCESS; asynced := ?] ( afs-cons(dirs, files0) → ⟪asynced4 := asynced0; if err = ESUCCESS then let asynced = false in {icache_set#(inode, asynced; err, icache); pcache_truncate#(inode.ino, m2, n; err, pcache); if asynced4 then pcache_set#(inode.ino, m2 / VFS_PAGE_SIZE, buf-opt.buf, asynced; err, pcache)}; if ¬ asynced4 ∨ err ≠ ESUCCESS then buf-opt := none⟫ ( icache-cons(icache, dirs, files0) ∧ dcache-cons(dcache, dirs, files0) ∧ pcache-cons(pcache, dirs, files0) ∧ synced(dirs, icache, pcache) ∧ (asynced2 → synced(files0, icache, pcache)))), VFS_PAGE_SIZE = 0, datakey(m, m2 / VFS_PAGE_SIZE) ∈ pcache

Rule argument

Additional information