[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 112 from proof prepost-write-once (previous step)

# apebs2 = # wlar0, # apebs0 = # wlar1, n2 + m1 = n + n0, q0.head = eq-entry(m4, lref0), LEB_SIZE = (n0 + n) + m0, LEB_SIZE = (n2 + m0) + m1, apebs2[vtblpnum1] = mkpeb(aehdr, empty, mkempbuf(LEB_SIZE), 0, false), wlar0[vtblpnum1] = wl-entry(m5, free), vols0[v][m] = unmapped, aehdr.valid?, m < # vols0[v], vtblpnum1 < # wlar0, n < m1, n < LEB_SIZE, bflipset-cons(bflipset, wlar0), bflipset-cons(bflipset, wlar1), id(apebs2, apebs0, mapped-pebs(vols0)), is-aligned(m0, EB_PAGE_SIZE), is-aligned(m1, EB_PAGE_SIZE), is-aligned(n, EB_PAGE_SIZE), ubi-io-inv(apebs2), ubi-io-inv(apebs0), ubi-io-inv(apebs2[vtblpnum1, mkpeb(aehdr, avidhdr(v, m, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false)]), ubi-io-inv(apebs2[vtblpnum1, mkpeb(aehdr, avidhdr(v, m, sqnum, 0, 0), mkempbuf(m0) + subarray(buf, m2, n) + mkempbuf(n0), m0 + n, false)]), unique-sqns(apebs2), unique-sqns(apebs0), valid-ebatbl(apebs2, wlar0, vols0, vtblpnum2), valid-ebatbl(apebs0, wlar1, vols0, vtblpnum2), valid-eraseq(q1 + eq-entry(vtblpnum1, v × m) '), valid-eraseq(apebs2, q1), valid-eraseq(wlar0, q1), valid-eraseq(q1), valid-eraseq(q0), valid-eraseq(wlar1, q0), valid-eraseq(apebs0, q0), valid-global-sqn(apebs2, sqnum), valid-global-sqn(apebs0, sqnum), valid-peb(mkpeb(aehdr, avidhdr(v, m, sqnum, 0, 0), mkempbuf(m0) + subarray(buf, m2, n) + mkempbuf(n0), m0 + n, false)), valid-vtbl(apebs2, vols0, wlar0, vtblpnum2), valid-vtbl(apebs0, vols0, wlar1, vtblpnum2), valid-wl(apebs2, wlar0), valid-wl(apebs0, wlar1), v ∈ vols0, m0 + m1 ≤ LEB_SIZE, m1 + m2 ≤ # buf, m1 ≤ LEB_SIZE, m2 + n ≤ # buf, m0 ≤ LEB_SIZE, n + m0 ≤ LEB_SIZE, q1.lebrefs ⊆ q0.lebrefs, ⌊err0⌋ , apebs0 = apebs2 ∧ wlar1 = wlar0 ∧ q0 = q1 ∨ id○(apebs0, apebs2, vtblpnum1) ∧ id○(wlar1, wlar0, vtblpnum1) ∧ q0 = eq-entry(vtblpnum1, lref0) ' + q1 ⊦ n0 + m0 = 0, n = 0, vtblpnum2 = vtblpnum1, valid-eraseq (apebs2[vtblpnum1, mkpeb(aehdr, avidhdr(v, m, sqnum, 0, 0), mkempbuf(m0) + subarray(buf, m2, n) + mkempbuf(n0), m0 + n, false)], q1 + eq-entry(vtblpnum1, v × m) '), vtblpnum2 ∈ q0, VTBL_VOLID ∈ vols0, vtblpnum2 ∈ q1

User applied rule insert rewrite lemma

And obtained the following new goals

Proof step 113:
⊦ valid-eraseq(apebs, q) → (valid-eraseq(apebs, q + eq-entry(n, lref) ') ↔ n < # apebs ∧ (valid-peb(apebs[n]) → lref = apebs[n].vidhdr.vol × apebs[n].vidhdr.leb))
Proof step 114:
# apebs0 = # wlar1, # apebs2 = # wlar0, n2 + m1 = n + n0, q0.head = eq-entry(m4, lref0), LEB_SIZE = (n2 + m0) + m1, LEB_SIZE = (n0 + n) + m0, vols0[v][m] = unmapped, wlar0[vtblpnum1] = wl-entry(m5, free), apebs2[vtblpnum1] = mkpeb(aehdr, empty, mkempbuf(LEB_SIZE), 0, false), aehdr.valid?, n < LEB_SIZE, n < m1, vtblpnum1 < # wlar0, m < # vols0[v], bflipset-cons(bflipset, wlar1), bflipset-cons(bflipset, wlar0), id(apebs2, apebs0, mapped-pebs(vols0)), is-aligned(n, EB_PAGE_SIZE), is-aligned(m1, EB_PAGE_SIZE), is-aligned(m0, EB_PAGE_SIZE), ubi-io-inv(apebs2[vtblpnum1, mkpeb(aehdr, avidhdr(v, m, sqnum, 0, 0), mkempbuf(m0) + subarray(buf, m2, n) + mkempbuf(n0), m0 + n, false)]), ubi-io-inv(apebs2[vtblpnum1, mkpeb(aehdr, avidhdr(v, m, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false)]), ubi-io-inv(apebs0), ubi-io-inv(apebs2), unique-sqns(apebs0), unique-sqns(apebs2), valid-ebatbl(apebs0, wlar1, vols0, vtblpnum2), valid-ebatbl(apebs2, wlar0, vols0, vtblpnum2), valid-eraseq(apebs0, q0), valid-eraseq(wlar1, q0), valid-eraseq(q0), valid-eraseq(q1), valid-eraseq(wlar0, q1), valid-eraseq(apebs2, q1), valid-eraseq(q1 + eq-entry(vtblpnum1, v × m) '), valid-global-sqn(apebs0, sqnum), valid-global-sqn(apebs2, sqnum), valid-peb(mkpeb(aehdr, avidhdr(v, m, sqnum, 0, 0), mkempbuf(m0) + subarray(buf, m2, n) + mkempbuf(n0), m0 + n, false)), valid-vtbl(apebs0, vols0, wlar1, vtblpnum2), valid-vtbl(apebs2, vols0, wlar0, vtblpnum2), valid-wl(apebs0, wlar1), valid-wl(apebs2, wlar0), v ∈ vols0, n + m0 ≤ LEB_SIZE, m0 ≤ LEB_SIZE, m2 + n ≤ # buf, m1 ≤ LEB_SIZE, m1 + m2 ≤ # buf, m0 + m1 ≤ LEB_SIZE, q1.lebrefs ⊆ q0.lebrefs, ⌊err0⌋ , apebs0 = apebs2 ∧ wlar1 = wlar0 ∧ q0 = q1 ∨ id○(apebs0, apebs2, vtblpnum1) ∧ id○(wlar1, wlar0, vtblpnum1) ∧ q0 = eq-entry(vtblpnum1, lref0) ' + q1 ⊦ n0 + m0 = 0, n = 0, vtblpnum2 = vtblpnum1, valid-eraseq (apebs2[vtblpnum1, mkpeb(aehdr, avidhdr(v, m, sqnum, 0, 0), mkempbuf(m0) + subarray(buf, m2, n) + mkempbuf(n0), m0 + n, false)], q1 + eq-entry(vtblpnum1, v × m) '), valid-eraseq(apebs2[vtblpnum1, mkpeb(aehdr, avidhdr(v, m, sqnum, 0, 0), mkempbuf(m0) + subarray(buf, m2, n) + mkempbuf(n0), m0 + n, false)], q1), vtblpnum2 ∈ q1, VTBL_VOLID ∈ vols0, vtblpnum2 ∈ q0

Rule argument

spec: ubi-base name: valid-eraseqp-append seq: ⊦ valid-eraseq(apebs, q) → ( valid-eraseq(apebs, q + eq-entry(n, lref) ') ↔ n < # apebs ∧ ( valid-peb(apebs[n]) → lref = apebs[n].vidhdr.vol × apebs[n].vidhdr.leb)) subst: [lref, n, q, apebs] → [v × m, vtblpnum1, q1, apebs2 [vtblpnum1, mkpeb (aehdr, avidhdr(v, m, sqnum, 0, 0), mkempbuf(m0) + subarray(buf, m2, n) + mkempbuf(n0), m0 + n, false) ]] flags: <all paths>

Additional information

Used simplifier rules: ls-array-append-length0: # buf0 = 0 ⊦ buf + buf0 = buf;% ⊦ # apebs[n, apeb] = # apebs; (s)% ⊦ # mkempbuf(n) = n; (s)% ⊦ m < # apebs → apebs[m, apeb][m] = apeb; (s)% ⊦ mkpeb(aehdr, avhdr, buf, m, boolvar).vidhdr = avhdr; (s)% ⊦ avidhdr(v, m, m0, m1, m2).vol = v; (s)% ⊦ avidhdr(v, m, m0, m1, m2).leb = m; (s)%append-a: ⊦ (buf + buf0) + buf1 = buf + buf0 + buf1; from specification array-splice[buffer]% ⊦ m < n ↔ ¬ n ≤ m; (ss)%fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat%fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat% ⊦ ¬ n < n; (s) Used terms: v × m, vtblpnum1, q1, apebs2 [vtblpnum1, mkpeb (aehdr, avidhdr(v, m, sqnum, 0, 0), mkempbuf(m0) + subarray(buf, m2, n) + mkempbuf(n0), m0 + n, false) ]