| # links(m, dirs) = 0, files[m] = mkfile(m0, md, 0, content), dirs[key.ino] = mkdir(m1, md0, m2, m3, entries), afs-cons(dirs, files -- m), afs-cons(dirs, files), synced(dirs, icache, pcache), m ∈ files, key ∈ dcache, asynced1 → synced(files, icache, pcache), ∀ key. key ∈ pcache → key.data?, ∀ key. key ∈ evict(m, pcache) → key.data? ∧ key.ino ≠ m, ∀ key0. key0 ∈ dcache → key0.dentry? ∧ key0.name = dcache[key0].name ∧ key0.ino ∈ dirs ∧ (links(key0.ino, dirs) ≠ ∅ ∨ key0.ino = ROOT_INO) ∧ (dcache[key0].ino ∈ dirs ∨ dcache[key0].ino ∈ files) ∧ dcache[key0].name ∈ dirs[key0.ino].entries ∧ dcache[key0].ino = dirs[key0.ino].entries[dcache[key0].name] ∧ dcache[key0].dentry? ⊦ m = ROOT_INO, m ∈ dirs, key.dentry? ∧ key.name = dcache[key].name ∧ key.ino ∈ dirs ∧ (links(key.ino, dirs) ≠ ∅ ∨ key.ino = ROOT_INO) ∧ (dcache[key].ino ∈ dirs ∨ dcache[key].ino ≠ m ∧ dcache[key].ino ∈ files) ∧ dcache[key].name ∈ entries ∧ dcache[key].ino = entries[dcache[key].name] ∧ dcache[key].dentry? |
Used simplifier rules: 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% ⊦ mkdir(m, md, m0, m1, entries).entries = entries; (s)%size-zero-02: ⊦ # ls = 0 → ls = ∅; (forward) from specification set-basic[alink-set]%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%⊦ p_ino ∈ dirs ∧ dirs[p_ino] = mkdir(m, md, n, n0, entries) ∧ str ∈ entries → links(entries[str], dirs) ≠ ∅; (s)%⊦ afs-cons(dirs, files) → ( links(ino, dirs) = ∅ ↔ (ino ∈ dirs → dirs[ino].nlink = 0) ∧ (ino ∈ files → files[ino].nlink = 0)); (ws)% ⊦ afs-cons(dirs, files) ∧ ino ∈ dirs → ¬ ino ∈ files; (s)%size-zero-01: ⊦ ls ≠ ∅ → # ls ≠ 0; (forward) from specification set-basic[alink-set] Used terms: key