Proof step 3 from proof inv-create-volume (previous step)

Heuristic nonrec nowhile calls applied rule call right

And obtained the following new goals

• Proof step 4:

  # apebs = # wlar, apebs0 = apebs, q0 = q, vols0 = vols, vtblpnum0 = vtblpnum, vtblpnum1 = EB_PAGE_SIZE, vtblpnum2 = LEB_SIZE, bflipset-cons(bflipset, wlar), 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) ⊦ ⟪if v ∈ vols ∨ v = VTBL_VOLID then err := EINVAL else if ENCODED_NAT_SIZE + (# vols + 1) * (ENCODED_VOLID_SIZE + ENCODED_NAT_SIZE) > vtblpnum2 then err := ENOSPC else let vtblpnum = ? in {ubi_erase_all#(vols, bflipset, vtblpnum0, sqnum; wlar, q, apebs; err); if err = ESUCCESS then {ubi_wl_get_peb#(; vtblpnum, wlar, q, apebs; err); if err = ESUCCESS then let vtbl = to-vtbl(vols) in {vtbl[v] := n; let buf = mkbuf(vtblpnum2), vtbl = to-vtbl(vols) in {vtbl[v] := n; encode_vtbl#(; vtbl, buf; err); if err = ESUCCESS then {ubi_atomic_leb_change# (VTBL_VOLID, VTBL_LNUM, vtblpnum, vtblpnum2, buf, vtblpnum1 ; vols, wlar, q, bflipset, vtblpnum0, sqnum, apebs ; err); if err = ESUCCESS then {vols[v] := mkebatbl(n); vols[v] := fill(vols[v], unmapped)}}}}}}⟫ ( # apebs = # wlar ∧ unique-sqns(apebs) ∧ valid-global-sqn(apebs, sqnum) ∧ valid-wl(apebs, wlar) ∧ valid-eraseq(q) ∧ valid-eraseq(wlar, q) ∧ valid-eraseq(apebs, q) ∧ ¬ VTBL_VOLID ∈ vols ∧ bflipset-cons(bflipset, wlar) ∧ valid-ebatbl(apebs, wlar, vols, vtblpnum0) ∧ valid-vtbl(apebs, vols, wlar, vtblpnum0) ∧ ubi-io-inv(apebs) ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ id(apebs, apebs0, mapped-pebs(vols)) ∧ (err = ESUCCESS → ¬ v ∈ vols0 ∧ vols = vols0[v, fill(mkebatbl(n), unmapped)] ∧ q.lebrefs ⊆ ∅ ++ (VTBL_VOLID × VTBL_LNUM)) ∧ (err ≠ ESUCCESS → q.lebrefs ⊆ q0.lebrefs ∧ vols = vols0)), VTBL_VOLID ∈ vols, vtblpnum ∈ q

Rule argument

Additional information

Used simplifier rules: create-volume: ⊦ ;