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

⟨ebm_change#(v, vtblpnum3, vtblpnum5 + n5, subarray(buf2, 0, vtblpnum5) + subarray(buf, n3, n5); avols0; err1)⟩ (avols0 = avols1 ∧ err1 = err2), # apebs0 = # wlar, LEB_SIZE = (n + n2) + vtblpnum5, vols[v][vtblpnum3] = ⌜n4⌝ , avols[v][vtblpnum3] = mapped(buf2, m), wlar[n4] = wl-entry(m1, used), apebs0[n4] = mkpeb(aehdr, avhdr, buf2, m0, false), avols0 = avols[v, avols[v][vtblpnum3, mapped(subarray(buf2, 0, vtblpnum5) + subarray(buf, n3, n2) + mkempbuf(n), vtblpnum5 + n2)]], aehdr.valid?, avhdr.valid?, n2 < n5, vtblpnum3 < # vols[v], vtblpnum3 < # avols[v], n4 < # wlar, abs(avols1, apebs1, vols0, q0), abs (avols[v, avols[v][vtblpnum3, mapped(subarray(buf2, 0, vtblpnum5) + subarray(buf, n3, n2) + mkempbuf(n), vtblpnum5 + n2)]], apebs0[n4, mkpeb(aehdr, avhdr, subarray(buf2, 0, vtblpnum5) + subarray(buf, n3, n2) + mkempbuf(n), vtblpnum5 + n2, false)], vols, q), abs(avols, apebs0, vols, q), bflipset-cons(bflipset, wlar), ebm-cons(avols[v, avols[v][vtblpnum3, mapped(subarray(buf2, 0, vtblpnum5) + subarray(buf, n3, n2) + mkempbuf(n), vtblpnum5 + n2)]]), ebm-cons(avols), is-aligned(vtblpnum5, EB_PAGE_SIZE), is-aligned(n5, EB_PAGE_SIZE), is-aligned(n2, EB_PAGE_SIZE), ubi-io-inv(apebs0[n4, mkpeb(aehdr, avhdr, subarray(buf2, 0, vtblpnum5) + subarray(buf, n3, n2) + mkempbuf(n), vtblpnum5 + n2, false)]), ubi-io-inv(apebs0), ubi-io-peb-inv(mkpeb(aehdr, avhdr, buf2, m0, false)), unique-sqns(apebs0), unique-sqns(apebs0[n4, mkpeb(aehdr, avhdr, subarray(buf2, 0, vtblpnum5) + subarray(buf, n3, n2) + mkempbuf(n), vtblpnum5 + n2, false)]), valid-ebatbl(apebs0, wlar, vols, vtblpnum4), valid-ebatbl (apebs0[n4, mkpeb(aehdr, avhdr, subarray(buf2, 0, vtblpnum5) + subarray(buf, n3, n2) + mkempbuf(n), vtblpnum5 + n2, false)], wlar, vols, vtblpnum4), valid-eraseq(q), valid-eraseq(wlar, q), valid-eraseq(apebs0, q), valid-eraseq(apebs0[n4, mkpeb(aehdr, avhdr, subarray(buf2, 0, vtblpnum5) + subarray(buf, n3, n2) + mkempbuf(n), vtblpnum5 + n2, false)], q), valid-global-sqn(apebs0, sqnum), valid-global-sqn(apebs0[n4, mkpeb(aehdr, avhdr, subarray(buf2, 0, vtblpnum5) + subarray(buf, n3, n2) + mkempbuf(n), vtblpnum5 + n2, false)], sqnum), valid-vtbl(apebs0, vols, wlar, vtblpnum4), valid-wl(apebs0, wlar), valid-wl(apebs0[n4, mkpeb(aehdr, avhdr, subarray(buf2, 0, vtblpnum5) + subarray(buf, n3, n2) + mkempbuf(n), vtblpnum5 + n2, false)], wlar), v ∈ vols, v ∈ avols, n3 + n2 ≤ # buf, vtblpnum5 + n5 ≤ LEB_SIZE, n5 + n3 ≤ # buf, m ≤ vtblpnum5, m0 ≤ vtblpnum5, n2 + vtblpnum5 ≤ LEB_SIZE, m ≤ LEB_SIZE, m0 ≤ LEB_SIZE, n3 + n5 ≤ # buf, vtblpnum5 ≤ LEB_SIZE, ⌊err3⌋ ⊦ ∃ err0. (⌊err0⌋ ∨ err0 = ESUCCESS) ∧ ⟨err := err0; if err = ESUCCESS then if avols[v][vtblpnum3].mapped? then if n5 ≠ 0 then avols[v][vtblpnum3] := mapped (subarray(avols[v][vtblpnum3].data, 0, vtblpnum5) + subarray(buf, n3, n5) + mkempbuf(LEB_SIZE - vtblpnum5 - n5), vtblpnum5 + n5) else avols[v][vtblpnum3] := mapped(mkempbuf(vtblpnum5) + subarray(buf, n3, n5) + mkempbuf(LEB_SIZE - vtblpnum5 - n5), vtblpnum5 + n5) else if avols[v][vtblpnum3].mapped? then choose n with n < n5 ∧ is-aligned(n, EB_PAGE_SIZE) in if n ≠ 0 then avols[v][vtblpnum3] := mapped (subarray(avols[v][vtblpnum3].data, 0, vtblpnum5) + subarray(buf, n3, n) + mkempbuf(LEB_SIZE - vtblpnum5 - n), vtblpnum5 + n) ifnone skip else if n5 ≠ 0 then avols[v][vtblpnum3] := unmapped⟩ (abs(avols, apebs1, vols0, q0) ∧ err2 = err), n2 = 0, vtblpnum4 = n4, VTBL_VOLID ∈ vols

