| of0[fd] = mkfile(m, mode, m0), ofh[fd] = mkfh(fid, mode0, m1), fs = abs-files(files), ofh = abs-of(of0), 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, fd ∈ of0 → mode ≠ MODE_W ∧ mode ≠ MODE_RW ⊦ (¬ fd ∈ ofh ∨ mode0 ≠ MODE_W ∧ mode0 ≠ MODE_RW) ∧ ⟨err0 := EBADFD; 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 ∧ EBADFD = err0) |
abs-of(of0)[fd] = mkfh(fid, mode0, m1), of0[fd] = mkfile(m, mode, m0), fs = abs-files(files), ofh = abs-of(of0), 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, fd ∈ of0 → mode ≠ MODE_W ∧ mode ≠ MODE_RW, psynced → asynced ⊦ (¬ fd ∈ ofh ∨ mode0 ≠ MODE_W ∧ mode0 ≠ MODE_RW) ∧ ⟨err0 := EBADFD; 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 ∧ EBADFD = err0)