Proof step 19 from proof inv-recover (previous step)

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 20:

  # apebs0 = # wlar1, err = EINVAL, bflipset-cons(bflipset1, wlar1), ubi-io-inv(apebs0), unique-sqns(apebs0), valid-ebatbl(apebs0, wlar1, vols1, vtblpnum1), valid-eraseq(q1), valid-eraseq(wlar1, q1), valid-eraseq(apebs0, q1), valid-global-sqn(apebs0, vtblpnum5), valid-vtbl(apebs0, vols1, wlar1, vtblpnum1), valid-wl(apebs0, wlar1), err0 = ESUCCESS → # wlar1 = # wlar ∧ ¬ dups(nx) ∧ nx < # wlar1 ∧ indices-erasing(wlar, nx) ∧ valid-global-sqn(apebs0, sqnum) ∧ valid-eraseq(wlar, q) ∧ bflipset-cons(bflipset, wlar) ∧ valid-eraseq-stronger(apebs0, q) ∧ valid-wl(apebs0, wlar) ∧ valid-recs-sqns(apebs0, recs0) ∧ valid-recs(apebs0, wlar, recs0), err0 = ESUCCESS ∨ ⌊err0⌋ ⊦ ⟪vols := ∅; vtblpnum2 := LEB_SIZE; if err = ESUCCESS then let buf = mkbuf(vtblpnum2), bitflips = ? in {vtblpnum3 := recs0[VTBL_VOLID × VTBL_LNUM].pnum; aubi_io_read_data#(vtblpnum3, 0, 0, vtblpnum2, apebs0; buf; bitflips, err); if bitflips then bflipset := bflipset ++ vtblpnum3; if err = ESUCCESS then let vtbl = ? in {decode_vtbl#(buf; ; vtbl, err); if err = ESUCCESS then {ubi_init_vols_sizes#(recs0, wlar, apebs0; vtbl, vols); ubi_init_vols_mappings#(vtblpnum3, apebs0; recs0, vols, wlar, q, bflipset); let n = (vtblpnum0 = 0 ⊃ 0;vtblpnum / vtblpnum0) in ubi_fix_ecs#(n; nx, wlar)}}}⟫ ( ( err = ESUCCESS → # wlar1 = # wlar ∧ 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, vtblpnum3) ∧ valid-vtbl(apebs0, vols, wlar, vtblpnum3) ∧ vtblpnum2 = LEB_SIZE) ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ (err = ESUCCESS → is-max(apebs0, vols, wlar, q, bflipset, vtblpnum3, sqnum) ∧ q.lebrefs ⊆ q1.lebrefs ∧ vols1 ⊆ vols ∧ vols⌈vols1, q1⌉)), vtblpnum1 ∈ q1, VTBL_VOLID ∈ vols1, VTBL_VOLID × VTBL_LNUM ∈ recs0

Rule argument

Additional information