[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 36 from proof inv-create (previous step)

adr = adr1, fs = fs1[adr1, inodenode(inodekey(m), md0, true, fs1[ri[inodekey(m)]].nlink, fs1[ri[inodekey(m)]].nsubdirs, fs1[ri[inodekey(m)]].size + 1)] [adr2, dentrynode(dentrykey(m, str), n) ] [adr3, inodenode(inodekey(n), md, false, 1, 0, 0) ], key = inodekey(m), log = ((log0 + adr1 ') + adr2 ') + adr3 ', nd1 = inodenode(inodekey(m), md0, true, fs1[ri[inodekey(m)]].nlink, fs1[ri[inodekey(m)]].nsubdirs, fs1[ri[inodekey(m)]].size + 1), ri0 = ri, fs1[ri[inodekey(m)]].directory, fs1[ri[inodekey(m)]].inode?, ro.inodes?, fo.inodes?, file-node-cons(fs1, ri), log-cons(log0, fs1), orphans-cons(fs1, ri, ro), replay-cons-strong(fs1, ri, ro, fi, fo, log0), ri-inj(ri), ri-inj(fi), ubifs-cons(fs1, ri, ro, fi, fo, log0), inodekey(m) ∈ ri, ri[inodekey(m)] ∈ fs1, fs1[ri[inodekey(m)]].nlink ≠ 0 ∨ m = ROOT_INO ⊦ ⟪if ¬ adr ∈ ri ∧ adr ∈ fs ∧ key-cons(key, fs[adr]) then ri[key] := adr else abort; aubifs_core_index_store#(dentrykey(m, str), adr2, fi, ro, fo, fs, ((log0 + adr1 ') + adr2 ') + adr3 ', boolvar; ri); aubifs_core_index_store#(inodekey(n), adr3, fi, ro, fo, fs, ((log0 + adr1 ') + adr2 ') + adr3 ', boolvar; ri); dent := mkdentry(str, n); p_inode := mkinode (mkinode(m, md0, true, fs1[ri0[inodekey(m)]].nlink, fs1[ri0[inodekey(m)]].nsubdirs, fs1[ri0[inodekey(m)]].size).ino, nd1.meta, nd1.directory, nd1.nlink, nd1.nsubdirs, nd1.size); c_inode := mkinode (n, inodenode(inodekey(n), md, false, 1, 0, 0).meta, inodenode(inodekey(n), md, false, 1, 0, 0).directory, inodenode(inodekey(n), md, false, 1, 0, 0).nlink, inodenode(inodekey(n), md, false, 1, 0, 0).nsubdirs, inodenode(inodekey(n), md, false, 1, 0, 0).size)⟫ ( ubifs-cons(fs, ri, ro, fi, fo, ((log0 + adr1 ') + adr2 ') + adr3 ') ∧ replay-cons-strong(fs, ri, ro, fi, fo, ((log0 + adr1 ') + adr2 ') + adr3 ') ∧ file-node-cons(fs, ri) ∧ orphans-cons(fs, ri, ro)), adr1 = adr2, adr1 = adr3, adr2 = adr3, n = 0, adr3 ∈ fs1, adr2 ∈ fs1, adr1 ∈ fs1, inodekey(n) ∈ ri, inodekey(n) ∈ fo, dentrykey(m, str) ∈ ri, inodekey(m) ∈ ro

Heuristic symbolic execution applied rule if positive right

And obtained the following new goals

