[Imprint][Data Privacy Statement][E-Mail]

View long theorem info. View the proof. Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Proof step 450 from proof refine-rmdir (previous step)

# entries0 = m + 1, files[ino].nlink = 0, (entries0[str] ∈ dirs ⊃ mkinode(entries0[str], dirs[entries0[str]].meta, true, dirs[entries0[str]].nlink, dirs[entries0[str]].nsubdirs, dirs[entries0[str]].size) ;mkinode(entries0[str], files[entries0[str]].meta, false, files[entries0[str]].nlink, 0, files[entries0[str]].size) ) = mkinode(m5, md3, boolvar, m6, m7, m8), dirs1[entries0[str]] = mkdir(m0, md0, m1, m4, entries), dirs0[entries0[str]] = mkdir(0, md, # links(entries0[str], dirs0), m3, ∅), dirs0[ino1] = mkdir(m + 1, md2, # links(ino1, dirs0), m2, entries0), root[q + str '] = dnode(md1, ∅), err = ESUCCESS, fs = abs-files(files), ino = inode.ino, inode = getinode(entries0[str], dirs, files), root.dir?, root[q].dir?, dom of < ino0, abs(root, ROOT_INO)(dirs0), afs-cons(dirs, files -- ino), afs-cons(dirs0, files), fids-cons(root, abs-files(files), abs-of(of)), ispath(q, ROOT_INO, ino1, dirs0, files), of-cons(of, dirs, files -- ino), of-cons(of, dirs0, files), pre-evict(inode, dirs, files), pw(user, md2), px(user, md2), px-parent(user, q, ROOT_INO, dirs0, files), str ∈ entries0, ino1 ∈ dirs0, entries0[str] ∈ dirs0, entries0[str] ∈ dirs1, dirs1 ≡ dirs0[ino1, mkdir(m, md2, # links(ino1, dirs0), m2 - 1, entries0 -- str)], dirs ≡ dirs1[entries0[str], mkdir(m0, md, m1 - 1, m4, entries)], 1 ≤ m1, 1 ≤ m2, psynced → asynced0, links(ino1, dirs0) ≠ ∅ ∨ ino1 = ROOT_INO ⊦ ⟨posix_rmdir#(q + str ', user, fs, abs-of(of); err1, root; psynced)⟩ (fs = abs-files(files -- ino) ∧ abs(root, ROOT_INO)(dirs) ∧ (psynced → asynced) ∧ ESUCCESS = err1), entries0 = ∅, m1 = 0, m2 = 0, is-open(m5, of), ino1 ∈ dirs1, ino1 ∈ dirs, ino ∈ dirs

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 451:
# entries0 = m + 1, (entries0[str] ∈ dirs ⊃ mkinode(entries0[str], dirs[entries0[str]].meta, true, dirs[entries0[str]].nlink, dirs[entries0[str]].nsubdirs, dirs[entries0[str]].size) ;mkinode(entries0[str], files[entries0[str]].meta, false, files[entries0[str]].nlink, 0, files[entries0[str]].size) ) = mkinode(m5, md3, false, 0, 0, m8), 0 = files[m5].nlink, root[q + str '] = dnode(md1, ∅), dirs0[ino1] = mkdir(m + 1, md2, # links(ino1, dirs0), m2, entries0), dirs0[entries0[str]] = mkdir(0, md, # links(entries0[str], dirs0), m3, ∅), dirs1[entries0[str]] = mkdir(m0, md0, m1, m4, entries), # links(ino1, dirs0) ≠ 0, entries0 ≠ ∅, ino1 ≠ ROOT_INO, links(ino1, dirs0) ≠ ∅, m1 ≠ 0, m2 ≠ 0, m5 ≠ ROOT_INO, root[q].dir?, root.dir?, dom of < ino0, abs(root, ROOT_INO)(dirs0), afs-cons(dirs0, files), afs-cons(dirs, files -- m5), fids-cons(root, abs-files(files), abs-of(of)), ispath(q, ROOT_INO, ino1, dirs0, files), of-cons(of, dirs, files -- m5), of-cons(of, dirs0, files), pw(user, md2), px(user, md2), px-parent(user, q, ROOT_INO, dirs0, files), m5 ∈ files, entries0[str] ∈ dirs1, entries0[str] ∈ dirs0, ino1 ∈ dirs0, str ∈ entries0, dirs ≡ dirs1[entries0[str], mkdir(m0, md, m1 - 1, m4, entries)], dirs1 ≡ dirs0[ino1, mkdir(m, md2, # links(ino1, dirs0), m2 - 1, entries0 -- str)], 1 ≤ m2, 1 ≤ m1, ¬ is-open(m5, of), ¬ m5 ∈ dirs, ¬ ino1 ∈ dirs, ¬ ino1 ∈ dirs1, psynced → asynced0 ⊦ ⟨posix_rmdir#(q + str ', user, abs-files(files), abs-of(of); err1, root; psynced)⟩ (abs-files(files) = abs-files(files -- entries0[str]) ∧ abs(root, ROOT_INO)(dirs) ∧ (psynced → asynced) ∧ ESUCCESS = err1)

