[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 232 from proof prepost-atomic-leb-change (previous step)

# apebs0 = # wlar, LEB_SIZE = n2 + n0, wlar[n1] = wl-entry(m1, free), apebs0[n1] = mkpeb(aehdr, empty, mkempbuf(LEB_SIZE), 0, false), apebs = apebs0[n1, mkpeb(aehdr, avidhdr(v, m0, sqnum, datasize(buf, n0), checksum(buf, datasize(buf, n0))), mkempbuf(LEB_SIZE), 0, false)], buf0 = buf, err = err0, err1 = err, n = align↑(datasize(buf, n0), EB_PAGE_SIZE), q0 = q, vols0 = vols, vtblpnum = n1, vtblpnum0 = vtblpnum1, aehdr.valid?, n1 < # apebs0, n1 < # wlar, vtblpnum < # apebs, bflipset-cons(bflipset, wlar), is-aligned(# buf1, EB_PAGE_SIZE), is-aligned(n0, EB_PAGE_SIZE), ubi-io-inv(apebs0), ubi-io-inv(apebs0[n1, mkpeb(aehdr, avidhdr(v, m0, sqnum, datasize(buf, n0), checksum(buf, datasize(buf, n0))), mkempbuf(LEB_SIZE), 0, false)]), ubi-io-inv (apebs[vtblpnum, mkpeb(apebs[vtblpnum].echdr, apebs[vtblpnum].vidhdr, buf1 + mkempbuf(LEB_SIZE - # buf1), # buf1, apebs[vtblpnum].bad)]), unique-sqns(apebs0), valid-ebatbl(apebs0, wlar, vols, vtblpnum1), valid-eraseq(q), valid-eraseq(wlar, q), valid-eraseq(apebs0, q), valid-global-sqn(apebs0, sqnum), valid-vtbl(apebs0, vols, wlar, vtblpnum1), valid-wl(apebs0, wlar), # buf1 ≤ n, n0 ≤ # buf, n0 ≤ LEB_SIZE, align↑(datasize(buf, n0), EB_PAGE_SIZE) ≤ LEB_SIZE, align↑(datasize(buf, n0), EB_PAGE_SIZE) ≤ # buf, LEB_SIZE ≥ # buf1, # buf1 ≤ n → is-aligned(# buf1, EB_PAGE_SIZE) → ¬ datasize(buf1, # buf1) < datasize(buf0, n) → n ≥ # buf1, datasize(buf1, # buf1) < datasize(buf0, n) ∨ checksum(buf1 + mkempbuf(n - # buf1), datasize(buf0, n)) ≠ checksum(buf0, datasize(buf0, n)), v ∈ vols ∧ m0 < # vols[v] ∨ v = VTBL_VOLID ∧ m0 = VTBL_LNUM, ⌊err0⌋ ∨ err0 = ESUCCESS ⊦ ⟪ubi_wl_put_peb#(none, n1; wlar, q)⟫ ( (err1 = ESUCCESS ∨ ⌊err1⌋ ) ∧ id○ (apebs [vtblpnum, mkpeb(apebs[vtblpnum].echdr, apebs[vtblpnum].vidhdr, buf1 + mkempbuf(LEB_SIZE - # buf1), # buf1, apebs[vtblpnum].bad) ], apebs0, n1) ∧ # apebs [vtblpnum, mkpeb(apebs[vtblpnum].echdr, apebs[vtblpnum].vidhdr, buf1 + mkempbuf(LEB_SIZE - # buf1), # buf1, apebs[vtblpnum].bad) ] = # wlar ∧ unique-sqns (apebs [vtblpnum, mkpeb(apebs[vtblpnum].echdr, apebs[vtblpnum].vidhdr, buf1 + mkempbuf(LEB_SIZE - # buf1), # buf1, apebs[vtblpnum].bad) ]) ∧ valid-global-sqn (apebs [vtblpnum, mkpeb(apebs[vtblpnum].echdr, apebs[vtblpnum].vidhdr, buf1 + mkempbuf(LEB_SIZE - # buf1), # buf1, apebs[vtblpnum].bad) ], sqnum + 1) ∧ valid-wl (apebs [vtblpnum, mkpeb(apebs[vtblpnum].echdr, apebs[vtblpnum].vidhdr, buf1 + mkempbuf(LEB_SIZE - # buf1), # buf1, apebs[vtblpnum].bad) ], wlar) ∧ valid-eraseq(q) ∧ valid-eraseq(wlar, q) ∧ valid-eraseq (apebs [vtblpnum, mkpeb(apebs[vtblpnum].echdr, apebs[vtblpnum].vidhdr, buf1 + mkempbuf(LEB_SIZE - # buf1), # buf1, apebs[vtblpnum].bad) ], q) ∧ ¬ VTBL_VOLID ∈ vols ∧ bflipset-cons(bflipset, wlar) ∧ ( v ∈ vols0 ∨ is-encoded(to-vtbl(vols0), subarray(buf, 0, LEB_SIZE)) ∧ n0 = LEB_SIZE ∨ err1 ≠ ESUCCESS → valid-ebatbl (apebs [vtblpnum, mkpeb(apebs[vtblpnum].echdr, apebs[vtblpnum].vidhdr, buf1 + mkempbuf(LEB_SIZE - # buf1), # buf1, apebs[vtblpnum].bad) ], wlar, vols, vtblpnum0) ∧ valid-vtbl (apebs [vtblpnum, mkpeb(apebs[vtblpnum].echdr, apebs[vtblpnum].vidhdr, buf1 + mkempbuf(LEB_SIZE - # buf1), # buf1, apebs[vtblpnum].bad) ], vols, wlar, vtblpnum0)) ∧ ( err1 = ESUCCESS ∧ v = VTBL_VOLID ∧ m0 = VTBL_LNUM → (∀ v0, m0. ¬ v0 ∈ vols0 ∧ is-encoded(to-vtbl(vols0)[v0, m0], subarray(buf, 0, LEB_SIZE)) ∧ n0 = LEB_SIZE → valid-ebatbl (apebs [vtblpnum, mkpeb(apebs[vtblpnum].echdr, apebs[vtblpnum].vidhdr, buf1 + mkempbuf(LEB_SIZE - # buf1), # buf1, apebs[vtblpnum].bad) ], wlar, vols[v0, fill(mkebatbl(m0), unmapped)], vtblpnum0) ∧ valid-vtbl (apebs [vtblpnum, mkpeb(apebs[vtblpnum].echdr, apebs[vtblpnum].vidhdr, buf1 + mkempbuf(LEB_SIZE - # buf1), # buf1, apebs[vtblpnum].bad) ], vols[v0, fill(mkebatbl(m0), unmapped)], wlar, vtblpnum0))) ∧ (err1 = ESUCCESS ∧ v ∈ vols0 ∧ vols0[v][m0] ≠ unmapped → q = q0 + eq-entry(vols0[v][m0].pnum, v × m0) ') ∧ (err1 = ESUCCESS ∧ v = VTBL_VOLID ∧ m0 = VTBL_LNUM → q = q0 + eq-entry(vtblpnum1, VTBL_VOLID × VTBL_LNUM) ') ∧ id (apebs [vtblpnum, mkpeb(apebs[vtblpnum].echdr, apebs[vtblpnum].vidhdr, buf1 + mkempbuf(LEB_SIZE - # buf1), # buf1, apebs[vtblpnum].bad) ], apebs0, mapped-pebs(vols0)) ∧ (v = VTBL_VOLID ∧ m0 = VTBL_LNUM ∨ err1 ≠ ESUCCESS → vols = vols0) ∧ (v ∈ vols0 ∧ err1 = ESUCCESS → vols = vols0[v, vols0[v][m0, ⌜n1⌝ ]]) ∧ ( err1 = ESUCCESS → apebs [vtblpnum, mkpeb(apebs[vtblpnum].echdr, apebs[vtblpnum].vidhdr, buf1 + mkempbuf(LEB_SIZE - # buf1), # buf1, apebs[vtblpnum].bad) ] [n1 ] .fill = align↑(datasize(buf, n0), EB_PAGE_SIZE) ∧ apebs [vtblpnum, mkpeb(apebs[vtblpnum].echdr, apebs[vtblpnum].vidhdr, buf1 + mkempbuf(LEB_SIZE - # buf1), # buf1, apebs[vtblpnum].bad) ] [n1 ] .data = subarray(buf, 0, n0) + mkempbuf(n2) ∧ q.lebrefs ⊆ q0.lebrefs ++ (v × m0)) ∧ (err1 ≠ ESUCCESS → q.lebrefs = q0.lebrefs)), err = ESUCCESS, vtblpnum1 = n1, vtblpnum1 ∈ q, VTBL_VOLID ∈ vols, ∃ buf0. buf = mkempbuf(n0) + buf0

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 233:
# apebs0 = # wlar, LEB_SIZE = n2 + n0, apebs0[n1] = mkpeb(aehdr, empty, mkempbuf(LEB_SIZE), 0, false), wlar[n1] = wl-entry(m1, free), q0 = q, vtblpnum1 ≠ n1, aehdr.valid?, n1 < # wlar, bflipset-cons(bflipset, wlar), is-aligned(n0, EB_PAGE_SIZE), is-aligned(# buf1, EB_PAGE_SIZE), ubi-io-inv (apebs0 [n1, mkpeb(aehdr, avidhdr(v, m0, sqnum, datasize(buf, n0), checksum(buf, datasize(buf, n0))), buf1 + mkempbuf(LEB_SIZE - # buf1), # buf1, false) ]), ubi-io-inv(apebs0[n1, mkpeb(aehdr, avidhdr(v, m0, sqnum, datasize(buf, n0), checksum(buf, datasize(buf, n0))), mkempbuf(LEB_SIZE), 0, false)]), ubi-io-inv(apebs0), unique-sqns(apebs0), valid-ebatbl(apebs0, wlar, vols, vtblpnum1), valid-eraseq(apebs0, q), valid-eraseq(wlar, q), valid-eraseq(q), valid-global-sqn(apebs0, sqnum), valid-vtbl(apebs0, vols, wlar, vtblpnum1), valid-wl(apebs0, wlar), align↑(datasize(buf, n0), EB_PAGE_SIZE) ≤ # buf, align↑(datasize(buf, n0), EB_PAGE_SIZE) ≤ LEB_SIZE, n0 ≤ LEB_SIZE, n0 ≤ # buf, # buf1 ≤ align↑(datasize(buf, n0), EB_PAGE_SIZE), # buf1 ≤ # buf, # buf1 ≤ LEB_SIZE, ⌊err0⌋ , ¬ VTBL_VOLID ∈ vols, ¬ vtblpnum1 ∈ q, v ∈ vols ∧ m0 < # vols[v] ∨ v = VTBL_VOLID ∧ m0 = VTBL_LNUM, datasize(buf1, # buf1) < datasize(buf, n0) ∨ checksum(buf1 + mkempbuf(align↑(datasize(buf, n0), EB_PAGE_SIZE) - # buf1), datasize(buf, n0)) ≠ checksum(buf, datasize(buf, n0)) ⊦ ⟪ubi_wl_put_peb#(none, n1; wlar, q)⟫ ( # apebs0 = # wlar ∧ unique-sqns (apebs0 [n1, mkpeb (aehdr, avidhdr(v, m0, sqnum, datasize(buf, n0), checksum(buf, datasize(buf, n0))), buf1 + mkempbuf(LEB_SIZE - # buf1), # buf1, false) ]) ∧ valid-global-sqn (apebs0 [n1, mkpeb (aehdr, avidhdr(v, m0, sqnum, datasize(buf, n0), checksum(buf, datasize(buf, n0))), buf1 + mkempbuf(LEB_SIZE - # buf1), # buf1, false) ], sqnum + 1) ∧ valid-wl (apebs0 [n1, mkpeb (aehdr, avidhdr(v, m0, sqnum, datasize(buf, n0), checksum(buf, datasize(buf, n0))), buf1 + mkempbuf(LEB_SIZE - # buf1), # buf1, false) ], wlar) ∧ valid-eraseq(q) ∧ valid-eraseq(wlar, q) ∧ valid-eraseq (apebs0 [n1, mkpeb (aehdr, avidhdr(v, m0, sqnum, datasize(buf, n0), checksum(buf, datasize(buf, n0))), buf1 + mkempbuf(LEB_SIZE - # buf1), # buf1, false) ], q) ∧ bflipset-cons(bflipset, wlar) ∧ valid-ebatbl (apebs0 [n1, mkpeb (aehdr, avidhdr(v, m0, sqnum, datasize(buf, n0), checksum(buf, datasize(buf, n0))), buf1 + mkempbuf(LEB_SIZE - # buf1), # buf1, false) ], wlar, vols, vtblpnum1) ∧ valid-vtbl(apebs0, vols, wlar, vtblpnum1) ∧ id (apebs0 [n1, mkpeb (aehdr, avidhdr(v, m0, sqnum, datasize(buf, n0), checksum(buf, datasize(buf, n0))), buf1 + mkempbuf(LEB_SIZE - # buf1), # buf1, false) ], apebs0, mapped-pebs(vols)) ∧ q.lebrefs = q0.lebrefs), ∃ buf0. buf = mkempbuf(n0) + buf0

Rule argument

Additional information

Used simplifier rules: ⊦ m ≠ n0 → ( valid-vtbl(apebs[m, apeb], vols, wlar, n0) ↔ valid-vtbl(apebs, vols, wlar, n0)); (s)%# buf = n ⊦ subarray(buf, 0, n) = buf; (s)% ⊦ ¬ ⌊ESUCCESS⌋ ; (s)%c: ⊦ m + n = n + m; from specification nat-basic%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic% ⊦ m = m + n ↔ n = 0; (s)% ⊦ m < n → n ≠ 0; (s)%let: ⊦ n ≤ n0 ∧ n0 ≤ n1 → n ≤ n1; (forward) from specification nat%lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic%f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic%fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat%⊦ apeb = apebs[n] ∧ apeb = apebs0[n] → (id○(apebs, apebs0, n) ↔ apebs = apebs0); (s)% ⊦ id○(apebs[n, apeb], apebs0, n) ↔ id○(apebs, apebs0, n); (s)%n ≠ 0 ⊦ is-aligned(m0, n) ∧ m0 ≤ m → align↑(m, n) ≥ m0; (s)%n ≤ # buf ⊦ datasize(buf, datasize(buf, n)) = datasize(buf, n); (s)%n ≠ 0, m % n = 0 ⊦ align↑(m, n) = m; (s)% ⊦ m ≤ n → (n < m ↔ false); (s)% ⊦ m ≤ n ↔ ¬ n < m; (ss)% ⊦ EB_PAGE_SIZE ≠ 0; (s)%⊦ n ≤ # buf ∧ is-aligned(n, EB_PAGE_SIZE) → datasize(buf, align↑(datasize(buf, n), EB_PAGE_SIZE)) = datasize(buf, n); (s)% ⊦ ⌊err⌋ → err ≠ ESUCCESS; (s)% ⊦ # apebs[n, apeb] = # apebs; (s)%m < # apebs ⊦ apebs[m, apeb][m, apeb0] = apebs[m, apeb0]; (s)% ⊦ m < n → (n ≤ m ↔ false); (s)% ⊦ m < n ↔ ¬ n ≤ m; (ss)% ⊦ mkpeb(aehdr, avhdr, buf, m, boolvar).bad ↔ boolvar; (s)% ⊦ mkpeb(aehdr, avhdr, buf, m, boolvar).vidhdr = avhdr; (s)% ⊦ mkpeb(aehdr, avhdr, buf, m, boolvar).echdr = aehdr; (s)% ⊦ m < # apebs → apebs[m, apeb][m] = apeb; (s)% ⊦ n ≥ m ↔ m ≤ n; (s)