[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 20 from proof crash-neutral-link (previous step)

dirs[ino] = mkdir(m4, md3, # links(ino, dirs), m6, entries0), dirs[m] = mkdir(m0, md1, # links(m, dirs), m2, entries), files[entries0[str]] = mkfile(m1, md2, # links(entries0[str], dirs), content), c_inode = mkinode(entries0[str], md0, false, # links(entries0[str], dirs), 0, m3), dirs0 = dirs \ orphans(dirs, files), files0 = files \ orphans(dirs, files), new_dent = negdentry(str0), old_dent = mkdentry(str, entries0[str]), p_inode = mkinode(m, md, true, # links(m, dirs), m2, m0), afs-cons(dirs, files), pre-link(p_inode, c_inode, old_dent, new_dent, dirs, files), entries0[str] ∈ files, m ∈ dirs, str ∈ entries0, ino ∈ dirs, links(m, dirs) ≠ ∅ ∨ m = ROOT_INO, links(ino, dirs) ≠ ∅ ∨ ino = ROOT_INO ⊦ ⟨fail#(; ; err); asynced := ?⟩ (asynced ∧ dirs0 = dirs \ orphans(dirs, files) ∧ files0 = files \ orphans(dirs, files)), ⟨let p_ino = p_inode.ino in {dirs[p_ino].entries[new_dent.name] := old_dent.ino; dirs[p_ino].size := dirs[p_ino].size + 1; let ino = old_dent.ino in afs_inc_nlink#(ino; dirs, files); new_dent := mkdentry(new_dent.name, old_dent.ino); afs_inode_sync#(p_inode; dirs, files); afs_inode_sync#(c_inode; dirs, files); p_inode := getinode(p_inode.ino, dirs, files); c_inode := getinode(old_dent.ino, dirs, files); err := ESUCCESS}; asynced := ?⟩ (asynced ∧ dirs0 = dirs \ orphans(dirs, files) ∧ files0 = files \ orphans(dirs, files)), str0 ∈ entries

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 21:
# links(entries0[str], dirs) = files[entries0[str]].nlink, # links(m, dirs) = dirs[m].nlink, entries0[str] = dirs[ino0].entries[str], dirs[ino] = mkdir(m4, md3, # links(ino, dirs), m6, entries0), dirs[m] = mkdir(dirs[m].size, md1, dirs[m].nlink, dirs[m].nsubdirs, entries), files[entries0[str]] = mkfile(m1, md2, files[entries0[str]].nlink, content), afs-cons(dirs, files), str ∈ dirs[ino0].entries, ino0 ∈ dirs, entries0[str] ∈ files, m ∈ dirs, str ∈ entries0, ino ∈ dirs, ¬ str0 ∈ dirs[m].entries, ¬ str0 ∈ entries, links(ino0, dirs) ≠ ∅ ∨ ino0 = ROOT_INO, links(m, dirs) ≠ ∅ ∨ m = ROOT_INO, links(ino, dirs) ≠ ∅ ∨ ino = ROOT_INO ⊦ ⟨let p_ino = m in {dirs1 := dirs[p_ino, dirs[p_ino].entries:= dirs[p_ino].entries[str0, mkdentry(str, entries0[str]).ino]]; dirs1[p_ino].size := dirs1[p_ino].size + 1; let ino = mkdentry(str, entries0[str]).ino in {files1 := files; files0 := files; afs_inc_nlink#(ino; dirs1, files)}; new_dent := mkdentry(str0, mkdentry(str, entries0[str]).ino); afs_inode_sync#(mkinode(m, md, true, # links(m, dirs), dirs[m].nsubdirs, dirs[m].size); dirs1, files); afs_inode_sync#(mkinode(entries0[str], md0, false, # links(entries0[str], dirs), 0, m3); dirs1, files); p_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) ); c_inode := getinode(mkdentry(str, entries0[str]).ino, dirs1, files); err := ESUCCESS}; asynced := ?⟩ (asynced ∧ dirs \ orphans(dirs, files0) = dirs1 \ orphans(dirs1, files) ∧ files1 \ orphans(dirs, files1) = files \ orphans(dirs1, files)), ⟨fail#(; ; err); asynced := ?⟩ asynced

Rule argument

Additional information

Used simplifier rules: afs-cons-file-nlink: ⊦ afs-cons(dirs, files) ∧ ino ∈ files ∧ files[ino] = mkfile(m, md, n, content) → # links(ino, dirs) = n; (forward) from specification afs-base%afs-cons-dir-nlink: ⊦ afs-cons(dirs, files) ∧ ino ∈ dirs ∧ dirs[ino] = mkdir(n0, md, n, n1, entries) → # links(ino, dirs) = n; (forward) from specification afs-base%⊦ 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)% ⊦ 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)% ⊦ mkinode(m, md, boolvar, m0, m1, m2).directory ↔ boolvar; (s)% ⊦ mkinode(m, md, boolvar, m0, m1, m2).nsubdirs = m1; (s)% ⊦ mkinode(m, md, boolvar, m0, m1, m2).size = m2; (s)% ⊦ mkinode(m, md, boolvar, m0, m1, m2).nlink = m0; (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)%⊦ p_ino ∈ dirs ∧ dirs[p_ino] = mkdir(m, md, n, n0, entries) ∧ str ∈ entries → links(entries[str], dirs) ≠ ∅; (s)% ⊦ negdentry(str).negdentry?; (s)% ⊦ negdentry(str).name = str; (s)%⊦ valid-negdentry(ino, dent, dirs, files) ↔ valid-parent-ino(ino, dirs, files) ∧ ¬ dent.name ∈ dirs[ino].entries ∧ dent.negdentry?; (s)% ⊦ mkinode(m, md, boolvar, m0, m1, m2).ino = m; (s)% ⊦ mkdentry(str, m).dentry?; (s)% ⊦ mkdentry(str, m).name = str; (s)% ⊦ valid-ino(ino, dirs, files) ↔ ino ∈ dirs ∨ ino ∈ files; (s)% ⊦ mkdentry(str, m).ino = m; (s)%⊦ valid-parent-ino(ino, dirs, files) ↔ ino ∈ dirs ∧ (links(ino, dirs) ≠ ∅ ∨ ino = ROOT_INO); (s)%⊦ valid-dentry(ino, dent, dirs, files) ↔ valid-parent-ino(ino, dirs, files) ∧ valid-ino(dent.ino, dirs, files) ∧ dent.name ∈ dirs[ino].entries ∧ dent.ino = dirs[ino].entries[dent.name] ∧ dent.dentry?; (s)%⊦ valid-dentry(dent, dirs, files) ↔ (∃ ino. valid-dentry(ino, dent, dirs, files)); (s)%⊦ pre-link(p_inode, c_inode, old_dent, new_dent, dirs, files) ↔ valid-dentry(old_dent, dirs, files) ∧ valid-negdentry(p_inode.ino, new_dent, dirs, files) ∧ (links(old_dent.ino, dirs) ≠ ∅ ∨ old_dent.ino = ROOT_INO) ∧ valid-dir-inode(p_inode, dirs, files) ∧ valid-file-inode(c_inode, dirs, files) ∧ c_inode.ino = old_dent.ino; (s)