Proof step 11 from proof refine-truncate (previous step)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  err = err0, ino = ROOT_INO, root.dir?, dom of < ino0, abs(root, ROOT_INO)(dirs), afs-cons(dirs, files), fids-cons(root, abs-files(files), abs-of(of)), of-cons(of, dirs, files), psynced → asynced ⊦ [vfs_walk#(path, user, dirs, files, asynced; ino, err)] ( ⌊err⌋ ∨ err = ESUCCESS ∧ ispath(path, ROOT_INO, ino, dirs, files) ∧ px-parent(user, path, ROOT_INO, dirs, files) ∨ err = ENOENT ∧ ¬ ispath(path, ROOT_INO, dirs, files) ∨ err = EACCESS ∧ path ≠ ε ∧ (∃ p'. p' ⊑ parent(path) ∧ ispath(p', ROOT_INO, dirs, files) ∧ ¬ px(user, p', ROOT_INO, dirs, files)) → [if err = ESUCCESS then let isdir = false in vfs_may_open#(ino, isdir, MODE_W, user, dirs, files, asynced; inode, err); if err = ESUCCESS then afs_check_commit#(dirs, files; err; asynced); pageno := 0; if err = ESUCCESS then pageno := inode.size / VFS_PAGE_SIZE; fs := abs-files(files); if err = ESUCCESS then {buf-opt := none; afs_truncate#(n, pageno; buf-opt, inode, isdir0, err, dirs, files, asynced)}] ( of-cons(of, dirs, files) ∧ afs-cons(dirs, files) → ⟨posix_truncate#(path, n, user, root, abs-of(of); err0, fs; psynced)⟩ (fs = abs-files(files) ∧ abs(root, ROOT_INO)(dirs) ∧ (psynced → asynced) ∧ err = err0)))

Rule argument

Additional information