| wlar[n2] = wl-entry(m0, stat), wlar[n1] = wl-entry(m1, stat0), avhdr = avidhdr(v, m2, sqnum, datasize(buf, n), 0).checksum:= checksum(buf, datasize(buf, n)), vtblpnum = n2, avidhdr(v, m2, sqnum, datasize(buf, n), 0).valid?, n2 < # wlar, n1 < # wlar, v ∈ vols ∧ m2 < # vols[v] ∧ vols[v][m2] = ⌜n1⌝ ∨ v = VTBL_VOLID ∧ m2 = VTBL_LNUM ∧ vtblpnum1 = n1 ⊦ [abort; vtblpnum2 := n2; if err = ESUCCESS then if datasize(buf, n) ≠ 0 then aubi_io_write_data_wl#(vtblpnum2, align↑(datasize(buf, n), EB_PAGE_SIZE), buf; apebs; err); wlar0 := wlar; if err = ESUCCESS then {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, vtblpnum2; 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)), datasize(buf, n) = 0, n2 = n1, ubi-io-write-vidhdr-pre(vtblpnum, avhdr, apebs) |