| of[fd] = mkfile(m3, mode0, m4), files[m3] = mkfile(m1, md, m2, content), buf = buf0, 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)), of-cons(of, dirs, files), read-inv(m4, m4 + n0, mkinode(m3, md, false, m2, 0, m1), buf0, buf1, 0, dirs, files), read-inv(m4, m4 + n0, mkinode(m3, md, false, m2, 0, m1), buf0, buf0, 0, dirs, files), fd ∈ of, m4 ≤ m1, n0 ≤ # buf0, psynced → asynced, ⌊err1⌋ ∨ err1 = ESUCCESS ⊦ ∃ 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[fd, of[fd].pos:= m4]) ∧ (psynced → asynced) ∧ buf1 = buf ∧ 0 = n0 ∧ err1 = err0), mode0 ≠ MODE_R ∧ mode0 ≠ MODE_RW |
files[m3] = mkfile(m1, md, m2, content), of[fd] = mkfile(m3, mode0, m4), 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)), of-cons(of, dirs, files), read-inv(m4, m4 + n0, mkinode(m3, md, false, m2, 0, m1), buf0, buf0, 0, dirs, files), read-inv(m4, m4 + n0, mkinode(m3, md, false, m2, 0, m1), buf0, buf1, 0, dirs, files), fd ∈ of, n0 ≤ # buf0, m4 ≤ m1, psynced → asynced, ⌊err1⌋ ∨ err1 = ESUCCESS ⊦ ∃ 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; buf0 := copy(f.content, fh.pos, buf0, 0, n0); ofh[fd].pos := fh.pos + n0} ifnone n0 := 0 else n0 := ?⟩ (ofh = abs-of(of[fd, of[fd].pos:= m4]) ∧ (psynced → asynced) ∧ buf1 = buf0 ∧ 0 = n0 ∧ err1 = err0), mode0 ≠ MODE_R ∧ mode0 ≠ MODE_RW