| wlar[n1] = wl-entry(m1, stat0), wlar[n2] = wl-entry(m0, stat), apebs0[n2] = mkpeb(aehdr, empty, buf1, m, false), apebs = apebs0[n2, mkpeb(aehdr, avidhdr(v, m2, sqnum, datasize(buf, n0), checksum(buf, datasize(buf, n0))), buf1, m, false)], buf0 = buf, n = align↑(datasize(buf, n0), EB_PAGE_SIZE), vtblpnum = n2, aehdr.valid?, n1 < # wlar, n2 < # wlar, n2 < # apebs0, v ∈ vols ∧ m2 < # vols[v] ∧ vols[v][m2] = ⌜n1⌝ ∨ v = VTBL_VOLID ∧ m2 = VTBL_LNUM ∧ vtblpnum1 = n1 ⊦ [if ubi-io-write-data-wl-pre(vtblpnum, n, buf0, apebs) then {fail_or_success#(; ; err); if err = ESUCCESS then apebs[vtblpnum] := mkpeb(apebs[vtblpnum].echdr, apebs[vtblpnum].vidhdr, subarray(buf0, 0, n) + mkempbuf(LEB_SIZE - n), n, apebs[vtblpnum].bad) else choose buf with # buf ≤ n ∧ is-aligned(# buf, EB_PAGE_SIZE) ∧ ( datasize(buf, # buf) < datasize(buf0, n) ∨ checksum(buf + mkempbuf(n - # buf), datasize(buf0, n)) ≠ checksum(buf0, datasize(buf0, n))) in apebs[vtblpnum] := mkpeb(apebs[vtblpnum].echdr, apebs[vtblpnum].vidhdr, buf + mkempbuf(LEB_SIZE - # buf), # buf, apebs[vtblpnum].bad)} else abort; wlar0 := wlar; err0 := err; if err0 = 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) ∧ (err0 = ESUCCESS → wlar[n2].ec = m0 ∧ wlar[n1].ec = m1)), datasize(buf, n0) = 0, n2 = n1 |
apebs0[n2] = mkpeb(aehdr, empty, buf1, m, false), wlar[n2] = wl-entry(m0, stat), wlar[n1] = wl-entry(m1, stat0), apebs = apebs0[n2, mkpeb(aehdr, avidhdr(v, m2, sqnum, datasize(buf, n0), checksum(buf, datasize(buf, n0))), buf1, m, false)], buf0 = buf, n = align↑(datasize(buf, n0), EB_PAGE_SIZE), vtblpnum = n2, aehdr.valid?, n2 < # apebs0, n2 < # wlar, n1 < # wlar, ubi-io-write-data-wl-pre(vtblpnum, n, buf0, apebs), v ∈ vols ∧ m2 < # vols[v] ∧ vols[v][m2] = ⌜n1⌝ ∨ v = VTBL_VOLID ∧ m2 = VTBL_LNUM ∧ vtblpnum1 = n1 ⊦ [fail_or_success#(; ; err); if err = ESUCCESS then apebs[vtblpnum] := mkpeb(apebs[vtblpnum].echdr, apebs[vtblpnum].vidhdr, subarray(buf0, 0, n) + mkempbuf(LEB_SIZE - n), n, apebs[vtblpnum].bad) else choose buf with # buf ≤ n ∧ is-aligned(# buf, EB_PAGE_SIZE) ∧ ( datasize(buf, # buf) < datasize(buf0, n) ∨ checksum(buf + mkempbuf(n - # buf), datasize(buf0, n)) ≠ checksum(buf0, datasize(buf0, n))) in apebs[vtblpnum] := mkpeb(apebs[vtblpnum].echdr, apebs[vtblpnum].vidhdr, buf + mkempbuf(LEB_SIZE - # buf), # buf, apebs[vtblpnum].bad); wlar0 := wlar; err0 := err; if err0 = 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) ∧ (err0 = ESUCCESS → wlar[n2].ec = m0 ∧ wlar[n1].ec = m1)), datasize(buf, n0) = 0, n2 = n1
apebs0[n2] = mkpeb(aehdr, empty, buf1, m, false), wlar[n2] = wl-entry(m0, stat), wlar[n1] = wl-entry(m1, stat0), apebs = apebs0[n2, mkpeb(aehdr, avidhdr(v, m2, sqnum, datasize(buf, n0), checksum(buf, datasize(buf, n0))), buf1, m, false)], buf0 = buf, n = align↑(datasize(buf, n0), EB_PAGE_SIZE), vtblpnum = n2, aehdr.valid?, n2 < # apebs0, n2 < # wlar, n1 < # wlar, v ∈ vols ∧ m2 < # vols[v] ∧ vols[v][m2] = ⌜n1⌝ ∨ v = VTBL_VOLID ∧ m2 = VTBL_LNUM ∧ vtblpnum1 = n1 ⊦ [abort; wlar0 := wlar; err0 := err; if err0 = 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) ∧ (err0 = ESUCCESS → wlar[n2].ec = m0 ∧ wlar[n1].ec = m1)), datasize(buf, n0) = 0, n2 = n1, ubi-io-write-data-wl-pre(vtblpnum, n, buf0, apebs)