Proof step 56 from proof prepost-write-once (previous step)

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 57:

  # apebs0 = # wlar, # apebs2 = # wlar0, q0.head = eq-entry(m4, lref), LEB_SIZE = (n2 + m0) + m1, vols0[v][m] = unmapped, wlar0[vtblpnum1] = wl-entry(m5, free), apebs2[vtblpnum1] = mkpeb(aehdr, empty, mkempbuf(LEB_SIZE), 0, false), apebs = apebs2[vtblpnum1, mkpeb(aehdr, avidhdr(v, m, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false)], err = err0, err = ESUCCESS, aehdr.valid?, vtblpnum1 < # apebs, m < # vols0[v], vtblpnum1 < # wlar0, vtblpnum1 < # apebs2, bflipset-cons(bflipset, wlar), bflipset-cons(bflipset, wlar0), id(apebs2, apebs0, mapped-pebs(vols0)), is-aligned(m1, EB_PAGE_SIZE), is-aligned(m0, EB_PAGE_SIZE), ubi-io-inv (apebs [vtblpnum1, mkpeb (apebs[vtblpnum1].echdr, apebs[vtblpnum1].vidhdr, subarray(apebs[vtblpnum1].data, 0, m0) + subarray(buf, m2, m1) + mkempbuf(LEB_SIZE - m0 - m1), m0 + m1, apebs[vtblpnum1].bad) ]), ubi-io-inv(apebs2[vtblpnum1, mkpeb(aehdr, avidhdr(v, m, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false)]), ubi-io-inv(apebs0), ubi-io-inv(apebs2), unique-sqns(apebs0), unique-sqns(apebs2), valid-ebatbl(apebs0, wlar, vols0, vtblpnum2), valid-ebatbl(apebs2, wlar0, vols0, vtblpnum2), valid-eraseq(apebs0, q0), valid-eraseq(wlar, q0), valid-eraseq(q0), valid-eraseq(q1), valid-eraseq(wlar0, q1), valid-eraseq(apebs2, q1), valid-global-sqn(apebs0, sqnum), valid-global-sqn(apebs2, sqnum), valid-vtbl(apebs0, vols0, wlar, vtblpnum2), valid-vtbl(apebs2, vols0, wlar0, vtblpnum2), valid-wl(apebs0, wlar), valid-wl(apebs2, wlar0), v ∈ vols0, 0 + m0 ≤ # apebs[vtblpnum1].data, m2 + m1 ≤ # buf, m1 ≤ LEB_SIZE, m1 + m2 ≤ # buf, m0 + m1 ≤ LEB_SIZE, LEB_SIZE - m0 ≥ m1, LEB_SIZE ≥ m0, q1.lebrefs ⊆ q0.lebrefs, ⌊err0⌋ ∨ err0 = ESUCCESS, apebs0 = apebs2 ∧ wlar = wlar0 ∧ q0 = q1 ∨ id○(apebs0, apebs2, vtblpnum1) ∧ id○(wlar, wlar0, vtblpnum1) ∧ q0 = eq-entry(vtblpnum1, lref) ' + q1 ⊦ ⟪vols := vols0; if err = ESUCCESS then {vols[v][m] := ⌜vtblpnum1⌝ ; wlar0[vtblpnum1] := wl-entry(wlar0[vtblpnum1].ec, used)} else ubi_wl_put_peb#(v × m, vtblpnum1; wlar0, q1); skip⟫ ( # apebs [vtblpnum1, mkpeb (apebs[vtblpnum1].echdr, apebs[vtblpnum1].vidhdr, subarray(apebs[vtblpnum1].data, 0, m0) + subarray(buf, m2, m1) + mkempbuf(LEB_SIZE - m0 - m1), m0 + m1, apebs[vtblpnum1].bad) ] = # wlar0 ∧ unique-sqns (apebs [vtblpnum1, mkpeb (apebs[vtblpnum1].echdr, apebs[vtblpnum1].vidhdr, subarray(apebs[vtblpnum1].data, 0, m0) + subarray(buf, m2, m1) + mkempbuf(LEB_SIZE - m0 - m1), m0 + m1, apebs[vtblpnum1].bad) ]) ∧ valid-global-sqn (apebs [vtblpnum1, mkpeb (apebs[vtblpnum1].echdr, apebs[vtblpnum1].vidhdr, subarray(apebs[vtblpnum1].data, 0, m0) + subarray(buf, m2, m1) + mkempbuf(LEB_SIZE - m0 - m1), m0 + m1, apebs[vtblpnum1].bad) ], sqnum + 1) ∧ valid-wl (apebs [vtblpnum1, mkpeb (apebs[vtblpnum1].echdr, apebs[vtblpnum1].vidhdr, subarray(apebs[vtblpnum1].data, 0, m0) + subarray(buf, m2, m1) + mkempbuf(LEB_SIZE - m0 - m1), m0 + m1, apebs[vtblpnum1].bad) ], wlar0) ∧ valid-eraseq(q1) ∧ valid-eraseq(wlar0, q1) ∧ valid-eraseq (apebs [vtblpnum1, mkpeb (apebs[vtblpnum1].echdr, apebs[vtblpnum1].vidhdr, subarray(apebs[vtblpnum1].data, 0, m0) + subarray(buf, m2, m1) + mkempbuf(LEB_SIZE - m0 - m1), m0 + m1, apebs[vtblpnum1].bad) ], q1) ∧ ¬ VTBL_VOLID ∈ vols ∧ bflipset-cons(bflipset, wlar0) ∧ valid-ebatbl (apebs [vtblpnum1, mkpeb (apebs[vtblpnum1].echdr, apebs[vtblpnum1].vidhdr, subarray(apebs[vtblpnum1].data, 0, m0) + subarray(buf, m2, m1) + mkempbuf(LEB_SIZE - m0 - m1), m0 + m1, apebs[vtblpnum1].bad) ], wlar0, vols, vtblpnum2) ∧ valid-vtbl (apebs [vtblpnum1, mkpeb (apebs[vtblpnum1].echdr, apebs[vtblpnum1].vidhdr, subarray(apebs[vtblpnum1].data, 0, m0) + subarray(buf, m2, m1) + mkempbuf(LEB_SIZE - m0 - m1), m0 + m1, apebs[vtblpnum1].bad) ], vols, wlar0, vtblpnum2) ∧ id (apebs [vtblpnum1, mkpeb (apebs[vtblpnum1].echdr, apebs[vtblpnum1].vidhdr, subarray(apebs[vtblpnum1].data, 0, m0) + subarray(buf, m2, m1) + mkempbuf(LEB_SIZE - m0 - m1), m0 + m1, apebs[vtblpnum1].bad) ], apebs0, mapped-pebs(vols0)) ∧ q1.lebrefs ⊆ q0.lebrefs ++ (v × m) ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ (err ≠ ESUCCESS → vols = vols0) ∧ ( err = ESUCCESS → (∃ n. vols = vols0[v, vols0[v][m, ⌜n⌝ ]] ∧ apebs [vtblpnum1, mkpeb (apebs[vtblpnum1].echdr, apebs[vtblpnum1].vidhdr, subarray(apebs[vtblpnum1].data, 0, m0) + subarray(buf, m2, m1) + mkempbuf(LEB_SIZE - m0 - m1), m0 + m1, apebs[vtblpnum1].bad) ] [n ] .fill = m0 + m1 ∧ apebs [vtblpnum1, mkpeb (apebs[vtblpnum1].echdr, apebs[vtblpnum1].vidhdr, subarray(apebs[vtblpnum1].data, 0, m0) + subarray(buf, m2, m1) + mkempbuf(LEB_SIZE - m0 - m1), m0 + m1, apebs[vtblpnum1].bad) ] [n ] .data = mkempbuf(m0) + subarray(buf, m2, m1) + mkempbuf(n2)))), m1 = 0, vtblpnum2 = vtblpnum1, vtblpnum2 ∈ q0, VTBL_VOLID ∈ vols0, vtblpnum2 ∈ q1

Rule argument

Additional information