| files1[m] = mkfile(m0, md0, m1, content0), m ∈ files1, buf-opt0.some? → # buf-opt0.buf = VFS_PAGE_SIZE ⊦ ⟨choose err0 with ⌊err0⌋ in err := err0; asynced := ?⟩ ( mkinode(m, md, false, m1, 0, m2) = (m ∈ dirs1 ⊃ mkinode(m, dirs1[m].meta, true, dirs1[m].nlink, dirs1[m].nsubdirs, dirs1[m].size);mkinode(m, md, false, m1, 0, n0)) ∧ ¬ boolvar ∧ err = ESUCCESS ∧ files1 = files1[m, mkfile(n0, md, m1, content0 upto min(n0, m2))]), ⟨let ino = m, content = content0, buf = ? in {pageno0 := m2 % VFS_PAGE_SIZE, pageno := min(n0, m2); boolvar := m2 ≤ n0 ∧ pageno0 ≠ 0 ∧ (m2 / VFS_PAGE_SIZE ∈ content ∨ buf-opt0.some?); buf-opt := buf-opt0; if boolvar then {pageno1 := m2 / VFS_PAGE_SIZE; if buf-opt.some? then buf := buf-opt.buf else buf := files1[ino].content[pageno1]; buf := fill(buf, zero, pageno0, VFS_PAGE_SIZE - pageno0); content[pageno1] := buf; buf-opt := some(buf)}; files := files1[ino, files1[ino].content:= (content upto pageno)]; let new_inode = mkinode(m, md, false, m1, 0, m2) in {new_inode.size := n0; dirs0 := dirs1; afs_inode_sync#(new_inode; dirs1, files)}; inode := (m ∈ dirs1 ⊃ mkinode(m, dirs1[m].meta, true, dirs1[m].nlink, dirs1[m].nsubdirs, dirs1[m].size) ;mkinode(m, files[m].meta, false, files[m].nlink, 0, files[m].size) ); err := ESUCCESS}; asynced := ?⟩ ( buf-opt = buf-opt0 ∧ inode = (m ∈ dirs0 ⊃ mkinode(m, dirs0[m].meta, true, dirs0[m].nlink, dirs0[m].nsubdirs, dirs0[m].size);mkinode(m, md, false, m1, 0, n0)) ∧ ¬ boolvar ∧ err = ESUCCESS ∧ dirs1 = dirs0 ∧ files = files1[m, mkfile(n0, md, m1, content0 upto min(n0, m2))]), m2 ≤ n0 ∧ m2 % VFS_PAGE_SIZE ≠ 0 ∧ (m2 / VFS_PAGE_SIZE ∈ content0 ∨ buf-opt0.some?) |
files1[m] = mkfile(m0, md0, m1, content0), m ∈ files1, buf-opt0.some? → # buf-opt0.buf = VFS_PAGE_SIZE ⊦ ∃ err0. ⌊err0⌋ ∧ ⟨err := err0; asynced := ?⟩ ( mkinode(m, md, false, m1, 0, m2) = (m ∈ dirs1 ⊃ mkinode(m, dirs1[m].meta, true, dirs1[m].nlink, dirs1[m].nsubdirs, dirs1[m].size);mkinode(m, md, false, m1, 0, n0)) ∧ ¬ boolvar ∧ err = ESUCCESS ∧ files1 = files1[m, mkfile(n0, md, m1, content0 upto min(n0, m2))]), ⟨let ino = m, content = content0, buf = ? in {pageno0 := m2 % VFS_PAGE_SIZE, pageno := min(n0, m2); boolvar := m2 ≤ n0 ∧ pageno0 ≠ 0 ∧ (m2 / VFS_PAGE_SIZE ∈ content ∨ buf-opt0.some?); buf-opt := buf-opt0; if boolvar then {pageno1 := m2 / VFS_PAGE_SIZE; if buf-opt.some? then buf := buf-opt.buf else buf := files1[ino].content[pageno1]; buf := fill(buf, zero, pageno0, VFS_PAGE_SIZE - pageno0); content[pageno1] := buf; buf-opt := some(buf)}; files := files1[ino, files1[ino].content:= (content upto pageno)]; let new_inode = mkinode(m, md, false, m1, 0, m2) in {new_inode.size := n0; dirs0 := dirs1; afs_inode_sync#(new_inode; dirs1, files)}; inode := (m ∈ dirs1 ⊃ mkinode(m, dirs1[m].meta, true, dirs1[m].nlink, dirs1[m].nsubdirs, dirs1[m].size) ;mkinode(m, files[m].meta, false, files[m].nlink, 0, files[m].size) ); err := ESUCCESS}; asynced := ?⟩ ( buf-opt = buf-opt0 ∧ inode = (m ∈ dirs0 ⊃ mkinode(m, dirs0[m].meta, true, dirs0[m].nlink, dirs0[m].nsubdirs, dirs0[m].size);mkinode(m, md, false, m1, 0, n0)) ∧ ¬ boolvar ∧ err = ESUCCESS ∧ dirs1 = dirs0 ∧ files = files1[m, mkfile(n0, md, m1, content0 upto min(n0, m2))]), m2 ≤ n0 ∧ m2 % VFS_PAGE_SIZE ≠ 0 ∧ (m2 / VFS_PAGE_SIZE ∈ content0 ∨ buf-opt0.some?)