[Imprint][Data Privacy Statement][E-Mail]

View long theorem info. View the proof. Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Proof step 22 from proof prepost-write-multiple (previous step)

# apebs0 = # wlar0, # apebs = # wlar, LEB_SIZE - m1 = n1 + m0, LEB_SIZE = (n0 + m0) + m1, vols0[v][m] = unmapped, apebs1 = apebs, q1 = q, vols = vols0, m < # vols0[v], bflipset-cons(bflipset, wlar0), bflipset-cons(bflipset, wlar), id(apebs, apebs0, mapped-pebs(vols0)), is-aligned(m1, EB_PAGE_SIZE), is-aligned(m0, EB_PAGE_SIZE), ubi-io-inv(apebs), ubi-io-inv(apebs0), unique-sqns(apebs0), unique-sqns(apebs), valid-ebatbl(apebs0, wlar0, vols0, vtblpnum3), valid-ebatbl(apebs, wlar, vols0, vtblpnum3), valid-eraseq(apebs0, q0), valid-eraseq(wlar0, q0), valid-eraseq(q0), valid-eraseq(q), valid-eraseq(wlar, q), valid-eraseq(apebs, q), valid-global-sqn(apebs0, sqnum0), valid-global-sqn(apebs, sqnum), valid-vtbl(apebs0, vols0, wlar0, vtblpnum3), valid-vtbl(apebs, vols0, wlar, vtblpnum3), valid-wl(apebs0, wlar0), valid-wl(apebs, wlar), v ∈ vols0, m0 + m1 ≤ LEB_SIZE, m1 + m2 ≤ # buf, vtblpnum4 ≤ UBI_WRITE_RETRIES, m2 + m1 ≤ # buf, m1 ≤ LEB_SIZE, m0 ≤ LEB_SIZE - m1, q.lebrefs ⊆ q0.lebrefs ++ (v × m), ⌊err⌋ , m1 = 0 → q.lebrefs ⊆ q0.lebrefs ⊦ [ubi_write_once#(v, m, m0, m2, m1, buf; vols, wlar, q, sqnum, apebs; err)] ( # 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, vtblpnum3) ∧ valid-vtbl(apebs, vols, wlar, vtblpnum3) ∧ ubi-io-inv(apebs) ∧ id(apebs, apebs1, mapped-pebs(vols0)) ∧ q.lebrefs ⊆ q1.lebrefs ++ (v × m) ∧ (m1 = 0 → q.lebrefs ⊆ q1.lebrefs) ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ (err ≠ ESUCCESS → vols = vols0) ∧ ( err = ESUCCESS → (∃ n. vols = vols0[v, vols0[v][m, ⌜n⌝ ]] ∧ (m1 ≠ 0 → apebs[n].fill = m0 + m1) ∧ (m1 = 0 → apebs[n].fill = 0) ∧ apebs[n].data = mkempbuf(m0) + subarray(buf, m2, m1) + mkempbuf(n1))) → ⟪vtblpnum := vtblpnum4 + 1⟫ ( v ∈ vols ∧ m < # vols[v] ∧ id(apebs, apebs0, mapped-pebs(vols0)) ∧ q.lebrefs ⊆ q0.lebrefs ++ (v × m) ∧ (m1 = 0 → q.lebrefs ⊆ q0.lebrefs) ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ (err ≠ ESUCCESS → vols = vols0) ∧ ( err = ESUCCESS → (∃ n. vols = vols0[v, vols0[v][m, ⌜n⌝ ]] ∧ (m1 ≠ 0 → apebs[n].fill = m0 + m1) ∧ (m1 = 0 → apebs[n].fill = 0) ∧ apebs[n].data = mkempbuf(m0) + subarray(buf, m2, m1) + mkempbuf(n0))) ∧ ¬ UBI_WRITE_RETRIES < (UBI_WRITE_RETRIES + 1 - vtblpnum) + vtblpnum4)), VTBL_VOLID ∈ vols0, vtblpnum3 ∈ q0, vtblpnum3 ∈ q

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 23:
# apebs = # wlar, # apebs0 = # wlar0, LEB_SIZE - m1 = n1 + m0, LEB_SIZE = (n0 + m0) + m1, vols0[v][m] = unmapped, apebs1 = apebs, q1 = q, vols = vols0, m < # vols0[v], bflipset-cons(bflipset, wlar), bflipset-cons(bflipset, wlar0), id(apebs, apebs0, mapped-pebs(vols0)), is-aligned(m0, EB_PAGE_SIZE), is-aligned(m1, EB_PAGE_SIZE), ubi-io-inv(apebs0), ubi-io-inv(apebs), unique-sqns(apebs), unique-sqns(apebs0), valid-ebatbl(apebs, wlar, vols0, vtblpnum3), valid-ebatbl(apebs0, wlar0, vols0, vtblpnum3), valid-eraseq(apebs, q), valid-eraseq(wlar, q), valid-eraseq(q), valid-eraseq(q0), valid-eraseq(wlar0, q0), valid-eraseq(apebs0, q0), valid-global-sqn(apebs, sqnum), valid-global-sqn(apebs0, sqnum0), valid-vtbl(apebs, vols0, wlar, vtblpnum3), valid-vtbl(apebs0, vols0, wlar0, vtblpnum3), valid-wl(apebs, wlar), valid-wl(apebs0, wlar0), v ∈ vols0, m1 ≤ LEB_SIZE, m2 + m1 ≤ # buf, vtblpnum4 ≤ UBI_WRITE_RETRIES, m1 + m2 ≤ # buf, m0 + m1 ≤ LEB_SIZE, q.lebrefs ⊆ q0.lebrefs ++ (v × m), ⌊err⌋ , ¬ vtblpnum3 ∈ q, ¬ vtblpnum3 ∈ q0, ¬ VTBL_VOLID ∈ vols0, m1 = 0 → q.lebrefs ⊆ q0.lebrefs ⊦ [ubi_write_once#(v, m, m0, m2, m1, buf; vols, wlar, q, sqnum, apebs; err)] ( # 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, vtblpnum3) ∧ valid-vtbl(apebs, vols, wlar, vtblpnum3) ∧ ubi-io-inv(apebs) ∧ id(apebs, apebs1, mapped-pebs(vols0)) ∧ q.lebrefs ⊆ q1.lebrefs ++ (v × m) ∧ (m1 = 0 → q.lebrefs ⊆ q1.lebrefs) ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ (err ≠ ESUCCESS → vols = vols0) ∧ ( err = ESUCCESS → (∃ n. vols = vols0[v, vols0[v][m, ⌜n⌝ ]] ∧ (m1 ≠ 0 → apebs[n].fill = m0 + m1) ∧ (m1 = 0 → apebs[n].fill = 0) ∧ apebs[n].data = mkempbuf(m0) + subarray(buf, m2, m1) + mkempbuf(n1))) → ⟪vtblpnum := vtblpnum4 + 1⟫ ( v ∈ vols ∧ m < # vols[v] ∧ id(apebs, apebs0, mapped-pebs(vols0)) ∧ q.lebrefs ⊆ q0.lebrefs ++ (v × m) ∧ (m1 = 0 → q.lebrefs ⊆ q0.lebrefs) ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ (err ≠ ESUCCESS → vols = vols0) ∧ ( err = ESUCCESS → (∃ n. vols = vols0[v, vols0[v][m, ⌜n⌝ ]] ∧ (m1 ≠ 0 → apebs[n].fill = m0 + m1) ∧ (m1 = 0 → apebs[n].fill = 0) ∧ apebs[n].data = mkempbuf(m0) + subarray(buf, m2, m1) + mkempbuf(n0))) ∧ ¬ UBI_WRITE_RETRIES < (UBI_WRITE_RETRIES + 1 - vtblpnum) + vtblpnum4))

Rule argument

Additional information

Used simplifier rules: n0 ≤ n ⊦ m ≤ n - n0 ↔ m + n0 ≤ n; (s)% ⊦ m ≤ n → (n < m ↔ false); (s)% ⊦ m ≤ n ↔ ¬ n < m; (ss)