| jvalid1 ↔ jvalid, err = err0, fi0 = fi, fi3 = fi2, fi4 = fi5, gstore1 = gstore, gstore3 = crash(gstore2, gstore5, jro5, nx4), gstore4 = gstore5, jmaxino1 = pmaxino, jro1 = p_os, jro3 = jro5, jro4 = jro, nx1 = nx, nx2 = nx0, nx3 = nx4, p_os0 = jro6, pmaxino0 = jmaxino0, remove-refsize0(gstore5) = gstore5, elems nx4 ∩ jro5 = ∅, dom gstore5 ∪ elems nx4 = dom gstore2 ∪ jro5, fi5.inos < jmaxino0, fi1.inos < jmaxino3, jro6 < jmaxino0, jro2 < jmaxino3, inv(gstore5), inv(gstore2 \ jro5), refsize-cons(gstore5, range fi5), refsize-cons(gstore2, range fi1), ri-inj(fi5), ri-inj(fi1), jmaxino0 ≤ jmaxino3, fi5.lebs ⊆ dom gstore5, fi1.lebs ⊆ dom gstore2, jvalid0 ∧ nx4 ≠ [] → valid-journal-head(nx4, gstore2, jro5), ⌊err0⌋ ∨ err0 = ESUCCESS ⊦ ⟪if err ≠ ESUCCESS then debug#("gjournal: persistence recover failed") else {gjournal_restore_log#(nx2, fi0, fi3, jro4, gstore0, gstore1, nx1, jmaxino1, jro1, jvalid1; log; err); ks := jro0.keys}⟫ ( err = ESUCCESS → jvalid1 ∧ jro0 < jmaxino ∧ jro1 < jmaxino1 ∧ jmaxino1 ≤ jmaxino ∧ fi0.inos < jmaxino ∧ fi3.inos < jmaxino1 ∧ jmaxino ≠ 0 ∧ jmaxino1 ≠ 0 ∧ fi0.lebs ⊆ dom gstore0 ∧ fi3.lebs ⊆ dom gstore1 ∧ refsize-cons(gstore0, range fi0) ∧ refsize-cons(gstore1, range fi3) ∧ inv(gstore0 \ jro4) ∧ inv(gstore1) ∧ elems nx1 ∩ jro4 = ∅ ∧ ¬ dups(nx1) ∧ dom gstore1 ∪ elems nx1 = dom gstore0 ∪ jro4 ∧ remove-refsize0(gstore1) = gstore1 ∧ ri-inj(fi0) ∧ ri-inj(fi3)), err = ESUCCESS, jmaxino0 = 0, jmaxino3 = 0, dups(nx4) |
jvalid1 ↔ jvalid, err = err0, fi0 = fi, fi3 = fi2, fi4 = fi5, gstore1 = gstore, gstore3 = crash(gstore2, gstore5, jro5, nx4), gstore4 = gstore5, jmaxino1 = pmaxino, jro1 = p_os, jro3 = jro5, jro4 = jro, nx1 = nx, nx2 = nx0, nx3 = nx4, p_os0 = jro6, pmaxino0 = jmaxino0, remove-refsize0(gstore5) = gstore5, elems nx4 ∩ jro5 = ∅, dom gstore5 ∪ elems nx4 = dom gstore2 ∪ jro5, jro2 < jmaxino3, jro6 < jmaxino0, fi1.inos < jmaxino3, fi5.inos < jmaxino0, inv(gstore2 \ jro5), inv(gstore5), refsize-cons(gstore2, range fi1), refsize-cons(gstore5, range fi5), ri-inj(fi1), ri-inj(fi5), jmaxino0 ≤ jmaxino3, fi1.lebs ⊆ dom gstore2, fi5.lebs ⊆ dom gstore5, jvalid0 ∧ nx4 ≠ [] → valid-journal-head(nx4, gstore2, jro5), ⌊err0⌋ ∨ err0 = ESUCCESS ⊦ ⟪debug#("gjournal: persistence recover failed")⟫ ( err = ESUCCESS → jvalid1 ∧ jro0 < jmaxino ∧ jro1 < jmaxino1 ∧ jmaxino1 ≤ jmaxino ∧ fi0.inos < jmaxino ∧ fi3.inos < jmaxino1 ∧ jmaxino ≠ 0 ∧ jmaxino1 ≠ 0 ∧ fi0.lebs ⊆ dom gstore0 ∧ fi3.lebs ⊆ dom gstore1 ∧ refsize-cons(gstore0, range fi0) ∧ refsize-cons(gstore1, range fi3) ∧ inv(gstore0 \ jro4) ∧ inv(gstore1) ∧ elems nx1 ∩ jro4 = ∅ ∧ ¬ dups(nx1) ∧ dom gstore1 ∪ elems nx1 = dom gstore0 ∪ jro4 ∧ remove-refsize0(gstore1) = gstore1 ∧ ri-inj(fi0) ∧ ri-inj(fi3)), err = ESUCCESS, jmaxino0 = 0, jmaxino3 = 0, dups(nx4)