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

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 10:

  sqnum = n1, vtblpnum0 = 0, vtblpnum3 = LEB_SIZE, ubi-io-inv(apebs), unique-sqns(apebs) ⊦ ⟪sqnum := 0; err := ESUCCESS; aubi_io_get_blockcount#(apebs; ; n); wlar := mkwlarray(n); wlar := fill(wlar, wl-entry(0, free)); recs := ∅; bflipset := ∅; vtblpnum2 := 0; vtblpnum1 := 0; nx := []; q := []; while vtblpnum0 < n ∧ err = ESUCCESS do {/* (prepost-scan-all: invariant scan-all-inv(vtblpnum0, apebs, recs, wlar, q, bflipset, nx, sqnum, err) wfbound # apebs - vtblpnum0) */; let isbad = ? in {aubi_io_isbad#(vtblpnum0, apebs; ; isbad, err); if err = ESUCCESS then if isbad then wlar[vtblpnum0].status := erroneous else let aehdr = ?, bitflips = ? in {aubi_io_read_echdr#(vtblpnum0, apebs; aehdr; bitflips, err); if err = ESUCCESS then if ¬ aehdr.valid? then {nx := vtblpnum0 + nx; wlar[vtblpnum0].status := erasing; q := q + eq-entry(vtblpnum0, none)} else let avhdr = ? in {vtblpnum2 := vtblpnum2 + 1; vtblpnum1 := vtblpnum1 + aehdr.ec; wlar[vtblpnum0].ec := aehdr.ec; aubi_io_read_vidhdr#(vtblpnum0, apebs; avhdr; bitflips, err); if err = ESUCCESS then if avhdr = empty then if bitflips then {wlar[vtblpnum0].status := erasing; q := q + eq-entry(vtblpnum0, none)} else wlar[vtblpnum0].status := free else if avhdr.valid? then let buf = mkbuf(vtblpnum3) in {if avhdr.size ≠ 0 then let boolvar = ? in {aubi_io_read_data#(vtblpnum0, 0, 0, vtblpnum3, apebs; buf; boolvar, err); bitflips := bitflips ∨ boolvar}; if err = ESUCCESS then let ladr = avhdr.vol × avhdr.leb, n = 0 in {if ladr ∈ recs then n := recs[ladr].sqn; if avhdr.size ≠ 0 → avhdr.size ≤ datasize(buf) ∧ avhdr.checksum = checksum(buf, avhdr.size) then {sqnum := max(sqnum, avhdr.sqn + 1); if avhdr.sqn ≥ n then {wlar[vtblpnum0].status := used; if bitflips then bflipset := bflipset ++ vtblpnum0; if ladr ∈ recs then let vtblpnum = recs[ladr].pnum in {bflipset := bflipset -- vtblpnum; wlar[vtblpnum].status := erasing; q := q + eq-entry(vtblpnum, avhdr.vol × avhdr.leb)}; recs[ladr] := recovery-entry(vtblpnum0, avhdr.sqn)} else {wlar[vtblpnum0].status := erasing; q := q + eq-entry(vtblpnum0, ladr.vol × ladr.leb)}} else {wlar[vtblpnum0].status := erasing; q := q + eq-entry(vtblpnum0, none)}}} else {wlar[vtblpnum0].status := erasing; q := q + eq-entry(vtblpnum0, none)}}}; vtblpnum0 := vtblpnum0 + 1}}⟫ ( (err = ESUCCESS ∨ ⌊err⌋ ) ∧ ( err = ESUCCESS → # apebs = # wlar ∧ ¬ dups(nx) ∧ nx < # apebs ∧ indices-erasing(wlar, nx) ∧ valid-global-sqn(apebs, sqnum) ∧ valid-eraseq(wlar, q) ∧ bflipset-cons(bflipset, wlar) ∧ valid-eraseq-stronger(apebs, q) ∧ valid-wl(apebs, wlar) ∧ valid-recs-sqns(apebs, recs) ∧ valid-recs(apebs, wlar, recs)))

Rule argument

Additional information