Proof step 100 from proof refine-write-inode (previous step)

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 101:

  fs0[ri[inodekey(m)]] = inodenode(key, md0, boolvar2, m0, m1, m3), ¬ boolvar0, dirs = abs-dirs(fs0, ri), files = abs-files(fs0, ri), orphans(fs0, ri).inodes?, fo.inodes?, afs-cons(abs-dirs(fs0, ri), abs-files(fs0, ri)), file-node-cons(fs0, ri), log-cons(log0, fs0), orphans-cons(fs0, ri, orphans(fs0, ri)), replay-cons-strong(fs0, ri, orphans(fs0, ri), fi, fo, log0), ri-cons(ri, fs0), ri-inj(ri), ri-inj(fi), ubifs-cons(fs0, ri, orphans(fs0, ri), fi, fo, log0), inodekey(m) ∈ ri, ri[inodekey(m)] ∈ fs0, asynced → boolvar1, ¬ boolvar2 ∧ ¬ boolvar0 ∨ boolvar2 ∧ boolvar0 ∧ m2 = m3, boolvar2 ∧ m2 = m3 ∧ boolvar0 ∨ ¬ boolvar2 ∧ m1 = 0 ∧ ¬ boolvar0 ⊦ ⟨err := ESUCCESS; asynced := ?⟩ ( afs-cons(dirs, files[m, files[m].meta:= md][m, files[m, files[m].meta:= md][m].size:= m2]) → dirs = abs-dirs(fs0[adr1, inodenode(inodekey(m), md, boolvar0, m0, m1, m2)], ri[inodekey(m), adr1]) ∧ files[m, files[m].meta:= md][m, files[m, files[m].meta:= md][m].size:= m2] = abs-files(fs0[adr1, inodenode(inodekey(m), md, boolvar0, m0, m1, m2)], ri[inodekey(m), adr1]) ∧ orphans(fs0[adr1, inodenode(inodekey(m), md, boolvar0, m0, m1, m2)], ri[inodekey(m), adr1]) = orphans(fs0, ri) ∧ (asynced → boolvar) ∧ ESUCCESS = err), ⟨fail#(; ; err); asynced := ?⟩ ( abs-dirs(fs0, ri) = abs-dirs(fs0[adr1, inodenode(inodekey(m), md, boolvar0, m0, m1, m2)], ri[inodekey(m), adr1]) ∧ abs-files(fs0, ri) = abs-files(fs0[adr1, inodenode(inodekey(m), md, boolvar0, m0, m1, m2)], ri[inodekey(m), adr1]) ∧ orphans(fs0[adr1, inodenode(inodekey(m), md, boolvar0, m0, m1, m2)], ri[inodekey(m), adr1]) = orphans(fs0, ri) ∧ (asynced → boolvar) ∧ ESUCCESS = err), m = 0, adr1 ∈ fs0

Rule argument

Additional information