[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 360 from proof prepost-scan-all (previous step)

# apebs = n0 + vtblpnum, # wlar0 = n0 + vtblpnum, avhdr.sqn = valid-sqns(v, m1, apebs, vtblpnum).max, apebs[vtblpnum] = mkpeb(aechdr(m), avidhdr(v, m1, m2, 0, m4), buf1, m0, false), recs[v × m1] = recovery-entry(m3, avhdr.sqn), apebs[m3] = mkpeb(aehdr, avhdr, buf, m5, boolvar), wlar0[m3] = wl-entry(m6, stat), m3 < n0 + vtblpnum, m3 < vtblpnum, nx < vtblpnum, bflipset-cons(bflipset0, subarray(wlar0, 0, vtblpnum)), indices-erasing(wlar0, nx), ubi-io-inv(apebs), ubi-io-peb-inv(mkpeb(aehdr, avhdr, buf, m5, boolvar)), ubi-io-peb-inv(mkpeb(aechdr(m), avidhdr(v, m1, m2, 0, m4), buf1, m0, false)), unique-sqns(apebs), valid-eraseq(subarray(wlar0, 0, vtblpnum), q), valid-eraseq-stronger(subarray(apebs, 0, vtblpnum), q), valid-global-sqn(subarray(apebs, 0, vtblpnum), sqnum), valid-peb(mkpeb(aechdr(m), avidhdr(v, m1, m2, 0, m4), buf1, m0, false)), valid-peb(v, m1, mkpeb(aehdr, avhdr, buf, m5, boolvar)), valid-recs(subarray(apebs, 0, vtblpnum), subarray(wlar0, 0, vtblpnum), recs), valid-recs-sqns(apebs, recs), valid-wl(subarray(apebs, 0, vtblpnum), subarray(wlar0, 0, vtblpnum)), v × m1 ∈ recs, avhdr.sqn ≤ m2 ⊦ n0 = 0, dups(nx), m3 ∈ q, indices-erasing(wlar0[vtblpnum, wl-entry(m, used)][m3, wl-entry(m6, erasing)], nx) ∧ valid-eraseq-stronger(subarray(apebs, 0, vtblpnum + 1), q + eq-entry(m3, v × m1) ') ∧ valid-wl(subarray(apebs, 0, vtblpnum + 1), subarray(wlar0[vtblpnum, wl-entry(m, used)][m3, wl-entry(m6, erasing)], 0, vtblpnum + 1)) ∧ valid-recs-sqns(apebs, recs[v × m1, recovery-entry(vtblpnum, m2)])

User applied rule insert rewrite lemma

And obtained the following new goals

Proof step 361:
m < # apebs, m0 < m ⊦ valid-eraseq-stronger(subarray(apebs, 0, m), q) ∧ valid-peb(v, n, apebs[m]) ∧ valid-sqns(v, n, apebs, m).max < apebs[m].vidhdr.sqn ∧ valid-peb(v, n, apebs[m0]) ∧ ¬ m0 ∈ q → valid-eraseq-stronger(subarray(apebs, 0, m + 1), q + eq-entry(m0, v × n) ')
Proof step 362:
# wlar0 = n0 + vtblpnum, # apebs = n0 + vtblpnum, avhdr.sqn = valid-sqns(v, m1, apebs, vtblpnum).max, wlar0[m3] = wl-entry(m6, stat), apebs[m3] = mkpeb(aehdr, avhdr, buf, m5, boolvar), recs[v × m1] = recovery-entry(m3, avhdr.sqn), apebs[vtblpnum] = mkpeb(aechdr(m), avidhdr(v, m1, m2, 0, m4), buf1, m0, false), nx < vtblpnum, m3 < vtblpnum, m3 < n0 + vtblpnum, bflipset-cons(bflipset0, subarray(wlar0, 0, vtblpnum)), indices-erasing(wlar0, nx), ubi-io-inv(apebs), ubi-io-peb-inv(mkpeb(aechdr(m), avidhdr(v, m1, m2, 0, m4), buf1, m0, false)), ubi-io-peb-inv(mkpeb(aehdr, avhdr, buf, m5, boolvar)), unique-sqns(apebs), valid-eraseq(subarray(wlar0, 0, vtblpnum), q), valid-eraseq-stronger(subarray(apebs, 0, vtblpnum), q), valid-global-sqn(subarray(apebs, 0, vtblpnum), sqnum), valid-peb(v, m1, mkpeb(aehdr, avhdr, buf, m5, boolvar)), valid-peb(mkpeb(aechdr(m), avidhdr(v, m1, m2, 0, m4), buf1, m0, false)), valid-recs(subarray(apebs, 0, vtblpnum), subarray(wlar0, 0, vtblpnum), recs), valid-recs-sqns(apebs, recs), valid-wl(subarray(apebs, 0, vtblpnum), subarray(wlar0, 0, vtblpnum)), v × m1 ∈ recs, avhdr.sqn ≤ m2 ⊦ n0 = 0, dups(nx), m3 ∈ q, indices-erasing(wlar0[vtblpnum, wl-entry(m, used)][m3, wl-entry(m6, erasing)], nx) ∧ valid-eraseq-stronger(subarray(apebs, 0, vtblpnum + 1), q + eq-entry(m3, v × m1) ') ∧ valid-wl(subarray(apebs, 0, vtblpnum + 1), subarray(wlar0[vtblpnum, wl-entry(m, used)][m3, wl-entry(m6, erasing)], 0, vtblpnum + 1)) ∧ valid-recs-sqns(apebs, recs[v × m1, recovery-entry(vtblpnum, m2)]), vtblpnum < # apebs ∧ m3 < vtblpnum ∧ valid-eraseq-stronger(subarray(apebs, 0, vtblpnum), q) ∧ valid-peb(v, m1, apebs[vtblpnum]) ∧ valid-sqns(v, m1, apebs, vtblpnum).max < apebs[vtblpnum].vidhdr.sqn ∧ valid-peb(v, m1, apebs[m3]) ∧ ¬ m3 ∈ q
Proof step 365:
# wlar0 = n0 + vtblpnum, # apebs = n0 + vtblpnum, avhdr.sqn = valid-sqns(v, m1, apebs, vtblpnum).max, wlar0[m3] = wl-entry(m6, stat), apebs[m3] = mkpeb(aehdr, avhdr, buf, m5, boolvar), recs[v × m1] = recovery-entry(m3, avhdr.sqn), apebs[vtblpnum] = mkpeb(aechdr(m), avidhdr(v, m1, m2, 0, m4), buf1, m0, false), nx < vtblpnum, m3 < n0 + vtblpnum, vtblpnum < # apebs, m3 < vtblpnum, valid-sqns(v, m1, apebs, vtblpnum).max < apebs[vtblpnum].vidhdr.sqn, bflipset-cons(bflipset0, subarray(wlar0, 0, vtblpnum)), indices-erasing(wlar0, nx), ubi-io-inv(apebs), ubi-io-peb-inv(mkpeb(aechdr(m), avidhdr(v, m1, m2, 0, m4), buf1, m0, false)), ubi-io-peb-inv(mkpeb(aehdr, avhdr, buf, m5, boolvar)), unique-sqns(apebs), valid-eraseq(subarray(wlar0, 0, vtblpnum), q), valid-eraseq-stronger(subarray(apebs, 0, vtblpnum), q), valid-global-sqn(subarray(apebs, 0, vtblpnum), sqnum), valid-peb(v, m1, mkpeb(aehdr, avhdr, buf, m5, boolvar)), valid-peb(mkpeb(aechdr(m), avidhdr(v, m1, m2, 0, m4), buf1, m0, false)), valid-peb(v, m1, apebs[vtblpnum]), valid-peb(v, m1, apebs[m3]), valid-recs(subarray(apebs, 0, vtblpnum), subarray(wlar0, 0, vtblpnum), recs), valid-recs-sqns(apebs, recs), valid-wl(subarray(apebs, 0, vtblpnum), subarray(wlar0, 0, vtblpnum)), v × m1 ∈ recs, avhdr.sqn ≤ m2 ⊦ n0 = 0, dups(nx), m3 ∈ q, indices-erasing(wlar0[vtblpnum, wl-entry(m, used)][m3, wl-entry(m6, erasing)], nx) ∧ true ∧ valid-wl(subarray(apebs, 0, vtblpnum + 1), subarray(wlar0[vtblpnum, wl-entry(m, used)][m3, wl-entry(m6, erasing)], 0, vtblpnum + 1)) ∧ valid-recs-sqns(apebs, recs[v × m1, recovery-entry(vtblpnum, m2)])

Rule argument

spec: ubi-crash-recovery-base name: valid-eraseq-stronger-prev-append-lref seq: m < # apebs, m0 < m ⊦ valid-eraseq-stronger(subarray(apebs, 0, m), q) ∧ valid-peb(v, n, apebs[m]) ∧ valid-sqns(v, n, apebs, m).max < apebs[m].vidhdr.sqn ∧ valid-peb(v, n, apebs[m0]) ∧ ¬ m0 ∈ q → valid-eraseq-stronger (subarray(apebs, 0, m + 1), q + eq-entry(m0, v × n) ') subst: [n, v, m0, q, m, apebs] → [m1, v, m3, q, vtblpnum, apebs] flags: <all paths>

Additional information

Used terms: m1, v, m3, q, vtblpnum, apebs