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

Heuristic conditional right split applied rule or split right

And obtained the following new goals

• Proof step 46:

  files[m] = mkfile(m1, md1, # links(m, dirs), content0), buf-opt = none, err = ESUCCESS, inode = mkinode(m, md, false, # links(m, dirs), 0, m2), old_ino = 0, pageno = m2 / VFS_PAGE_SIZE, size = 0, 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, asynced2 → synced(files, icache, pcache) ⊦ [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 := ?] ( 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, buf-opt.buf, asynced; err, pcache)}; if ¬ asynced4 ∨ err ≠ ESUCCESS then buf-opt := 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, datakey(m, m2 / VFS_PAGE_SIZE) ∈ pcache

• Proof step 409:

  files[m] = mkfile(m1, md1, # links(m, dirs), content0), buf-opt = none, err = ESUCCESS, inode = mkinode(m, md, false, # links(m, dirs), 0, m2), old_ino = 0, pageno = m2 / VFS_PAGE_SIZE, size = 0, 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, asynced2 → synced(files, icache, pcache) ⊦ [fail#(; ; err); 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, buf-opt.buf, asynced; err, pcache)}; if ¬ asynced4 ∨ err ≠ ESUCCESS then buf-opt := 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, datakey(m, m2 / VFS_PAGE_SIZE) ∈ pcache

Rule argument

Additional information