| apebs = apebs0, apebs1 = apebs0, apebs2 = apebs0, err0 = ESUCCESS, vtblpnum = 0, vtblpnum1 = LEB_SIZE, ubi-io-initial(apebs0) ⊦ ⟪aubi_io_get_blockcount#(apebs1; ; n); wlar := mkwlarray(n); vtblpnum2 := n; err0 := ESUCCESS; while vtblpnum < n ∧ err0 = ESUCCESS do {/* (inv-format : invariant vtblpnum ≤ # apebs1 ∧ n = # apebs1 ∧ # wlar = # apebs1 ∧ (err0 = ESUCCESS ∨ ⌊err0⌋ ) ∧ ( err0 = ESUCCESS → ubi-io-initial(apebs1) ∧ vtblpnum2 ≤ # apebs1 ∧ (∀ n3. n3 < vtblpnum → (apebs1[n3].bad → wlar[n3] = wl-entry(0, erroneous)) ∧ ( ¬ apebs1[n3].bad → apebs1[n3].echdr.valid? ∧ wlar[n3] = wl-entry(apebs1[n3].echdr.ec, free) ∧ apebs1[n3].vidhdr = empty)) ∧ (vtblpnum2 ≠ # apebs1 → ¬ apebs1[vtblpnum2].bad)) wfbound n - vtblpnum) */; let isbad = ? in {aubi_io_isbad#(vtblpnum, apebs1; ; isbad, err0); if err0 = ESUCCESS then if ¬ isbad then let aehdr = ?, bitflips = ? in {aubi_io_read_echdr#(vtblpnum, apebs1; aehdr; bitflips, err0); if err0 = ESUCCESS ∧ vtblpnum2 = n then vtblpnum2 := vtblpnum; if err0 = ESUCCESS ∧ aehdr.valid? then wlar[vtblpnum] := wl-entry(aehdr.ec, free)} else wlar[vtblpnum] := wl-entry(0, erroneous); vtblpnum := vtblpnum + 1}}; if err0 = ESUCCESS then if vtblpnum2 = n then err0 := ENOSPC else {aubi_io_write_vidhdr#(vtblpnum2, avidhdr(VTBL_VOLID, VTBL_LNUM, 0, 0, 0); apebs1; err0); if err0 = ESUCCESS then if vtblpnum1 < ENCODED_NAT_SIZE then err0 := ENOSPC else let buf = mkbuf(vtblpnum1), vtbl = ∅ in {encode_vtbl#(; vtbl, buf; err0); if err0 = ESUCCESS then aubi_io_write_data#(vtblpnum2, 0, 0, vtblpnum1, buf; apebs1; err0)}; vols := ∅; wlar[vtblpnum2] := wl-entry(wlar[vtblpnum2].ec, used); q := []; sqnum := 1; bflipset := ∅}⟫ ( ( err0 = ESUCCESS → # apebs1 = # wlar ∧ unique-sqns(apebs1) ∧ valid-global-sqn(apebs1, sqnum) ∧ valid-wl(apebs1, wlar) ∧ valid-eraseq(q) ∧ valid-eraseq(wlar, q) ∧ valid-eraseq(apebs1, q) ∧ ¬ VTBL_VOLID ∈ vols ∧ bflipset-cons(bflipset, wlar) ∧ valid-ebatbl(apebs1, wlar, vols, vtblpnum2) ∧ valid-vtbl(apebs1, vols, wlar, vtblpnum2) ∧ vtblpnum1 = LEB_SIZE ∧ EB_PAGE_SIZE = EB_PAGE_SIZE ∧ ubi-io-inv(apebs1)) ∧ (err0 = ESUCCESS ∨ ⌊err0⌋ ) ∧ (err0 = ESUCCESS → vols = ∅)) |
ubi-io-initial(apebs0) ⊦ ⟪aubi_io_get_blockcount#(apebs0; ; n); wlar := mkwlarray(n); vtblpnum2 := n; err0 := ESUCCESS; vtblpnum := 0; while vtblpnum < n ∧ err0 = ESUCCESS do {/* (inv-format : invariant vtblpnum ≤ # apebs0 ∧ n = # apebs0 ∧ # wlar = # apebs0 ∧ (err0 = ESUCCESS ∨ ⌊err0⌋ ) ∧ ( err0 = ESUCCESS → ubi-io-initial(apebs0) ∧ vtblpnum2 ≤ # apebs0 ∧ (∀ n3. n3 < vtblpnum → (apebs0[n3].bad → wlar[n3] = wl-entry(0, erroneous)) ∧ ( ¬ apebs0[n3].bad → apebs0[n3].echdr.valid? ∧ wlar[n3] = wl-entry(apebs0[n3].echdr.ec, free) ∧ apebs0[n3].vidhdr = empty)) ∧ (vtblpnum2 ≠ # apebs0 → ¬ apebs0[vtblpnum2].bad)) wfbound n - vtblpnum) */; let isbad = ? in {aubi_io_isbad#(vtblpnum, apebs0; ; isbad, err0); if err0 = ESUCCESS then if ¬ isbad then let aehdr = ?, bitflips = ? in {aubi_io_read_echdr#(vtblpnum, apebs0; aehdr; bitflips, err0); if err0 = ESUCCESS ∧ vtblpnum2 = n then vtblpnum2 := vtblpnum; if err0 = ESUCCESS ∧ aehdr.valid? then wlar[vtblpnum] := wl-entry(aehdr.ec, free)} else wlar[vtblpnum] := wl-entry(0, erroneous); vtblpnum := vtblpnum + 1}}; vtblpnum1 := LEB_SIZE; if err0 = ESUCCESS then if vtblpnum2 = n then err0 := ENOSPC else {aubi_io_write_vidhdr#(vtblpnum2, avidhdr(VTBL_VOLID, VTBL_LNUM, 0, 0, 0); apebs0; err0); if err0 = ESUCCESS then if vtblpnum1 < ENCODED_NAT_SIZE then err0 := ENOSPC else let buf = mkbuf(vtblpnum1), vtbl = ∅ in {encode_vtbl#(; vtbl, buf; err0); if err0 = ESUCCESS then aubi_io_write_data#(vtblpnum2, 0, 0, vtblpnum1, buf; apebs0; err0)}; vols := ∅; wlar[vtblpnum2] := wl-entry(wlar[vtblpnum2].ec, used); q := []; sqnum := 1; bflipset := ∅}⟫ ( ( err0 = ESUCCESS → # apebs0 = # wlar ∧ unique-sqns(apebs0) ∧ valid-global-sqn(apebs0, sqnum) ∧ valid-wl(apebs0, wlar) ∧ valid-eraseq(q) ∧ valid-eraseq(wlar, q) ∧ valid-eraseq(apebs0, q) ∧ ¬ VTBL_VOLID ∈ vols ∧ bflipset-cons(bflipset, wlar) ∧ valid-ebatbl(apebs0, wlar, vols, vtblpnum2) ∧ valid-vtbl(apebs0, vols, wlar, vtblpnum2) ∧ vtblpnum1 = LEB_SIZE ∧ ubi-io-inv(apebs0)) ∧ (err0 = ESUCCESS ∨ ⌊err0⌋ ) ∧ (err0 = ESUCCESS → vols = ∅))