Proof step 54 from proof prepost-read-superblock (previous step)

Heuristic symbolic execution applied rule choose right

And obtained the following new goals

• Proof step 55:

  # buf1 = # buf, avol[0] = mapped(buf0), buf = mkbuf(LEB_SIZE), err = err0, m2 = LEB_SIZE, n0 = 0, ebm-vol-inv(avol), is-encoded(sb0, buf0), range=(buf, 0, buf1, 0, n0), range=(buf, n0 + m2, buf1, n0 + m2, # buf - n0 + m2), ⌊err0⌋ ∨ err0 = ESUCCESS ⊦ ⟪buf := buf1; if err = ESUCCESS then let m = ? in decode_superblock#(0, buf, EB_PAGE_SIZE; sb, m; err)⟫ ((err = ESUCCESS ∨ ⌊err⌋ ) ∧ (err = ESUCCESS → sb = sb0)), # avol = 0, err = ESUCCESS

• Proof step 58:

  avol[0] = mapped(buf1), buf = mkbuf(LEB_SIZE), err = err0, m2 = LEB_SIZE, n0 = 0, ebm-vol-inv(avol), is-encoded(sb0, buf1), ⌊err0⌋ ∨ err0 = ESUCCESS ⊦ # avol = 0, err = ESUCCESS, ∃ buf1. # buf1 = # buf ∧ range=(buf, 0, buf1, 0, n0) ∧ range=(buf, n0 + m2, buf1, n0 + m2, # buf - n0 + m2)

• Proof step 60:

  avol[0] = mapped(buf1), buf = mkbuf(LEB_SIZE), err = err0, m2 = LEB_SIZE, n0 = 0, ebm-vol-inv(avol), is-encoded(sb0, buf1), ⌊err0⌋ ∨ err0 = ESUCCESS ⊦ # avol = 0, err = ESUCCESS, ∀ buf1. # buf1 = # buf → range=(buf, 0, buf1, 0, n0) → # buf ≥ n0 + m2

Rule argument

Additional information