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

# wlar0 = n1 + vtblpnum1, # apebs = n1 + vtblpnum1, avhdr.sqn = valid-sqns(v, m1, apebs, vtblpnum1).max, apebs[vtblpnum1] = mkpeb(aechdr(m), avidhdr(v, m1, m2, m3, checksum(buf1, m3)), buf1, m0, false), recs[v × m1] = recovery-entry(m4, avhdr.sqn), apebs[m4] = mkpeb(aehdr, avhdr, buf, m5, boolvar), wlar0[m4] = wl-entry(m6, stat), m4 < vtblpnum1, nx < vtblpnum1, avhdr.sqn < m2, m4 < n1 + vtblpnum1, m4 + 1 < n1 + vtblpnum1, bflipset-cons(bflipset0, subarray(wlar0, 0, vtblpnum1)), 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, m3, checksum(buf1, m3)), buf1, m0, false)), unique-sqns(apebs), valid-eraseq(subarray(wlar0, 0, vtblpnum1), q), valid-eraseq-stronger(subarray(apebs, 0, vtblpnum1), q), valid-global-sqn(subarray(apebs, 0, vtblpnum1), sqnum), valid-peb(v, m1, mkpeb(aehdr, avhdr, buf, m5, boolvar)), valid-peb(v, m1, mkpeb(aechdr(m), avidhdr(v, m1, m2, m3, checksum(buf1, m3)), buf1, m0, false)), valid-peb(mkpeb(aechdr(m), avidhdr(v, m1, m2, m3, checksum(buf1, m3)), buf1, m0, false)), valid-recs(subarray(apebs, 0, vtblpnum1), subarray(wlar0, 0, vtblpnum1), recs), valid-recs-sqns(apebs, recs), valid-wl(subarray(apebs, 0, vtblpnum1), subarray(wlar0, 0, vtblpnum1)), v × m1 ∈ recs, m3 ≤ LEB_SIZE, m3 ≤ datasize(buf1), bitflips0 ∨ bitflips ⊦ m3 = 0, n1 = 0, dups(nx), m4 ∈ q, indices-erasing(wlar0[vtblpnum1, wl-entry(m, used)][m4, wl-entry(m6, erasing)], nx) ∧ valid-wl(subarray(apebs, 0, vtblpnum1 + 1), subarray(wlar0[vtblpnum1, wl-entry(m, used)][m4, wl-entry(m6, erasing)], 0, vtblpnum1 + 1)) ∧ valid-recs-sqns(apebs, recs[v × m1, recovery-entry(vtblpnum1, m2)])

User applied rule insert rewrite lemma

And obtained the following new goals

