| ri[key] = @(m, m0, m1), err = err0, err = ESUCCESS, err2 = err, nd = nd0, remove-refsize0(gstore1) = gstore1, elems nx ∩ jro0 = ∅, dom gstore1 ∪ elems nx = dom gstore2 ∪ jro0, jro1.keys.inodes?, p_os.keys.inodes?, jro1 < jmaxino, p_os < pmaxino, ri.inos < jmaxino, fi1.inos < pmaxino, inv(gstore2 \ jro0), inv(gstore1), log-cons(abs-log(nx, gstore2 ↓), nodes(gstore2 ↓, jro0)), refsize-cons(gstore2, range ri), refsize-cons(gstore1, range fi1), ri-cons(ri, nodes(gstore2 ↓, jro0)), ri-inj(ri), ri-inj(fi1), m ∈ gstore2, key ∈ ri, @(m, m0, m1) ∈ gstore2, pmaxino ≤ jmaxino, ri.lebs ⊆ dom gstore2, fi1.lebs ⊆ dom gstore1, jvalid4 → jvalid0, jvalid1 ∧ nx ≠ [] → valid-journal-head(nx, gstore2, jro0), ⌊err0⌋ ∨ err0 = ESUCCESS ⊦ ⟪if err2 = ESUCCESS then nd := gstore2[ri[key]].nd⟫ ⟨aubifs_core_index_lookup#(key, ri, fi1, jro1.keys, p_os.keys, nodes(gstore2 ↓, jro0), abs-log(nx, gstore2 ↓), jvalid4; jvalid3, nd0; err1)⟩ ((jvalid4 → jvalid0) ∧ jvalid3 ∧ nd = nd0 ∧ err2 = err1), jmaxino = 0, pmaxino = 0, dups(nx), m ∈ jro0 |
ri[key] = @(m, m0, m1), err = ESUCCESS, err = err0, err2 = err, nd = nd0, remove-refsize0(gstore1) = gstore1, elems nx ∩ jro0 = ∅, dom gstore1 ∪ elems nx = dom gstore2 ∪ jro0, p_os.keys.inodes?, jro1.keys.inodes?, fi1.inos < pmaxino, ri.inos < jmaxino, p_os < pmaxino, jro1 < jmaxino, inv(gstore1), inv(gstore2 \ jro0), log-cons(abs-log(nx, gstore2 ↓), nodes(gstore2 ↓, jro0)), refsize-cons(gstore1, range fi1), refsize-cons(gstore2, range ri), ri-cons(ri, nodes(gstore2 ↓, jro0)), ri-inj(fi1), ri-inj(ri), @(m, m0, m1) ∈ gstore2, key ∈ ri, m ∈ gstore2, pmaxino ≤ jmaxino, fi1.lebs ⊆ dom gstore1, ri.lebs ⊆ dom gstore2, jvalid1 ∧ nx ≠ [] → valid-journal-head(nx, gstore2, jro0), jvalid4 → jvalid0, ⌊err0⌋ ∨ err0 = ESUCCESS ⊦ ⟪nd := gstore2[ri[key]].nd⟫ ⟨aubifs_core_index_lookup#(key, ri, fi1, jro1.keys, p_os.keys, nodes(gstore2 ↓, jro0), abs-log(nx, gstore2 ↓), jvalid4; jvalid3, nd0; err1)⟩ ((jvalid4 → jvalid0) ∧ jvalid3 ∧ nd = nd0 ∧ err2 = err1), jmaxino = 0, pmaxino = 0, dups(nx), m ∈ jro0