Proof step 37:
adr = adr1, fs = fs1[adr1, inodenode(inodekey(m), md0, true, fs1[ri[inodekey(m)]].nlink, fs1[ri[inodekey(m)]].nsubdirs, fs1[ri[inodekey(m)]].size + 1)] [adr2, dentrynode(dentrykey(m, str), n) ] [adr3, inodenode(inodekey(n), md, false, 1, 0, 0) ], key = inodekey(m), log = ((log0 + adr1 ') + adr2 ') + adr3 ', nd1 = inodenode(inodekey(m), md0, true, fs1[ri[inodekey(m)]].nlink, fs1[ri[inodekey(m)]].nsubdirs, fs1[ri[inodekey(m)]].size + 1), ri0 = ri, fs1[ri[inodekey(m)]].directory, fs1[ri[inodekey(m)]].inode?, fo.inodes?, ro.inodes?, file-node-cons(fs1, ri), log-cons(log0, fs1), orphans-cons(fs1, ri, ro), replay-cons-strong(fs1, ri, ro, fi, fo, log0), ri-inj(fi), ri-inj(ri), ubifs-cons(fs1, ri, ro, fi, fo, log0), ri[inodekey(m)] ∈ fs1, inodekey(m) ∈ ri, fs1[ri[inodekey(m)]].nlink ≠ 0 ∨ m = ROOT_INO ⊦ ⟪ri[key] := adr; aubifs_core_index_store#(dentrykey(m, str), adr2, fi, ro, fo, fs, ((log0 + adr1 ') + adr2 ') + adr3 ', boolvar; ri); aubifs_core_index_store#(inodekey(n), adr3, fi, ro, fo, fs, ((log0 + adr1 ') + adr2 ') + adr3 ', boolvar; ri); dent := mkdentry(str, n); p_inode := mkinode (mkinode(m, md0, true, fs1[ri0[inodekey(m)]].nlink, fs1[ri0[inodekey(m)]].nsubdirs, fs1[ri0[inodekey(m)]].size).ino, nd1.meta, nd1.directory, nd1.nlink, nd1.nsubdirs, nd1.size); c_inode := mkinode (n, inodenode(inodekey(n), md, false, 1, 0, 0).meta, inodenode(inodekey(n), md, false, 1, 0, 0).directory, inodenode(inodekey(n), md, false, 1, 0, 0).nlink, inodenode(inodekey(n), md, false, 1, 0, 0).nsubdirs, inodenode(inodekey(n), md, false, 1, 0, 0).size)⟫ ( ubifs-cons(fs, ri, ro, fi, fo, ((log0 + adr1 ') + adr2 ') + adr3 ') ∧ replay-cons-strong(fs, ri, ro, fi, fo, ((log0 + adr1 ') + adr2 ') + adr3 ') ∧ file-node-cons(fs, ri) ∧ orphans-cons(fs, ri, ro)), adr1 = adr3, adr1 = adr2, adr2 = adr3, n = 0, inodekey(m) ∈ ro, dentrykey(m, str) ∈ ri, inodekey(n) ∈ fo, inodekey(n) ∈ ri, adr1 ∈ fs1, adr2 ∈ fs1, adr3 ∈ fs1

Rule argument

pos: right 1

Additional information

Used simplifier rules: at-fs: ⊦ fs[adr0, nd][adr1] = (adr0 = adr1 ⊃ nd;fs[adr1]);% ⊦ adr ≠ adr0 → (adr ∈ fs[adr0, nd] ↔ adr ∈ fs); (s)% ⊦ adr ∈ fs[adr1, nd] ↔ adr = adr1 ∨ adr ∈ fs; (s)% ⊦ adr ≠ adr0 → fs[adr0, nd][adr] = fs[adr]; (s)%⊦ key-cons(inodekey(ino), nd) ↔ nd.inode? ∧ nd.key = inodekey(ino) ∧ ino ≠ 0; (s)% ⊦ inodenode(key, md, boolvar, m, m0, m1).inode?; (s)% ⊦ inodenode(key, md, boolvar, m, m0, m1).key = key; (s)% ⊦ inodekey(m) = inodekey(m0) ↔ m = m0; (s)% ⊦ adr ∈ ri ∧ ubifs-cons(fs, ri, ro, fi, fo, log) → adr ∈ fs; (ss)% ⊦ ubifs-cons(fs, ri, ro, fi, fo, log) → ¬ inodekey(0) ∈ ri; (s)