| jvalid1 ↔ jvalid5, jvalid2 ↔ jvalid6, fi = fi3, fi0 = fi2, gstore = gstore1, gstore0 = gstore3, gstore3 = crash(gstore2, gstore1, jro4, nx), jmaxino0 = jmaxino1, jro = jro4, jro0 = jro3, nx0 = nx, p_os = jro1, pmaxino = jmaxino, remove-refsize0(gstore1) = gstore1, elems nx ∩ jro4 = ∅, dom gstore1 ∪ elems nx = dom gstore2 ∪ jro4, jro2 < jmaxino3, jro1 < jmaxino, fi1.inos < jmaxino3, fi3.inos < jmaxino, inv(gstore2 \ jro4), inv(gstore1), refsize-cons(gstore2, range fi1), refsize-cons(gstore1, range fi3), ri-inj(fi1), ri-inj(fi3), jmaxino ≤ jmaxino3, fi1.lebs ⊆ dom gstore2, fi3.lebs ⊆ dom gstore1, jvalid0 ∧ nx ≠ [] → valid-journal-head(nx, gstore2, jro4) ⊦ ⟪let nx = ? in {index_recover#(; jmaxino0, nx, jro0, fi, nx0, pmaxino, p_os, jro, gstore0, gstore; fi0, jvalid1, err); if err ≠ ESUCCESS then debug#("gjournal: persistence recover failed") else {gjournal_restore_log#(nx, fi0, fi, jro, gstore0, gstore, nx0, pmaxino, p_os, jvalid1; log; err); ks := jro0.keys}}⟫ ( err = ESUCCESS → jvalid1 ∧ jro0 < jmaxino0 ∧ p_os < pmaxino ∧ pmaxino ≤ jmaxino0 ∧ fi0.inos < jmaxino0 ∧ fi.inos < pmaxino ∧ jmaxino0 ≠ 0 ∧ pmaxino ≠ 0 ∧ (false ∧ nx0 ≠ [] → valid-journal-head(nx0, gstore0, jro)) ∧ fi0.lebs ⊆ dom gstore0 ∧ fi.lebs ⊆ dom gstore ∧ refsize-cons(gstore0, range fi0) ∧ refsize-cons(gstore, range fi) ∧ inv(gstore0 \ jro) ∧ inv(gstore) ∧ elems nx0 ∩ jro = ∅ ∧ ¬ dups(nx0) ∧ dom gstore ∪ elems nx0 = dom gstore0 ∪ jro ∧ remove-refsize0(gstore) = gstore ∧ ri-inj(fi0) ∧ ri-inj(fi)), jmaxino = 0, jmaxino3 = 0, dups(nx) |
jvalid2 ↔ jvalid6, jvalid1 ↔ jvalid5, fi = fi3, fi0 = fi2, gstore = gstore1, gstore0 = gstore3, gstore3 = crash(gstore2, gstore1, jro4, nx1), jmaxino0 = jmaxino1, jro = jro4, jro0 = jro3, nx0 = nx1, p_os = jro1, pmaxino = jmaxino, remove-refsize0(gstore1) = gstore1, elems nx1 ∩ jro4 = ∅, dom gstore1 ∪ elems nx1 = dom gstore2 ∪ jro4, fi3.inos < jmaxino, fi1.inos < jmaxino3, jro1 < jmaxino, jro2 < jmaxino3, inv(gstore1), inv(gstore2 \ jro4), refsize-cons(gstore1, range fi3), refsize-cons(gstore2, range fi1), ri-inj(fi3), ri-inj(fi1), jmaxino ≤ jmaxino3, fi3.lebs ⊆ dom gstore1, fi1.lebs ⊆ dom gstore2, jvalid0 ∧ nx1 ≠ [] → valid-journal-head(nx1, gstore2, jro4) ⊦ ⟪index_recover#(; jmaxino0, nx, jro0, fi, nx0, pmaxino, p_os, jro, gstore0, gstore; fi0, jvalid1, err); if err ≠ ESUCCESS then debug#("gjournal: persistence recover failed") else {gjournal_restore_log#(nx, fi0, fi, jro, gstore0, gstore, nx0, pmaxino, p_os, jvalid1; log; err); ks := jro0.keys}⟫ ( err = ESUCCESS → jvalid1 ∧ jro0 < jmaxino0 ∧ p_os < pmaxino ∧ pmaxino ≤ jmaxino0 ∧ fi0.inos < jmaxino0 ∧ fi.inos < pmaxino ∧ jmaxino0 ≠ 0 ∧ pmaxino ≠ 0 ∧ (false ∧ nx0 ≠ [] → valid-journal-head(nx0, gstore0, jro)) ∧ fi0.lebs ⊆ dom gstore0 ∧ fi.lebs ⊆ dom gstore ∧ refsize-cons(gstore0, range fi0) ∧ refsize-cons(gstore, range fi) ∧ inv(gstore0 \ jro) ∧ inv(gstore) ∧ elems nx0 ∩ jro = ∅ ∧ ¬ dups(nx0) ∧ dom gstore ∪ elems nx0 = dom gstore0 ∪ jro ∧ remove-refsize0(gstore) = gstore ∧ ri-inj(fi0) ∧ ri-inj(fi)), jmaxino = 0, jmaxino3 = 0, dups(nx1)