Proof step 26 from proof inv-allocate (previous step)

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 27:

  jvalid ↔ jvalid0, fi = fi1, fi0 = fi2, gstore = gstore2, gstore0 = gstore3, gstore1 = gstore3, jro0 = jro, nx0 = nx, remove-refsize0(gstore2) = gstore2, elems nx ∩ jro = ∅, dom gstore2 ∪ elems nx = dom gstore3 ∪ jro, fi1.inos < pmaxino, fi2.inos < jmaxino1, p_os < pmaxino, inv(gstore2), inv(gstore3 \ jro), inv(gstore3[nx.last]), refsize-cons(gstore2, range fi1), refsize-cons(gstore3, range fi2), ri-inj(fi1), ri-inj(fi2), valid-journal-head(nx, gstore3, jro), nx.last ∈ gstore3, n0 ≤ LEB_SIZE, pmaxino ≤ jmaxino1, jmaxino ≤ LEB_SIZE, fi1.lebs ⊆ dom gstore2, fi2.lebs ⊆ dom gstore3 ⊦ ⟪jvalid1 := true; if jvalid1 ∧ jmaxino ≤ n0 then err := ESUCCESS else {index_sync#(fi2, fi1, jro, gstore3, gstore2, nx, pmaxino, p_os; ; jvalid0, err); if err = ESUCCESS then index_allocate_gnd#(fi2, fi1, gstore2, pmaxino, p_os, jvalid0; jro, gstore3, nx; err); if err = ESUCCESS then jvalid1 := true}⟫ ( (jvalid1 ∧ nx ≠ [] → valid-journal-head(nx, gstore3, jro)) ∧ fi2.lebs ⊆ dom gstore3 ∧ refsize-cons(gstore3, range fi2) ∧ inv(gstore3 \ jro) ∧ elems nx ∩ jro = ∅ ∧ ¬ dups(nx) ∧ dom gstore2 ∪ elems nx = dom gstore3 ∪ jro ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ dom gstore1 ⊆ dom gstore3 ∧ (nx.toSet \ nx0.toSet) ∩ dom gstore1 = ∅ ∧ abs-log(nx, gstore3 ↓) = abs-log(nx0, gstore1 ↓) ∧ nodes(gstore3 ↓, jro) = nodes(gstore1 ↓, jro0) ∧ (err = ESUCCESS → jvalid1 ∧ nx ≠ [])), nx = [], pmaxino = 0, dups(nx)

Rule argument

Additional information