[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 48 from proof prepost-write-once (previous step)

# apebs2 = # wlar0, # apebs0 = # wlar, q0.head = eq-entry(m4, lref), LEB_SIZE = (n1 + m0) + m1, apebs2[vtblpnum] = mkpeb(aehdr, empty, mkempbuf(LEB_SIZE), 0, false), wlar0[vtblpnum] = wl-entry(m5, free), vols0[v][m] = unmapped, apebs1 = apebs2[vtblpnum, mkpeb(aehdr, avidhdr(v, m, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false)], m1 ≠ 0, vtblpnum2 ≠ vtblpnum, aehdr.valid?, m < # vols0[v], vtblpnum < # wlar0, bflipset-cons(bflipset, wlar0), bflipset-cons(bflipset, wlar), id(apebs2, apebs0, mapped-pebs(vols0)), is-aligned(m0, EB_PAGE_SIZE), is-aligned(m1, EB_PAGE_SIZE), ubi-io-inv(apebs2), ubi-io-inv(apebs0), ubi-io-inv(apebs2[vtblpnum, mkpeb(aehdr, avidhdr(v, m, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false)]), unique-sqns(apebs2), unique-sqns(apebs0), valid-ebatbl(apebs2, wlar0, vols0, vtblpnum2), valid-ebatbl(apebs0, wlar, vols0, vtblpnum2), valid-eraseq(apebs2, q1), valid-eraseq(wlar0, q1), valid-eraseq(q1), valid-eraseq(q0), valid-eraseq(wlar, q0), valid-eraseq(apebs0, q0), valid-global-sqn(apebs2, sqnum), valid-global-sqn(apebs0, sqnum), valid-vtbl(apebs2, vols0, wlar0, vtblpnum2), valid-vtbl(apebs0, vols0, wlar, vtblpnum2), valid-wl(apebs2, wlar0), valid-wl(apebs0, wlar), v ∈ vols0, m0 + m1 ≤ LEB_SIZE, m1 + m2 ≤ # buf, m1 ≤ LEB_SIZE, q1.lebrefs ⊆ q0.lebrefs, ¬ vtblpnum2 ∈ q1, ¬ VTBL_VOLID ∈ vols0, ¬ vtblpnum2 ∈ q0, apebs0 = apebs2 ∧ wlar = wlar0 ∧ q0 = q1 ∨ id○(apebs0, apebs2, vtblpnum) ∧ id○(wlar, wlar0, vtblpnum) ∧ q0 = eq-entry(vtblpnum, lref) ' + q1 ⊦ [aubi_io_write_data#(vtblpnum, m0, m2, m1, buf; apebs1; err)] ( ubi-io-inv(apebs1) → ⟪vols := vols0; if err = ESUCCESS then {vols[v][m] := ⌜vtblpnum⌝ ; wlar0[vtblpnum] := wl-entry(wlar0[vtblpnum].ec, used)} else ubi_wl_put_peb#(v × m, vtblpnum; wlar0, q1); skip⟫ ( # apebs1 = # wlar0 ∧ unique-sqns(apebs1) ∧ valid-global-sqn(apebs1, sqnum + 1) ∧ valid-wl(apebs1, wlar0) ∧ valid-eraseq(q1) ∧ valid-eraseq(wlar0, q1) ∧ valid-eraseq(apebs1, q1) ∧ ¬ VTBL_VOLID ∈ vols ∧ bflipset-cons(bflipset, wlar0) ∧ valid-ebatbl(apebs1, wlar0, vols, vtblpnum2) ∧ valid-vtbl(apebs1, vols, wlar0, vtblpnum2) ∧ id(apebs1, apebs0, mapped-pebs(vols0)) ∧ q1.lebrefs ⊆ q0.lebrefs ++ (v × m) ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ (err ≠ ESUCCESS → vols = vols0) ∧ ( err = ESUCCESS → (∃ n. vols = vols0[v, vols0[v][m, ⌜n⌝ ]] ∧ apebs1[n].fill = m0 + m1 ∧ apebs1[n].data = mkempbuf(m0) + subarray(buf, m2, m1) + mkempbuf(n1)))))

Heuristic nonrecursive calls applied rule call right

And obtained the following new goals

Proof step 49:
# apebs0 = # wlar, # apebs2 = # wlar0, q0.head = eq-entry(m4, lref), LEB_SIZE = (n2 + m0) + m1, vols0[v][m] = unmapped, wlar0[vtblpnum1] = wl-entry(m5, free), apebs2[vtblpnum1] = mkpeb(aehdr, empty, mkempbuf(LEB_SIZE), 0, false), apebs = apebs1, apebs1 = apebs2[vtblpnum1, mkpeb(aehdr, avidhdr(v, m, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false)], n0 = m1, n1 = m2, vtblpnum = m0, vtblpnum0 = vtblpnum1, aehdr.valid?, vtblpnum1 < # wlar0, m < # vols0[v], bflipset-cons(bflipset, wlar), bflipset-cons(bflipset, wlar0), id(apebs2, apebs0, mapped-pebs(vols0)), is-aligned(m1, EB_PAGE_SIZE), is-aligned(m0, EB_PAGE_SIZE), ubi-io-inv(apebs2[vtblpnum1, mkpeb(aehdr, avidhdr(v, m, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false)]), ubi-io-inv(apebs0), ubi-io-inv(apebs2), unique-sqns(apebs0), unique-sqns(apebs2), valid-ebatbl(apebs0, wlar, vols0, vtblpnum2), valid-ebatbl(apebs2, wlar0, vols0, vtblpnum2), valid-eraseq(apebs0, q0), valid-eraseq(wlar, q0), valid-eraseq(q0), valid-eraseq(q1), valid-eraseq(wlar0, q1), valid-eraseq(apebs2, q1), valid-global-sqn(apebs0, sqnum), valid-global-sqn(apebs2, sqnum), valid-vtbl(apebs0, vols0, wlar, vtblpnum2), valid-vtbl(apebs2, vols0, wlar0, vtblpnum2), valid-wl(apebs0, wlar), valid-wl(apebs2, wlar0), v ∈ vols0, m1 ≤ LEB_SIZE, m1 + m2 ≤ # buf, m0 + m1 ≤ LEB_SIZE, q1.lebrefs ⊆ q0.lebrefs, apebs0 = apebs2 ∧ wlar = wlar0 ∧ q0 = q1 ∨ id○(apebs0, apebs2, vtblpnum1) ∧ id○(wlar, wlar0, vtblpnum1) ∧ q0 = eq-entry(vtblpnum1, lref) ' + q1 ⊦ [if ubi-io-write-data-pre(vtblpnum0, vtblpnum, n1, n0, buf, apebs) then {fail_or_success#(; ; err); if err = ESUCCESS then apebs[vtblpnum0] := mkpeb (apebs[vtblpnum0].echdr, apebs[vtblpnum0].vidhdr, subarray(apebs[vtblpnum0].data, 0, vtblpnum) + subarray(buf, n1, n0) + mkempbuf(LEB_SIZE - vtblpnum - n0), vtblpnum + n0, apebs[vtblpnum0].bad) else choose n with (n < n0 ∨ n = 0 ∧ n0 = 0) ∧ is-aligned(n, EB_PAGE_SIZE) in if n ≠ 0 then apebs[vtblpnum0] := mkpeb (apebs[vtblpnum0].echdr, apebs[vtblpnum0].vidhdr, subarray(apebs[vtblpnum0].data, 0, vtblpnum) + subarray(buf, n1, n) + mkempbuf(LEB_SIZE - vtblpnum - n), vtblpnum + n, apebs[vtblpnum0].bad)} else abort] ( ubi-io-inv(apebs) → ⟪vols := vols0; if err = ESUCCESS then {vols[v][m] := ⌜vtblpnum1⌝ ; wlar0[vtblpnum1] := wl-entry(wlar0[vtblpnum1].ec, used)} else ubi_wl_put_peb#(v × m, vtblpnum1; wlar0, q1); skip⟫ ( # apebs = # wlar0 ∧ unique-sqns(apebs) ∧ valid-global-sqn(apebs, sqnum + 1) ∧ valid-wl(apebs, wlar0) ∧ valid-eraseq(q1) ∧ valid-eraseq(wlar0, q1) ∧ valid-eraseq(apebs, q1) ∧ ¬ VTBL_VOLID ∈ vols ∧ bflipset-cons(bflipset, wlar0) ∧ valid-ebatbl(apebs, wlar0, vols, vtblpnum2) ∧ valid-vtbl(apebs, vols, wlar0, vtblpnum2) ∧ id(apebs, apebs0, mapped-pebs(vols0)) ∧ q1.lebrefs ⊆ q0.lebrefs ++ (v × m) ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ (err ≠ ESUCCESS → vols = vols0) ∧ ( err = ESUCCESS → (∃ n. vols = vols0[v, vols0[v][m, ⌜n⌝ ]] ∧ apebs[n].fill = m0 + m1 ∧ apebs[n].data = mkempbuf(m0) + subarray(buf, m2, m1) + mkempbuf(n2))))), m1 = 0, vtblpnum2 = vtblpnum1, vtblpnum2 ∈ q1, VTBL_VOLID ∈ vols0, vtblpnum2 ∈ q0

Rule argument

pos: right 1

Additional information

Used simplifier rules: aubi_io_write_data#(PNUM, OFFSET, N0, N, BUF; APEBS; ERR) {if ubi-io-write-data-pre(PNUM, OFFSET, N0, N, BUF, APEBS) then {fail_or_success#(; ; ERR); if ERR = ESUCCESS then APEBS[PNUM] := mkpeb (APEBS[PNUM].echdr, APEBS[PNUM].vidhdr, subarray(APEBS[PNUM].data, 0, OFFSET) + subarray(BUF, N0, N) + mkempbuf(LEB_SIZE - OFFSET - N), OFFSET + N, APEBS[PNUM].bad) else choose N1 with (N1 < N ∨ N1 = 0 ∧ N = 0) ∧ is-aligned(N1, EB_PAGE_SIZE) in if N1 ≠ 0 then APEBS[PNUM] := mkpeb (APEBS[PNUM].echdr, APEBS[PNUM].vidhdr, subarray(APEBS[PNUM].data, 0, OFFSET) + subarray(BUF, N0, N1) + mkempbuf(LEB_SIZE - OFFSET - N1), OFFSET + N1, APEBS[PNUM].bad)} else abort };