Proof step 123 from proof refine-write (previous step)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 124:

  # apebs0 = # wlar, LEB_SIZE = (n1 + n2) + vtblpnum5, apebs0[n4] = mkpeb(aehdr, avhdr, buf2, m0, false), wlar[n4] = wl-entry(m1, used), avols[v][vtblpnum3] = mapped(buf2, m), vols[v][vtblpnum3] = ⌜n4⌝ , n2 ≠ 0, vtblpnum4 ≠ n4, avhdr.valid?, aehdr.valid?, n2 < n5, vtblpnum3 < # avols[v], vtblpnum3 < # vols[v], n4 < # wlar, abs(avols, apebs0, vols, q), bflipset-cons(bflipset, wlar), ebm-cons(avols), is-aligned(n2, EB_PAGE_SIZE), is-aligned(n5, EB_PAGE_SIZE), is-aligned(vtblpnum5, EB_PAGE_SIZE), ubi-io-inv(apebs0[n4, mkpeb(aehdr, avhdr, subarray(buf2, 0, vtblpnum5) + subarray(buf, n3, n2) + mkempbuf(n1), vtblpnum5 + n2, false)]), ubi-io-inv(apebs0), ubi-io-peb-inv(mkpeb(aehdr, avhdr, buf2, m0, false)), unique-sqns(apebs0[n4, mkpeb(aehdr, avhdr, subarray(buf2, 0, vtblpnum5) + subarray(buf, n3, n2) + mkempbuf(n1), vtblpnum5 + n2, false)]), unique-sqns(apebs0), valid-ebatbl (apebs0[n4, mkpeb(aehdr, avhdr, subarray(buf2, 0, vtblpnum5) + subarray(buf, n3, n2) + mkempbuf(n1), vtblpnum5 + n2, false)], wlar, vols, vtblpnum4), valid-ebatbl(apebs0, wlar, vols, vtblpnum4), valid-eraseq(apebs0[n4, mkpeb(aehdr, avhdr, subarray(buf2, 0, vtblpnum5) + subarray(buf, n3, n2) + mkempbuf(n1), vtblpnum5 + n2, false)], q), valid-eraseq(apebs0, q), valid-eraseq(wlar, q), valid-eraseq(q), valid-global-sqn(apebs0[n4, mkpeb(aehdr, avhdr, subarray(buf2, 0, vtblpnum5) + subarray(buf, n3, n2) + mkempbuf(n1), vtblpnum5 + n2, false)], sqnum), valid-global-sqn(apebs0, sqnum), valid-vtbl(apebs0, vols, wlar, vtblpnum4), valid-wl(apebs0[n4, mkpeb(aehdr, avhdr, subarray(buf2, 0, vtblpnum5) + subarray(buf, n3, n2) + mkempbuf(n1), vtblpnum5 + n2, false)], wlar), valid-wl(apebs0, wlar), v ∈ avols, v ∈ vols, m0 ≤ LEB_SIZE, m ≤ LEB_SIZE, n3 + n2 ≤ # buf, n2 + vtblpnum5 ≤ LEB_SIZE, m0 ≤ vtblpnum5, m ≤ vtblpnum5, n5 + n3 ≤ # buf, n3 + n5 ≤ # buf, vtblpnum5 + n5 ≤ LEB_SIZE, vtblpnum5 ≤ LEB_SIZE, ⌊err0⌋ , ¬ VTBL_VOLID ∈ vols ⊦ ⟪fail_or_success#(; ; err); bitflips := ?; buf0 := mkbuf(vtblpnum5 + n5); if err = ESUCCESS then buf0 := copy (apebs0 [vols[v][vtblpnum3].pnum, mkpeb(aehdr, avhdr, subarray(buf2, 0, vtblpnum5) + subarray(buf, n3, n2) + mkempbuf(n1), vtblpnum5 + n2, false) ] [vols[v][vtblpnum3].pnum ] .data, 0, buf0, 0, vtblpnum5) else {n0 := 0; n := vtblpnum5; choose buf with # buf = # buf0 ∧ range=(buf, 0, buf0, 0, n0) ∧ range=(buf, n0 + n, buf0, n0 + n, # buf0 - n0 + n) in buf0 := buf}; apebs := apebs0[vols[v][vtblpnum3].pnum, mkpeb(aehdr, avhdr, subarray(buf2, 0, vtblpnum5) + subarray(buf, n3, n2) + mkempbuf(n1), vtblpnum5 + n2, false)]; err0 := err, buf1 := buf0; if err0 = ESUCCESS then {buf1 := copy(buf, n3, buf1, vtblpnum5, n5); debug#("ubi: moving data from PEB " + vols[v][vtblpnum3].pnum.toString); ubi_change#(v, vtblpnum3, vtblpnum5 + n5, buf1, EB_PAGE_SIZE; vols, wlar, q, bflipset, vtblpnum4, sqnum, apebs; err0)} else debug#("ubi: failed to read data from PEB " + vols[v][vtblpnum3].pnum.toString)⟫ ⟨ebm_write#(v, vtblpnum3, vtblpnum5, n3, n5, buf; avols; err1)⟩ (abs(avols, apebs, vols, q) ∧ err0 = err1)

Rule argument

Additional information

Used simplifier rules: lf-mapped-in-apebs: ⊦ v ∈ vols ∧ m < # vols[v] ∧ vols[v][m] = ⌜n⌝ ∧ valid-ebatbl(apebs, wlar, vols, n0) → n < # apebs;% ⊦ ⌜m⌝ .pnum = m; (s)% ⊦ unmapped ≠ ⌜m⌝ ; (s)% ⊦ m < n → n ≠ 0; (s)%f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic% ⊦ m ≤ m + n; (s)% ⊦ # mkbuf(n) = n; (s)% ⊦ mkpeb(aehdr, avhdr, buf, m, boolvar).bad ↔ boolvar; (s)% ⊦ m < # apebs → apebs[m, apeb][m] = apeb; (s)% ⊦ # apebs[n, apeb] = # apebs; (s)%⊦ ubi-io-read-data-pre(n, n0, m0, n1, buf, apebs) ↔ n < # apebs ∧ ¬ apebs[n].bad ∧ n0 + n1 ≤ LEB_SIZE ∧ m0 + n1 ≤ # buf; (s)%⊦ v ∈ avols ∧ m < # avols[v] ∧ avols[v][m] = mapped(buf, n) ∧ ebm-cons(avols) → # buf = LEB_SIZE; (s)%c: ⊦ m + n = n + m; from specification nat-basic%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic% ⊦ n + 0 = n; (s)