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

# apebs0 = # wlar, # buf0 = vtblpnum5 + n5, LEB_SIZE = (n1 + n2) + vtblpnum5, apebs0[n4] = mkpeb(aehdr, avhdr, buf2, m0, false), wlar[n4] = wl-entry(m1, used), avols[v][vtblpnum3] = mapped(buf2, m), vols[v][vtblpnum3] = ⌜n4⌝ , avhdr.valid?, aehdr.valid?, n2 < n5, vtblpnum3 < # avols[v], vtblpnum3 < # vols[v], n4 < # wlar, abs(avols, apebs0, vols, q), bflipset-cons(bflipset, wlar), ebm-cons(avols), is-aligned(n2, EB_PAGE_SIZE), is-aligned(n5, EB_PAGE_SIZE), is-aligned(vtblpnum5, EB_PAGE_SIZE), range=(buf0, vtblpnum5, mkbuf(vtblpnum5 + n5), vtblpnum5, n5), ubi-io-inv(apebs0[n4, mkpeb(aehdr, avhdr, subarray(buf2, 0, vtblpnum5) + subarray(buf3, n3, n2) + mkempbuf(n1), vtblpnum5 + n2, false)]), ubi-io-inv(apebs0), ubi-io-peb-inv(mkpeb(aehdr, avhdr, buf2, m0, false)), unique-sqns(apebs0[n4, mkpeb(aehdr, avhdr, subarray(buf2, 0, vtblpnum5) + subarray(buf3, n3, n2) + mkempbuf(n1), vtblpnum5 + n2, false)]), unique-sqns(apebs0), valid-ebatbl (apebs0[n4, mkpeb(aehdr, avhdr, subarray(buf2, 0, vtblpnum5) + subarray(buf3, n3, n2) + mkempbuf(n1), vtblpnum5 + n2, false)], wlar, vols, vtblpnum4), valid-ebatbl(apebs0, wlar, vols, vtblpnum4), valid-eraseq(apebs0[n4, mkpeb(aehdr, avhdr, subarray(buf2, 0, vtblpnum5) + subarray(buf3, n3, n2) + mkempbuf(n1), vtblpnum5 + n2, false)], q), valid-eraseq(apebs0, q), valid-eraseq(wlar, q), valid-eraseq(q), valid-global-sqn(apebs0[n4, mkpeb(aehdr, avhdr, subarray(buf2, 0, vtblpnum5) + subarray(buf3, n3, n2) + mkempbuf(n1), vtblpnum5 + n2, false)], sqnum), valid-global-sqn(apebs0, sqnum), valid-vtbl(apebs0, vols, wlar, vtblpnum4), valid-wl(apebs0[n4, mkpeb(aehdr, avhdr, subarray(buf2, 0, vtblpnum5) + subarray(buf3, n3, n2) + mkempbuf(n1), vtblpnum5 + n2, false)], wlar), valid-wl(apebs0, wlar), v ∈ avols, v ∈ vols, n3 + n2 ≤ # buf3, m0 ≤ vtblpnum5, m ≤ vtblpnum5, n5 + n3 ≤ # buf3, n3 + n5 ≤ # buf3, vtblpnum5 + n5 ≤ LEB_SIZE, m0 ≤ LEB_SIZE, m ≤ LEB_SIZE, vtblpnum5 ≤ LEB_SIZE, n2 + vtblpnum5 ≤ LEB_SIZE, ⌊err3⌋ , ⌊err1⌋ ⊦ n2 = 0, vtblpnum4 = n4, abs(avols, apebs0[n4, mkpeb(aehdr, avhdr, subarray(buf2, 0, vtblpnum5) + subarray(buf3, n3, n2) + mkempbuf(n1), vtblpnum5 + n2, false)], vols, q), abs (avols[v, avols[v][vtblpnum3, mapped(subarray(buf2, 0, vtblpnum5) + subarray(buf3, n3, n2) + mkempbuf(n1), vtblpnum5 + n2)]], apebs0[n4, mkpeb(aehdr, avhdr, subarray(buf2, 0, vtblpnum5) + subarray(buf3, n3, n2) + mkempbuf(n1), vtblpnum5 + n2, false)], vols, q), VTBL_VOLID ∈ vols

User applied rule insert rewrite lemma

And obtained the following new goals

Rule argument

