| # wlar0 = n0 + vtblpnum, # apebs = n0 + vtblpnum, apebs[vtblpnum].vidhdr = empty, apebs[vtblpnum] = mkpeb(aechdr(m), avhdr1, buf1, m0, false), ¬ bitflips, err = ESUCCESS, err = err0, wlar = wlar0[vtblpnum, wlar0[vtblpnum].ec:= m], vtblpnum < # wlar, nx < vtblpnum, vtblpnum < # apebs, vtblpnum < # wlar0, bflipset-cons(bflipset, subarray(wlar0, 0, vtblpnum)), indices-erasing(wlar0, nx), ubi-io-inv(apebs), ubi-io-peb-inv(mkpeb(aechdr(m), avhdr1, buf1, m0, false)), unique-sqns(apebs), valid-eraseq(subarray(wlar0, 0, vtblpnum), q), valid-eraseq-stronger(subarray(apebs, 0, vtblpnum), q), valid-global-sqn(subarray(apebs, 0, vtblpnum), sqnum), valid-recs(subarray(apebs, 0, vtblpnum), subarray(wlar0, 0, vtblpnum), recs), valid-recs-sqns(apebs, recs), valid-wl(subarray(apebs, 0, vtblpnum), subarray(wlar0, 0, vtblpnum)), ⌊err0⌋ ∨ err0 = ESUCCESS ⊦ ⟪vtblpnum0 := vtblpnum + 1⟫ ( vtblpnum0 ≤ # apebs ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ ( err = ESUCCESS → # apebs = # wlar[vtblpnum, wl-entry(wlar[vtblpnum].ec, free)] ∧ nx < vtblpnum0 ∧ indices-erasing(wlar[vtblpnum, wl-entry(wlar[vtblpnum].ec, free)], nx) ∧ valid-global-sqn(subarray(apebs, 0, vtblpnum0), sqnum) ∧ valid-eraseq(subarray(wlar[vtblpnum, wl-entry(wlar[vtblpnum].ec, free)], 0, vtblpnum0), q) ∧ bflipset-cons(bflipset, subarray(wlar[vtblpnum, wl-entry(wlar[vtblpnum].ec, free)], 0, vtblpnum0)) ∧ valid-eraseq-stronger(subarray(apebs, 0, vtblpnum0), q) ∧ valid-wl(subarray(apebs, 0, vtblpnum0), subarray(wlar[vtblpnum, wl-entry(wlar[vtblpnum].ec, free)], 0, vtblpnum0)) ∧ valid-recs-sqns(apebs, recs) ∧ valid-recs(subarray(apebs, 0, vtblpnum0), subarray(wlar[vtblpnum, wl-entry(wlar[vtblpnum].ec, free)], 0, vtblpnum0), recs)) ∧ # apebs < n0 + vtblpnum0), n0 = 0, dups(nx) |
Used simplifier rules: ubi-io-inv-fwd: n < # apebs ⊦ apebs[n] = apeb ∧ ubi-io-inv(apebs) → ubi-io-peb-inv(apeb);% ⊦ # wlar[n, wle] = # wlar; (s)% ⊦ ¬ ⌊ESUCCESS⌋ ; (s)% ⊦ m + 1 ≤ n ↔ m < n; (s)%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic%c: ⊦ m + n = n + m; from specification nat-basic% ⊦ m < # wlar → wlar[m, wle][m] = wle; (s)% ⊦ (wle.ec:= m).ec = m; (s)% ⊦ m < n ↔ ¬ n ≤ m; (ss)% ⊦ m + m0 ≤ m ↔ m0 = 0; (s)%m < # wlar ⊦ wlar[m, wle][m, wle0] = wlar[m, wle0]; (s)% ⊦ nx < m → nx < m + n; (ss)%⊦ nx < m ∧ indices-erasing(wlar, nx) → indices-erasing(wlar[m, wle], nx); (ss)% ⊦ m < m + n ↔ n ≠ 0; (s)% ⊦ free ≠ erasing; (s)%n < # wlar, stat ≠ erasing ⊦ valid-eraseq(subarray(wlar, 0, n), q) → valid-eraseq(subarray(wlar[n, wl-entry(m, stat)], 0, n + 1), q); (ss)%n < # wlar ⊦ bflipset-cons(bflipset, subarray(wlar, 0, n)) → bflipset-cons(bflipset, subarray(wlar[n, wle], 0, n + 1)); (ss)%m < # apebs ⊦ valid-eraseq-stronger(subarray(apebs, 0, m), q) → valid-eraseq-stronger(subarray(apebs, 0, m + 1), q); (ss)% ⊦ used ≠ free; (s)%m < # apebs, # wlar = # apebs, stat ≠ used ⊦ valid-recs(subarray(apebs, 0, m), subarray(wlar, 0, m), recs) → valid-recs (subarray(apebs, 0, m + 1), subarray(wlar[m, wl-entry(m0, stat)], 0, m + 1), recs); (ss)% ⊦ m < n + 1 ↔ ¬ n < m; (s)%lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic% ⊦ mkpeb(aehdr, avhdr, buf, m, boolvar).vidhdr = avhdr; (s)% ⊦ m + n < m + n0 ↔ n < n0; (s)% ⊦ ¬ n < n; (s)%m < # apebs, # apebs = # wlar ⊦ valid-wl(subarray(apebs, 0, m), subarray(wlar, 0, m)) ∧ apebs[m] = mkpeb(aechdr(m0), empty, buf, m1, false) → valid-wl (subarray(apebs, 0, m + 1), subarray(wlar[m, wl-entry(m0, free)], 0, m + 1)); (ss)%m < # apebs ⊦ valid-global-sqn(subarray(apebs, 0, m), n) → ( valid-global-sqn(subarray(apebs, 0, m + 1), n) ↔ ¬ valid-peb(apebs[m]) ∨ apebs[m].vidhdr.sqn < n); (ss)% ⊦ ¬ valid-peb(mkpeb(aehdr, empty, buf, m, boolvar)); (s)