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

# apebs0 = # wlar0, # apebs = # wlar, LEB_SIZE = n2 + n, apebs0[n0] = mkpeb(aehdr, avhdr, subarray(buf, 0, n) + mkempbuf(n2), align↑(datasize(buf, n), EB_PAGE_SIZE), boolvar), vtblpnum < # vols[v], vtblpnum < # avols[v], abs(avols, apebs, vols, q), bflipset-cons(bflipset0, wlar0), bflipset-cons(bflipset, wlar), ebm-cons(avols), is-aligned(n, EB_PAGE_SIZE), ubi-io-inv(apebs0), ubi-io-inv(apebs), unique-sqns(apebs0), unique-sqns(apebs), valid-ebatbl(apebs0, wlar0, vols[v, vols[v][vtblpnum, ⌜n0⌝ ]], vtblpnum1), valid-ebatbl(apebs, wlar, vols, vtblpnum0), valid-eraseq(q0), valid-eraseq(wlar0, q0), valid-eraseq(apebs0, q0), valid-eraseq(apebs, q), valid-eraseq(wlar, q), valid-eraseq(q), valid-global-sqn(apebs0, sqnum0), valid-global-sqn(apebs, sqnum), valid-vtbl(apebs, vols, wlar, vtblpnum0), valid-vtbl(apebs0, vols, wlar0, vtblpnum1), valid-wl(apebs0, wlar0), valid-wl(apebs, wlar), v ∈ vols, v ∈ avols, n ≤ # buf, n ≤ LEB_SIZE, q0.lebrefs ⊆ q.lebrefs ++ (v × vtblpnum), vols[v][vtblpnum] = unmapped → id(apebs0, apebs, mapped-pebs(vols)), vols[v][vtblpnum] ≠ unmapped → id(apebs0, apebs, mapped-pebs(vols) -- vols[v][vtblpnum].pnum) ⊦ abs(avols[v, avols[v][vtblpnum, mapped(subarray(buf, 0, n) + mkempbuf(n2), n)]], apebs0, vols[v, vols[v][vtblpnum, ⌜n0⌝ ]], q), abs(avols[v, avols[v][vtblpnum, mapped(subarray(buf, 0, n) + mkempbuf(n2), n)]], apebs0, vols[v, vols[v][vtblpnum, ⌜n0⌝ ]], q0), VTBL_VOLID ∈ vols, abs○(avols[v, avols[v][vtblpnum, mapped(subarray(buf, 0, n) + mkempbuf(n2), n)]], apebs0, vols[v, vols[v][vtblpnum, ⌜n0⌝ ]], q, v, vtblpnum) ∧ v ∈ vols[v, vols[v][vtblpnum, ⌜n0⌝ ]] ∧ vtblpnum < # vols[v, vols[v][vtblpnum, ⌜n0⌝ ]][v] ∧ avols[v, avols[v][vtblpnum, mapped(subarray(buf, 0, n) + mkempbuf(n2), n)]][v][vtblpnum] = mapped(subarray(buf, 0, n) + mkempbuf(n2), n) ∧ vols[v, vols[v][vtblpnum, ⌜n0⌝ ]][v][vtblpnum] = ⌜n0⌝ ∧ apebs0[n0].data = subarray(buf, 0, n) + mkempbuf(n2) ∧ apebs0[n0].fill ≤ n

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 30:
# apebs0 = # wlar0, # apebs = # wlar, LEB_SIZE = n2 + n, apebs0[n0] = mkpeb(aehdr, avhdr, subarray(buf, 0, n) + mkempbuf(n2), align↑(datasize(buf, n), EB_PAGE_SIZE), boolvar), vtblpnum < # vols[v], vtblpnum < # avols[v], abs(avols, apebs, vols, q), bflipset-cons(bflipset0, wlar0), bflipset-cons(bflipset, wlar), ebm-cons(avols), is-aligned(n, EB_PAGE_SIZE), ubi-io-inv(apebs0), ubi-io-inv(apebs), unique-sqns(apebs0), unique-sqns(apebs), valid-ebatbl(apebs0, wlar0, vols[v, vols[v][vtblpnum, ⌜n0⌝ ]], vtblpnum1), valid-ebatbl(apebs, wlar, vols, vtblpnum0), valid-eraseq(q0), valid-eraseq(wlar0, q0), valid-eraseq(apebs0, q0), valid-eraseq(apebs, q), valid-eraseq(wlar, q), valid-eraseq(q), valid-global-sqn(apebs0, sqnum0), valid-global-sqn(apebs, sqnum), valid-vtbl(apebs, vols, wlar, vtblpnum0), valid-vtbl(apebs0, vols, wlar0, vtblpnum1), valid-wl(apebs0, wlar0), valid-wl(apebs, wlar), v ∈ vols, v ∈ avols, n ≤ # buf, n ≤ LEB_SIZE, q0.lebrefs ⊆ q.lebrefs ++ (v × vtblpnum), vols[v][vtblpnum] = unmapped → id(apebs0, apebs, mapped-pebs(vols)), vols[v][vtblpnum] ≠ unmapped → id(apebs0, apebs, mapped-pebs(vols) -- vols[v][vtblpnum].pnum) ⊦ abs(avols[v, avols[v][vtblpnum, mapped(subarray(buf, 0, n) + mkempbuf(n2), n)]], apebs0, vols[v, vols[v][vtblpnum, ⌜n0⌝ ]], q), abs(avols[v, avols[v][vtblpnum, mapped(subarray(buf, 0, n) + mkempbuf(n2), n)]], apebs0, vols[v, vols[v][vtblpnum, ⌜n0⌝ ]], q0), VTBL_VOLID ∈ vols, abs○(avols[v, avols[v][vtblpnum, mapped(subarray(buf, 0, n) + mkempbuf(n2), n)]], apebs0, vols[v, vols[v][vtblpnum, ⌜n0⌝ ]], q, v, vtblpnum) ∧ align↑(datasize(buf, n), EB_PAGE_SIZE) ≤ n

Rule argument

Additional information

Used simplifier rules: ⊦ mkpeb(aehdr, avhdr, buf, m, boolvar).fill = m; (s)%append-a: ⊦ (buf + buf0) + buf1 = buf + buf0 + buf1; from specification array-splice[buffer]% ⊦ buf + buf0 = buf + buf1 ↔ buf0 = buf1; (s)% ⊦ mkpeb(aehdr, avhdr, buf, m, boolvar).data = buf; (s)% ⊦ ⌜m⌝ = ⌜m0⌝ ↔ m = m0; (s)% ⊦ m < # ebatbl → ebatbl[m, ebae][m] = ebae; (s)% ⊦ m < # evol → evol[m, leb][m] = leb; (s)% ⊦ avols[v, evol][v] = evol; (s)%⊦ v ∈ avols ∧ m < # avols[v] ∧ abs(avols, apebs, vols, q) → m < # vols[v]; (ss)% ⊦ # ebatbl[n, ebae] = # ebatbl; (s)% ⊦ vols[v, ebatbl][v] = ebatbl; (s)% ⊦ v ∈ vols[v, ebatbl]; (s)