[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 83 from proof truncate-smaller (previous step)

files1[m] = mkfile(m0, md0, # links(m, dirs), content0), files = files1[m, mkfile(m0, md0, # links(m, dirs), content0 upto n)], ino = inode.ino, inode = mkinode(m, md, false, # links(m, dirs), 0, n), inode0 = mkinode(m, md, false, # links(m, dirs), 0, m2), afs-cons(dirs, files1), m ∈ files1, ino ∈ dirs, n ≤ m2 ⊦ [asynced := ?] (ESUCCESS = ESUCCESS ⊃ files [(inode0.ino ∈ dirs[ino, dirs[ino].meta:= inode.meta] ⊃ mkinode (inode0.ino, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].meta, true, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].nlink, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].nsubdirs, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].size) ;mkinode(inode0.ino, files[inode0.ino].meta, false, files[inode0.ino].nlink, 0, files[inode0.ino].size) ) .ino ] .content .stream to files [(inode0.ino ∈ dirs[ino, dirs[ino].meta:= inode.meta] ⊃ mkinode (inode0.ino, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].meta, true, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].nlink, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].nsubdirs, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].size) ;mkinode(inode0.ino, files[inode0.ino].meta, false, files[inode0.ino].nlink, 0, files[inode0.ino].size) ) .ino ] .size = files1 [(inode0.ino ∈ dirs[ino, dirs[ino].meta:= inode.meta] ⊃ mkinode (inode0.ino, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].meta, true, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].nlink, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].nsubdirs, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].size) ;mkinode(inode0.ino, files[inode0.ino].meta, false, files[inode0.ino].nlink, 0, files[inode0.ino].size) ) .ino ] .content .stream to files [(inode0.ino ∈ dirs[ino, dirs[ino].meta:= inode.meta] ⊃ mkinode (inode0.ino, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].meta, true, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].nlink, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].nsubdirs, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].size) ;mkinode(inode0.ino, files[inode0.ino].meta, false, files[inode0.ino].nlink, 0, files[inode0.ino].size) ) .ino ] .size ∧ (inode0.ino ∈ dirs[ino, dirs[ino].meta:= inode.meta] ⊃ mkinode (inode0.ino, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].meta, true, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].nlink, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].nsubdirs, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].size) ;mkinode(inode0.ino, files[inode0.ino].meta, false, files[inode0.ino].nlink, 0, files[inode0.ino].size) ) .ino ∈ files ∧ n = files [(inode0.ino ∈ dirs[ino, dirs[ino].meta:= inode.meta] ⊃ mkinode (inode0.ino, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].meta, true, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].nlink, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].nsubdirs, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].size) ;mkinode(inode0.ino, files[inode0.ino].meta, false, files[inode0.ino].nlink, 0, files[inode0.ino].size) ) .ino ] .size ∧ files1 [(inode0.ino ∈ dirs[ino, dirs[ino].meta:= inode.meta] ⊃ mkinode (inode0.ino, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].meta, true, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].nlink, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].nsubdirs, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].size) ;mkinode(inode0.ino, files[inode0.ino].meta, false, files[inode0.ino].nlink, 0, files[inode0.ino].size) ) .ino ] .nlink = files [(inode0.ino ∈ dirs[ino, dirs[ino].meta:= inode.meta] ⊃ mkinode (inode0.ino, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].meta, true, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].nlink, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].nsubdirs, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].size) ;mkinode(inode0.ino, files[inode0.ino].meta, false, files[inode0.ino].nlink, 0, files[inode0.ino].size) ) .ino ] .nlink ∧ files1 -- (inode0.ino ∈ dirs[ino, dirs[ino].meta:= inode.meta] ⊃ mkinode (inode0.ino, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].meta, true, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].nlink, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].nsubdirs, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].size) ;mkinode(inode0.ino, files[inode0.ino].meta, false, files[inode0.ino].nlink, 0, files[inode0.ino].size) ) .ino = files -- (inode0.ino ∈ dirs[ino, dirs[ino].meta:= inode.meta] ⊃ mkinode (inode0.ino, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].meta, true, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].nlink, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].nsubdirs, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].size) ;mkinode(inode0.ino, files[inode0.ino].meta, false, files[inode0.ino].nlink, 0, files[inode0.ino].size) ) .ino ;⌊ESUCCESS⌋ ∧ files1 = files ), ino ∈ files, n = m2 ∧ m2 % VFS_PAGE_SIZE ≠ 0 ∧ m2 / VFS_PAGE_SIZE ∈ content0

Heuristic symbolic execution applied rule assign right

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ mkinode(m, md, boolvar, m0, m1, m2).ino = m; (s)% ⊦ afs-cons(dirs, files) ∧ ino ∈ dirs → ¬ ino ∈ files; (s)