[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 268 from proof prepost-scan-all (previous step)

# apebs = n1 + vtblpnum1, # wlar0 = n1 + vtblpnum1, apebs[vtblpnum1] = mkpeb(aechdr(m), avidhdr(v, m1, m2, m3, m4), buf1, m0, false), avhdr = apebs[vtblpnum1].vidhdr, bflipset = bflipset0 ++ vtblpnum1, buf = mkbuf(LEB_SIZE), err = ESUCCESS, err = err0, ladr = apebs[vtblpnum1].vidhdr.vol × apebs[vtblpnum1].vidhdr.leb, n = 0, wlar = wlar1[vtblpnum1, wl-entry(wlar1[vtblpnum1].ec, used)], wlar1 = wlar0[vtblpnum1, wlar0[vtblpnum1].ec:= m], apebs[vtblpnum1].vidhdr.valid?, avhdr.valid?, vtblpnum1 < # wlar1, vtblpnum1 < # wlar0, nx < vtblpnum1, vtblpnum1 < # apebs, bflipset-cons(bflipset0, subarray(wlar0, 0, vtblpnum1)), indices-erasing(wlar0, nx), ubi-io-inv(apebs), ubi-io-peb-inv(mkpeb(aechdr(m), avidhdr(v, m1, m2, m3, m4), buf1, m0, false)), unique-sqns(apebs), valid-eraseq(subarray(wlar0, 0, vtblpnum1), q), valid-eraseq-stronger(subarray(apebs, 0, vtblpnum1), q), valid-global-sqn(subarray(apebs, 0, vtblpnum1), sqnum), valid-recs(subarray(apebs, 0, vtblpnum1), subarray(wlar0, 0, vtblpnum1), recs), valid-recs-sqns(apebs, recs), valid-wl(subarray(apebs, 0, vtblpnum1), subarray(wlar0, 0, vtblpnum1)), 0 + LEB_SIZE ≤ # buf, 0 + LEB_SIZE ≤ # apebs[vtblpnum1].data, apebs[vtblpnum1].vidhdr.size ≠ 0 → apebs[vtblpnum1].vidhdr.size ≤ datasize(copy(apebs[vtblpnum1].data, 0, buf, 0, LEB_SIZE)) ∧ apebs[vtblpnum1].vidhdr.checksum = checksum(copy(apebs[vtblpnum1].data, 0, buf, 0, LEB_SIZE), apebs[vtblpnum1].vidhdr.size), apebs[vtblpnum1].vidhdr.size ≠ 0 → ( (apebs[vtblpnum1].vidhdr.valid? ∧ vtblpnum1 < # apebs) ∧ (0 + LEB_SIZE ≤ # apebs[vtblpnum1].data ∧ 0 + LEB_SIZE ≤ # buf) ∧ vtblpnum1 < # apebs) ∧ ( apebs[vtblpnum1].vidhdr.size ≤ datasize(copy(apebs[vtblpnum1].data, 0, buf, 0, LEB_SIZE)) → (apebs[vtblpnum1].vidhdr.valid? ∧ vtblpnum1 < # apebs) ∧ ((0 + LEB_SIZE ≤ # apebs[vtblpnum1].data ∧ 0 + LEB_SIZE ≤ # buf) ∧ vtblpnum1 < # apebs) ∧ apebs[vtblpnum1].vidhdr.valid? ∧ vtblpnum1 < # apebs), bitflips0 ∨ bitflips, ⌊err0⌋ ∨ err0 = ESUCCESS ⊦ m3 = 0, n1 = 0, dups(nx), ladr ∈ recs, vtblpnum1 + 1 ≤ # apebs ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ ( err = ESUCCESS → # apebs = # wlar ∧ nx < vtblpnum1 + 1 ∧ indices-erasing(wlar, nx) ∧ valid-global-sqn(subarray(apebs, 0, vtblpnum1 + 1), max(sqnum, apebs[vtblpnum1].vidhdr.sqn + 1)) ∧ valid-eraseq(subarray(wlar, 0, vtblpnum1 + 1), q) ∧ bflipset-cons(bflipset, subarray(wlar, 0, vtblpnum1 + 1)) ∧ valid-eraseq-stronger(subarray(apebs, 0, vtblpnum1 + 1), q) ∧ valid-wl(subarray(apebs, 0, vtblpnum1 + 1), subarray(wlar, 0, vtblpnum1 + 1)) ∧ valid-recs-sqns(apebs, recs[ladr, recovery-entry(vtblpnum1, avhdr.sqn)]) ∧ valid-recs(subarray(apebs, 0, vtblpnum1 + 1), subarray(wlar, 0, vtblpnum1 + 1), recs[ladr, recovery-entry(vtblpnum1, avhdr.sqn)])) ∧ # apebs < n1 + vtblpnum1 + 1

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Rule argument

Additional information

Used simplifier rules: lf-valid-eraseq-stronger-notin-recs: # apebs = # wlar ⊦ valid-eraseq-stronger(apebs, q) ∧ valid-eraseq(wlar, q) ∧ valid-recs(apebs, wlar, recs) ∧ valid-wl(apebs, wlar) ∧ ¬ v × m ∈ recs → valid-sqns(v, m, apebs) = ∅;%ubi-io-inv-fwd: n < # apebs ⊦ apebs[n] = apeb ∧ ubi-io-inv(apebs) → ubi-io-peb-inv(apeb);% ⊦ ¬ m + n < m; (s)% ⊦ m ≤ n ↔ ¬ n < m; (ss)%datasize-le-fwd: ⊦ m ≤ datasize(buf) → m ≤ # buf; (forward) from specification datasize% ⊦ ¬ n < n; (s)% ⊦ m + n < m + n0 ↔ n < n0; (s)%m < # apebs, # wlar = # apebs ⊦ valid-recs(subarray(apebs, 0, m), subarray(wlar, 0, m), recs) ∧ apebs[m] = mkpeb(aehdr, avidhdr(v, n, m0, m1, m4), buf, m2, boolvar) ∧ ¬ v × n ∈ recs → valid-recs (subarray(apebs, 0, m + 1), subarray(wlar[m, wl-entry(m3, used)], 0, m + 1), recs[v × n, recovery-entry(m, m0)]); (ss)% ⊦ avidhdr(v, m, m0, m1, m2).sqn = m0; (s)% ⊦ avidhdr(v, m, m0, m1, m2).checksum = m2; (s)% ⊦ avidhdr(v, m, m0, m1, m2).size = m1; (s)% ⊦ avidhdr(v, m, m0, m1, m2).valid?; (s)%n ≤ # apebs ⊦ valid-sqns(v, m, subarray(apebs, 0, n)) = valid-sqns(v, m, apebs, n); (s)% ⊦ m < n → m ≤ n; (s)% ⊦ avidhdr(v, m, m0, m1, m2).leb = m; (s)% ⊦ avidhdr(v, m, m0, m1, m2).vol = v; (s)% ⊦ mkpeb(aehdr, avhdr, buf, m, boolvar).vidhdr = avhdr; (s)% ⊦ # subarray(wlar, m, n) = n; (s)% ⊦ # subarray(apebs, m, n) = n; (s)% ⊦ m < n + 1 ↔ ¬ n < m; (s)%m < # apebs ⊦ valid-eraseq-stronger(subarray(apebs, 0, m), q) → valid-eraseq-stronger(subarray(apebs, 0, m + 1), q); (ss)%n < # wlar ⊦ bflipset-cons(bflipset, subarray(wlar, 0, n)) → bflipset-cons (bflipset ++ n, subarray(wlar[n, wl-entry(m0, used)], 0, n + 1)); (ss)%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)% ⊦ used ≠ erasing; (s)% ⊦ m < m + n ↔ n ≠ 0; (s)%⊦ nx < m ∧ indices-erasing(wlar, nx) → indices-erasing(wlar[m, wle], nx); (ss)% ⊦ nx < m → nx < m + n; (ss)%m < # wlar ⊦ wlar[m, wle][m, wle0] = wlar[m, wle0]; (s)% ⊦ m + m0 ≤ m ↔ m0 = 0; (s)% ⊦ m < n ↔ ¬ n ≤ m; (ss)% ⊦ (wle.ec:= m).ec = m; (s)% ⊦ m < # wlar → wlar[m, wle][m] = wle; (s)% ⊦ m + 1 ≤ n ↔ m < n; (s)%# buf = m, # buf0 = m ⊦ copy(buf, 0, buf0, 0, m) = buf; (s)%⊦ ubi-io-peb-inv(mkpeb(aehdr, avhdr, buf, n, boolvar)) → # buf = LEB_SIZE; (s)% ⊦ mkpeb(aehdr, avhdr, buf, m, boolvar).data = buf; (s)% ⊦ ¬ ⌊ESUCCESS⌋ ; (s)% ⊦ # wlar[n, wle] = # wlar; (s)% ⊦ m ≤ m; (s)% ⊦ # mkbuf(n) = n; (s)%c: ⊦ m + n = n + m; from specification nat-basic%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic% ⊦ n + 0 = n; (s)