| # ax = # ndx3, # lax = # gndx0, ndx3 + ndx2 = nodes(gstore2 ↓, jro0)[referenced-adrs(lax.to-adr(n1), ri)], gstore2[n1] = groupblock(gndx0, lax, m0), abs-log(nx0, gstore ↓) = abs-log(nx, gstore2 ↓) + ax, nodes(gstore ↓, jro) = nodes(gstore2 ↓, jro0)[ax, ndx3], remove-refsize0(gstore1) = gstore1, str0 = "gjournal: failed to copy nodes of LEB " + n1.toString + " to journal head during GC", elems nx0 ∩ jro = ∅, (nx0.toSet \ nx.toSet) ∩ dom gstore2 = ∅, elems nx ∩ jro0 = ∅, dom gstore1 ∪ elems nx0 = dom gstore ∪ jro, dom gstore1 ∪ elems nx = dom gstore2 ∪ jro0, p_os.keys.inodes?, jro1.keys.inodes?, jro1 < jmaxino0, ri[ndx3.keys, ax].inos < jmaxino0, jro1 < jmaxino, p_os < pmaxino, ri.inos < jmaxino, fi1.inos < pmaxino, inv(gstore \ jro), inv(groupblock(gndx0, lax, m0)), inv(gstore1), inv(gstore2 \ jro0), log-cons(abs-log(nx, gstore2 ↓), nodes(gstore2 ↓, jro0)), new(ax, nodes(gstore2 ↓, jro0)), refsize-cons(gstore, range ri[ndx3.keys, ax]), refsize-cons(gstore2, range ri), refsize-cons(gstore1, range fi1), ri-cons(ri, nodes(gstore2 ↓, jro0)), ri-inj(ri[ndx3.keys, ax]), ri-inj(ri), ri-inj(fi1), n1 ∈ gstore1, n1 ∈ gstore2, pmaxino ≤ jmaxino0, jmaxino ≤ jmaxino0, pmaxino ≤ jmaxino, ri[ndx3.keys, ax].lebs ⊆ dom gstore, dom gstore2 ⊆ dom gstore, ri.lebs ⊆ dom gstore2, fi1.lebs ⊆ dom gstore1, range ri ⊆ dom nodes(gstore2 ↓, jro0), ri.lebs ⊆ dom gstore, ⌊err⌋ , jvalid0 ∧ nx0 ≠ [] → valid-journal-head(nx0, gstore, jro), jvalid5 → jvalid4, jvalid3 ∧ nx ≠ [] → valid-journal-head(nx, gstore2, jro0) ⊦ ∀ . true → [fi0 := fi1; fi2 := ri[ndx3.keys, ax]; if err = ESUCCESS then index_sync#(fi2, fi0, jro, gstore, gstore1, nx0, pmaxino, p_os; ; jvalid, err); if err = ESUCCESS then index_deallocate_gnd#(n1, fi2, fi0, gstore1, nx0, pmaxino, p_os, jvalid; jro, gstore; err)] ( (jvalid0 ∧ nx0 ≠ [] → valid-journal-head(nx0, gstore, jro)) ∧ fi2.lebs ⊆ dom gstore ∧ refsize-cons(gstore, range fi2) ∧ inv(gstore \ jro) ∧ elems nx0 ∩ jro = ∅ ∧ dom gstore1 ∪ elems nx0 = dom gstore ∪ jro → ⟨log := abs-log(nx, gstore2 ↓); fs := nodes(gstore2 ↓, jro0); aubifs_core_journal_gc#(fi1, jro1.keys, p_os.keys; ri, fs, log; jvalid5)⟩ (fi2 = ri ∧ log = abs-log(nx0, gstore ↓) ∧ fs = nodes(gstore ↓, jro) ∧ (jvalid5 → jvalid))), jmaxino = 0, jmaxino0 = 0, m0 = 0, pmaxino = 0, dups(ndx2.keys), dups(ndx3.keys), dups(ndx3.keys + ndx2.keys), dups(ax), dups(nx0), dups(nx), n1 ∈ jro0, n1 ∈ nx |
# lax = # gndx0, # ax = # ndx3, ndx3 + ndx2 = nodes(gstore2 ↓, jro0)[referenced-adrs(lax.to-adr(n1), ri)], gstore2[n1] = groupblock(gndx0, lax, m0), abs-log(nx0, gstore ↓) = abs-log(nx, gstore2 ↓) + ax, nodes(gstore ↓, jro) = nodes(gstore2 ↓, jro0)[ax, ndx3], remove-refsize0(gstore1) = gstore1, elems nx ∩ jro0 = ∅, (nx0.toSet \ nx.toSet) ∩ dom gstore2 = ∅, elems nx0 ∩ jro = ∅, dom gstore1 ∪ elems nx = dom gstore2 ∪ jro0, dom gstore1 ∪ elems nx0 = dom gstore ∪ jro, jmaxino ≠ 0, jmaxino0 ≠ 0, m0 ≠ 0, pmaxino ≠ 0, jro1.keys.inodes?, p_os.keys.inodes?, fi1.inos < pmaxino, ri.inos < jmaxino, p_os < pmaxino, jro1 < jmaxino, ri[ndx3.keys, ax].inos < jmaxino0, jro1 < jmaxino0, inv(gstore2 \ jro0), inv(gstore1), inv(groupblock(gndx0, lax, m0)), inv(gstore \ jro), log-cons(abs-log(nx, gstore2 ↓), nodes(gstore2 ↓, jro0)), new(ax, nodes(gstore2 ↓, jro0)), refsize-cons(gstore1, range fi1), refsize-cons(gstore2, range ri), refsize-cons(gstore, range ri[ndx3.keys, ax]), ri-cons(ri, nodes(gstore2 ↓, jro0)), ri-inj(fi1), ri-inj(ri), ri-inj(ri[ndx3.keys, ax]), n1 ∈ gstore2, n1 ∈ gstore1, pmaxino ≤ jmaxino, jmaxino ≤ jmaxino0, pmaxino ≤ jmaxino0, ri.lebs ⊆ dom gstore, range ri ⊆ dom nodes(gstore2 ↓, jro0), fi1.lebs ⊆ dom gstore1, ri.lebs ⊆ dom gstore2, dom gstore2 ⊆ dom gstore, ri[ndx3.keys, ax].lebs ⊆ dom gstore, ⌊err⌋ , ¬ dups(nx), ¬ dups(nx0), ¬ dups(ax), ¬ dups(ndx3.keys + ndx2.keys), ¬ dups(ndx3.keys), ¬ dups(ndx2.keys), ¬ n1 ∈ nx, ¬ n1 ∈ jro0, jvalid3 ∧ nx ≠ [] → valid-journal-head(nx, gstore2, jro0), jvalid5 → jvalid4, jvalid0 ∧ nx0 ≠ [] → valid-journal-head(nx0, gstore, jro) ⊦ [fi0 := fi1; fi2 := ri[ndx3.keys, ax]; if err = ESUCCESS then index_sync#(fi2, fi0, jro, gstore, gstore1, nx0, pmaxino, p_os; ; jvalid, err); if err = ESUCCESS then index_deallocate_gnd#(n1, fi2, fi0, gstore1, nx0, pmaxino, p_os, jvalid; jro, gstore; err)] ( (jvalid0 ∧ nx0 ≠ [] → valid-journal-head(nx0, gstore, jro)) ∧ fi2.lebs ⊆ dom gstore ∧ refsize-cons(gstore, range fi2) ∧ inv(gstore \ jro) ∧ elems nx0 ∩ jro = ∅ ∧ dom gstore1 ∪ elems nx0 = dom gstore ∪ jro → ⟨log := abs-log(nx, gstore2 ↓); fs := nodes(gstore2 ↓, jro0); aubifs_core_journal_gc#(fi1, jro1.keys, p_os.keys; ri, fs, log; jvalid5)⟩ (fi2 = ri ∧ log = abs-log(nx0, gstore ↓) ∧ fs = nodes(gstore ↓, jro) ∧ (jvalid5 → jvalid)))