| 0 = datasize(buf, n), wlar[n1] = wl-entry(m1, stat0), wlar[n2] = wl-entry(m0, stat), apebs[n2] = mkpeb(aehdr, empty, buf0, m, false), err = err0, vtblpnum = n2, wlar0 = wlar, aehdr.valid?, vtblpnum < # apebs, n1 < # wlar, n2 < # wlar, n2 < # apebs, v ∈ vols ∧ m2 < # vols[v] ∧ vols[v][m2] = ⌜n1⌝ ∨ v = VTBL_VOLID ∧ m2 = VTBL_LNUM ∧ vtblpnum1 = n1, ⌊err0⌋ ∨ err0 = ESUCCESS ⊦ [if err = 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) ∧ (err = ESUCCESS → wlar[n2].ec = m0 ∧ wlar[n1].ec = m1)), err = ESUCCESS, n2 = n1, avhdr.valid? |
0 = datasize(buf, n), apebs[n2] = mkpeb(aehdr, empty, buf0, m, false), wlar[n2] = wl-entry(m0, stat), wlar[n1] = wl-entry(m1, stat0), err = err0, vtblpnum = n2, wlar0 = wlar, aehdr.valid?, n2 < # apebs, n2 < # wlar, n1 < # wlar, vtblpnum < # apebs, ⌊err0⌋ ∨ err0 = ESUCCESS, v ∈ vols ∧ m2 < # vols[v] ∧ vols[v][m2] = ⌜n1⌝ ∨ v = VTBL_VOLID ∧ m2 = VTBL_LNUM ∧ vtblpnum1 = n1 ⊦ [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) ∧ (err = ESUCCESS → wlar[n2].ec = m0 ∧ wlar[n1].ec = m1)), err = ESUCCESS, n2 = n1, avhdr.valid?