| cache_files[entries[str]] = mkfile(m1, md3, # links(entries[str], cache_dirs), content), ((cache_files ⊕ cache_pcache) ⊕ cache_icache)[entries[str]] = mkfile(m7, md2, # links(entries[str], cache_dirs), content0), cache_dirs[m] = mkdir(m0, md4, # links(m, cache_dirs), m3, entries), err = err0, p_inode = mkinode(m, md, true, # links(m, cache_dirs), m3, m0), afs-cons(cache_dirs, (cache_files ⊕ cache_pcache) ⊕ cache_icache), afs-cons(cache_dirs, cache_files), dcache-cons(cache_dcache, cache_dirs, cache_files), icache-cons(cache_icache, cache_dirs, cache_files), pcache-cons(cache_pcache, cache_dirs, cache_files), synced(cache_dirs, cache_icache, cache_pcache), entries[str] ∈ cache_files, str ∈ entries, m ∈ cache_dirs, ⌊err0⌋ , cache_sync → synced(cache_files, cache_icache, cache_pcache), links(m, cache_dirs) ≠ ∅ ∨ m = ROOT_INO ⊦ [dent := mkdentry(str, entries[str]); c_inode := mkinode(entries[str], md0, false, # links(entries[str], cache_dirs), 0, m6); afs_files := (cache_files ⊕ cache_pcache) ⊕ cache_icache; if err = ESUCCESS then let asynced = false in {icache_set#(c_inode, asynced; err, cache_icache); icache_set#(p_inode, asynced; err, cache_icache); dcache_delete#(p_inode.ino, dent.name; err, cache_dcache)}] ( icache-cons(cache_icache, cache_dirs, cache_files) ∧ dcache-cons(cache_dcache, cache_dirs, cache_files) ∧ synced(cache_dirs, cache_icache, cache_pcache) ∧ (cache_sync → synced(cache_files, cache_icache, cache_pcache)) → ⟨dent0 := mkdentry(str, entries[str]); p_inode0 := mkinode(m, md, true, # links(m, cache_dirs), m3, m0); p_inode1 := mkinode(entries[str], md0, false, # links(entries[str], cache_dirs), 0, m6); cache_dirs0 := cache_dirs; afs_unlink#(; p_inode0, p_inode1, dent0, err1, cache_dirs, afs_files; afs_asynced)⟩ ( cache_dirs = cache_dirs0 ∧ afs_files = (cache_files ⊕ cache_pcache) ⊕ cache_icache ∧ (afs_asynced ↔ asynced) ∧ p_inode = p_inode0 ∧ c_inode = p_inode1 ∧ dent = dent0 ∧ err = err1)) |
cache_dirs[m] = mkdir(m0, md4, # links(m, cache_dirs), m3, entries), ((cache_files ⊕ cache_pcache) ⊕ cache_icache)[entries[str]] = mkfile(m7, md2, # links(entries[str], cache_dirs), content0), cache_files[entries[str]] = mkfile(m1, md3, # links(entries[str], cache_dirs), content), dent = mkdentry(str, entries[str]), err = err0, p_inode = mkinode(m, md, true, # links(m, cache_dirs), m3, m0), afs-cons(cache_dirs, cache_files), afs-cons(cache_dirs, (cache_files ⊕ cache_pcache) ⊕ cache_icache), dcache-cons(cache_dcache, cache_dirs, cache_files), icache-cons(cache_icache, cache_dirs, cache_files), pcache-cons(cache_pcache, cache_dirs, cache_files), synced(cache_dirs, cache_icache, cache_pcache), m ∈ cache_dirs, entries[str] ∈ cache_files, str ∈ entries, ⌊err0⌋ , cache_sync → synced(cache_files, cache_icache, cache_pcache), links(m, cache_dirs) ≠ ∅ ∨ m = ROOT_INO ⊦ [c_inode := mkinode(entries[str], md0, false, # links(entries[str], cache_dirs), 0, m6); afs_files := (cache_files ⊕ cache_pcache) ⊕ cache_icache; if err = ESUCCESS then let asynced = false in {icache_set#(c_inode, asynced; err, cache_icache); icache_set#(p_inode, asynced; err, cache_icache); dcache_delete#(p_inode.ino, dent.name; err, cache_dcache)}] ( icache-cons(cache_icache, cache_dirs, cache_files) ∧ dcache-cons(cache_dcache, cache_dirs, cache_files) ∧ synced(cache_dirs, cache_icache, cache_pcache) ∧ (cache_sync → synced(cache_files, cache_icache, cache_pcache)) → ⟨dent0 := mkdentry(str, entries[str]); p_inode0 := mkinode(m, md, true, # links(m, cache_dirs), m3, m0); p_inode1 := mkinode(entries[str], md0, false, # links(entries[str], cache_dirs), 0, m6); cache_dirs0 := cache_dirs; afs_unlink#(; p_inode0, p_inode1, dent0, err1, cache_dirs, afs_files; afs_asynced)⟩ ( cache_dirs = cache_dirs0 ∧ afs_files = (cache_files ⊕ cache_pcache) ⊕ cache_icache ∧ (afs_asynced ↔ asynced) ∧ p_inode = p_inode0 ∧ c_inode = p_inode1 ∧ dent = dent0 ∧ err = err1))