[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 3 from proof refine-change (previous step)

# apebs = # wlar, vtblpnum < # avols[v], abs(avols, apebs, vols, q), bflipset-cons(bflipset, wlar), ebm-cons(avols), is-aligned(n, EB_PAGE_SIZE), ubi-io-inv(apebs), unique-sqns(apebs), valid-ebatbl(apebs, wlar, vols, vtblpnum0), valid-eraseq(apebs, q), valid-eraseq(wlar, q), valid-eraseq(q), valid-global-sqn(apebs, sqnum), valid-vtbl(apebs, vols, wlar, vtblpnum0), valid-wl(apebs, wlar), v ∈ avols, n ≤ # buf, n ≤ LEB_SIZE, ¬ VTBL_VOLID ∈ vols ⊦ ⟪ubi_change#(v, vtblpnum, n, buf, EB_PAGE_SIZE; vols, wlar, q, bflipset, vtblpnum0, sqnum, apebs; err)⟫ ⟨ebm_change#(v, vtblpnum, n, buf; avols; err0)⟩ (abs(avols, apebs, vols, q) ∧ err = err0)

User applied rule insert program lemma

And obtained the following new goals

Proof step 4:
ubi-cons(apebs, vols, wlar, q, bflipset, vtblpnum, sqnum), vtblpnum0 = EB_PAGE_SIZE, ubi-io-inv(apebs), n0 ≤ LEB_SIZE, n0 ≤ # buf, v ∈ vols, vtblpnum1 < # vols[v], is-aligned(n0, EB_PAGE_SIZE), vols0 = vols, apebs0 = apebs, q0 = q ⊦ ⟪ubi_change#(v, vtblpnum1, n0, buf, vtblpnum0; vols, wlar, q, bflipset, vtblpnum, sqnum, apebs; err)⟫ ( ubi-cons(apebs, vols, wlar, q, bflipset, vtblpnum, sqnum) ∧ ubi-io-inv(apebs) ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ (err ≠ ESUCCESS → vols = vols0 ∧ id(apebs, apebs0, mapped-pebs(vols)) ∧ q.lebrefs ⊆ q0.lebrefs) ∧ ( err = ESUCCESS → v ∈ vols0 ∧ vtblpnum1 < # vols0[v] ∧ q.lebrefs ⊆ q0.lebrefs ++ (v × vtblpnum1) ∧ (vols0[v][vtblpnum1] ≠ unmapped → id(apebs, apebs0, mapped-pebs(vols0) -- vols0[v][vtblpnum1].pnum)) ∧ (vols0[v][vtblpnum1] = unmapped → id(apebs, apebs0, mapped-pebs(vols0))) ∧ (∃ n. vols = vols0[v, vols0[v][vtblpnum1, ⌜n⌝ ]] ∧ apebs[n].data = subarray(buf, 0, n0) + mkempbuf(LEB_SIZE - n0) ∧ apebs[n].fill = align↑(datasize(buf, n0), EB_PAGE_SIZE))))
Proof step 5:
# apebs = # wlar, EB_PAGE_SIZE = EB_PAGE_SIZE, apebs = apebs, apebs1 = apebs, buf0 = buf, n1 = n, q = q, q1 = q, v0 = v, vols = vols, vols1 = vols, vtblpnum2 = EB_PAGE_SIZE, vtblpnum3 = vtblpnum, vtblpnum < # avols[v], vtblpnum < # vols[v], abs(avols, apebs, vols, q), bflipset-cons(bflipset, wlar), ebm-cons(avols), is-aligned(n, EB_PAGE_SIZE), ubi-cons(apebs, vols, wlar, q, bflipset, vtblpnum0, sqnum), ubi-io-inv(apebs), unique-sqns(apebs), valid-ebatbl(apebs, wlar, vols, vtblpnum0), valid-eraseq(q), valid-eraseq(wlar, q), valid-eraseq(apebs, q), valid-global-sqn(apebs, sqnum), valid-vtbl(apebs, vols, wlar, vtblpnum0), valid-wl(apebs, wlar), v ∈ avols, v ∈ vols, n ≤ LEB_SIZE, n ≤ # buf ⊦ [ubi_change#(v, vtblpnum, n, buf, EB_PAGE_SIZE; vols, wlar, q, bflipset, vtblpnum0, sqnum, apebs; err)] ( ubi-cons(apebs, vols, wlar, q, bflipset, vtblpnum0, sqnum) ∧ ubi-io-inv(apebs) ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ (err ≠ ESUCCESS → vols = vols1 ∧ id(apebs, apebs1, mapped-pebs(vols)) ∧ q.lebrefs ⊆ q1.lebrefs) ∧ ( err = ESUCCESS → v0 ∈ vols1 ∧ vtblpnum3 < # vols1[v0] ∧ q.lebrefs ⊆ q1.lebrefs ++ (v0 × vtblpnum3) ∧ (vols1[v0][vtblpnum3] ≠ unmapped → id(apebs, apebs1, mapped-pebs(vols1) -- vols1[v0][vtblpnum3].pnum)) ∧ (vols1[v0][vtblpnum3] = unmapped → id(apebs, apebs1, mapped-pebs(vols1))) ∧ (∃ n. vols = vols1[v0, vols1[v0][vtblpnum3, ⌜n⌝ ]] ∧ apebs[n].data = subarray(buf0, 0, n1) + mkempbuf(LEB_SIZE - n1) ∧ apebs[n].fill = align↑(datasize(buf0, n1), EB_PAGE_SIZE))) → ⟨ebm_change#(v, vtblpnum, n, buf; avols; err0)⟩ (abs(avols, apebs, vols, q) ∧ err = err0)), VTBL_VOLID ∈ vols

Rule argument

spec: ubi-asm name: inv-change seq: ubi-cons(apebs, vols, wlar, q, bflipset, vtblpnum, sqnum), vtblpnum0 = EB_PAGE_SIZE, ubi-io-inv(apebs), n0 ≤ LEB_SIZE, n0 ≤ # buf, v ∈ vols, vtblpnum1 < # vols[v], is-aligned(n0, EB_PAGE_SIZE), vols0 = vols, apebs0 = apebs, q0 = q ⊦ ⟪ubi_change# (v, vtblpnum1, n0, buf, vtblpnum0 ; vols, wlar, q, bflipset, vtblpnum, sqnum, apebs ; err)⟫ ( ubi-cons(apebs, vols, wlar, q, bflipset, vtblpnum, sqnum) ∧ ubi-io-inv(apebs) ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ ( err ≠ ESUCCESS → vols = vols0 ∧ id(apebs, apebs0, mapped-pebs(vols)) ∧ q.lebrefs ⊆ q0.lebrefs) ∧ ( err = ESUCCESS → v ∈ vols0 ∧ vtblpnum1 < # vols0[v] ∧ q.lebrefs ⊆ q0.lebrefs ++ (v × vtblpnum1) ∧ ( vols0[v][vtblpnum1] ≠ unmapped → id (apebs, apebs0, mapped-pebs(vols0) -- vols0[v][vtblpnum1].pnum)) ∧ ( vols0[v][vtblpnum1] = unmapped → id(apebs, apebs0, mapped-pebs(vols0))) ∧ (∃ n. vols = vols0[v, vols0[v][vtblpnum1, ⌜n⌝ ]] ∧ apebs[n].data = subarray(buf, 0, n0) + mkempbuf(LEB_SIZE - n0) ∧ apebs[n].fill = align↑(datasize(buf, n0), EB_PAGE_SIZE)))) subst: [vtblpnum0, buf, n0, vtblpnum1, v, apebs, sqnum, vtblpnum, bflipset, q, wlar, vols, err, vols0, apebs0, q0] → [EB_PAGE_SIZE, buf, n, vtblpnum, v, apebs, sqnum, vtblpnum0, bflipset, q, wlar, vols, err, vols, apebs, q] flags: <all paths>

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)% ⊦ v ∈ avols ∧ abs(avols, apebs, vols, q) → v ∈ vols; (ss)%⊦ v ∈ avols ∧ m < # avols[v] ∧ abs(avols, apebs, vols, q) → m < # vols[v]; (ss)