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

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 56:

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

• Proof step 74:

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

Rule argument

Additional information