[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 67 from proof fsync-inode-inv (previous step)

dirs[m1] = mkdir(m7, md2, m8, m9, entries), icache[m] = mkientry(true, mkinode(m1, md, boolvar, m2, m3, m4)), files[m] = mkfile(m0, md0, # links(m, dirs), content), files[m1] = mkfile(m5, md1, m6, content0), err = ESUCCESS, err0 = ESUCCESS, inode = mkinode(m1, md, boolvar, m2, m3, m4), afs-cons(dirs, files), afs-cons (dirs, files[inode.ino, files[inode.ino].meta:= inode.meta][inode.ino, files[inode.ino, files[inode.ino].meta:= inode.meta][inode.ino].size:= inode.size]), dcache-cons(dcache, dirs, files), icache-cons(icache, dirs, files), pcache-cons(pcache, dirs, files), pre-write-inode(inode, dirs, files), synced(dirs, icache, pcache), m ∈ icache, m ∈ files, m1 ∈ dirs ∧ m2 = m8 ∧ m4 = m7 ∧ m3 = m9 ∧ boolvar ∨ m1 ∈ files ∧ m2 = m6 ∧ m3 = 0 ∧ ¬ boolvar ⊦ ⟪icache_set_status#(m, false; err, icache)⟫ ( icache-cons (icache, dirs, files[inode.ino, files[inode.ino].meta:= inode.meta] [inode.ino, files[inode.ino, files[inode.ino].meta:= inode.meta][inode.ino].size:= inode.size ]) ∧ dcache-cons (dcache, dirs, files[inode.ino, files[inode.ino].meta:= inode.meta] [inode.ino, files[inode.ino, files[inode.ino].meta:= inode.meta][inode.ino].size:= inode.size ]) ∧ pcache-cons (pcache, dirs, files[inode.ino, files[inode.ino].meta:= inode.meta] [inode.ino, files[inode.ino, files[inode.ino].meta:= inode.meta][inode.ino].size:= inode.size ]) ∧ synced(dirs, icache, pcache) ∧ mkinode(m1, md, boolvar, m2, m3, m4).ino ∈ files[inode.ino, files[inode.ino].meta:= inode.meta] [inode.ino, files[inode.ino, files[inode.ino].meta:= inode.meta][inode.ino].size:= inode.size ] ∧ mkinode(m1, md, boolvar, m2, m3, m4).nlink = files[inode.ino, files[inode.ino].meta:= inode.meta] [inode.ino, files[inode.ino, files[inode.ino].meta:= inode.meta][inode.ino].size:= inode.size ] [mkinode(m1, md, boolvar, m2, m3, m4).ino ] .nlink ∧ mkinode(m1, md, boolvar, m2, m3, m4).nsubdirs = 0 ∧ ¬ mkinode(m1, md, boolvar, m2, m3, m4).directory), inode.directory

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 68:
files[m] = mkfile(m0, md0, # links(m, dirs), content), files[m1] = mkfile(m5, md1, # links(m1, dirs), content0), dirs[m1] = mkdir(m7, md2, m8, m9, entries), icache[m] = mkientry(true, mkinode(m1, md, false, # links(m1, dirs), 0, m4)), err = ESUCCESS, afs-cons(dirs, files), afs-cons(dirs, files[m1, mkfile(m4, md, # links(m1, dirs), content0)]), dcache-cons(dcache, dirs, files), icache-cons(icache, dirs, files), pcache-cons(pcache, dirs, files), synced(dirs, icache, pcache), m1 ∈ files, m ∈ icache, m ∈ files ⊦ ⟪icache_set_status#(m, false; err, icache)⟫ ( icache-cons(icache, dirs, files[m1, mkfile(m4, md, # links(m1, dirs), content0)]) ∧ dcache-cons(dcache, dirs, files[m1, mkfile(m4, md, # links(m1, dirs), content0)]) ∧ pcache-cons(pcache, dirs, files[m1, mkfile(m4, md, # links(m1, dirs), content0)]) ∧ synced(dirs, icache, pcache))

Rule argument

Additional information

Used simplifier rules: ⊦ mkfile(m, md, m0, content).size:= m1 = mkfile(m1, md, m0, content); (s)% ⊦ mkfile(m, md, m0, content).meta:= md0 = mkfile(m, md0, m0, content); (s)% ⊦ mkfile(m, md, m0, content).nlink = m0; (s)%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% ⊦ (af.meta:= md).nlink = af.nlink; (s)% ⊦ (af.size:= m).nlink = af.nlink; (s)% ⊦ ino ∈ files[ino0, af] ↔ ino ∈ files; (s)% ⊦ files[ino, af][ino, af0] = files[ino, af0]; (s)% ⊦ mkinode(m, md, boolvar, m0, m1, m2).size = m2; (s)% ⊦ files[ino, af][ino0] = (ino0 = ino ∧ ino ∈ files ⊃ af;files[ino0]); (s)% ⊦ mkinode(m, md, boolvar, m0, m1, m2).meta = md; (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).nlink = m0; (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)% ⊦ valid-dir-ino(ino, dirs, files) ↔ ino ∈ dirs; (s)% ⊦ mkinode(m, md, boolvar, m0, m1, m2).ino = m; (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)%⊦ valid-wb-inode(inode, dirs, files) ↔ valid-dir-inode(inode, dirs, files) ∨ valid-file-inode(inode, dirs, files); (s)%⊦ pre-write-inode(inode, dirs, files) ↔ valid-wb-inode(inode, dirs, files); (s)