Proof step 92 from proof inv-gc-copy (previous step)

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 93:

  # ax = # ndx1, jvalid ↔ jvalid0, abs-log(nx, gstore3 ↓) = abs-log(nx1, gstore2 ↓) + ax, fi = fi1, fi0 = fi2[ndx1.keys, ax], gstore = gstore1, gstore0 = gstore3, nodes(gstore3 ↓, jro) = nodes(gstore2 ↓, jro0)[ax, ndx1], remove-refsize0(gstore1) = gstore1, elems nx ∩ jro = ∅, (nx.toSet \ nx1.toSet) ∩ dom gstore2 = ∅, elems nx1 ∩ jro0 = ∅, dom gstore1 ∪ elems nx = dom gstore3 ∪ jro, dom gstore1 ∪ elems nx1 = dom gstore2 ∪ jro0, fi2[ndx1.keys, ax].inos < jmaxino0, fi1.inos < pmaxino, fi2.inos < jmaxino3, p_os < pmaxino, jro2 < jmaxino3, inv(gstore3 \ jro), inv(gstore1), inv(gstore2 \ jro0), inv(gstore3[nx.last]), key-cons(ndx2), key-cons(nd.key, nd), key-cons(ndx1), new(ax, nodes(gstore2 ↓, jro0)), refsize-cons(gstore3, range fi2[ndx1.keys, ax]), refsize-cons(gstore1, range fi1), refsize-cons(gstore2, range fi2), ri-inj(fi2[ndx1.keys, ax]), ri-inj(fi1), ri-inj(fi2), nx.last ∈ gstore3, nd.key ∈ fi2, nd.flashsize ≤ LEB_SIZE, nd.flashsize ≤ n0, n0 ≤ LEB_SIZE, pmaxino ≤ jmaxino0, pmaxino ≤ jmaxino3, jmaxino3 ≤ jmaxino0, dom gstore2 ⊆ dom gstore3, range fi2[ndx1.keys, ax] ⊆ dom nodes(gstore3 ↓, jro), fi2[ndx1.keys, ax].lebs ⊆ dom gstore3, range fi2 ⊆ dom nodes(gstore2 ↓, jro0), ndx2.keys.toSet ⊆ dom fi2, ndx1.keys.toSet ⊆ dom fi2, fi1.lebs ⊆ dom gstore1, fi2.lebs ⊆ dom gstore2, fi2.lebs ⊆ dom gstore3, jvalid7 ∧ nx1 ≠ [] → valid-journal-head(nx1, gstore2, jro0), jvalid1 → valid-journal-head(nx, gstore3, jro) ⊦ ⟪ndx3 := nd ' + ndx2; ndx := []; ndx4 := nd ' + ndx2; gjournal_split_nodes#(LEB_SIZE - n0; ndx4, ndx); fi := fi2[ndx1.keys, ax]; if ndx = [] then err := EINVAL else {ax0 := []; gjournal_journal_addn#(ndx, jvalid2, fi, fi1, gstore1, pmaxino, p_os; ax0, jvalid1, jmaxino1, jro, gstore3, nx, jvalid0; err); if err = ESUCCESS then gjournal_gc_update_index#(jvalid1, fi1, jro, gstore1, nx, pmaxino, p_os, jvalid0; ax0, ndx, jmaxino0, fi, gstore3)}⟫ ( (err = ESUCCESS ∨ ⌊err⌋ ) ∧ (∃ ndx3. ndx1 + nd ' + ndx2 = ndx3 + ndx4) ∧ jmaxino3 ≤ jmaxino0 ∧ (jvalid1 ∧ nx ≠ [] → valid-journal-head(nx, gstore3, jro)) ∧ fi.inos < jmaxino0 ∧ fi.lebs ⊆ dom gstore3 ∧ refsize-cons(gstore3, range fi) ∧ inv(gstore3 \ jro) ∧ elems nx ∩ jro = ∅ ∧ ¬ dups(nx) ∧ dom gstore1 ∪ elems nx = dom gstore3 ∪ jro ∧ ri-inj(fi) ∧ ndx4.keys.toSet ⊆ dom fi ∧ range fi ⊆ dom nodes(gstore3 ↓, jro) ∧ dom gstore2 ⊆ dom gstore3 ∧ (nx.toSet \ nx1.toSet) ∩ dom gstore2 = ∅ ∧ (∃ ax, ndx3, ndx. ndx1 + nd ' + ndx2 = ndx3 + ndx ∧ (err = ESUCCESS → ndx = ndx4) ∧ new(ax, nodes(gstore2 ↓, jro0)) ∧ ¬ dups(ax) ∧ # ax = # ndx3 ∧ fi = fi2[ndx3.keys, ax] ∧ nodes(gstore3 ↓, jro) = nodes(gstore2 ↓, jro0)[ax, ndx3] ∧ abs-log(nx, gstore3 ↓) = abs-log(nx1, gstore2 ↓) + ax) ∧ (err = ESUCCESS ⊃ # ndx4;0) < # ndx3), jmaxino3 = 0, nx = [], pmaxino = 0, dups(nx1), dups(nx), dups(ax), dups(ndx1.keys + ndx2.keys), dups(ndx1.keys), dups(ndx2.keys), nd.key ∈ ndx2.keys, nd.key ∈ ndx1.keys

Rule argument

Additional information