Proof step 16 from proof refine-write (previous step)

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 17:

  avols[default-volid][m2] = mapped(buf0, n2), avol = abs(avols[default-volid]), err = err0, err = ESUCCESS, avols[default-volid][m2].mapped?, m2 < # avols[default-volid], ebm-cons(avols), ebm-vol-inv(abs(avols[default-volid])), is-aligned(n, EB_PAGE_SIZE), is-aligned(m1, EB_PAGE_SIZE), default-volid ∈ avols, 0 + m1 ≤ # avols[default-volid][m2].data, n3 + n ≤ # buf, m1 + n ≤ LEB_SIZE, n2 ≤ m1, LEB_SIZE - m1 ≥ n, LEB_SIZE ≥ m1, ⌊err0⌋ ∨ err0 = ESUCCESS ⊦ ⟨ebm_avol_write#(m2, m1, n3, n, buf; avol; err1)⟩ ( avol = abs (avols [default-volid, avols[default-volid] [m2, mapped(subarray(avols[default-volid][m2].data, 0, m1) + subarray(buf, n3, n) + mkempbuf(LEB_SIZE - m1 - n), m1 + n) ] ] [default-volid ]) ∧ err = err1), n = 0

• Proof step 65:

  avols[default-volid][m2] = mapped(buf0, n2), avol = abs(avols[default-volid]), err = err0, err = ESUCCESS, m2 < # avols[default-volid], ebm-cons(avols), ebm-vol-inv(abs(avols[default-volid])), is-aligned(n, EB_PAGE_SIZE), is-aligned(m1, EB_PAGE_SIZE), default-volid ∈ avols, n3 + n ≤ # buf, m1 + n ≤ LEB_SIZE, n2 ≤ m1, ⌊err0⌋ ∨ err0 = ESUCCESS ⊦ n = 0, m2 < # avols[default-volid] ∧ default-volid ∈ avols ∧ (0 + m1 ≤ # avols[default-volid][m2].data ∧ avols[default-volid][m2].mapped? ∧ m2 < # avols[default-volid] ∧ default-volid ∈ avols) ∧ n3 + n ≤ # buf ∧ LEB_SIZE - m1 ≥ n ∧ LEB_SIZE ≥ m1

Rule argument

Additional information