| err = err0, fi4 = fi3, gstore3 = crash(gstore2, gstore1, jro4, nx1), gstore4 = gstore1, jro3 = jro4, nx3 = nx1, p_os0 = jro1, pmaxino0 = jmaxino1, remove-refsize0(gstore1) = gstore1, elems nx1 ∩ jro4 = ∅, dom gstore1 ∪ elems nx1 = dom gstore2 ∪ jro4, jro2 < jmaxino3, jro1 < jmaxino1, fi1.inos < jmaxino3, fi3.inos < jmaxino1, inv(gstore2 \ jro4), inv(gstore1), refsize-cons(gstore2, range fi1), refsize-cons(gstore1, range fi3), ri-inj(fi1), ri-inj(fi3), jmaxino1 ≤ jmaxino3, fi1.lebs ⊆ dom gstore2, fi3.lebs ⊆ dom gstore1, jvalid0 ∧ nx1 ≠ [] → valid-journal-head(nx1, gstore2, jro4), ⌊err0⌋ ∨ err0 = ESUCCESS ⊦ ⟪jvalid1 := jvalid, fi0 := fi, gstore1 := gstore, jro4 := jro, jro1 := p_os, jmaxino1 := pmaxino, nx1 := nx, fi3 := fi0, nx2 := nx0; 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, jmaxino1 = 0, jmaxino3 = 0, dups(nx1) |
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)