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

# apebs = n1 + vtblpnum1, # wlar0 = n1 + vtblpnum1, avhdr.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), nx < vtblpnum1, m4 < vtblpnum1, m4 < n1 + vtblpnum1, 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(v, m1, mkpeb(aehdr, avhdr, buf, m5, boolvar)), 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), avhdr.sqn ≤ m2, m3 ≤ LEB_SIZE, bitflips0 ∨ bitflips ⊦ m3 = 0, n1 = 0, dups(nx), valid-peb(v, m1, mkpeb(aechdr(m), avidhdr(v, m1, m2, m3, checksum(buf1, m3)), buf1, m0, false)), m4 ∈ q, indices-erasing(wlar0[vtblpnum1, wl-entry(m, used)][m4, wl-entry(m6, erasing)], nx) ∧ valid-global-sqn(subarray(apebs, 0, vtblpnum1 + 1), max(sqnum, m2 + 1)) ∧ valid-eraseq-stronger(subarray(apebs, 0, vtblpnum1 + 1), q + eq-entry(m4, v × m1) ') ∧ 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 165:
⊦ valid-peb(v, m, apeb) ↔ ¬ apeb.bad ∧ apeb.echdr.valid? ∧ (∃ m0, m1, m2. apeb.vidhdr = avidhdr(v, m, m0, m1, m2) ∧ (m1 ≠ 0 → m1 ≤ datasize(apeb.data) ∧ m2 = checksum(apeb.data, m1)))
Proof step 166:
# 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 < n1 + vtblpnum1, m4 < vtblpnum1, nx < 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-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, avhdr.sqn ≤ m2, 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-global-sqn(subarray(apebs, 0, vtblpnum1 + 1), max(sqnum, m2 + 1)) ∧ valid-eraseq-stronger(subarray(apebs, 0, vtblpnum1 + 1), q + eq-entry(m4, v × m1) ') ∧ 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)]), ¬ mkpeb(aechdr(m), avidhdr(v, m1, m2, m3, checksum(buf1, m3)), buf1, m0, false).bad ∧ mkpeb(aechdr(m), avidhdr(v, m1, m2, m3, checksum(buf1, m3)), buf1, m0, false).echdr.valid? ∧ (∃ m6, m4, m5. mkpeb(aechdr(m), avidhdr(v, m1, m2, m3, checksum(buf1, m3)), buf1, m0, false).vidhdr = avidhdr(v, m1, m6, m4, m5) ∧ ( m4 ≠ 0 → m4 ≤ datasize(mkpeb(aechdr(m), avidhdr(v, m1, m2, m3, checksum(buf1, m3)), buf1, m0, false).data) ∧ m5 = checksum(mkpeb(aechdr(m), avidhdr(v, m1, m2, m3, checksum(buf1, m3)), buf1, m0, false).data, m4)))

Rule argument

spec: valid-peb name: valid-peb2 seq: ⊦ valid-peb(v, m, apeb) ↔ ¬ apeb.bad ∧ apeb.echdr.valid? ∧ (∃ m0, m1, m2. apeb.vidhdr = avidhdr(v, m, m0, m1, m2) ∧ ( m1 ≠ 0 → m1 ≤ datasize(apeb.data) ∧ m2 = checksum(apeb.data, m1))) subst: [apeb, m, v] → [mkpeb (aechdr(m), avidhdr(v, m1, m2, m3, checksum(buf1, m3)), buf1, m0, false), m1, v] flags: <all paths>

Additional information

Used terms: mkpeb (aechdr(m), avidhdr(v, m1, m2, m3, checksum(buf1, m3)), buf1, m0, false), m1, v