Proof step 8 from proof refine-gc (previous step)

Heuristic symbolic execution applied rule let right

And obtained the following new goals

• Proof step 9:

  jvalid1 ↔ jvalid2, jvalid0 ↔ jvalid3, jvalid ↔ jvalid4, fi = ri, fi0 = fi1, fs = nodes(gstore ↓, jro0), jro = jro0, log = abs-log(nx, gstore ↓), remove-refsize0(gstore0) = gstore0, elems nx ∩ jro0 = ∅, dom gstore0 ∪ elems nx = dom gstore ∪ jro0, p_os.keys.inodes?, jro1.keys.inodes?, ri.inos < jmaxino, jro1 < jmaxino, p_os < pmaxino, fi1.inos < pmaxino, inv(gstore0), inv(gstore \ jro0), log-cons(abs-log(nx, gstore ↓), nodes(gstore ↓, jro0)), refsize-cons(gstore, range ri), refsize-cons(gstore0, range fi1), ri-cons(ri, nodes(gstore ↓, jro0)), ri-inj(ri), ri-inj(fi1), pmaxino ≤ jmaxino, ri.lebs ⊆ dom gstore, fi1.lebs ⊆ dom gstore0, jvalid5 → jvalid4, jvalid3 ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro0) ⊦ [index_get_gc_block#(fi, fi0, jro, gstore, gstore0, nx, pmaxino, p_os, jvalid; lnum; err); if err = ESUCCESS then let n = ? in {debug#("gjournal: garbage collecting LEB " + lnum.toString); index_get_gblock_refsize#(lnum, fi, fi0, jro, gstore, gstore0, nx, pmaxino, p_os, jvalid; ; n); if n ≠ 0 then let ax = [], gndx = [], ndx = [] in {index_read_gblock_nodes#(lnum, fi, fi0, jro, gstore, gstore0, nx, pmaxino, p_os, jvalid; ax, gndx; err); if err ≠ ESUCCESS then debug#("gjournal: failed to read LEB " + lnum.toString + " during GC") else gjournal_gc_referenced_nodes#(lnum, fi, fi0, jro, gstore, gstore0, nx, pmaxino, p_os, jvalid; ax, gndx; ndx, err); if err = ESUCCESS then {gjournal_gc_copy# (jvalid1, fi0, gstore0, pmaxino, p_os; ndx, jvalid0, jmaxino0, jmaxino, fi, jro, gstore, nx, jvalid; err); if err ≠ ESUCCESS then debug#("gjournal: failed to copy nodes of LEB " + lnum.toString + " to journal head during GC")}}}; if err = ESUCCESS then index_sync#(fi, fi0, jro, gstore, gstore0, nx, pmaxino, p_os; ; jvalid, err); if err = ESUCCESS then index_deallocate_gnd#(lnum, fi, fi0, gstore0, nx, pmaxino, p_os, jvalid; jro, gstore; err)] ( jro1 < jmaxino ∧ pmaxino ≤ jmaxino ∧ fi.inos < jmaxino ∧ jmaxino ≠ 0 ∧ (jvalid0 ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro)) ∧ fi.lebs ⊆ dom gstore ∧ refsize-cons(gstore, range fi) ∧ inv(gstore \ jro) ∧ elems nx ∩ jro = ∅ ∧ ¬ dups(nx) ∧ dom gstore0 ∪ elems nx = dom gstore ∪ jro ∧ ri-inj(fi) → ⟨aubifs_core_journal_gc#(fi1, jro1.keys, p_os.keys; ri, fs, log; jvalid5)⟩ (fi = ri ∧ log = abs-log(nx, gstore ↓) ∧ fs = nodes(gstore ↓, jro) ∧ (jvalid5 → jvalid))), jmaxino = 0, pmaxino = 0, dups(nx)

Rule argument

Additional information