Proof step 29 from proof prepost-write-orphans (previous step)

User applied rule insert program lemma

And obtained the following new goals

• Proof step 30:

  ebm-vol-inv(avol), m < # avol, avol[m].mapped?, # avol[m].data ≤ m0, is-aligned(m0, EB_PAGE_SIZE), is-aligned(n, EB_PAGE_SIZE), m0 + n ≤ LEB_SIZE, n0 + n ≤ # buf ⊦ ⟪ebm_avol_write#(m, m0, n0, n, buf; avol; err)⟫ ebm-vol-inv(avol)

• Proof step 31:

  avol = avol1[n, mapped(mkbuf(0))], n < # avol1, ebm-vol-inv(avol1[n, mapped(mkbuf(0))]), ebm-vol-inv(avol1), is-encoded-pad(orphans0, # orphans0, buf0), # buf0 ≤ LEB_SIZE ⊦ ebm-vol-inv(avol) ∧ n < # avol ∧ avol[n].mapped? ∧ # avol[n].data ≤ 0 ∧ is-aligned(0, EB_PAGE_SIZE) ∧ is-aligned(# buf0, EB_PAGE_SIZE) ∧ 0 + # buf0 ≤ LEB_SIZE ∧ 0 + # buf0 ≤ # buf0

• Proof step 34:

  avol = avol1[n, mapped(mkbuf(0))], buf1 = buf0, m1 = n, m2 = 0, n1 = # buf0, n2 = 0, avol[n].mapped?, n < # avol1, n < # avol, ebm-vol-inv(avol1[n, mapped(mkbuf(0))]), ebm-vol-inv(avol1), ebm-vol-inv(avol), is-aligned(0, EB_PAGE_SIZE), is-aligned(# buf0, EB_PAGE_SIZE), is-encoded-pad(orphans0, # orphans0, buf0), # buf0 ≤ LEB_SIZE, # avol[n].data ≤ 0, 0 + # buf0 ≤ LEB_SIZE, 0 + # buf0 ≤ # buf0 ⊦ [ebm_avol_write#(n, 0, 0, # buf0, buf0; avol; err0)] ( ebm-vol-inv(avol) → (err0 = ESUCCESS ∨ ⌊err0⌋ ) ∧ ebm-vol-inv(avol) ∧ id○(avol, avol1, n) ∧ (err0 = ESUCCESS → avol[n].mapped? ∧ is-encoded-pad(orphans0, # orphans0, avol[n].data)))

Rule argument

Additional information