Proof step 2 from proof inv-format (previous step)

Heuristic nonrecursive calls applied rule call right

And obtained the following new goals

• Proof step 3:

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

Rule argument

Additional information

Used simplifier rules: format: ⊦ ;