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

Heuristic symbolic execution applied rule let right

And obtained the following new goals

• Proof step 12:

  # apebs0 = # wlar1, apebs = apebs0, bflipset = bflipset0, nx = [], q = q0, recs = ∅, vols = vols0, vtblpnum = 0, vtblpnum0 = 0, vtblpnum2 = vtblpnum4, wlar = wlar0, bflipset-cons(bflipset1, wlar1), ubi-io-inv(apebs0), unique-sqns(apebs0), valid-ebatbl(apebs0, wlar1, vols1, vtblpnum1), valid-eraseq(apebs0, q1), valid-eraseq(wlar1, q1), valid-eraseq(q1), valid-global-sqn(apebs0, vtblpnum5), valid-vtbl(apebs0, vols1, wlar1, vtblpnum1), valid-wl(apebs0, wlar1) ⊦ ⟪ubi_scan_all#(LEB_SIZE, apebs; recs, wlar, q, bflipset, sqnum; vtblpnum0, vtblpnum, nx, err); if ¬ VTBL_VOLID × VTBL_LNUM ∈ recs then err := EINVAL; vols := ∅; vtblpnum2 := LEB_SIZE; if err = ESUCCESS then let buf = mkbuf(vtblpnum2), bitflips = ? in {vtblpnum3 := recs[VTBL_VOLID × VTBL_LNUM].pnum; aubi_io_read_data#(vtblpnum3, 0, 0, vtblpnum2, apebs; 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#(recs, wlar, apebs; vtbl, vols); ubi_init_vols_mappings#(vtblpnum3, apebs; recs, 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 ∧ EB_PAGE_SIZE = EB_PAGE_SIZE) ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ (err = ESUCCESS → is-max(apebs0, vols, wlar, q, bflipset, vtblpnum3, sqnum) ∧ q.lebrefs ⊆ q1.lebrefs ∧ vols1 ⊆ vols ∧ vols⌈vols1, q1⌉)), VTBL_VOLID ∈ vols1, vtblpnum1 ∈ q1

Rule argument

Additional information