| gstore2[n1] = groupblock(gndx0, lax, m), remove-refsize0(gstore1) = gstore1, elems nx ∩ jro0 = ∅, dom gstore1 ∪ elems nx = dom gstore2 ∪ jro0, jmaxino ≠ 0, m ≠ 0, pmaxino ≠ 0, jro1.keys.inodes?, p_os.keys.inodes?, fi1.inos < pmaxino, p_os < pmaxino, jro1 < jmaxino, ri.inos < jmaxino, inv(groupblock(gndx0, lax, m)), inv(gstore2 \ jro0), inv(gstore1), log-cons(abs-log(nx, gstore2 ↓), nodes(gstore2 ↓, jro0)), refsize-cons(gstore1, range fi1), refsize-cons(gstore2, range ri), ri-cons(ri, nodes(gstore2 ↓, jro0)), ri-inj(fi1), ri-inj(ri), n1 ∈ gstore1, n1 ∈ gstore2, pmaxino ≤ jmaxino, fi1.lebs ⊆ dom gstore1, ri.lebs ⊆ dom gstore2, ⌊err0⌋ , ¬ dups(nx), ¬ n1 ∈ nx, ¬ n1 ∈ jro0, jvalid3 ∧ nx ≠ [] → valid-journal-head(nx, gstore2, jro0), jvalid5 → jvalid4 ⊦ [debug#("gjournal: failed to read LEB " + n1.toString + " during GC"); log := abs-log(nx, gstore2 ↓); fs := nodes(gstore2 ↓, jro0); fi0 := fi1; fi := ri; if err0 = ESUCCESS then {ndx := []; gjournal_gc_copy#(jvalid1, fi0, gstore1, pmaxino, p_os; ndx, jvalid3, jmaxino0, jmaxino, fi, jro0, gstore2, nx, jvalid4; err0); if err0 ≠ ESUCCESS then debug#("gjournal: failed to copy nodes of LEB " + n1.toString + " to journal head during GC")}; if err0 = ESUCCESS then index_sync#(fi, fi0, jro0, gstore2, gstore1, nx, pmaxino, p_os; ; jvalid4, err0); if err0 = ESUCCESS then index_deallocate_gnd#(n1, fi, fi0, gstore1, nx, pmaxino, p_os, jvalid4; jro0, gstore2; err0)] ( jro1 < jmaxino ∧ pmaxino ≤ jmaxino ∧ fi.inos < jmaxino ∧ jmaxino ≠ 0 ∧ (jvalid3 ∧ nx ≠ [] → valid-journal-head(nx, gstore2, jro0)) ∧ fi.lebs ⊆ dom gstore2 ∧ refsize-cons(gstore2, range fi) ∧ inv(gstore2 \ jro0) ∧ elems nx ∩ jro0 = ∅ ∧ ¬ dups(nx) ∧ dom gstore1 ∪ elems nx = dom gstore2 ∪ jro0 ∧ ri-inj(fi) → ⟨aubifs_core_journal_gc#(fi1, jro1.keys, p_os.keys; ri, fs, log; jvalid5)⟩ (fi = ri ∧ log = abs-log(nx, gstore2 ↓) ∧ fs = nodes(gstore2 ↓, jro0) ∧ (jvalid5 → jvalid4))) |
⊦ ⟪debug#(str)⟫ true
gstore2[n1] = groupblock(gndx0, lax, m), remove-refsize0(gstore1) = gstore1, str0 = "gjournal: failed to read LEB " + n1.toString + " during GC", elems nx ∩ jro0 = ∅, dom gstore1 ∪ elems nx = dom gstore2 ∪ jro0, p_os.keys.inodes?, jro1.keys.inodes?, ri.inos < jmaxino, jro1 < jmaxino, p_os < pmaxino, fi1.inos < pmaxino, inv(gstore1), inv(gstore2 \ jro0), inv(groupblock(gndx0, lax, m)), log-cons(abs-log(nx, gstore2 ↓), nodes(gstore2 ↓, jro0)), refsize-cons(gstore2, range ri), refsize-cons(gstore1, range fi1), ri-cons(ri, nodes(gstore2 ↓, jro0)), ri-inj(ri), ri-inj(fi1), n1 ∈ gstore2, n1 ∈ gstore1, pmaxino ≤ jmaxino, ri.lebs ⊆ dom gstore2, fi1.lebs ⊆ dom gstore1, ⌊err0⌋ , jvalid5 → jvalid4, jvalid3 ∧ nx ≠ [] → valid-journal-head(nx, gstore2, jro0) ⊦ ∀ . true → [log := abs-log(nx, gstore2 ↓); fs := nodes(gstore2 ↓, jro0); fi0 := fi1; fi := ri; if err0 = ESUCCESS then {ndx := []; gjournal_gc_copy#(jvalid1, fi0, gstore1, pmaxino, p_os; ndx, jvalid3, jmaxino0, jmaxino, fi, jro0, gstore2, nx, jvalid4; err0); if err0 ≠ ESUCCESS then debug#("gjournal: failed to copy nodes of LEB " + n1.toString + " to journal head during GC")}; if err0 = ESUCCESS then index_sync#(fi, fi0, jro0, gstore2, gstore1, nx, pmaxino, p_os; ; jvalid4, err0); if err0 = ESUCCESS then index_deallocate_gnd#(n1, fi, fi0, gstore1, nx, pmaxino, p_os, jvalid4; jro0, gstore2; err0)] ( jro1 < jmaxino ∧ pmaxino ≤ jmaxino ∧ fi.inos < jmaxino ∧ jmaxino ≠ 0 ∧ (jvalid3 ∧ nx ≠ [] → valid-journal-head(nx, gstore2, jro0)) ∧ fi.lebs ⊆ dom gstore2 ∧ refsize-cons(gstore2, range fi) ∧ inv(gstore2 \ jro0) ∧ elems nx ∩ jro0 = ∅ ∧ ¬ dups(nx) ∧ dom gstore1 ∪ elems nx = dom gstore2 ∪ jro0 ∧ ri-inj(fi) → ⟨aubifs_core_journal_gc#(fi1, jro1.keys, p_os.keys; ri, fs, log; jvalid5)⟩ (fi = ri ∧ log = abs-log(nx, gstore2 ↓) ∧ fs = nodes(gstore2 ↓, jro0) ∧ (jvalid5 → jvalid4))), jmaxino = 0, m = 0, pmaxino = 0, dups(nx), n1 ∈ nx, n1 ∈ jro0