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