Proof step 73 from proof refine-read (previous step)

Heuristic symbolic execution applied rule choose right

And obtained the following new goals

• Proof step 74:

  # buf1 = # buf, avols[default-volid][m2] = mapped(buf0, n1), buf = buf2, err = err0, n = n2, n0 = n3, m2 < # avols[default-volid], ebm-cons(avols), ebm-vol-inv(abs(avols[default-volid])), range=(buf1, 0, buf, 0, n0), range=(buf1, n0 + n, buf, n0 + n, # buf - n0 + n), default-volid ∈ avols, m1 + n2 ≤ LEB_SIZE, n3 + n2 ≤ # buf2, ⌊err0⌋ ∨ err0 = ESUCCESS ⊦ ⟪buf := buf1⟫ ⟨ebm_avol_read#(m2, m1, n3, n2, abs(avols[default-volid]); buf2; err1)⟩ (buf = buf2 ∧ err = err1), err = ESUCCESS

• Proof step 98:

  avols[default-volid][m2] = mapped(buf1, n1), buf = buf2, err = err0, n = n2, n0 = n3, m2 < # avols[default-volid], ebm-cons(avols), ebm-vol-inv(abs(avols[default-volid])), default-volid ∈ avols, m1 + n2 ≤ LEB_SIZE, n3 + n2 ≤ # buf2, ⌊err0⌋ ∨ err0 = ESUCCESS ⊦ err = ESUCCESS, ∃ buf1. # buf1 = # buf ∧ range=(buf1, 0, buf, 0, n0) ∧ range=(buf1, n0 + n, buf, n0 + n, # buf - n0 + n)

• Proof step 101:

  avols[default-volid][m2] = mapped(buf1, n1), buf = buf2, err = err0, n = n2, n0 = n3, m2 < # avols[default-volid], ebm-cons(avols), ebm-vol-inv(abs(avols[default-volid])), default-volid ∈ avols, m1 + n2 ≤ LEB_SIZE, n3 + n2 ≤ # buf2, ⌊err0⌋ ∨ err0 = ESUCCESS ⊦ err = ESUCCESS, ∀ buf1. # buf1 = # buf → range=(buf1, 0, buf, 0, n0) → # buf ≥ n0 + n

Rule argument

Additional information