Heuristic nonrecursive calls applied rule call left

And obtained the following new goals

Proof step 190:
⟨if v ∈ avols ∧ vtblpnum < # avols[v] ∧ n ≤ LEB_SIZE ∧ n ≤ # buf ∧ is-aligned(n, EB_PAGE_SIZE) then {fail_or_success#(; ; err); if err = ESUCCESS then avols[v][vtblpnum] := mapped(subarray(buf, 0, n) + mkempbuf(LEB_SIZE - n), n)} else abort⟩ (avols = avols1 ∧ err = err2), # apebs0 = # wlar, LEB_SIZE = (n0 + n2) + vtblpnum5, apebs0[n4] = mkpeb(aehdr, avhdr, buf2, m0, false), wlar[n4] = wl-entry(m1, used), avols2[v][vtblpnum3] = mapped(buf2, m), vols[v][vtblpnum3] = ⌜n4⌝ , avols = avols0, avols0 = avols2[v, avols2[v][vtblpnum3, mapped(subarray(buf2, 0, vtblpnum5) + subarray(buf0, n3, n2) + mkempbuf(n0), vtblpnum5 + n2)]], buf = subarray(buf2, 0, vtblpnum5) + subarray(buf0, n3, n5), n = vtblpnum5 + n5, vtblpnum = vtblpnum3, avhdr.valid?, aehdr.valid?, n4 < # wlar, vtblpnum3 < # avols2[v], vtblpnum3 < # vols[v], n2 < n5, abs(avols2, apebs0, vols, q), abs (avols2[v, avols2[v][vtblpnum3, mapped(subarray(buf2, 0, vtblpnum5) + subarray(buf0, n3, n2) + mkempbuf(n0), vtblpnum5 + n2)]], apebs0[n4, mkpeb(aehdr, avhdr, subarray(buf2, 0, vtblpnum5) + subarray(buf0, n3, n2) + mkempbuf(n0), vtblpnum5 + n2, false)], vols, q), abs(avols1, apebs1, vols0, q0), bflipset-cons(bflipset, wlar), ebm-cons(avols2), ebm-cons(avols2[v, avols2[v][vtblpnum3, mapped(subarray(buf2, 0, vtblpnum5) + subarray(buf0, n3, n2) + mkempbuf(n0), vtblpnum5 + n2)]]), is-aligned(n2, EB_PAGE_SIZE), is-aligned(n5, EB_PAGE_SIZE), is-aligned(vtblpnum5, EB_PAGE_SIZE), ubi-io-inv(apebs0), ubi-io-inv(apebs0[n4, mkpeb(aehdr, avhdr, subarray(buf2, 0, vtblpnum5) + subarray(buf0, n3, n2) + mkempbuf(n0), vtblpnum5 + n2, false)]), ubi-io-peb-inv(mkpeb(aehdr, avhdr, buf2, m0, false)), unique-sqns(apebs0[n4, mkpeb(aehdr, avhdr, subarray(buf2, 0, vtblpnum5) + subarray(buf0, n3, n2) + mkempbuf(n0), vtblpnum5 + n2, false)]), unique-sqns(apebs0), valid-ebatbl (apebs0[n4, mkpeb(aehdr, avhdr, subarray(buf2, 0, vtblpnum5) + subarray(buf0, n3, n2) + mkempbuf(n0), vtblpnum5 + n2, false)], wlar, vols, vtblpnum4), valid-ebatbl(apebs0, wlar, vols, vtblpnum4), valid-eraseq(apebs0[n4, mkpeb(aehdr, avhdr, subarray(buf2, 0, vtblpnum5) + subarray(buf0, n3, n2) + mkempbuf(n0), vtblpnum5 + n2, false)], q), valid-eraseq(apebs0, q), valid-eraseq(wlar, q), valid-eraseq(q), valid-global-sqn(apebs0[n4, mkpeb(aehdr, avhdr, subarray(buf2, 0, vtblpnum5) + subarray(buf0, n3, n2) + mkempbuf(n0), vtblpnum5 + n2, false)], sqnum), valid-global-sqn(apebs0, sqnum), valid-vtbl(apebs0, vols, wlar, vtblpnum4), valid-wl(apebs0[n4, mkpeb(aehdr, avhdr, subarray(buf2, 0, vtblpnum5) + subarray(buf0, n3, n2) + mkempbuf(n0), vtblpnum5 + n2, false)], wlar), valid-wl(apebs0, wlar), v ∈ avols2, v ∈ vols, vtblpnum5 ≤ LEB_SIZE, m0 ≤ LEB_SIZE, m ≤ LEB_SIZE, n2 + vtblpnum5 ≤ LEB_SIZE, m0 ≤ vtblpnum5, m ≤ vtblpnum5, n5 + n3 ≤ # buf0, vtblpnum5 + n5 ≤ LEB_SIZE, n3 + n2 ≤ # buf0, 0 + vtblpnum5 ≤ # buf2, n3 + n5 ≤ # buf0, ⌊err3⌋ ⊦ ∃ err0. (⌊err0⌋ ∨ err0 = ESUCCESS) ∧ ⟨err := err0; if err = ESUCCESS then if avols2[v][vtblpnum3].mapped? then if n5 ≠ 0 then avols2[v][vtblpnum3] := mapped (subarray(avols2[v][vtblpnum3].data, 0, vtblpnum5) + subarray(buf0, n3, n5) + mkempbuf(LEB_SIZE - vtblpnum5 - n5), vtblpnum5 + n5) else avols2[v][vtblpnum3] := mapped(mkempbuf(vtblpnum5) + subarray(buf0, n3, n5) + mkempbuf(LEB_SIZE - vtblpnum5 - n5), vtblpnum5 + n5) else if avols2[v][vtblpnum3].mapped? then choose n with n < n5 ∧ is-aligned(n, EB_PAGE_SIZE) in if n ≠ 0 then avols2[v][vtblpnum3] := mapped (subarray(avols2[v][vtblpnum3].data, 0, vtblpnum5) + subarray(buf0, n3, n) + mkempbuf(LEB_SIZE - vtblpnum5 - n), vtblpnum5 + n) ifnone skip else if n5 ≠ 0 then avols2[v][vtblpnum3] := unmapped⟩ (abs(avols2, apebs1, vols0, q0) ∧ err2 = err), n2 = 0, vtblpnum4 = n4, VTBL_VOLID ∈ vols

Rule argument

pos: left 1

Additional information

Used simplifier rules: ebm_change#(VOLID, LNUM, N, BUF; AVOLS; ERR) {if VOLID ∈ AVOLS ∧ LNUM < # AVOLS[VOLID] ∧ N ≤ LEB_SIZE ∧ N ≤ # BUF ∧ is-aligned(N, EB_PAGE_SIZE) then {fail_or_success#(; ; ERR); if ERR = ESUCCESS then AVOLS[VOLID][LNUM] := mapped(subarray(BUF, 0, N) + mkempbuf(LEB_SIZE - N), N)} else abort };