[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 12 from proof prepost-write-multiple (previous step)

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

Heuristic annotation applied rule annotation right

And obtained the following new goals

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

Rule argument

rule: invariant right arg: bound: UBI_WRITE_RETRIES + 1 - vtblpnum inv: ubi-cons(apebs, vols, wlar, q, bflipset, vtblpnum0, sqnum) ∧ ubi-io-inv(apebs) ∧ v ∈ vols ∧ vtblpnum2 < # vols[v] ∧ (vols`)[v][vtblpnum2] = unmapped ∧ id(apebs, apebs`, mapped-pebs(vols`)) ∧ q.lebrefs ⊆ q`.lebrefs ++ (v × vtblpnum2) ∧ n1 + n0 ≤ # buf ∧ (n0 = 0 → q.lebrefs ⊆ q`.lebrefs) ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ (err ≠ ESUCCESS → vols = vols`) ∧ ( err = ESUCCESS → (∃ n. vols = (vols`)[v, (vols`)[v][vtblpnum2, ⌜n⌝ ]] ∧ (n0 ≠ 0 → apebs[n].fill = vtblpnum1 + n0) ∧ (n0 = 0 → apebs[n].fill = 0) ∧ apebs[n].data = mkempbuf(vtblpnum1) + subarray(buf, n1, n0) + mkempbuf(LEB_SIZE - n0 - vtblpnum1))) ∧ is-aligned(vtblpnum1, EB_PAGE_SIZE) ∧ is-aligned(n0, EB_PAGE_SIZE) ∧ vtblpnum1 + n0 ≤ LEB_SIZE fmapos: right 1 pos: right 1

Additional information

Used simplifier rules: ⊦ ubi-cons(apebs, vols, wlar, q, bflipset, n0, n1) ↔ # apebs = # wlar ∧ unique-sqns(apebs) ∧ valid-global-sqn(apebs, n1) ∧ 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, n0) ∧ valid-vtbl(apebs, vols, wlar, n0); (s)% ⊦ id(apebs, apebs, ns); (s)% ⊦ s0 ⊆ s0 ++ lref; (s)%c: ⊦ m + n = n + m; from specification nat-basic% ⊦ s0 ⊆ s0; (s)% ⊦ ESUCCESS ≠ EIO; (s)% ⊦ ⌊EIO⌋ ; (s) Used formulas: ubi-cons(apebs, vols, wlar, q, bflipset, vtblpnum0, sqnum) ∧ ubi-io-inv(apebs) ∧ v ∈ vols ∧ vtblpnum2 < # vols[v] ∧ (vols`)[v][vtblpnum2] = unmapped ∧ id(apebs, apebs`, mapped-pebs(vols`)) ∧ q.lebrefs ⊆ q`.lebrefs ++ (v × vtblpnum2) ∧ n1 + n0 ≤ # buf ∧ (n0 = 0 → q.lebrefs ⊆ q`.lebrefs) ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ (err ≠ ESUCCESS → vols = vols`) ∧ ( err = ESUCCESS → (∃ n. vols = (vols`)[v, (vols`)[v][vtblpnum2, ⌜n⌝ ]] ∧ (n0 ≠ 0 → apebs[n].fill = vtblpnum1 + n0) ∧ (n0 = 0 → apebs[n].fill = 0) ∧ apebs[n].data = mkempbuf(vtblpnum1) + subarray(buf, n1, n0) + mkempbuf(LEB_SIZE - n0 - vtblpnum1))) ∧ is-aligned(vtblpnum1, EB_PAGE_SIZE) ∧ is-aligned(n0, EB_PAGE_SIZE) ∧ vtblpnum1 + n0 ≤ LEB_SIZE, UBI_WRITE_RETRIES + 1 - vtblpnum = UBI_WRITE_RETRIES + 1 - vtblpnum