Proof step 157:
m < # apebs, # apebs = # wlar, m0 < m ⊦ valid-wl(subarray(apebs, 0, m), subarray(wlar, 0, m)) ∧ valid-peb(v, n, apebs[m]) ∧ valid-peb(v, n, apebs[m0]) ∧ apebs[m0].vidhdr.sqn = valid-sqns(v, n, apebs, m).max ∧ apebs[m].vidhdr.sqn > apebs[m0].vidhdr.sqn ∧ unique-sqns(apebs) ∧ apebs[m].echdr.ec = m2 → valid-wl(subarray(apebs, 0, m + 1), subarray(wlar[m, wl-entry(m2, used)][m0, wl-entry(m1, erasing)], 0, m + 1))
Proof step 158:
# apebs = n1 + vtblpnum1, # wlar0 = n1 + vtblpnum1, # apebs = # wlar0, apebs[vtblpnum1].echdr.ec = m, avhdr.sqn = valid-sqns(v, m1, apebs, vtblpnum1).max, apebs[m4].vidhdr.sqn = valid-sqns(v, m1, apebs, vtblpnum1).max, wlar0[m4] = wl-entry(m6, stat), apebs[m4] = mkpeb(aehdr, avhdr, buf, m5, boolvar), recs[v × m1] = recovery-entry(m4, avhdr.sqn), apebs[vtblpnum1] = mkpeb(aechdr(m), avidhdr(v, m1, m2, m3, checksum(buf1, m3)), buf1, m0, false), m4 + 1 < n1 + vtblpnum1, m4 < n1 + vtblpnum1, avhdr.sqn < m2, nx < vtblpnum1, vtblpnum1 < # apebs, m4 < vtblpnum1, apebs[vtblpnum1].vidhdr.sqn > apebs[m4].vidhdr.sqn, bflipset-cons(bflipset0, subarray(wlar0, 0, vtblpnum1)), indices-erasing(wlar0, nx), ubi-io-inv(apebs), ubi-io-peb-inv(mkpeb(aechdr(m), avidhdr(v, m1, m2, m3, checksum(buf1, m3)), buf1, m0, false)), ubi-io-peb-inv(mkpeb(aehdr, avhdr, buf, m5, boolvar)), unique-sqns(apebs), valid-eraseq(subarray(wlar0, 0, vtblpnum1), q), valid-eraseq-stronger(subarray(apebs, 0, vtblpnum1), q), valid-global-sqn(subarray(apebs, 0, vtblpnum1), sqnum), valid-peb(mkpeb(aechdr(m), avidhdr(v, m1, m2, m3, checksum(buf1, m3)), buf1, m0, false)), valid-peb(v, m1, mkpeb(aechdr(m), avidhdr(v, m1, m2, m3, checksum(buf1, m3)), buf1, m0, false)), valid-peb(v, m1, mkpeb(aehdr, avhdr, buf, m5, boolvar)), valid-peb(v, m1, apebs[vtblpnum1]), valid-peb(v, m1, apebs[m4]), valid-recs(subarray(apebs, 0, vtblpnum1), subarray(wlar0, 0, vtblpnum1), recs), valid-recs-sqns(apebs, recs), valid-wl(subarray(apebs, 0, vtblpnum1), subarray(wlar0, 0, vtblpnum1)), v × m1 ∈ recs, m3 ≤ datasize(buf1), m3 ≤ LEB_SIZE, bitflips0 ∨ bitflips ⊦ m3 = 0, n1 = 0, dups(nx), m4 ∈ q, indices-erasing(wlar0[vtblpnum1, wl-entry(m, used)][m4, wl-entry(m6, erasing)], nx) ∧ true ∧ valid-recs-sqns(apebs, recs[v × m1, recovery-entry(vtblpnum1, m2)])

Rule argument

spec: ubi-base name: valid-wl-next-valid-update seq: m < # apebs, # apebs = # wlar, m0 < m ⊦ valid-wl(subarray(apebs, 0, m), subarray(wlar, 0, m)) ∧ valid-peb(v, n, apebs[m]) ∧ valid-peb(v, n, apebs[m0]) ∧ apebs[m0].vidhdr.sqn = valid-sqns(v, n, apebs, m).max ∧ apebs[m].vidhdr.sqn > apebs[m0].vidhdr.sqn ∧ unique-sqns(apebs) ∧ apebs[m].echdr.ec = m2 → valid-wl (subarray(apebs, 0, m + 1), subarray (wlar[m, wl-entry(m2, used)][m0, wl-entry(m1, erasing)], 0, m + 1)) subst: [v, n, m1, m0, m2, wlar, m, apebs] → [v, m1, m6, m4, m, wlar0, vtblpnum1, apebs] flags: <all paths>

Additional information

Used simplifier rules: ⊦ m > n ↔ n < m; (s)% ⊦ m < m + n ↔ n ≠ 0; (s)%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic%c: ⊦ m + n = n + m; from specification nat-basic%⊦ valid-peb(v0, m0, apeb) → (valid-peb(v1, m1, apeb) ↔ v0 = v1 ∧ m0 = m1); (s)% ⊦ mkpeb(aehdr, avhdr, buf, m, boolvar).vidhdr = avhdr; (s)% ⊦ avidhdr(v, m, m0, m1, m2).sqn = m0; (s)% ⊦ mkpeb(aehdr, avhdr, buf, m, boolvar).echdr = aehdr; (s)% ⊦ aechdr(m).ec = m; (s) Used terms: v, m1, m6, m4, m, wlar0, vtblpnum1, apebs