| err = err0, 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 ⊦ ⟪p_os := jro1; nx := nx1; jro := jro4; gstore0 := crash(gstore2, gstore1, jro4, nx1); gstore := gstore1; fi0 := fi3; if err = ESUCCESS then jmaxino := pmaxino, jvalid := true, nx0 := nx, jro0 := p_os, fi := fi0 else jro := ?, jvalid := ?, gstore0 := ?, gstore := ?, nx := ?, pmaxino := ?, p_os := ?, jmaxino := ?, nx0 := ?, jro0 := ?, fi := ?, fi0 := ?; 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) |
err = err0, p_os = jro1, pmaxino = jmaxino1, remove-refsize0(gstore1) = gstore1, elems nx1 ∩ jro4 = ∅, dom gstore1 ∪ elems nx1 = dom gstore2 ∪ jro4, fi3.inos < jmaxino1, fi1.inos < jmaxino3, jro1 < jmaxino1, jro2 < jmaxino3, inv(gstore1), inv(gstore2 \ jro4), refsize-cons(gstore1, range fi3), refsize-cons(gstore2, range fi1), ri-inj(fi3), ri-inj(fi1), jmaxino1 ≤ jmaxino3, fi3.lebs ⊆ dom gstore1, fi1.lebs ⊆ dom gstore2, jvalid0 ∧ nx1 ≠ [] → valid-journal-head(nx1, gstore2, jro4), ⌊err0⌋ ∨ err0 = ESUCCESS ⊦ ⟪nx := nx1; jro := jro4; gstore0 := crash(gstore2, gstore1, jro4, nx1); gstore := gstore1; fi0 := fi3; if err = ESUCCESS then jmaxino := pmaxino, jvalid := true, nx0 := nx, jro0 := p_os, fi := fi0 else jro := ?, jvalid := ?, gstore0 := ?, gstore := ?, nx := ?, pmaxino := ?, p_os := ?, jmaxino := ?, nx0 := ?, jro0 := ?, fi := ?, fi0 := ?; 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)