Proof step 319 from proof prepost-scan-all (previous step)

Heuristic symbolic execution applied rule choose right

And obtained the following new goals

• Proof step 320:

  # buf1 = # buf, # wlar0 = n1 + vtblpnum1, # apebs = n1 + vtblpnum1, apebs[vtblpnum1] = mkpeb(aechdr(m), avidhdr(v, m1, m2, m3, m4), buf0, m0, false), buf = mkbuf(LEB_SIZE), err = err0, n = LEB_SIZE, n0 = 0, nx < vtblpnum1, bflipset-cons(bflipset, subarray(wlar0, 0, vtblpnum1)), indices-erasing(wlar0, nx), range=(buf1, 0, buf, 0, n0), range=(buf1, n0 + n, buf, n0 + n, # buf - n0 + n), ubi-io-inv(apebs), ubi-io-peb-inv(mkpeb(aechdr(m), avidhdr(v, m1, m2, m3, m4), buf0, 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)), ⌊err0⌋ ∨ err0 = ESUCCESS ⊦ ⟪buf := buf1; bitflips0 := bitflips0 ∨ bitflips; wlar := wlar0[vtblpnum1, wlar0[vtblpnum1].ec:= m]; if err = ESUCCESS then let ladr = apebs[vtblpnum1].vidhdr.vol × apebs[vtblpnum1].vidhdr.leb, n = 0 in {if ladr ∈ recs then n := recs[ladr].sqn; if apebs[vtblpnum1].vidhdr.size ≠ 0 → apebs[vtblpnum1].vidhdr.size ≤ datasize(buf) ∧ apebs[vtblpnum1].vidhdr.checksum = checksum(buf, apebs[vtblpnum1].vidhdr.size) then {sqnum := max(sqnum, apebs[vtblpnum1].vidhdr.sqn + 1); if n ≤ apebs[vtblpnum1].vidhdr.sqn then {wlar[vtblpnum1] := wl-entry(wlar[vtblpnum1].ec, used); if bitflips0 then bflipset := bflipset ++ vtblpnum1; avhdr := apebs[vtblpnum1].vidhdr; if ladr ∈ recs then let vtblpnum0 = recs[ladr].pnum in {bflipset := bflipset -- vtblpnum0; wlar[vtblpnum0] := wl-entry(wlar[vtblpnum0].ec, erasing); q := q + eq-entry(vtblpnum0, avhdr.vol × avhdr.leb) '}; recs[ladr] := recovery-entry(vtblpnum1, avhdr.sqn)} else {wlar[vtblpnum1] := wl-entry(wlar[vtblpnum1].ec, erasing); q := q + eq-entry(vtblpnum1, ladr.vol × ladr.leb) '}} else {wlar[vtblpnum1] := wl-entry(wlar[vtblpnum1].ec, erasing); q := q + eq-entry(vtblpnum1, none) '}}; vtblpnum1 := vtblpnum1 + 1⟫ ( vtblpnum1 ≤ # apebs ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ ( err = ESUCCESS → # apebs = # wlar ∧ nx < vtblpnum1 ∧ indices-erasing(wlar, nx) ∧ valid-global-sqn(subarray(apebs, 0, vtblpnum1), sqnum) ∧ valid-eraseq(subarray(wlar, 0, vtblpnum1), q) ∧ bflipset-cons(bflipset, subarray(wlar, 0, vtblpnum1)) ∧ valid-eraseq-stronger(subarray(apebs, 0, vtblpnum1), q) ∧ valid-wl(subarray(apebs, 0, vtblpnum1), subarray(wlar, 0, vtblpnum1)) ∧ valid-recs-sqns(apebs, recs) ∧ valid-recs(subarray(apebs, 0, vtblpnum1), subarray(wlar, 0, vtblpnum1), recs)) ∧ # apebs < n1 + vtblpnum1), err = ESUCCESS, m3 = 0, n1 = 0, dups(nx)

• Proof step 326:

  # wlar0 = n1 + vtblpnum1, # apebs = n1 + vtblpnum1, apebs[vtblpnum1] = mkpeb(aechdr(m), avidhdr(v, m1, m2, m3, m4), buf1, m0, false), buf = mkbuf(LEB_SIZE), err = err0, n = LEB_SIZE, n0 = 0, nx < vtblpnum1, bflipset-cons(bflipset, 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)), ⌊err0⌋ ∨ err0 = ESUCCESS ⊦ err = ESUCCESS, m3 = 0, n1 = 0, dups(nx), ∃ buf1. # buf1 = # buf ∧ range=(buf1, 0, buf, 0, n0) ∧ range=(buf1, n0 + n, buf, n0 + n, # buf - n0 + n)

• Proof step 328:

  # wlar0 = n1 + vtblpnum1, # apebs = n1 + vtblpnum1, apebs[vtblpnum1] = mkpeb(aechdr(m), avidhdr(v, m1, m2, m3, m4), buf1, m0, false), buf = mkbuf(LEB_SIZE), err = err0, n = LEB_SIZE, n0 = 0, nx < vtblpnum1, bflipset-cons(bflipset, 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)), ⌊err0⌋ ∨ err0 = ESUCCESS ⊦ err = ESUCCESS, m3 = 0, n1 = 0, dups(nx), ∀ buf1. # buf1 = # buf → range=(buf1, 0, buf, 0, n0) → # buf ≥ n0 + n

Rule argument

Additional information