| files0[m] = mkfile(m1, md0, # links(m, dirs), content), files[m] = mkfile(m0, md1, # links(m, dirs), content0), err = ESUCCESS, ino = m, inode = mkinode(m, md, false, # links(m, dirs), 0, m2), key = datakey(ino, pageno), n = n0, pageno = n0, n0 * VFS_PAGE_SIZE < m2, afs-cons(dirs, files), afs-cons(dirs, files0), dcache-cons(dcache, dirs, files), dcache-cons(dcache, dirs, files0), icache-cons(icache, dirs, files), icache-cons(icache, dirs, files0), pcache-cons(pcache, dirs, files), pcache-cons(pcache0, dirs, files0), synced(dirs, icache, pcache), synced(dirs, icache, pcache0), key ∈ pcache, m ∈ files, m ∈ files0 ⊦ ⟪n := n + 1⟫ ( icache-cons(icache, dirs, files) ∧ dcache-cons(dcache, dirs, files) ∧ pcache-cons(pcache, dirs, files) ∧ synced(dirs, icache, pcache) ∧ afs-cons(dirs, files) ∧ m ∈ files ∧ # links(m, dirs) = files[m].nlink ∧ inode.size + VFS_PAGE_SIZE - n * VFS_PAGE_SIZE < inode.size + VFS_PAGE_SIZE - n0 * VFS_PAGE_SIZE), true ∧ pcache[key].dirty |
Used simplifier rules: ⊦ mkinode(m, md, boolvar, m0, m1, m2).size = m2; (s)% ⊦ m * (n + 1) = m * n + m; (s)%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic%c: ⊦ m + n = n + m; from specification nat-basic%mult-a: ⊦ m0 * m * n = (m0 * m) * n; from specification nat-mult%mult-c: ⊦ m * n = n * m; from specification nat-mult% ⊦ m + n - n + n1 = m - n1; (s)% ⊦ m < n → m ≤ n; (s)%n0 ≤ n ⊦ n - n0 < m ↔ n < m + n0; (s)% ⊦ mkfile(m, md, m0, content).nlink = m0; (s)% ⊦ m < n ↔ ¬ n ≤ m; (ss)% ⊦ m ≤ n ↔ ¬ n < m; (ss)%f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic%lf: ⊦ m < n ∧ n < n0 → m +1 < n0; (forward) from specification nat-basic%trans: ⊦ n < n0 ∧ n0 < n1 → n < n1; (forward) from specification nat-basic% ⊦ m0 * m = 0 ↔ m0 = 0 ∨ m = 0; (ws)% ⊦ VFS_PAGE_SIZE ≠ 0; (s)% ⊦ m +1 = m + 1; (s)% ⊦ m + m0 < n → ¬ n + n0 < m; (s)%n ≤ m ⊦ (m - n) + m0 ≤ n0 ↔ m + m0 ≤ n0 + n; (s)% ⊦ m + n ≤ m + n0 ↔ n ≤ n0; (s)% ⊦ m * n + n ≤ m1 * n ↔ m + 1 ≤ m1 ∨ n = 0; (s)% ⊦ m + 1 ≤ n ↔ m < n; (s)% ⊦ ¬ n < n; (s)