| of[fd] = mkfile(m, mode, m0), files[m] = mkfile(m1, md, m2, content), buf = buf0, buf1 = buf0, fs = abs-files(files), ofh = abs-of(of), root.dir?, dom of < ino2, m1 < m0, abs(root, ROOT_INO)(dirs), afs-cons(dirs, files), fids-cons(root, abs-files(files), abs-of(of)), of-cons(of, dirs, files), fd ∈ of, n0 ≤ # buf0, psynced → asynced ⊦ ∃ err. pre-read(fd, n0, err, user, root, fs, ofh) ∧ ⟨err0 := err; if err0 = ESUCCESS then let fh = ofh[fd] in let f = fs[fh.fid] in choose n with n ≤ n0 ∧ fh.pos + n ≤ # f.content in {n0 := n; buf := copy(f.content, fh.pos, buf, 0, n0); ofh[fd].pos := fh.pos + n0} ifnone n0 := 0 else n0 := ?⟩ (ofh = abs-of(of) ∧ (psynced → asynced) ∧ buf1 = buf ∧ 0 = n0 ∧ ESUCCESS = err0), mode ≠ MODE_R ∧ mode ≠ MODE_RW |
files[m] = mkfile(m1, md, m2, content), of[fd] = mkfile(m, mode, m0), buf = buf0, ofh = abs-of(of), root.dir?, m1 < m0, dom of < ino2, abs(root, ROOT_INO)(dirs), afs-cons(dirs, files), fids-cons(root, abs-files(files), abs-of(of)), of-cons(of, dirs, files), fd ∈ of, n0 ≤ # buf0, psynced → asynced ⊦ ∃ err. pre-read(fd, n0, err, user, root, abs-files(files), ofh) ∧ ⟨err0 := err; if err0 = ESUCCESS then let fh = ofh[fd] in let f = abs-files(files)[fh.fid] in choose n with n ≤ n0 ∧ fh.pos + n ≤ # f.content in {n0 := n; buf := copy(f.content, fh.pos, buf, 0, n0); ofh[fd].pos := fh.pos + n0} ifnone n0 := 0 else n0 := ?⟩ (ofh = abs-of(of) ∧ (psynced → asynced) ∧ buf0 = buf ∧ 0 = n0 ∧ ESUCCESS = err0), mode ≠ MODE_R ∧ mode ≠ MODE_RW