Proof step 18 from proof inv-store (previous step)

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 19:

  jvalid ↔ key ∈ fi, gstore3[@(m0, m1, m2)] = mkgnode(nd, m, boolvar, boolvar0), adr0 = @(m0, m1, m2), fi1 = fi, gstore = gstore2, gstore0 = gstore3, jro = jro0, jvalid, remove-refsize0(gstore2) = gstore2, elems nx ∩ jro0 = ∅, dom gstore2 ∪ elems nx = dom gstore3 ∪ jro0, jro1 < jmaxino, p_os < pmaxino, fi.inos < jmaxino, fi0.inos < pmaxino, inv(gstore3 \ jro0), inv(gstore2), key-cons(key, nd), refsize-cons(gstore3, range fi), refsize-cons(gstore2, range fi0), ri-inj(fi0), ri-inj(fi), key ∈ fi, @(m0, m1, m2) ∈ gstore3, pmaxino ≤ jmaxino, fi.lebs ⊆ dom gstore3, fi0.lebs ⊆ dom gstore2, jvalid1 ∧ nx ≠ [] → valid-journal-head(nx, gstore3, jro0) ⊦ [fi2 := fi[key, adr0]] ( ri-inj(fi2) → ⟪let n = ? in {jro := jro0; gstore1 := gstore3; if jvalid then {index_get_gblock_refsize#(fi[key].lnum, fi2, fi0, jro, gstore3, gstore2, nx, pmaxino, p_os, jvalid0; ; n); index_set_gblock_refsize#(fi[key].lnum, n - fi[key].size, fi2, fi0, jro, gstore2, nx, pmaxino, p_os, jvalid0; gstore3)}; index_get_gblock_refsize#(m0, fi2, fi0, jro, gstore3, gstore2, nx, pmaxino, p_os, jvalid0; ; n); index_set_gblock_refsize#(m0, n + m2, fi2, fi0, jro, gstore2, nx, pmaxino, p_os, jvalid0; gstore3)}; jmaxino := max(key.ino + 1, jmaxino)⟫ ( jro1 < jmaxino ∧ pmaxino ≤ jmaxino ∧ fi1.inos ∪ (key.inode? ⊃ ∅ ++ key.ino;∅) < jmaxino ∧ jmaxino ≠ 0 ∧ (jvalid1 ∧ nx ≠ [] → valid-journal-head(nx, gstore3, jro0)) ∧ fi1[key, @(m0, m1, m2)].lebs ⊆ dom gstore3 ∧ refsize-cons(gstore3, range fi1[key, @(m0, m1, m2)]) ∧ inv(gstore3 \ jro0) ∧ dom gstore2 ∪ elems nx = dom gstore3 ∪ jro0 ∧ gstore3 =○refsize gstore1 ∧ fi2 = fi1[key, @(m0, m1, m2)])), jmaxino = 0, pmaxino = 0, dups(nx), @(m0, m1, m2) ∈ fi

Rule argument

Additional information