| fs = abs-files(files), of = of0, ofh = abs-of(of), root.dir?, dom of < ino, abs(root, ROOT_INO)(dirs), afs-cons(dirs, files), fids-cons(root, abs-files(files), abs-of(of)), of-cons(of, dirs, files), files0 ~ files, n0 ≤ # buf, psynced → asynced, err1 = EBADFD ∧ (fd ∈ of0 → of0[fd].mode ≠ MODE_W ∧ of0[fd].mode ≠ MODE_RW) ∨ ⌊err1⌋ ⊦ pre-write(fd, buf, n0, err1, user, root, fs, ofh) ∧ ⟨err0 := err1; if err0 = ESUCCESS then let fh = ofh[fd] in let f = fs[fh.fid] in choose n with n ≤ n0 in {n0 := n; f.content := splice(buf, 0, f.content, fh.pos, n0); fs[fh.fid] := f; ofh[fd].pos := fh.pos + n0} else n0 := ?; psynced := ?⟩ (ofh = abs-of(of0) ∧ fs = abs-files(files0) ∧ (psynced → asynced0) ∧ n1 = n0 ∧ err1 = err0), err1 = ESUCCESS |
fs = abs-files(files), ofh = abs-of(of0), err1 ≠ ESUCCESS, root.dir?, dom of0 < ino, abs(root, ROOT_INO)(dirs), afs-cons(dirs, files), fids-cons(root, abs-files(files), abs-of(of0)), of-cons(of0, dirs, files), files0 ~ files, n0 ≤ # buf, psynced → asynced, err1 = EBADFD ∧ (fd ∈ of0 → of0[fd].mode ≠ MODE_W ∧ of0[fd].mode ≠ MODE_RW) ∨ ⌊err1⌋ ⊦ pre-write(fd, buf, n0, err1, user, root, fs, ofh) ∧ ⟨err0 := err1; if err0 = ESUCCESS then let fh = ofh[fd] in let f = fs[fh.fid] in choose n with n ≤ n0 in {n0 := n; f.content := splice(buf, 0, f.content, fh.pos, n0); fs[fh.fid] := f; ofh[fd].pos := fh.pos + n0} else n0 := ?; psynced := ?⟩ (ofh = abs-of(of0) ∧ fs = abs-files(files0) ∧ (psynced → asynced0) ∧ n1 = n0 ∧ err1 = err0)