Proof step 13 from proof inv-write (previous step)

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 14:

  avols[v][m2].mapped?, m2 < # avols[v], ebm-cons(avols), is-aligned(m1, EB_PAGE_SIZE), is-aligned(n, EB_PAGE_SIZE), v ∈ avols, 0 + m1 ≤ # avols[v][m2].data, n2 + n ≤ # buf, m1 + n ≤ LEB_SIZE, n + n2 ≤ # buf, avols[v][m2].fill ≤ m1, LEB_SIZE - m1 ≥ n, LEB_SIZE ≥ m1 ⊦ n = 0, ebm-cons(avols[v, avols[v][m2, mapped(subarray(avols[v][m2].data, 0, m1) + subarray(buf, n2, n) + mkempbuf(LEB_SIZE - m1 - n), m1 + n)]])

• Proof step 32:

  avols[v][m2].mapped?, m2 < # avols[v], ebm-cons(avols), is-aligned(m1, EB_PAGE_SIZE), is-aligned(n, EB_PAGE_SIZE), v ∈ avols, m1 + n ≤ LEB_SIZE, n + n2 ≤ # buf, avols[v][m2].fill ≤ m1 ⊦ n = 0, m2 < # avols[v] ∧ v ∈ avols ∧ (0 + m1 ≤ # avols[v][m2].data ∧ avols[v][m2].mapped? ∧ m2 < # avols[v] ∧ v ∈ avols) ∧ n2 + n ≤ # buf ∧ LEB_SIZE - m1 ≥ n ∧ LEB_SIZE ≥ m1

Rule argument

Additional information