[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 109 from proof refine-write-data (previous step)

LEB_SIZE = (n1 + n3) + m1, pebs[m3] = mkpeb(buf1, 2 * EB_PAGE_SIZE + m2, false), apebs[m3] = mkpeb(aehdr, avhdr, buf0, m2, false), aehdr.valid?, avhdr.valid?, m3 < # pebs, m3 < # apebs, n3 < n, abs(pebs, apebs), abs-peb(mkpeb(buf1, 2 * EB_PAGE_SIZE + m2, false), mkpeb(aehdr, avhdr, buf0, m2, false)), is-aligned(n3, EB_PAGE_SIZE), is-aligned(n, EB_PAGE_SIZE), is-aligned(m1, EB_PAGE_SIZE), mtd-cons(pebs), ubi-io-inv(apebs), m2 ≤ m1, (m1 + 2 * EB_PAGE_SIZE) + n3 ≤ PEB_SIZE, n0 + n ≤ # buf, m1 + n ≤ LEB_SIZE, n0 + n3 ≤ # buf, m2 ≤ LEB_SIZE, m1 ≤ LEB_SIZE, n3 + m1 ≤ LEB_SIZE, ⌊err1⌋ ⊦ n3 = 0, abs-peb (mkpeb(copy(buf, n0, buf1, m1 + 2 * EB_PAGE_SIZE, n3), (m1 + 2 * EB_PAGE_SIZE) + n3, false), mkpeb(aehdr, avhdr, subarray(buf0, 0, m1) + subarray(buf, n0, n3) + mkempbuf(n1), m1 + n3, false))

User applied rule insert rewrite lemma

And obtained the following new goals

Proof step 110:
⊦ abs-peb(peb, apeb) ↔ (peb.bad ↔ apeb.bad) ∧ ( ¬ peb.bad → peb.fill = (apeb.echdr = empty ⊃ 0;(apeb.vidhdr = empty ⊃ EB_PAGE_SIZE;apeb.fill + 2 * EB_PAGE_SIZE)) ∧ abs-echdr(subarray(peb.data, 0, EB_PAGE_SIZE), apeb.echdr) ∧ abs-vidhdr(subarray(peb.data, EB_PAGE_SIZE, EB_PAGE_SIZE), apeb.vidhdr) ∧ subarray(peb.data, 2 * EB_PAGE_SIZE, LEB_SIZE) = apeb.data)
Proof step 111:
LEB_SIZE = (n1 + n3) + m1, apebs[m3] = mkpeb(aehdr, avhdr, buf0, m2, false), pebs[m3] = mkpeb(buf1, 2 * EB_PAGE_SIZE + m2, false), avhdr.valid?, aehdr.valid?, n3 < n, m3 < # apebs, m3 < # pebs, abs(pebs, apebs), abs-peb(mkpeb(buf1, 2 * EB_PAGE_SIZE + m2, false), mkpeb(aehdr, avhdr, buf0, m2, false)), is-aligned(m1, EB_PAGE_SIZE), is-aligned(n, EB_PAGE_SIZE), is-aligned(n3, EB_PAGE_SIZE), mtd-cons(pebs), ubi-io-inv(apebs), n3 + m1 ≤ LEB_SIZE, m1 ≤ LEB_SIZE, m2 ≤ LEB_SIZE, n0 + n3 ≤ # buf, m1 + n ≤ LEB_SIZE, n0 + n ≤ # buf, (m1 + 2 * EB_PAGE_SIZE) + n3 ≤ PEB_SIZE, m2 ≤ m1, ⌊err1⌋ ⊦ n3 = 0, ( mkpeb(copy(buf, n0, buf1, m1 + 2 * EB_PAGE_SIZE, n3), (m1 + 2 * EB_PAGE_SIZE) + n3, false).bad ↔ mkpeb(aehdr, avhdr, subarray(buf0, 0, m1) + subarray(buf, n0, n3) + mkempbuf(n1), m1 + n3, false).bad) ∧ ( ¬ mkpeb(copy(buf, n0, buf1, m1 + 2 * EB_PAGE_SIZE, n3), (m1 + 2 * EB_PAGE_SIZE) + n3, false).bad → mkpeb(copy(buf, n0, buf1, m1 + 2 * EB_PAGE_SIZE, n3), (m1 + 2 * EB_PAGE_SIZE) + n3, false).fill = (mkpeb(aehdr, avhdr, subarray(buf0, 0, m1) + subarray(buf, n0, n3) + mkempbuf(n1), m1 + n3, false).echdr = empty ⊃ 0 ;(mkpeb(aehdr, avhdr, subarray(buf0, 0, m1) + subarray(buf, n0, n3) + mkempbuf(n1), m1 + n3, false).vidhdr = empty ⊃ EB_PAGE_SIZE ;mkpeb(aehdr, avhdr, subarray(buf0, 0, m1) + subarray(buf, n0, n3) + mkempbuf(n1), m1 + n3, false).fill + 2 * EB_PAGE_SIZE ) ) ∧ abs-echdr (subarray(mkpeb(copy(buf, n0, buf1, m1 + 2 * EB_PAGE_SIZE, n3), (m1 + 2 * EB_PAGE_SIZE) + n3, false).data, 0, EB_PAGE_SIZE), mkpeb(aehdr, avhdr, subarray(buf0, 0, m1) + subarray(buf, n0, n3) + mkempbuf(n1), m1 + n3, false).echdr) ∧ abs-vidhdr (subarray(mkpeb(copy(buf, n0, buf1, m1 + 2 * EB_PAGE_SIZE, n3), (m1 + 2 * EB_PAGE_SIZE) + n3, false).data, EB_PAGE_SIZE, EB_PAGE_SIZE), mkpeb(aehdr, avhdr, subarray(buf0, 0, m1) + subarray(buf, n0, n3) + mkempbuf(n1), m1 + n3, false).vidhdr) ∧ subarray(mkpeb(copy(buf, n0, buf1, m1 + 2 * EB_PAGE_SIZE, n3), (m1 + 2 * EB_PAGE_SIZE) + n3, false).data, 2 * EB_PAGE_SIZE, LEB_SIZE) = mkpeb(aehdr, avhdr, subarray(buf0, 0, m1) + subarray(buf, n0, n3) + mkempbuf(n1), m1 + n3, false).data)

Rule argument

spec: ubi-io-abs name: abs-peb seq: ⊦ abs-peb(peb, apeb) ↔ (peb.bad ↔ apeb.bad) ∧ ( ¬ peb.bad → peb.fill = (apeb.echdr = empty ⊃ 0 ;(apeb.vidhdr = empty ⊃ EB_PAGE_SIZE ;apeb.fill + 2 * EB_PAGE_SIZE ) ) ∧ abs-echdr (subarray(peb.data, 0, EB_PAGE_SIZE), apeb.echdr) ∧ abs-vidhdr (subarray(peb.data, EB_PAGE_SIZE, EB_PAGE_SIZE), apeb.vidhdr) ∧ subarray(peb.data, 2 * EB_PAGE_SIZE, LEB_SIZE) = apeb.data) subst: [apeb, peb] → [mkpeb (aehdr, avhdr, subarray(buf0, 0, m1) + subarray(buf, n0, n3) + mkempbuf(n1), m1 + n3, false), mkpeb (copy(buf, n0, buf1, m1 + 2 * EB_PAGE_SIZE, n3), (m1 + 2 * EB_PAGE_SIZE) + n3, false)] flags: <all paths>

Additional information

Used terms: mkpeb (aehdr, avhdr, subarray(buf0, 0, m1) + subarray(buf, n0, n3) + mkempbuf(n1), m1 + n3, false), mkpeb (copy(buf, n0, buf1, m1 + 2 * EB_PAGE_SIZE, n3), (m1 + 2 * EB_PAGE_SIZE) + n3, false)