| jvalid1 ↔ jvalid, err = err0, fi = fi1, fi0 = fi4, fi2 = fi3, gstore1 = gstore, gstore3 = crash(gstore2, gstore5, jro4, nx1), gstore4 = gstore5, jmaxino1 = pmaxino, jro2 = jro, jro3 = p_os, jro5 = jro4, ks = ks0, log = ax, nx2 = nx0, nx3 = nx, nx4 = nx1, p_os0 = jro1, pmaxino0 = jmaxino, remove-refsize0(gstore5) = gstore5, elems nx1 ∩ jro4 = ∅, dom gstore5 ∪ elems nx1 = dom gstore2 ∪ jro4, jro1.keys.inodes?, jro6.keys.inodes?, fi3.inos < jmaxino, ri0.inos < jmaxino3, jro1 < jmaxino, jro6 < jmaxino3, inv(gstore5), inv(gstore2 \ jro4), log-cons(abs-log(nx1, gstore2 ↓), nodes(gstore2 ↓, jro4)), refsize-cons(gstore5, range fi3), refsize-cons(gstore2, range ri0), ri-inj(fi3), ri-inj(ri0), jmaxino ≤ jmaxino3, fi3.lebs ⊆ dom gstore5, ri0.lebs ⊆ dom gstore2, jvalid8 ∧ nx1 ≠ [] → valid-journal-head(nx1, gstore2, jro4), ⌊err0⌋ ∨ err0 = ESUCCESS ⊦ ⟪if err ≠ ESUCCESS then debug#("gjournal: persistence recover failed") else {gjournal_restore_log#(nx2, fi0, fi, jro2, gstore0, gstore1, nx3, jmaxino1, jro3, jvalid1; log; err); ks := jro0.keys}⟫ ( ( err = ESUCCESS → (∃ ro. ⟨log0 := abs-log(nx1, gstore2 ↓); fs0 := nodes(gstore2 ↓, jro4); fo0 := jro1.keys; aubifs_core_recover#(jvalid2; ax, ks0, fi3, ro, fo0, log0, fs0; ri, jvalid, err1)⟩ ( jro0.keys = ro ∧ jro3.keys = fo0 ∧ fi0 = ri ∧ fi = fi3 ∧ log0 = abs-log(nx3, gstore0 ↓) ∧ fs0 = nodes(gstore0 ↓, jro2) ∧ (jvalid → jvalid1) ∧ log = ax ∧ ks = ks0 ∧ ESUCCESS = err1))) ∧ ( err ≠ ESUCCESS → (∀ ri, fi, ro, fo, fs, log0, jvalid0. ⟨aubifs_core_recover#(jvalid2; ax, ks0, fi5, ro1, fo1, log, fs1; ri1, jvalid7, err1)⟩ (ri = ri1 ∧ fi = fi5 ∧ ro = ro1 ∧ fo = fo1 ∧ fs = fs1 ∧ log0 = ax ∧ (jvalid0 ↔ jvalid7) ∧ log = ax ∧ ks = ks0 ∧ err = err1)))), err = ESUCCESS, jmaxino = 0, jmaxino3 = 0, dups(nx1) |
jvalid1 ↔ jvalid, err = err0, fi = fi1, fi0 = fi4, fi2 = fi3, gstore1 = gstore, gstore3 = crash(gstore2, gstore5, jro4, nx1), gstore4 = gstore5, jmaxino1 = pmaxino, jro2 = jro, jro3 = p_os, jro5 = jro4, ks = ks0, log = ax, nx2 = nx0, nx3 = nx, nx4 = nx1, p_os0 = jro1, pmaxino0 = jmaxino, remove-refsize0(gstore5) = gstore5, elems nx1 ∩ jro4 = ∅, dom gstore5 ∪ elems nx1 = dom gstore2 ∪ jro4, jro6.keys.inodes?, jro1.keys.inodes?, jro6 < jmaxino3, jro1 < jmaxino, ri0.inos < jmaxino3, fi3.inos < jmaxino, inv(gstore2 \ jro4), inv(gstore5), log-cons(abs-log(nx1, gstore2 ↓), nodes(gstore2 ↓, jro4)), refsize-cons(gstore2, range ri0), refsize-cons(gstore5, range fi3), ri-inj(ri0), ri-inj(fi3), jmaxino ≤ jmaxino3, ri0.lebs ⊆ dom gstore2, fi3.lebs ⊆ dom gstore5, jvalid8 ∧ nx1 ≠ [] → valid-journal-head(nx1, gstore2, jro4), ⌊err0⌋ ∨ err0 = ESUCCESS ⊦ ⟪debug#("gjournal: persistence recover failed")⟫ ( ( err = ESUCCESS → (∃ ro. ⟨log0 := abs-log(nx1, gstore2 ↓); fs0 := nodes(gstore2 ↓, jro4); fo0 := jro1.keys; aubifs_core_recover#(jvalid2; ax, ks0, fi3, ro, fo0, log0, fs0; ri, jvalid, err1)⟩ ( jro0.keys = ro ∧ jro3.keys = fo0 ∧ fi0 = ri ∧ fi = fi3 ∧ log0 = abs-log(nx3, gstore0 ↓) ∧ fs0 = nodes(gstore0 ↓, jro2) ∧ (jvalid → jvalid1) ∧ log = ax ∧ ks = ks0 ∧ ESUCCESS = err1))) ∧ ( err ≠ ESUCCESS → (∀ ri, fi, ro, fo, fs, log0, jvalid0. ⟨aubifs_core_recover#(jvalid2; ax, ks0, fi5, ro1, fo1, log, fs1; ri1, jvalid7, err1)⟩ (ri = ri1 ∧ fi = fi5 ∧ ro = ro1 ∧ fo = fo1 ∧ fs = fs1 ∧ log0 = ax ∧ (jvalid0 ↔ jvalid7) ∧ log = ax ∧ ks = ks0 ∧ err = err1)))), err = ESUCCESS, jmaxino = 0, jmaxino3 = 0, dups(nx1)