Proof step 41 from proof delta-atomic-leb-change (previous step)

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 42:

  wlar[n1] = wl-entry(m1, stat0), wlar[n2] = wl-entry(m0, stat), apebs0[n2] = mkpeb(aehdr, empty, buf1, 0, false), align↑(datasize(buf, n0), EB_PAGE_SIZE) = align↑(datasize(buf, align↑(datasize(buf, n0), EB_PAGE_SIZE)), EB_PAGE_SIZE), err = err0, err = ESUCCESS, aehdr.valid?, n2 < # apebs0[n2, mkpeb(aehdr, avidhdr(v, m2, sqnum, datasize(buf, n0), checksum(buf, datasize(buf, n0))), buf1, 0, false)], n1 < # wlar, n2 < # wlar, n2 < # apebs0, 0 + align↑(datasize(buf, n0), EB_PAGE_SIZE) ≤ # buf, align↑(datasize(buf, n0), EB_PAGE_SIZE) ≤ LEB_SIZE, align↑(datasize(buf, n0), EB_PAGE_SIZE) ≤ # buf, LEB_SIZE ≥ align↑(datasize(buf, n0), EB_PAGE_SIZE), v ∈ vols ∧ m2 < # vols[v] ∧ vols[v][m2] = ⌜n1⌝ ∨ v = VTBL_VOLID ∧ m2 = VTBL_LNUM ∧ vtblpnum1 = n1, ⌊err0⌋ ∨ err0 = ESUCCESS ⊦ [wlar0 := wlar; err1 := err; if err1 = ESUCCESS then {vtblpnum2 := n2; if v = VTBL_VOLID ∧ m2 = VTBL_LNUM then {ubi_wl_put_peb#(VTBL_VOLID × VTBL_LNUM, vtblpnum1; wlar, q); bflipset := bflipset -- vtblpnum1; vtblpnum1 := vtblpnum2} else {if vols[v][m2] ≠ unmapped then let vtblpnum0 = vols[v][m2].pnum in {ubi_wl_put_peb#(v × m2, vtblpnum0; wlar, q); bflipset := bflipset -- vtblpnum0}; vols[v][m2] := ⌜vtblpnum2⌝ }; wlar[vtblpnum2] := wl-entry(wlar[vtblpnum2].ec, used)} else ubi_wl_put_peb#(none, n2; wlar, q)] ( sum-of-differences(ecs(wlar).max, ecs(wlar)) = sum-of-differences(ecs(wlar0).max, ecs(wlar0)) ∧ ecs(wlar) = ecs(wlar0) ∧ (err1 = ESUCCESS → wlar[n2].ec = m0 ∧ wlar[n1].ec = m1)), datasize(buf, align↑(datasize(buf, n0), EB_PAGE_SIZE)) = 0, datasize(buf, n0) = 0, n2 = n1

Rule argument

Additional information