| files[ino0] = mkfile(m, md, # links(ino0, dirs), content), fd = ino1, fd0 = ino1, fs = abs-files(files), ofh = abs-of(of), root.dir?, dom of < ino2, abs(root, ROOT_INO)(dirs), afs-cons(dirs, files), fids-cons(root, abs-files(files), abs-of(of)), ispath(path, ROOT_INO, ino0, dirs, files), of-cons(of, dirs, files), px-parent(user, path, ROOT_INO, dirs, files), ROOT_INO ∈ dirs, ino0 ∈ files, psynced → asynced, (mode = MODE_R ∨ mode = MODE_RW) ∧ ¬ pr(user, md) ∨ (mode = MODE_W ∨ mode = MODE_RW) ∧ ¬ pw(user, md) ⊦ ⟨choose err with pre-open(path, mode, err, user, root, fs, ofh) in err0 := err; if err0 = ESUCCESS then let fid = root[path].fid in choose n with ¬ n ∈ ofh in {ofh[n] := mkfh(fid, mode, 0); fd := n}⟩ (ofh = abs-of(of) ∧ (psynced → asynced) ∧ fd0 = fd ∧ EACCESS = err0), root[path].dir?, ino0 ∈ dirs |
files[ino0] = mkfile(m, md, # links(ino0, dirs), content), fd = ino1, fd0 = ino1, fs = abs-files(files), ofh = abs-of(of), root.dir?, dom of < ino2, abs(root, ROOT_INO)(dirs), afs-cons(dirs, files), fids-cons(root, abs-files(files), abs-of(of)), ispath(path, ROOT_INO, ino0, dirs, files), of-cons(of, dirs, files), px-parent(user, path, ROOT_INO, dirs, files), ino0 ∈ files, ROOT_INO ∈ dirs, psynced → asynced, (mode = MODE_R ∨ mode = MODE_RW) ∧ ¬ pr(user, md) ∨ (mode = MODE_W ∨ mode = MODE_RW) ∧ ¬ pw(user, md) ⊦ ∃ err. pre-open(path, mode, err, user, root, fs, ofh) ∧ ⟨err0 := err; if err0 = ESUCCESS then let fid = root[path].fid in choose n with ¬ n ∈ ofh in {ofh[n] := mkfh(fid, mode, 0); fd := n}⟩ (ofh = abs-of(of) ∧ (psynced → asynced) ∧ fd0 = fd ∧ EACCESS = err0), root[path].dir?, ino0 ∈ dirs