| p_os.keys = fo, fi = fi2, fi0 = ri, fi2 = fi1, fs = nodes(gstore2 ↓, jro2), gstore = gstore1, gstore0 = gstore2, jro = jro2, jro0 = jro1, log = abs-log(nx, gstore2 ↓), remove-refsize0(gstore1) = gstore1, dom remove-refsize0(gstore0) ∩ jro = ∅, elems nx ∩ jro2 = ∅, dom gstore1 ∪ elems nx = dom gstore2 ∪ jro2, jro1.keys.inodes?, p_os.keys.inodes?, jro1 < jmaxino, p_os < pmaxino, ri.inos < jmaxino, fi1.inos < pmaxino, inv(gstore2 \ jro2), inv(gstore1), log-cons(abs-log(nx, gstore2 ↓), nodes(gstore2 ↓, jro2)), refsize-cons(gstore2, range ri), refsize-cons(gstore1, range fi1), ri-cons(ri, nodes(gstore2 ↓, jro2)), ri-inj(ri), ri-inj(fi1), pmaxino ≤ jmaxino, fi0.lebs ⊆ dom remove-refsize0(gstore0), ri.lebs ⊆ dom gstore2, fi1.lebs ⊆ dom gstore1, jvalid → jvalid0, jvalid1 ∧ nx ≠ [] → valid-journal-head(nx, gstore2, jro2) ⊦ ⟪let jvalid = false in {index_requires_commit#(fi0, fi, jro, gstore0, gstore, nx, pmaxino, p_os, jvalid0; ; jvalid); if jvalid then gjournal_commit#(jmaxino, jro0, fi0; fi, jro, gstore0, gstore, nx, pmaxino, p_os, jvalid0; err) else err := ESUCCESS}⟫ ⟨aubifs_core_check_commit#(ri, jro1.keys; fi1, fo, fs, log, jvalid; err0)⟩ (p_os.keys = fo ∧ fi = fi1 ∧ log = abs-log(nx, gstore0 ↓) ∧ fs = nodes(gstore0 ↓, jro) ∧ (jvalid → jvalid0) ∧ err = err0), jmaxino = 0, pmaxino = 0, dups(nx) |
p_os.keys = fo, jvalid ↔ false, fi = fi2, fi0 = ri, fi2 = fi1, fs = nodes(gstore2 ↓, jro2), gstore = gstore1, gstore0 = gstore2, jro = jro2, jro0 = jro1, log = abs-log(nx, gstore2 ↓), remove-refsize0(gstore1) = gstore1, elems nx ∩ jro2 = ∅, dom remove-refsize0(gstore0) ∩ jro = ∅, dom gstore1 ∪ elems nx = dom gstore2 ∪ jro2, p_os.keys.inodes?, jro1.keys.inodes?, fi1.inos < pmaxino, ri.inos < jmaxino, p_os < pmaxino, jro1 < jmaxino, inv(gstore1), inv(gstore2 \ jro2), log-cons(abs-log(nx, gstore2 ↓), nodes(gstore2 ↓, jro2)), refsize-cons(gstore1, range fi1), refsize-cons(gstore2, range ri), ri-cons(ri, nodes(gstore2 ↓, jro2)), ri-inj(fi1), ri-inj(ri), pmaxino ≤ jmaxino, fi1.lebs ⊆ dom gstore1, ri.lebs ⊆ dom gstore2, fi0.lebs ⊆ dom remove-refsize0(gstore0), jvalid1 ∧ nx ≠ [] → valid-journal-head(nx, gstore2, jro2), jvalid2 → jvalid0 ⊦ ⟪index_requires_commit#(fi0, fi, jro, gstore0, gstore, nx, pmaxino, p_os, jvalid0; ; jvalid); if jvalid then gjournal_commit#(jmaxino, jro0, fi0; fi, jro, gstore0, gstore, nx, pmaxino, p_os, jvalid0; err) else err := ESUCCESS⟫ ⟨aubifs_core_check_commit#(ri, jro1.keys; fi1, fo, fs, log, jvalid2; err0)⟩ (p_os.keys = fo ∧ fi = fi1 ∧ log = abs-log(nx, gstore0 ↓) ∧ fs = nodes(gstore0 ↓, jro) ∧ (jvalid2 → jvalid0) ∧ err = err0), jmaxino = 0, pmaxino = 0, dups(nx)