| files[m3] = mkfile(m1, md, m2, content), of[fd] = mkfile(m3, mode0, m4), buf = buf0, err = ESUCCESS, ino3 = 0, 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), fd ∈ of, n0 ≤ # buf0, m4 ≤ m1, psynced → asynced ⊦ ∀ buf, ino3, err. read-inv(m4, m4 + n0, mkinode(m3, md, false, m2, 0, m1), buf0, buf, ino3, dirs, files) → ⌊err⌋ ∨ err = ESUCCESS → [if ino3 ≠ 0 then err := ESUCCESS; of0 := of[fd, of[fd].pos:= (m4 + ino3)]; n := ino3] ( of-cons(of0, dirs, files) ∧ dom of0 < ino2 → ⟨ofh := abs-of(of); posix_read#(fd, user, root, abs-files(files); buf0, n0, err0, ofh)⟩ (ofh = abs-of(of0) ∧ (psynced → asynced) ∧ buf = buf0 ∧ n = n0 ∧ err = err0)), mode0 ≠ MODE_R ∧ mode0 ≠ MODE_RW |
of[fd] = mkfile(m3, mode0, m4), files[m3] = mkfile(m1, md, m2, content), 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, ino, 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 ⊦ [if ino ≠ 0 then err1 := ESUCCESS; of0 := of[fd, of[fd].pos:= (m4 + ino)]; n := ino] ( of-cons(of0, dirs, files) ∧ dom of0 < ino2 → ⟨ofh := abs-of(of); posix_read#(fd, user, root, abs-files(files); buf0, n0, err0, ofh)⟩ (ofh = abs-of(of0) ∧ (psynced → asynced) ∧ buf1 = buf0 ∧ n = n0 ∧ err1 = err0)), mode0 ≠ MODE_R ∧ mode0 ≠ MODE_RW