Proof step 288 from proof prepost-atomic-leb-change (previous step)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 289:

  # apebs = # wlar, apebs[n1] = mkpeb(aehdr, empty, mkempbuf(LEB_SIZE), 0, false), wlar[n1] = wl-entry(m1, free), apebs1 = apebs, vtblpnum ≠ n1, aehdr.valid?, n1 < # wlar, bflipset-cons(bflipset, wlar), is-aligned(n0, EB_PAGE_SIZE), ubi-io-inv(apebs), unique-sqns(apebs), valid-ebatbl(apebs, wlar, vols, vtblpnum), valid-eraseq(apebs, q), valid-eraseq(wlar, q), valid-eraseq(q), valid-global-sqn(apebs, sqnum), valid-vtbl(apebs, vols, wlar, vtblpnum), valid-wl(apebs, wlar), n0 ≤ LEB_SIZE, ¬ vtblpnum ∈ q, ¬ VTBL_VOLID ∈ vols, v ∈ vols ∧ m0 < # vols[v] ∨ v = VTBL_VOLID ∧ m0 = VTBL_LNUM ⊦ ⟪aubi_io_write_vidhdr#(n1, avidhdr(v, m0, sqnum, 0, 0); apebs; err); vtblpnum2 := n1; buf := mkempbuf(n0) + buf0; if err = ESUCCESS then if datasize(buf, n0) ≠ 0 then aubi_io_write_data_wl#(vtblpnum2, align↑(datasize(buf, n0), EB_PAGE_SIZE), buf; apebs; err); vtblpnum0 := vtblpnum; vols0 := vols; q0 := q; if err = ESUCCESS then {if v = VTBL_VOLID ∧ m0 = VTBL_LNUM then {ubi_wl_put_peb#(VTBL_VOLID × VTBL_LNUM, vtblpnum0; wlar, q); bflipset := bflipset -- vtblpnum0; vtblpnum0 := vtblpnum2} else {vtblpnum3 := m0; if vols[v][vtblpnum3] ≠ unmapped then let vtblpnum0 = vols[v][vtblpnum3].pnum in {ubi_wl_put_peb#(v × vtblpnum3, vtblpnum0; wlar, q); bflipset := bflipset -- vtblpnum0}; vols[v][vtblpnum3] := ⌜vtblpnum2⌝ }; wlar[vtblpnum2] := wl-entry(wlar[vtblpnum2].ec, used)} else ubi_wl_put_peb#(none, vtblpnum2; wlar, q)⟫ ( (err = ESUCCESS ∨ ⌊err⌋ ) ∧ id○(apebs, apebs1, n1) ∧ ubi-io-inv(apebs) ∧ # apebs = # wlar ∧ unique-sqns(apebs) ∧ valid-global-sqn(apebs, sqnum + 1) ∧ valid-wl(apebs, wlar) ∧ valid-eraseq(q) ∧ valid-eraseq(wlar, q) ∧ valid-eraseq(apebs, q) ∧ ¬ VTBL_VOLID ∈ vols ∧ bflipset-cons(bflipset, wlar) ∧ ( v ∈ vols0 ∨ is-encoded(to-vtbl(vols0), subarray(buf, 0, LEB_SIZE)) ∧ n0 = LEB_SIZE ∨ err ≠ ESUCCESS → valid-ebatbl(apebs, wlar, vols, vtblpnum0) ∧ valid-vtbl(apebs, vols, wlar, vtblpnum0)) ∧ ( err = ESUCCESS ∧ v = VTBL_VOLID ∧ m0 = VTBL_LNUM → (∀ v0, m0. ¬ v0 ∈ vols0 ∧ is-encoded(to-vtbl(vols0)[v0, m0], subarray(buf, 0, LEB_SIZE)) ∧ n0 = LEB_SIZE → valid-ebatbl(apebs, wlar, vols[v0, fill(mkebatbl(m0), unmapped)], vtblpnum0) ∧ valid-vtbl(apebs, vols[v0, fill(mkebatbl(m0), unmapped)], wlar, vtblpnum0))) ∧ (err = ESUCCESS ∧ v ∈ vols0 ∧ vols0[v][m0] ≠ unmapped → q = q0 + eq-entry(vols0[v][m0].pnum, v × m0) ') ∧ (err = ESUCCESS ∧ v = VTBL_VOLID ∧ m0 = VTBL_LNUM → q = q0 + eq-entry(vtblpnum, VTBL_VOLID × VTBL_LNUM) ') ∧ id(apebs, apebs1, mapped-pebs(vols0)) ∧ (v = VTBL_VOLID ∧ m0 = VTBL_LNUM ∨ err ≠ ESUCCESS → vols = vols0) ∧ (v ∈ vols0 ∧ err = ESUCCESS → vols = vols0[v, vols0[v][m0, ⌜n1⌝ ]]) ∧ ( err = ESUCCESS → apebs[n1].fill = datasize(buf, n0) ∧ apebs[n1].data = subarray(buf, 0, n0) + mkempbuf(LEB_SIZE - n0) ∧ q.lebrefs ⊆ q0.lebrefs ++ (v × m0)) ∧ (err ≠ ESUCCESS → q.lebrefs = q0.lebrefs))

Rule argument

Additional information

Used simplifier rules: ls-datasize-zero: n ≤ # buf ⊦ datasize(buf, n) = 0 ↔ (∃ buf0. buf = mkempbuf(n) + buf0);%ls-datasize-empbuf-append-lower: ⊦ datasize(mkempbuf(n) + buf, n) = 0;%c: ⊦ m + n = n + m; from specification nat-basic%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic% ⊦ m ≤ m + n; (s)% ⊦ # mkempbuf(n) = n; (s)% ⊦ #(buf + buf0) = # buf + # buf0; (s)%n ≠ 0, is-aligned(m, n) ⊦ align↑(m, n) = m; (s)%n ≠ 0 ⊦ is-aligned(0, n); (s)% ⊦ EB_PAGE_SIZE ≠ 0; (s)%append-a: ⊦ (buf + buf0) + buf1 = buf + buf0 + buf1; from specification array-splice[buffer]% ⊦ m ≤ n → (n < m ↔ false); (s)% ⊦ m ≤ n ↔ ¬ n < m; (ss)