| of[fd] = mkfile(m, mode, m0), files[m] = mkfile(m1, md, # links(m, dirs), 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), of-cons(of[fd, mkfile(m, mode, m0 + ino)], dirs, files), read-inv(m0, m0 + n0, mkinode(m, md, false, # links(m, dirs), 0, m1), buf0, buf0, 0, dirs, files), read-inv(m0, m0 + n0, mkinode(m, md, false, # links(m, dirs), 0, m1), buf0, buf1, ino, dirs, files), m ∈ files, fd ∈ of, m0 + ino ≤ # (content.stream to m1).buf, 0 + ino ≤ # buf0, n ≤ n0, n ≤ # buf0, n0 ≤ # buf0, m0 ≤ m1, m0 + n ≤ m1, finp(content.stream) → ⌜m1⌝ < # content.stream ∨ ⌜m1⌝ = # content.stream, psynced → asynced, ⌊err1⌋ ∨ err1 = ESUCCESS ⊦ ⟨ofh := abs-of(of[fd, mkfile(m, mode, m0 + ino)])⟩ (ofh = abs-of(of[fd, of[fd].pos:= (m0 + ino)]) ∧ (psynced → asynced) ∧ buf1 = copy((content.stream to m1).buf, m0, buf0, 0, ino) ∧ ino = ino), ino = 0, mode ≠ MODE_R ∧ mode ≠ MODE_RW |
Used simplifier rules: ⊦ finp(σ0 to m); (s)%finp(σ) ⊦ # σ.buf = (# σ).n; (s)% ⊦ # content.stream = ∞; (s)% ⊦ ¬ ∞ < n∞; (s)%¬ # σ0 < ⌜n⌝ ⊦ #(σ0 to n) = ⌜n⌝ ; (s)% ⊦ ⌜m⌝ .n = m; (s)% ⊦ n + 0 = n; (s)%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic%c: ⊦ m + n = n + m; from specification nat-basic% ⊦ ⌜m⌝ < ∞; (s)%⊦ files[ino] = mkfile(m, md, m1, content) ∧ read-inv (n0, n1, mkinode(ino, md, false, m0, 0, m), buf0, buf1, n, dirs, files) → copy((content.stream to m).buf, n0, buf0, 0, n) = buf1; (s)% ⊦ mkfile(m, mode, m0).pos:= m2 = mkfile(m, mode, m2); (s)