Proof step 13 from proof refine-writemeta (previous step)

Heuristic symbolic execution applied rule choose right

And obtained the following new goals

• Proof step 14:

  err1 = ESUCCESS, fs = abs-files(files), 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, ⌊err1⌋ ∨ err1 = ESUCCESS ∧ ispath(path, ROOT_INO, ino1, dirs, files) ∧ px-parent(user, path, ROOT_INO, dirs, files) ∨ err1 = ENOENT ∧ ¬ ispath(path, ROOT_INO, dirs, files) ∨ err1 = EACCESS ∧ path ≠ ε ∧ p' ⊑ parent(path) ∧ ispath(p', ROOT_INO, dirs, files) ∧ ¬ px(user, p', ROOT_INO, dirs, files) ⊦ ⟪afs_iget#(ino1, dirs, files, asynced; inode, err1); if err1 = ESUCCESS then if pw(user, inode.meta) then {inode.meta := md; afs_check_commit#(dirs, files; err1; asynced); if err1 = ESUCCESS then afs_write_inode#(inode; err1, dirs, files; asynced)} else err1 := EACCESS⟫ ⟨posix_writemeta#(path, md, user, abs-of(of); err0, root, fs; psynced)⟩ (fs = abs-files(files) ∧ abs(root, ROOT_INO)(dirs) ∧ (psynced → asynced) ∧ err1 = err0)

• Proof step 211:

  err1 = ESUCCESS, fs = abs-files(files), 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, ⌊err1⌋ ∨ err1 = ESUCCESS ∧ ispath(path, ROOT_INO, ino1, dirs, files) ∧ px-parent(user, path, ROOT_INO, dirs, files) ∨ err1 = ENOENT ∧ ¬ ispath(path, ROOT_INO, dirs, files) ∨ err1 = EACCESS ∧ path ≠ ε ∧ p' ⊑ parent(path) ∧ ispath(p', ROOT_INO, dirs, files) ∧ ¬ px(user, p', ROOT_INO, dirs, files) ⊦ ∃ inode. true

Rule argument

Additional information