[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 511 from proof refine-rename-dir-dentry (previous step)

# links(m0, cache_dirs) = cache_dirs[m0].nlink, # links(entries0[str0], cache_dirs) = cache_dirs[entries0[str0]].nlink, cache_dirs[entries0[str0]].entries = ∅, (entries0[str0] = m0 ⊃ mkdir(cache_dirs[entries0[str0]].size, md0, cache_dirs[entries0[str0]].nlink, cache_dirs[entries0[str0]].nsubdirs, entries0) ;cache_dirs[entries0[str0]] ) .meta:= md = mkdir(m7, md5, m8, m9, entries1), (m0 = entries0[str0] ⊃ mkdir(cache_dirs[entries0[str0]].size, md, cache_dirs[entries0[str0]].nlink, cache_dirs[entries0[str0]].nsubdirs, entries0) ;mkdir(cache_dirs[m0].size, md0, cache_dirs[m0].nlink, cache_dirs[m0].nsubdirs, entries0) ) = mkdir(m, md1, m2, m5, entries), cache_dirs[entries0[str0]] = mkdir(cache_dirs[entries0[str0]].size, md4, cache_dirs[entries0[str0]].nlink, cache_dirs[entries0[str0]].nsubdirs, ∅), cache_dirs[m0] = mkdir(cache_dirs[m0].size, md3, cache_dirs[m0].nlink, cache_dirs[m0].nsubdirs, entries0), entries0[str0] = cache_dirs[m0].entries[str0], entries0[str0] ≠ ROOT_INO, afs-cons(cache_dirs, (cache_files ⊕ cache_pcache) ⊕ cache_icache), afs-cons(cache_dirs, cache_files), afs-cons (cache_dirs[m0, mkdir(cache_dirs[m0].size, md0, cache_dirs[m0].nlink, cache_dirs[m0].nsubdirs, entries0)] [entries0[str0], mkdir(m7, md5, m8, m9, entries1) ], cache_files), dcache-cons(cache_dcache, cache_dirs, cache_files), dcache-cons (cache_dcache[dentrykey(m0, str0), mkdentry(str0, entries0[str0])], cache_dirs[m0, mkdir(cache_dirs[m0].size, md0, cache_dirs[m0].nlink, cache_dirs[m0].nsubdirs, entries0)] [entries0[str0], mkdir(m7, md5, m8, m9, entries1) ], cache_files), icache-cons(cache_icache, cache_dirs, cache_files), icache-cons (cache_icache[m0, mkientry(false, mkinode(m0, md1, true, m2, m5, m))][entries0[str0], mkientry(false, mkinode(entries0[str0], md5, true, m8, m9, m7))], cache_dirs[m0, mkdir(cache_dirs[m0].size, md0, cache_dirs[m0].nlink, cache_dirs[m0].nsubdirs, entries0)] [entries0[str0], mkdir(m7, md5, m8, m9, entries1) ], cache_files), pcache-cons(cache_pcache, cache_dirs, cache_files), pcache-cons (cache_pcache, cache_dirs[m0, mkdir(cache_dirs[m0].size, md0, cache_dirs[m0].nlink, cache_dirs[m0].nsubdirs, entries0)] [entries0[str0], mkdir(m7, md5, m8, m9, entries1) ], cache_files), synced(cache_dirs, cache_icache, cache_pcache), synced (cache_dirs[m0, mkdir(cache_dirs[m0].size, md0, cache_dirs[m0].nlink, cache_dirs[m0].nsubdirs, entries0)] [entries0[str0], mkdir(m7, md5, m8, m9, entries1) ], cache_icache[m0, mkientry(false, mkinode(m0, md1, true, m2, m5, m))][entries0[str0], mkientry(false, mkinode(entries0[str0], md5, true, m8, m9, m7))], cache_pcache), str0 ∈ cache_dirs[m0].entries, str0 ∈ entries0, entries0[str0] ∈ cache_dirs, m0 ∈ cache_dirs, cache_sync → synced(cache_files, cache_icache, cache_pcache), cache_sync → synced (cache_files, cache_icache[m0, mkientry(false, mkinode(m0, md1, true, m2, m5, m))] [entries0[str0], mkientry(false, mkinode(entries0[str0], md5, true, m8, m9, m7)) ], cache_pcache), links(m0, cache_dirs) ≠ ∅ ∨ m0 = ROOT_INO ⊦ ⟨let old_ino = m0, new_ino = m0, asynced1 = true in let asynced0 = old_ino = new_ino ∧ mkdentry(str0, entries0[str0]) = mkdentry(str0, entries0[str0]) in {dirs := cache_dirs[old_ino, cache_dirs[old_ino].entries:= (cache_dirs[old_ino].entries -- mkdentry(str0, entries0[str0]).name)]; old_dent := mkdentry(str0, entries0[str0]); if ¬ asynced0 then {dirs[old_ino].size := dirs[old_ino].size - 1; if old_dent.ino ∈ dirs then dirs[old_ino].nsubdirs := dirs[old_ino].nsubdirs - 1}; dirs[new_ino].entries[mkdentry(str0, entries0[str0]).name] := old_dent.ino; new_dent := mkdentry(str0, entries0[str0]); afs_files := (cache_files ⊕ cache_pcache) ⊕ cache_icache; if asynced1 ∧ ¬ asynced0 then let ino = new_dent.ino in afs_drop_nlink#(ino; dirs, afs_files); if ¬ asynced1 then {dirs[new_ino].size := dirs[new_ino].size + 1; if old_dent.ino ∈ dirs then dirs[new_ino].nsubdirs := dirs[new_ino].nsubdirs + 1}; new_dent := mkdentry(new_dent.name, old_dent.ino); old_dent := negdentry(old_dent.name); afs_inode_sync#(mkinode(m0, md0, true, # links(m0, cache_dirs), cache_dirs[m0].nsubdirs, cache_dirs[m0].size); dirs, afs_files); afs_inode_sync#(mkinode(m0, md0, true, # links(m0, cache_dirs), cache_dirs[m0].nsubdirs, cache_dirs[m0].size); dirs, afs_files); new_child_inode := mkinode (entries0[str0], md, true, # links(entries0[str0], cache_dirs), cache_dirs[entries0[str0]].nsubdirs, cache_dirs[entries0[str0]].size); if asynced1 then {afs_inode_sync#(new_child_inode; dirs, afs_files); new_child_inode := (new_child_inode.ino ∈ dirs ⊃ mkinode (new_child_inode.ino, dirs[new_child_inode.ino].meta, true, dirs[new_child_inode.ino].nlink, dirs[new_child_inode.ino].nsubdirs, dirs[new_child_inode.ino].size) ;mkinode (new_child_inode.ino, afs_files[new_child_inode.ino].meta, false, afs_files[new_child_inode.ino].nlink, 0, afs_files[new_child_inode.ino].size) )}; old_parent_inode := (m0 ∈ dirs ⊃ mkinode(m0, dirs[m0].meta, true, dirs[m0].nlink, dirs[m0].nsubdirs, dirs[m0].size) ;mkinode(m0, afs_files[m0].meta, false, afs_files[m0].nlink, 0, afs_files[m0].size) ); new_parent_inode := (m0 ∈ dirs ⊃ mkinode(m0, dirs[m0].meta, true, dirs[m0].nlink, dirs[m0].nsubdirs, dirs[m0].size) ;mkinode(m0, afs_files[m0].meta, false, afs_files[m0].nlink, 0, afs_files[m0].size) ); err := ESUCCESS}; asynced := ?⟩ ( mkinode (m0, (m0 = entries0[str0] ⊃ mkdir(cache_dirs[entries0[str0]].size, md, # links(entries0[str0], cache_dirs), cache_dirs[entries0[str0]].nsubdirs, entries0) ;mkdir(cache_dirs[m0].size, md0, # links(m0, cache_dirs), cache_dirs[m0].nsubdirs, entries0) ) .meta, true, (m0 = entries0[str0] ⊃ mkdir(cache_dirs[entries0[str0]].size, md, # links(entries0[str0], cache_dirs), cache_dirs[entries0[str0]].nsubdirs, entries0) ;mkdir(cache_dirs[m0].size, md0, # links(m0, cache_dirs), cache_dirs[m0].nsubdirs, entries0) ) .nlink, (m0 = entries0[str0] ⊃ mkdir(cache_dirs[entries0[str0]].size, md, # links(entries0[str0], cache_dirs), cache_dirs[entries0[str0]].nsubdirs, entries0) ;mkdir(cache_dirs[m0].size, md0, # links(m0, cache_dirs), cache_dirs[m0].nsubdirs, entries0) ) .nsubdirs, (m0 = entries0[str0] ⊃ mkdir(cache_dirs[entries0[str0]].size, md, # links(entries0[str0], cache_dirs), cache_dirs[entries0[str0]].nsubdirs, entries0) ;mkdir(cache_dirs[m0].size, md0, # links(m0, cache_dirs), cache_dirs[m0].nsubdirs, entries0) ) .size) = old_parent_inode ∧ mkinode (m0, (m0 = entries0[str0] ⊃ mkdir(cache_dirs[entries0[str0]].size, md, # links(entries0[str0], cache_dirs), cache_dirs[entries0[str0]].nsubdirs, entries0) ;mkdir(cache_dirs[m0].size, md0, # links(m0, cache_dirs), cache_dirs[m0].nsubdirs, entries0) ) .meta, true, (m0 = entries0[str0] ⊃ mkdir(cache_dirs[entries0[str0]].size, md, # links(entries0[str0], cache_dirs), cache_dirs[entries0[str0]].nsubdirs, entries0) ;mkdir(cache_dirs[m0].size, md0, # links(m0, cache_dirs), cache_dirs[m0].nsubdirs, entries0) ) .nlink, (m0 = entries0[str0] ⊃ mkdir(cache_dirs[entries0[str0]].size, md, # links(entries0[str0], cache_dirs), cache_dirs[entries0[str0]].nsubdirs, entries0) ;mkdir(cache_dirs[m0].size, md0, # links(m0, cache_dirs), cache_dirs[m0].nsubdirs, entries0) ) .nsubdirs, (m0 = entries0[str0] ⊃ mkdir(cache_dirs[entries0[str0]].size, md, # links(entries0[str0], cache_dirs), cache_dirs[entries0[str0]].nsubdirs, entries0) ;mkdir(cache_dirs[m0].size, md0, # links(m0, cache_dirs), cache_dirs[m0].nsubdirs, entries0) ) .size) = new_parent_inode ∧ mkinode (entries0[str0], md, true, (entries0[str0] = m0 ⊃ mkdir(cache_dirs[entries0[str0]].size, md0, # links(entries0[str0], cache_dirs), cache_dirs[entries0[str0]].nsubdirs, entries0) ;cache_dirs[entries0[str0]] ) .nlink, (entries0[str0] = m0 ⊃ mkdir(cache_dirs[entries0[str0]].size, md0, # links(entries0[str0], cache_dirs), cache_dirs[entries0[str0]].nsubdirs, entries0) ;cache_dirs[entries0[str0]] ) .nsubdirs, (entries0[str0] = m0 ⊃ mkdir(cache_dirs[entries0[str0]].size, md0, # links(entries0[str0], cache_dirs), cache_dirs[entries0[str0]].nsubdirs, entries0) ;cache_dirs[entries0[str0]] ) .size) = new_child_inode ∧ negdentry(str0) = old_dent ∧ mkdentry(str0, entries0[str0]) = new_dent ∧ ESUCCESS = err ∧ dirs = cache_dirs[m0, mkdir(cache_dirs[m0].size, md0, # links(m0, cache_dirs), cache_dirs[m0].nsubdirs, entries0)] [entries0[str0], (entries0[str0] = m0 ⊃ mkdir (cache_dirs[entries0[str0]].size, md0, # links(entries0[str0], cache_dirs), cache_dirs[entries0[str0]].nsubdirs, entries0) ;cache_dirs[entries0[str0]] ) .meta:= md ] ∧ afs_files = (cache_files ⊕ cache_pcache) ⊕ cache_icache[m0, mkientry(false, mkinode(m0, md1, true, m2, m5, m))] [entries0[str0], mkientry(false, mkinode(entries0[str0], md5, true, m8, m9, m7)) ] ∧ (asynced ↔ asynced0))

Heuristic symbolic execution applied rule let right

And obtained the following new goals

Rule argument

Additional information