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

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 94:

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

• Proof step 149:

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

Rule argument

Additional information