Proof step 73 from proof inv-write (previous step)

Heuristic elimination applied rule insert elim lemma

And obtained the following new goals

• Proof step 74:

  m1 + n1 = m1 / VFS_PAGE_SIZE * VFS_PAGE_SIZE + VFS_PAGE_SIZE, of[fd] = mkfile(m, mode, m0), files1[m] = mkfile(m1, md, # links(m, dirs), content0), err = ESUCCESS, files0 = files1[m, mkfile(m1, md, # links(m, dirs), content0[m1 / VFS_PAGE_SIZE, fill(content0[m1 / VFS_PAGE_SIZE], zero, n2, n1)] upto m1)], ino4 = 0, m1 = n2 + m1 / VFS_PAGE_SIZE * VFS_PAGE_SIZE, dom of < ino3, afs-cons(dirs, files1), of-cons(of, dirs, files1), m ∈ files1, m1 / VFS_PAGE_SIZE ∈ content0, fd ∈ of, n0 ≤ # buf0, m1 / VFS_PAGE_SIZE * VFS_PAGE_SIZE ≤ m1 ⊦ [vfs_write_loop# (m0, mkinode (m, files1 [m, files1 [m, files1 [m, mkfile(m1, md, # links(m, dirs), content0[m1 / VFS_PAGE_SIZE, fill(content0[m1 / VFS_PAGE_SIZE], zero, n2, n1)] upto m1) ] [m ] .size:= m1 ] [m ] .meta:= md ] [m ] .meta, false, files1 [m, files1 [m, files1 [m, mkfile(m1, md, # links(m, dirs), content0[m1 / VFS_PAGE_SIZE, fill(content0[m1 / VFS_PAGE_SIZE], zero, n2, n1)] upto m1) ] [m ] .size:= m1 ] [m ] .meta:= md ] [m ] .nlink, 0, files1 [m, files1 [m, files1 [m, mkfile(m1, md, # links(m, dirs), content0[m1 / VFS_PAGE_SIZE, fill(content0[m1 / VFS_PAGE_SIZE], zero, n2, n1)] upto m1) ] [m ] .size:= m1 ] [m ] .meta:= md ] [m ] .size), m0 + n0, buf0, dirs ; ino4, err, files0, asynced); if ino4 ≠ 0 then err := ESUCCESS; dirs1 := dirs; if err = ESUCCESS then let ino0 = (m ∈ dirs ⊃ mkinode(m, dirs[m].meta, true, dirs[m].nlink, dirs[m].nsubdirs, dirs[m].size) ;mkinode (m, files1 [m, files1 [m, files1 [m, mkfile (m1, md, # links(m, dirs), content0[m1 / VFS_PAGE_SIZE, fill(content0[m1 / VFS_PAGE_SIZE], zero, m1 % VFS_PAGE_SIZE, n1)] upto m1) ] [m ] .size:= m1 ] [m ] .meta:= md ] [m ] .meta, false, files1 [m, files1 [m, files1 [m, mkfile (m1, md, # links(m, dirs), content0[m1 / VFS_PAGE_SIZE, fill(content0[m1 / VFS_PAGE_SIZE], zero, m1 % VFS_PAGE_SIZE, n1)] upto m1) ] [m ] .size:= m1 ] [m ] .meta:= md ] [m ] .nlink, 0, files1 [m, files1 [m, files1 [m, mkfile (m1, md, # links(m, dirs), content0[m1 / VFS_PAGE_SIZE, fill(content0[m1 / VFS_PAGE_SIZE], zero, m1 % VFS_PAGE_SIZE, n1)] upto m1) ] [m ] .size:= m1 ] [m ] .meta:= md ] [m ] .size) ) .size in {n0 := ino4, ino1 := m0 + ino4; if ino4 ≠ 0 ∧ ino0 < ino1 then {inode0 := (m ∈ dirs ⊃ mkinode(m, dirs[m].meta, true, dirs[m].nlink, dirs[m].nsubdirs, dirs[m].size) ;mkinode (m, files1 [m, files1 [m, files1 [m, mkfile (m1, md, # links(m, dirs), content0[m1 / VFS_PAGE_SIZE, fill(content0[m1 / VFS_PAGE_SIZE], zero, m1 % VFS_PAGE_SIZE, n1)] upto m1) ] [m ] .size:= m1 ] [m ] .meta:= md ] [m ] .meta, false, files1 [m, files1 [m, files1 [m, mkfile (m1, md, # links(m, dirs), content0[m1 / VFS_PAGE_SIZE, fill(content0[m1 / VFS_PAGE_SIZE], zero, m1 % VFS_PAGE_SIZE, n1)] upto m1) ] [m ] .size:= m1 ] [m ] .meta:= md ] [m ] .nlink, 0, files1 [m, files1 [m, files1 [m, mkfile (m1, md, # links(m, dirs), content0[m1 / VFS_PAGE_SIZE, fill(content0[m1 / VFS_PAGE_SIZE], zero, m1 % VFS_PAGE_SIZE, n1)] upto m1) ] [m ] .size:= m1 ] [m ] .meta:= md ] [m ] .size) ) .size:= ino1; afs_check_commit#(dirs, files0; err; asynced); if err = ESUCCESS then afs_write_inode#(inode0; err, dirs, files0; asynced)}; if err ≠ ESUCCESS then n0 := (m0 ≤ ino0 ⊃ ino0 - m0;0), err := ESUCCESS; of[fd].pos := m0 + n0}] (dirs1 = dirs → of-cons(of, dirs, files0) ∧ dom of < ino3 ∧ afs-cons(dirs, files0)), m1 = m1 / VFS_PAGE_SIZE * VFS_PAGE_SIZE, n0 = 0, mode ≠ MODE_W ∧ mode ≠ MODE_RW

Rule argument

Additional information

Used simplifier rules: ⊦ VFS_PAGE_SIZE ≠ 0; (s)%n ≠ 0 ⊦ m / n * n ≤ m; (s)%mult-a: ⊦ m0 * m * n = (m0 * m) * n; from specification nat-mult%mult-c: ⊦ m * n = n * m; from specification nat-mult%n ≤ m ⊦ n0 = m - n ↔ m = n0 + n; (elim) Used terms: m1 / VFS_PAGE_SIZE * VFS_PAGE_SIZE, m1, n