Proof step 74 from proof inv-truncate-buff-none-cached (previous step)

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 75:

  # buf0 = VFS_PAGE_SIZE, asynced0 ↔ inode.size ≤ n ∧ old_ino ≠ 0 ∧ (pageno ∈ content ∨ buf-opt.some?), files[m] = mkfile(m1, md1, # links(m, dirs), content0), pcache[datakey(m, m2 / VFS_PAGE_SIZE)] = mkpentry(boolvar, buf0), asynced0, buf-opt = some(buf0), 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, buf-opt.some?, afs-cons(dirs, files), dcache-cons(dcache, dirs, files), icache-cons(icache, dirs, files), pcache-cons(pcache, dirs, files), synced(dirs, icache, pcache), m ∈ files, datakey(m, m2 / VFS_PAGE_SIZE) ∈ pcache, old_ino + (VFS_PAGE_SIZE - old_ino) ≤ # buf-opt.buf, VFS_PAGE_SIZE ≥ old_ino, asynced2 → synced(files, icache, pcache) ⊦ [let new_inode = inode in {new_inode.size := n; files[ino].content := content[pageno, fill(buf-opt.buf, zero, old_ino, VFS_PAGE_SIZE - old_ino)] upto size; afs_inode_sync#(new_inode; dirs, files)}; inode := getinode(inode.ino, dirs, files); err := ESUCCESS; asynced := ?] ( afs-cons(dirs, files) → ⟪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, some(fill(buf-opt.buf, zero, old_ino, VFS_PAGE_SIZE - old_ino)).buf, asynced; err, pcache)}; if ¬ asynced4 ∨ err ≠ ESUCCESS then buf-opt0 := none⟫ ( icache-cons(icache, dirs, files) ∧ dcache-cons(dcache, dirs, files) ∧ pcache-cons(pcache, dirs, files) ∧ synced(dirs, icache, pcache) ∧ (asynced2 → synced(files, icache, pcache)))), VFS_PAGE_SIZE = 0

Rule argument

Additional information