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