spec: ubi-abs name: absexpt-mapped-abs seq: ⊦ abs○(avols, apebs, vols, q, v, m) ∧ v ∈ vols ∧ m < # vols[v] ∧ avols[v][m] = mapped(buf, m0) ∧ vols[v][m] = ⌜n⌝ ∧ apebs[n].data = buf ∧ apebs[n].fill ≤ m0 → abs(avols, apebs, vols, q) subst: [v, m, buf, m0, n, q, vols, apebs, avols] → [v, vtblpnum3, apebs0 [n4, mkpeb (aehdr, avhdr, subarray(buf2, 0, vtblpnum5) + subarray(buf3, n3, n2) + mkempbuf(n1), vtblpnum5 + n2, false) ] [n4 ] .data, apebs0 [n4, mkpeb (aehdr, avhdr, subarray(buf2, 0, vtblpnum5) + subarray(buf3, n3, n2) + mkempbuf(n1), vtblpnum5 + n2, false) ] [n4 ] .fill, n4, q, vols, apebs0 [n4, mkpeb (aehdr, avhdr, subarray(buf2, 0, vtblpnum5) + subarray(buf3, n3, n2) + mkempbuf(n1), vtblpnum5 + n2, false) ], avols [v, avols[v] [vtblpnum3, mapped ( subarray(buf2, 0, vtblpnum5) + subarray(buf3, n3, n2) + mkempbuf(n1), vtblpnum5 + n2) ] ]] flags: <all paths>

Additional information

Used simplifier rules: ⊦ v ∈ avols ∧ abs(avols, apebs, vols, q) → v ∈ vols; (ss)%⊦ v ∈ avols ∧ m < # avols[v] ∧ abs(avols, apebs, vols, q) → m < # vols[v]; (ss)% ⊦ avols[v, evol][v] = evol; (s)% ⊦ m < # evol → evol[m, leb][m] = leb; (s)% ⊦ m < n ↔ ¬ n ≤ m; (ss)% ⊦ m < n → (n ≤ m ↔ false); (s)%m < # apebs ⊦ apebs[m, apeb][m] = apeb; (s)% ⊦ mkpeb(aehdr, avhdr, buf, m, boolvar).data = buf; (s)% ⊦ mkpeb(aehdr, avhdr, buf, m, boolvar).fill = m; (s)%append-a: ⊦ (buf + buf0) + buf1 = buf + buf0 + buf1; from specification array-splice[buffer]% ⊦ m + n ≤ m + n0 ↔ n ≤ n0; (s)% ⊦ m ≤ m; (s)%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic%c: ⊦ m + n = n + m; from specification nat-basic%⊦ v ∈ avols ∧ m < # avols[v] ∧ avols[v][m] = mapped(buf, n) ∧ ebm-cons(avols) → # buf = LEB_SIZE; (s)% ⊦ m ≠ n → (m ≤ n ↔ m < n); (s)%⊦ v ∈ avols ∧ m < # avols[v] → ( abs○(avols[v, avols[v][m, leb]], apebs, vols, q, v, m) ↔ abs○(avols, apebs, vols, q, v, m)); (ss)%⊦ v ∈ vols ∧ m < # vols[v] ∧ vols[v][m] = ⌜n⌝ ∧ valid-ebatbl(apebs, wlar, vols, n0) → ( abs○(avols, apebs[n, apeb], vols, q, v, m) ↔ abs○(avols, apebs, vols, q, v, m)); (ss)% ⊦ abs(avols, apebs, vols, q) → abs○(avols, apebs, vols, q, v, m); (ss)%# buf = n ⊦ subarray(buf, 0, n) = buf; (s) Used terms: v, vtblpnum3, apebs0 [n4, mkpeb (aehdr, avhdr, subarray(buf2, 0, vtblpnum5) + subarray(buf3, n3, n2) + mkempbuf(n1), vtblpnum5 + n2, false) ] [n4 ] .data, apebs0 [n4, mkpeb (aehdr, avhdr, subarray(buf2, 0, vtblpnum5) + subarray(buf3, n3, n2) + mkempbuf(n1), vtblpnum5 + n2, false) ] [n4 ] .fill, n4, q, vols, apebs0 [n4, mkpeb (aehdr, avhdr, subarray(buf2, 0, vtblpnum5) + subarray(buf3, n3, n2) + mkempbuf(n1), vtblpnum5 + n2, false) ], avols [v, avols[v] [vtblpnum3, mapped ( subarray(buf2, 0, vtblpnum5) + subarray(buf3, n3, n2) + mkempbuf(n1), vtblpnum5 + n2) ] ]