[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 46 from proof inv-create-volume (previous step)

# buf0 = LEB_SIZE, # apebs0 = # wlar2, # apebs = # wlar, apebs0[vtblpnum] = mkpeb(aehdr, empty, mkempbuf(LEB_SIZE), 0, false), wlar2[vtblpnum] = wl-entry(m, free), q0 = [], vols0 = vols, v ≠ VTBL_VOLID, vtblpnum3 ≠ vtblpnum, aehdr.valid?, vtblpnum < # wlar2, bflipset-cons(bflipset, wlar2), bflipset-cons(bflipset, wlar), id(apebs0, apebs, mapped-pebs(vols)), is-encoded(to-vtbl(vols)[v, n], buf0), ubi-io-inv(apebs), ubi-io-inv(apebs0), unique-sqns(apebs0), unique-sqns(apebs), valid-ebatbl(apebs0, wlar2, vols, vtblpnum3), valid-ebatbl(apebs, wlar, vols, vtblpnum3), valid-eraseq(wlar2, []), valid-eraseq(apebs, q), valid-eraseq(wlar, q), valid-eraseq(q), valid-global-sqn(apebs0, sqnum), valid-global-sqn(apebs, sqnum), valid-vtbl(apebs0, vols, wlar2, vtblpnum3), valid-vtbl(apebs, vols, wlar, vtblpnum3), valid-wl(apebs0, wlar2), valid-wl(apebs, wlar), # to-vtbl(vols)[v, n] * (ENCODED_NAT_SIZE + ENCODED_VOLID_SIZE) + ENCODED_NAT_SIZE ≤ LEB_SIZE, 2 * ENCODED_NAT_SIZE + (ENCODED_VOLID_SIZE + ENCODED_NAT_SIZE) * # vols + ENCODED_VOLID_SIZE ≤ LEB_SIZE, ¬ vtblpnum3 ∈ q, ¬ VTBL_VOLID ∈ vols, ¬ v ∈ vols ⊦ ⟪ubi_atomic_leb_change#(VTBL_VOLID, VTBL_LNUM, vtblpnum, LEB_SIZE, buf0, EB_PAGE_SIZE; vols, wlar2, q0, bflipset, vtblpnum3, sqnum, apebs0; err); if err = ESUCCESS then {vols[v] := mkebatbl(n); vols[v] := fill(vols[v], unmapped)}⟫ ( # apebs0 = # wlar2 ∧ unique-sqns(apebs0) ∧ valid-global-sqn(apebs0, sqnum) ∧ valid-wl(apebs0, wlar2) ∧ valid-eraseq(q0) ∧ valid-eraseq(wlar2, q0) ∧ valid-eraseq(apebs0, q0) ∧ ¬ VTBL_VOLID ∈ vols ∧ bflipset-cons(bflipset, wlar2) ∧ valid-ebatbl(apebs0, wlar2, vols, vtblpnum3) ∧ valid-vtbl(apebs0, vols, wlar2, vtblpnum3) ∧ ubi-io-inv(apebs0) ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ id(apebs0, apebs, mapped-pebs(vols)) ∧ (err = ESUCCESS → ¬ v ∈ vols0 ∧ vols = vols0[v, fill(mkebatbl(n), unmapped)] ∧ q0.lebrefs ⊆ ∅ ++ (VTBL_VOLID × VTBL_LNUM)) ∧ (err ≠ ESUCCESS → q0.lebrefs ⊆ q.lebrefs ∧ vols = vols0))

User applied rule insert program lemma

And obtained the following new goals

Proof step 47:
ubi-cons(apebs, vols, wlar, q, bflipset, vtblpnum, sqnum), ubi-io-inv(apebs), n0 ≤ # buf, n < # wlar, n0 ≤ LEB_SIZE, wlar[n].status = free, apebs0 = apebs, is-aligned(n0, EB_PAGE_SIZE), v ∈ vols ∧ m < # vols[v] ∨ v = VTBL_VOLID ∧ m = VTBL_LNUM, vols0 = vols, q0 = q, vtblpnum0 = vtblpnum ⊦ ⟪ubi_atomic_leb_change#(v, m, n, n0, buf, EB_PAGE_SIZE; vols, wlar, q, bflipset, vtblpnum, sqnum, apebs; err)⟫ ( (err = ESUCCESS ∨ ⌊err⌋ ) ∧ id○(apebs, apebs0, n) ∧ ubi-io-inv(apebs) ∧ # 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) ∧ ( v ∈ vols0 ∨ is-encoded(to-vtbl(vols0), subarray(buf, 0, n0)) ∧ n0 = LEB_SIZE ∨ err ≠ ESUCCESS → valid-ebatbl(apebs, wlar, vols, vtblpnum) ∧ valid-vtbl(apebs, vols, wlar, vtblpnum)) ∧ ( err = ESUCCESS ∧ v = VTBL_VOLID ∧ m = VTBL_LNUM → (∀ v0, m0. ¬ v0 ∈ vols0 ∧ is-encoded(to-vtbl(vols0)[v0, m0], subarray(buf, 0, n0)) ∧ n0 = LEB_SIZE → valid-ebatbl(apebs, wlar, vols[v0, fill(mkebatbl(m0), unmapped)], vtblpnum) ∧ valid-vtbl(apebs, vols[v0, fill(mkebatbl(m0), unmapped)], wlar, vtblpnum))) ∧ (err = ESUCCESS ∧ v ∈ vols0 ∧ vols0[v][m] ≠ unmapped → q = q0 + eq-entry(vols0[v][m].pnum, v × m)) ∧ (err = ESUCCESS ∧ v = VTBL_VOLID ∧ m = VTBL_LNUM → q = q0 + eq-entry(vtblpnum0, v × m)) ∧ id(apebs, apebs0, mapped-pebs(vols0)) ∧ (v = VTBL_VOLID ∧ m = VTBL_LNUM ∨ err ≠ ESUCCESS → vols = vols0) ∧ (v ∈ vols0 ∧ err = ESUCCESS → vols = vols0[v, vols0[v][m, ⌜n⌝ ]]) ∧ ( err = ESUCCESS → apebs[n].fill = align↑(datasize(buf, n0), EB_PAGE_SIZE) ∧ apebs[n].data = subarray(buf, 0, n0) + mkempbuf(LEB_SIZE - n0) ∧ q.lebrefs ⊆ q0.lebrefs ++ (v × m)) ∧ (err ≠ ESUCCESS → q.lebrefs = q0.lebrefs))
Proof step 48:
# apebs = # wlar, # apebs0 = # wlar2, # buf0 = LEB_SIZE, wlar2[vtblpnum].status = free, wlar2[vtblpnum] = wl-entry(m, free), apebs0[vtblpnum] = mkpeb(aehdr, empty, mkempbuf(LEB_SIZE), 0, false), apebs0 = apebs0, apebs1 = apebs0, buf1 = buf0, m0 = VTBL_LNUM, n1 = LEB_SIZE, n2 = vtblpnum, q0 = [], q0 = q0, q1 = q0, v0 = VTBL_VOLID, vols = vols, vols0 = vols, vols1 = vols, vtblpnum1 = vtblpnum3, vtblpnum3 = vtblpnum3, aehdr.valid?, vtblpnum < # wlar2, bflipset-cons(bflipset, wlar), bflipset-cons(bflipset, wlar2), id(apebs0, apebs, mapped-pebs(vols)), is-aligned(LEB_SIZE, EB_PAGE_SIZE), is-encoded(to-vtbl(vols)[v, n], buf0), ubi-cons(apebs0, vols, wlar2, q0, bflipset, vtblpnum3, sqnum), ubi-io-inv(apebs), ubi-io-inv(apebs0), unique-sqns(apebs), unique-sqns(apebs0), valid-ebatbl(apebs, wlar, vols, vtblpnum3), valid-ebatbl(apebs0, wlar2, vols, vtblpnum3), valid-eraseq(q), valid-eraseq(wlar, q), valid-eraseq(apebs, q), valid-eraseq(wlar2, []), valid-global-sqn(apebs, sqnum), valid-global-sqn(apebs0, sqnum), valid-vtbl(apebs, vols, wlar, vtblpnum3), valid-vtbl(apebs0, vols, wlar2, vtblpnum3), valid-wl(apebs, wlar), valid-wl(apebs0, wlar2), 2 * ENCODED_NAT_SIZE + (ENCODED_VOLID_SIZE + ENCODED_NAT_SIZE) * # vols + ENCODED_VOLID_SIZE ≤ LEB_SIZE, # to-vtbl(vols)[v, n] * (ENCODED_NAT_SIZE + ENCODED_VOLID_SIZE) + ENCODED_NAT_SIZE ≤ LEB_SIZE, LEB_SIZE ≤ # buf0, LEB_SIZE ≤ LEB_SIZE, VTBL_VOLID ∈ vols ∧ VTBL_LNUM < # vols[VTBL_VOLID] ∨ VTBL_VOLID = VTBL_VOLID ∧ VTBL_LNUM = VTBL_LNUM ⊦ [ubi_atomic_leb_change#(VTBL_VOLID, VTBL_LNUM, vtblpnum, LEB_SIZE, buf0, EB_PAGE_SIZE; vols, wlar2, q0, bflipset, vtblpnum3, sqnum, apebs0; err)] ( (err = ESUCCESS ∨ ⌊err⌋ ) ∧ id○(apebs0, apebs1, n2) ∧ ubi-io-inv(apebs0) ∧ # apebs0 = # wlar2 ∧ unique-sqns(apebs0) ∧ valid-global-sqn(apebs0, sqnum) ∧ valid-wl(apebs0, wlar2) ∧ valid-eraseq(q0) ∧ valid-eraseq(wlar2, q0) ∧ valid-eraseq(apebs0, q0) ∧ ¬ VTBL_VOLID ∈ vols ∧ bflipset-cons(bflipset, wlar2) ∧ ( v0 ∈ vols1 ∨ is-encoded(to-vtbl(vols1), subarray(buf1, 0, n1)) ∧ n1 = LEB_SIZE ∨ err ≠ ESUCCESS → valid-ebatbl(apebs0, wlar2, vols, vtblpnum3) ∧ valid-vtbl(apebs0, vols, wlar2, vtblpnum3)) ∧ ( err = ESUCCESS ∧ v0 = VTBL_VOLID ∧ m0 = VTBL_LNUM → (∀ v0, m0. ¬ v0 ∈ vols1 ∧ is-encoded(to-vtbl(vols1)[v0, m0], subarray(buf1, 0, n1)) ∧ n1 = LEB_SIZE → valid-ebatbl(apebs0, wlar2, vols[v0, fill(mkebatbl(m0), unmapped)], vtblpnum3) ∧ valid-vtbl(apebs0, vols[v0, fill(mkebatbl(m0), unmapped)], wlar2, vtblpnum3))) ∧ (err = ESUCCESS ∧ v0 ∈ vols1 ∧ vols1[v0][m0] ≠ unmapped → q0 = q1 + eq-entry(vols1[v0][m0].pnum, v0 × m0)) ∧ (err = ESUCCESS ∧ v0 = VTBL_VOLID ∧ m0 = VTBL_LNUM → q0 = q1 + eq-entry(vtblpnum1, v0 × m0)) ∧ id(apebs0, apebs1, mapped-pebs(vols1)) ∧ (v0 = VTBL_VOLID ∧ m0 = VTBL_LNUM ∨ err ≠ ESUCCESS → vols = vols1) ∧ (v0 ∈ vols1 ∧ err = ESUCCESS → vols = vols1[v0, vols1[v0][m0, ⌜n2⌝ ]]) ∧ ( err = ESUCCESS → apebs0[n2].fill = align↑(datasize(buf1, n1), EB_PAGE_SIZE) ∧ apebs0[n2].data = subarray(buf1, 0, n1) + mkempbuf(LEB_SIZE - n1) ∧ q0.lebrefs ⊆ q1.lebrefs ++ (v0 × m0)) ∧ (err ≠ ESUCCESS → q0.lebrefs = q1.lebrefs) → ⟪if err = ESUCCESS then {vols[v] := mkebatbl(n); vols[v] := fill(vols[v], unmapped)}⟫ ( # apebs0 = # wlar2 ∧ unique-sqns(apebs0) ∧ valid-global-sqn(apebs0, sqnum) ∧ valid-wl(apebs0, wlar2) ∧ valid-eraseq(q0) ∧ valid-eraseq(wlar2, q0) ∧ valid-eraseq(apebs0, q0) ∧ ¬ VTBL_VOLID ∈ vols ∧ bflipset-cons(bflipset, wlar2) ∧ valid-ebatbl(apebs0, wlar2, vols, vtblpnum3) ∧ valid-vtbl(apebs0, vols, wlar2, vtblpnum3) ∧ ubi-io-inv(apebs0) ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ id(apebs0, apebs, mapped-pebs(vols)) ∧ (err = ESUCCESS → ¬ v ∈ vols0 ∧ vols = vols0[v, fill(mkebatbl(n), unmapped)] ∧ q0.lebrefs ⊆ ∅ ++ (VTBL_VOLID × VTBL_LNUM)) ∧ (err ≠ ESUCCESS → q0.lebrefs ⊆ q.lebrefs ∧ vols = vols0))), v = VTBL_VOLID, vtblpnum3 = vtblpnum, vtblpnum3 ∈ q, VTBL_VOLID ∈ vols, v ∈ vols

Rule argument

spec: <toplevel> name: prepost-atomic-leb-change seq: ubi-cons(apebs, vols, wlar, q, bflipset, vtblpnum, sqnum), ubi-io-inv(apebs), n0 ≤ # buf, n < # wlar, n0 ≤ LEB_SIZE, wlar[n].status = free, apebs0 = apebs, is-aligned(n0, EB_PAGE_SIZE), v ∈ vols ∧ m < # vols[v] ∨ v = VTBL_VOLID ∧ m = VTBL_LNUM, vols0 = vols, q0 = q, vtblpnum0 = vtblpnum ⊦ ⟪ubi_atomic_leb_change# (v, m, n, n0, buf, EB_PAGE_SIZE ; vols, wlar, q, bflipset, vtblpnum, sqnum, apebs ; err)⟫ ( (err = ESUCCESS ∨ ⌊err⌋ ) ∧ id○(apebs, apebs0, n) ∧ ubi-io-inv(apebs) ∧ # 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) ∧ ( v ∈ vols0 ∨ is-encoded(to-vtbl(vols0), subarray(buf, 0, n0)) ∧ n0 = LEB_SIZE ∨ err ≠ ESUCCESS → valid-ebatbl(apebs, wlar, vols, vtblpnum) ∧ valid-vtbl(apebs, vols, wlar, vtblpnum)) ∧ ( err = ESUCCESS ∧ v = VTBL_VOLID ∧ m = VTBL_LNUM → (∀ v0, m0. ¬ v0 ∈ vols0 ∧ is-encoded (to-vtbl(vols0)[v0, m0], subarray(buf, 0, n0)) ∧ n0 = LEB_SIZE → valid-ebatbl (apebs, wlar, vols[v0, fill(mkebatbl(m0), unmapped)], vtblpnum) ∧ valid-vtbl (apebs, vols[v0, fill(mkebatbl(m0), unmapped)], wlar, vtblpnum))) ∧ ( err = ESUCCESS ∧ v ∈ vols0 ∧ vols0[v][m] ≠ unmapped → q = q0 + eq-entry(vols0[v][m].pnum, v × m)) ∧ ( err = ESUCCESS ∧ v = VTBL_VOLID ∧ m = VTBL_LNUM → q = q0 + eq-entry(vtblpnum0, v × m)) ∧ id(apebs, apebs0, mapped-pebs(vols0)) ∧ ( v = VTBL_VOLID ∧ m = VTBL_LNUM ∨ err ≠ ESUCCESS → vols = vols0) ∧ ( v ∈ vols0 ∧ err = ESUCCESS → vols = vols0[v, vols0[v][m, ⌜n⌝ ]]) ∧ ( err = ESUCCESS → apebs[n].fill = align↑(datasize(buf, n0), EB_PAGE_SIZE) ∧ apebs[n].data = subarray(buf, 0, n0) + mkempbuf(LEB_SIZE - n0) ∧ q.lebrefs ⊆ q0.lebrefs ++ (v × m)) ∧ (err ≠ ESUCCESS → q.lebrefs = q0.lebrefs)) subst: [buf, n0, n, m, v, apebs, sqnum, vtblpnum, bflipset, q, wlar, vols, err, apebs0, vols0, q0, vtblpnum0] → [buf0, LEB_SIZE, vtblpnum, VTBL_LNUM, VTBL_VOLID, apebs0, sqnum, vtblpnum3, bflipset, q0, wlar2, vols, err, apebs0, vols, q0, vtblpnum3] 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)% ⊦ valid-eraseq([]); (s)% ⊦ valid-eraseq(apebs, []); (s)% ⊦ m ≤ m; (s)% ⊦ is-aligned(LEB_SIZE, EB_PAGE_SIZE); (ss)% ⊦ wl-entry(m, stat).status = stat; (s)