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