| (entries0[str0] = m7 ⊃ mkdir(m1, md2, # links(entries0[str0], dirs0), m4, entries0) ;mkdir(m3, md3, # links(entries0[str0], dirs0), m6, ∅) ) .meta:= md0 = mkdir(m, md4, m8, m9, entries1), (m7 = entries0[str0] ⊃ mkdir(m1, md0, # links(entries0[str0], dirs0), m4, entries0);mkdir(m1, md2, # links(m7, dirs0), m4, entries0)) = mkdir(m0, md, m2, m5, entries), pcache[key] = mkpentry(boolvar, buf), dirs0[m7] = mkdir(m1, md1, # links(m7, dirs0), m4, entries0), dirs0[entries0[str0]] = mkdir(m3, md3, # links(entries0[str0], dirs0), m6, ∅), files[key.ino] = mkfile(m10, md5, m11, content), afs-cons(dirs0, files), afs-cons(dirs0[m7, mkdir(m1, md2, # links(m7, dirs0), m4, entries0)][entries0[str0], mkdir(m, md4, m8, m9, entries1)], files), synced(dirs0, icache0, pcache), key ∈ pcache, entries0[str0] ∈ dirs0, str0 ∈ entries0, m7 ∈ dirs0, asynced2 → synced(files, icache0, pcache), ∀ key0. key0 ∈ pcache → key0.data? ∧ # pcache[key0].page = VFS_PAGE_SIZE ∧ key0.ino ∈ files ∧ (¬ pcache[key0].dirty → key0.part ∈ files[key0.ino].content ∧ pcache[key0].page = files[key0.ino].content[key0.part]), links(m7, dirs0) ≠ ∅ ∨ m7 = ROOT_INO ⊦ entries0[str0] = ROOT_INO, key.data? ∧ # buf = VFS_PAGE_SIZE ∧ key.ino ∈ files ∧ (¬ boolvar → key.part ∈ content ∧ buf = content[key.part]) |
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% ⊦ mkpentry(boolvar, buf).page = buf; (s)% ⊦ mkpentry(boolvar, buf).dirty ↔ boolvar; (s)% ⊦ mkfile(m, md, m0, content).content = content; (s) Used terms: key