| jro = jro0, gstore = crash(gstore0, gstore1, jro0, nx), gstore2 = gstore1, nx0 = nx, pmaxino = jmaxino, p_os = jro1, fi0 = fi1, jro2.keys = ro0, jro1.keys = fo0, fi2 = ri0, fi1 = fi3, log0 = abs-log(nx, gstore0 ↓), fs0 = nodes(gstore0 ↓, jro0), jvalid0 → jvalid1, jvalid1, ri-inj(ri0), ri-inj(fi3), log-cons(log0, fs0), ro0.inodes?, fo0.inodes?, jro2 < jmaxino0, jro1 < jmaxino, jmaxino ≤ jmaxino0, fi2.inos < jmaxino0, fi1.inos < jmaxino, jmaxino0 ≠ 0, jmaxino ≠ 0, jvalid2 ∧ nx ≠ [] → valid-journal-head(nx, gstore0, jro0), fi2.lebs ⊆ dom gstore0, fi1.lebs ⊆ dom gstore1, refsize-cons(gstore0, range fi2), refsize-cons(gstore1, range fi1), inv-journal(nx, gstore0, gstore1, jro0), ri-inj(fi2), ri-inj(fi1), log1 = ax, ks = ks0, jvalid3 ↔ jvalid4 ⊦ ⟪gjournal_recover# (jvalid3; log1, ks, jmaxino1, jro3, fi4, fi0, jro, gstore, gstore2, nx0, pmaxino, p_os, jvalid5; jvalid6, jmaxino2, jvalid4, err)⟫ ( ( err = ESUCCESS → (∃ ri, fi, ro, fo, fs, log, jvalid. (fi = fi3 ∧ fo = fo0 ∧ fs = fs0 ∧ log = log0) ∧ ⟨aubifs_core_recover#(jvalid4; ax, ks0, fi, ro, fo, log, fs; ri, jvalid, err0)⟩ ( ( jro3.keys = ro ∧ p_os.keys = fo ∧ fi4 = ri ∧ fi0 = fi ∧ log = abs-log(nx0, gstore ↓) ∧ fs = nodes(gstore ↓, jro) ∧ (jvalid → jvalid5)) ∧ log1 = ax ∧ ks = ks0 ∧ err = err0))) ∧ ( err ≠ ESUCCESS → (∀ ri, fi, ro, fo, fs, log, jvalid. ⟨aubifs_core_recover#(jvalid4; ax, ks0, fi5, ro1, fo1, log1, fs1; ri1, jvalid7, err0)⟩ (ri = ri1 ∧ fi = fi5 ∧ ro = ro1 ∧ fo = fo1 ∧ fs = fs1 ∧ log = log1 ∧ (jvalid ↔ jvalid7) ∧ log1 = ax ∧ ks = ks0 ∧ err = err0)))) |