[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 105 from proof write-prepost-partial (previous step)

⟨afs_truncate#(m1, m1 / VFS_PAGE_SIZE; buf-opt, inode1, isdir, err, dirs1, files1, asynced1)⟩ ( buf-opt = buf-opt0 ∧ inode1 = mkinode(m, md, false, m3, 0, m1) ∧ (isdir ↔ isdir0) ∧ err = ESUCCESS ∧ dirs1 = dirs0 ∧ files1 = files0 ∧ (asynced1 ↔ asynced0)), # links(m, dirs1) = m3, files1 -- m = files0 -- m, files1[m] = mkfile(m1, md, # links(m, dirs1), content0), of1[fd] = mkfile(m, mode, m0), files0[m] = mkfile(m1, md, # links(m, dirs1), content), files[m] = mkfile(m1, md, # links(m, dirs1), content1), buf-opt = none, err = ESUCCESS, err0 = ESUCCESS, content.stream from m1 = σ⊥, ino2 = of1[fd].pos, inode1 = mkinode(m, md, false, # links(m, dirs1), 0, m1), n = ino, content0.stream to m1 = content.stream to m1, m1 < m0 + ino, afs-cons(dirs1, files1), of-cons(of1, dirs1, files1), write-inv(m0, m0 + n1, mkinode(m, md, false, # links(m, dirs1), 0, m1), buf, 0, dirs0, files0, files0), write-inv(m0, m0 + n1, mkinode(m, md, false, # links(m, dirs1), 0, m1), buf, ino, dirs0, files0, files), files1 ~ files0, fd ∈ of1, m ∈ files, m ∈ files1, n1 ≤ # buf, err1 = ESUCCESS ∨ ⌊err1⌋ ⊦ ino = 0, n1 = 0, (err0 = ESUCCESS ⊃ ( files [mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).ino, files[mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).ino] .meta:= mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).meta ] [mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).ino, files [mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).ino, files[mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).ino] .meta:= mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).meta ] [mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).ino ] .size:= mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).size ] [m ] .content .stream to files [mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).ino, files[mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).ino] .meta:= mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).meta ] [mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).ino, files [mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).ino, files[mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).ino] .meta:= mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).meta ] [mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).ino ] .size:= mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).size ] [m ] .size ).buf = splice(buf, 0, (content0.stream to m1).buf, m0, n) ∧ of1[fd, of1[fd].pos:= (ino2 + n)] = of1[fd, of1[fd].pos:= (m0 + n)] ∧ n ≤ n1 ∧ m ∈ files [mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).ino, files[mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).ino] .meta:= mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).meta ] [mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).ino, files [mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).ino, files[mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).ino] .meta:= mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).meta ] [mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).ino ] .size:= mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).size ] ∧ files [mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).ino, files[mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).ino] .meta:= mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).meta ] [mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).ino, files [mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).ino, files[mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).ino] .meta:= mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).meta ] [mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).ino ] .size:= mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).size ] [m ] .meta = md ∧ files [mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).ino, files[mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).ino] .meta:= mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).meta ] [mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).ino, files [mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).ino, files[mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).ino] .meta:= mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).meta ] [mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).ino ] .size:= mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).size ] -- m = files1 -- m ∧ (mode = MODE_W ∨ mode = MODE_RW) ; files [mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).ino, files[mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).ino] .meta:= mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).meta ] [mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).ino, files [mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).ino, files[mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).ino] .meta:= mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).meta ] [mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).ino ] .size:= mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).size ] ~ files1 ∧ of1 = of1[fd, of1[fd].pos:= (ino2 + n)] ∧ ( err0 = EBADFD ∧ ( fd ∈ of1[fd, of1[fd].pos:= (ino2 + n)] → of1[fd, of1[fd].pos:= (ino2 + n)][fd].mode ≠ MODE_W ∧ of1[fd, of1[fd].pos:= (ino2 + n)][fd].mode ≠ MODE_RW) ∨ ⌊err0⌋ ) ), mode ≠ MODE_W ∧ mode ≠ MODE_RW

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Rule argument

Additional information

Used simplifier rules: write-inv-in0: ⊦ write-inv (n0, n1, mkinode(ino, md, false, m, m1, m0), buf, n, dirs, files0, files1) → ino ∈ files1;%write-inv-ls: ⊦ write-inv (n0, n0 + n1, mkinode(ino, md, false, m, m1, m0), buf, n2, dirs, files0, files1) → n2 ≤ n1;%write-inv-post: ⊦ write-inv (n0, n1, mkinode(ino, md, false, m, m3, m2), buf, n, dirs, files0, files1) ∧ files0[ino] = mkfile(m0, md0, n2, content0) ∧ files1[ino] = mkfile(m1, md1, n3, content1) ∧ content0.stream from m0 = σ⊥ → splice(buf, 0, (content0.stream to m0).buf, n0, n) = (content1.stream to (n ≠ 0 ∧ m0 < n0 + n ⊃ n0 + n;m0)).buf;% ⊦ mkfile(m, mode, m0).pos:= m2 = mkfile(m, mode, m2); (s)% ⊦ mkfile(m, mode, m0).pos = m0; (s)% ⊦ mkfile(m, md, m0, content).content = content; (s)%ino ∈ files ⊦ files[ino, af] -- ino = files -- ino; (s)% ⊦ (af.meta:= md).meta = md; (s)% ⊦ (af.size:= m).meta = af.meta; (s)% ⊦ ino ∈ files[ino0, af] ↔ ino ∈ files; (s)%c: ⊦ m + n = n + m; from specification nat-basic%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic% ⊦ (af.size:= m).size = m; (s)% ⊦ (af.meta:= md).content = af.content; (s)% ⊦ (af.size:= m).content = af.content; (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).ino = m; (s)