Rule argument

Additional information

Used simplifier rules: size-zero: ⊦ # ls ≠ 0 → ls ≠ ∅; (forward) from specification set-basic[alink-set]%size-zero-01: ⊦ ls ≠ ∅ → # ls ≠ 0; (forward) from specification set-basic[alink-set]%path-in-dirs: p ≠ ε ⊦ ispath(p, n, m, dirs, files) → n ∈ dirs; (forward) from specification afs-base%⊦ mkinode(m, md, boolvar, m0, m1, m2) = mkinode(m3, md0, boolvar0, m4, m5, m6) ↔ m = m3 ∧ md = md0 ∧ (boolvar ↔ boolvar0) ∧ m0 = m4 ∧ m1 = m5 ∧ m2 = m6; (ws)% ⊦ afs-cons(dirs, files) → ROOT_INO ∈ dirs; (ss)% ⊦ mkinode(m, md, boolvar, m0, m1, m2).directory ↔ boolvar; (s)% ⊦ mkinode(m, md, boolvar, m0, m1, m2).nlink = m0; (s)% ⊦ mkinode(m, md, boolvar, m0, m1, m2).ino = m; (s)% ⊦ mkinode(m, md, boolvar, m0, m1, m2).nsubdirs = m1; (s)% ⊦ valid-file-ino(ino, dirs, files) ↔ ino ∈ files; (s)%⊦ valid-file-inode(inode, dirs, files) ↔ valid-file-ino(inode.ino, dirs, files) ∧ inode.nlink = files[inode.ino].nlink ∧ inode.nsubdirs = 0 ∧ ¬ inode.directory; (s)% ⊦ valid-dir-ino(ino, dirs, files) ↔ ino ∈ dirs; (s)%⊦ valid-dir-inode(inode, dirs, files) ↔ valid-dir-ino(inode.ino, dirs, files) ∧ inode.nlink = dirs[inode.ino].nlink ∧ inode.size = dirs[inode.ino].size ∧ inode.nsubdirs = dirs[inode.ino].nsubdirs ∧ inode.directory; (s)%⊦ valid-wb-inode(inode, dirs, files) ↔ valid-dir-inode(inode, dirs, files) ∨ valid-file-inode(inode, dirs, files); (s)%⊦ pre-evict(inode, dirs, files) ↔ valid-wb-inode(inode, dirs, files) ∧ inode.ino ≠ ROOT_INO; (s)%⊦ getinode(ino, dirs, files) = (ino ∈ dirs ⊃ mkinode (ino, dirs[ino].meta, true, dirs[ino].nlink, dirs[ino].nsubdirs, dirs[ino].size) ;mkinode (ino, files[ino].meta, false, files[ino].nlink, 0, files[ino].size) ); (s)