Proof step 119 from proof prepost-read-log (previous step)

Heuristic symbolic execution applied rule choose right

And obtained the following new goals

• Proof step 120:

  # buf = # buf1, # buf2 = EB_PAGE_SIZE, LEB_SIZE = n1 + logoff0, avol[m5] = mapped(buf0), buf1 = buf2, err = err0, n = EB_PAGE_SIZE, n0 = 0, logoff0 < LEB_SIZE, m5 < # avol, ebm-vol-inv(avol), is-aligned(logoff0, EB_PAGE_SIZE), is-encoded(log, subarray(buf0, 0, logoff0)), is-encoded(log0, buf0), range=(buf1, 0, buf, 0, n0), range=(buf1, n0 + n, buf, n0 + n, # buf1 - n0 + n), logoff0 ≤ # buf0, logoff0 + EB_PAGE_SIZE ≤ LEB_SIZE, ⌊err0⌋ ∨ err0 = ESUCCESS ⊦ ⟪buf1 := buf; m0 := EB_PAGE_SIZE; buf2 := buf1; if err = ESUCCESS then if buf2 = mkempbuf(# buf2) then err := ENOENT else let rnd = ? in {decode_ref_node#(m0, buf2; rnd; err); if err = ESUCCESS then log := log + rnd.leb '}; logoff := logoff0 + m0⟫ ( logoff ≤ LEB_SIZE ∧ # buf2 = m0 ∧ is-aligned(logoff, # buf2) ∧ (err = ESUCCESS ∨ err = ENOENT ∨ ⌊err⌋ ) ∧ avol[m5].mapped? ∧ (err = ESUCCESS → logoff ≤ # avol[m5].data ∧ is-encoded(log, subarray(avol[m5].data, 0, logoff))) ∧ (err = ENOENT → is-encoded(log, avol[m5].data)) ∧ LEB_SIZE < n1 + logoff), err = ESUCCESS, n1 = 0

• Proof step 126:

  # buf = EB_PAGE_SIZE, LEB_SIZE = n1 + logoff0, avol[m5] = mapped(buf0), buf1 = buf, err = err0, n = EB_PAGE_SIZE, n0 = 0, logoff0 < LEB_SIZE, m5 < # avol, ebm-vol-inv(avol), is-aligned(logoff0, EB_PAGE_SIZE), is-encoded(log, subarray(buf0, 0, logoff0)), is-encoded(log0, buf0), logoff0 ≤ # buf0, logoff0 + EB_PAGE_SIZE ≤ LEB_SIZE, ⌊err0⌋ ∨ err0 = ESUCCESS ⊦ err = ESUCCESS, n1 = 0, ∃ buf. # buf = # buf1 ∧ range=(buf1, 0, buf, 0, n0) ∧ range=(buf1, n0 + n, buf, n0 + n, # buf1 - n0 + n)

• Proof step 128:

  # buf = EB_PAGE_SIZE, LEB_SIZE = n1 + logoff0, avol[m5] = mapped(buf0), buf1 = buf, err = err0, n = EB_PAGE_SIZE, n0 = 0, logoff0 < LEB_SIZE, m5 < # avol, ebm-vol-inv(avol), is-aligned(logoff0, EB_PAGE_SIZE), is-encoded(log, subarray(buf0, 0, logoff0)), is-encoded(log0, buf0), logoff0 ≤ # buf0, logoff0 + EB_PAGE_SIZE ≤ LEB_SIZE, ⌊err0⌋ ∨ err0 = ESUCCESS ⊦ err = ESUCCESS, n1 = 0, ∀ buf. # buf = # buf1 → range=(buf1, 0, buf, 0, n0) → # buf1 ≥ n0 + n

Rule argument

Additional information