Proof step 3 from proof inv-wl-worker (previous step)

Heuristic nonrecursive calls applied rule call right

And obtained the following new goals

• Proof step 4:

  # apebs = # wlar, apebs0 = apebs, q0 = q, vols0 = vols, vtblpnum1 = vtblpnum, vtblpnum2 = EB_PAGE_SIZE, vtblpnum3 = LEB_SIZE, bflipset-cons(bflipset, wlar), ubi-io-inv(apebs), unique-sqns(apebs), valid-ebatbl(apebs, wlar, vols, vtblpnum), valid-eraseq(apebs, q), valid-eraseq(wlar, q), valid-eraseq(q), valid-global-sqn(apebs, sqnum), valid-vtbl(apebs, vols, wlar, vtblpnum), valid-wl(apebs, wlar) ⊦ ⟪let boolvar = ?, vtblpnum0 = ?, vtblpnum = ? in {ubi_get_pebs_for_wl#(wlar; vtblpnum0, vtblpnum, bflipset; boolvar); if boolvar then let avhdr = ?, bitflips = ? in {aubi_io_read_vidhdr#(vtblpnum, apebs; avhdr; bitflips, err); if err = ESUCCESS then let buf = mkbuf(vtblpnum3) in {aubi_io_read_data#(vtblpnum, 0, 0, vtblpnum3, apebs; buf; bitflips, err); if err = ESUCCESS then ubi_atomic_leb_change# (avhdr.vol, avhdr.leb, vtblpnum0, vtblpnum3, buf, vtblpnum2; vols, wlar, q, bflipset, vtblpnum1, sqnum, apebs; err); if err ≠ ESUCCESS then debug#("ubi: wear-leveling of PEB " + vtblpnum.toString + " to PEB " + vtblpnum0.toString + " failed"); if err = ESUCCESS then {ubi_erase_worker_helper#(vtblpnum; wlar, apebs; err); if err = ESUCCESS then q := q.butlast}}} else err := ENOSPC}⟫ ( # apebs = # wlar ∧ unique-sqns(apebs) ∧ valid-global-sqn(apebs, sqnum) ∧ valid-wl(apebs, wlar) ∧ valid-eraseq(q) ∧ valid-eraseq(wlar, q) ∧ valid-eraseq(apebs, q) ∧ ¬ VTBL_VOLID ∈ vols ∧ bflipset-cons(bflipset, wlar) ∧ valid-ebatbl(apebs, wlar, vols, vtblpnum1) ∧ valid-vtbl(apebs, vols, wlar, vtblpnum1) ∧ ubi-io-inv(apebs) ∧ ( vols0 = vols ∧ id(apebs, apebs0, mapped-pebs(vols)) ∧ q.lebrefs ⊆ q0.lebrefs ++ (VTBL_VOLID × VTBL_LNUM) ∨ (∃ v, m, n. v ∈ vols0 ∧ m < # vols0[v] ∧ vols0[v][m] ≠ unmapped ∧ vols = vols0[v, vols0[v][m, ⌜n⌝ ]] ∧ id(apebs, apebs0, mapped-pebs(vols0) -- vols0[v][m].pnum) ∧ apebs[n].data = apebs0[vols0[v][m].pnum].data ∧ apebs[n].fill ≤ apebs0[vols0[v][m].pnum].fill ∧ q.lebrefs ⊆ q0.lebrefs ++ (v × m)))), VTBL_VOLID ∈ vols, vtblpnum ∈ q

Rule argument

Additional information

Used simplifier rules: wl-worker: ⊦ ;