Proof step 6 from proof refine-read-vidhdr (previous step)

Heuristic conditional right split applied rule if right

And obtained the following new goals

• Proof step 7:

  apebs[m2] = mkpeb(aehdr, avhdr1, buf, m1, false), avhdr = avhdr0, m = EB_PAGE_SIZE, m0 = m2, m0 < # pebs, m2 < # apebs, abs(pebs, apebs), mtd-cons(pebs), ubi-io-inv(apebs), m0 < # pebs → m0 < # pebs ⊦ ⟪let buf = mkbuf(m) in {ubi_io_read#(m0, m, 0, m, pebs; buf; bitflips, err); if err = ESUCCESS then if isempty(buf) then avhdr := empty else let vhdr = ? in {decode_vidheader#(m, buf; vhdr; err); if err = ESUCCESS then avhdr := avidhdr(vhdr.vol, vhdr.leb, vhdr.sqn, vhdr.size, vhdr.checksum)}}⟫ ⟨aubi_io_read_vidhdr#(m2, apebs; avhdr0; isbad, err0)⟩ (avhdr = avhdr0 ∧ (bitflips ↔ isbad) ∧ err = err0), pebs[m0].bad

• Proof step 108:

  apebs[m2] = mkpeb(aehdr, avhdr1, buf, m1, false), avhdr = avhdr0, m = EB_PAGE_SIZE, m0 = m2, m2 < # apebs, abs(pebs, apebs), mtd-cons(pebs), ubi-io-inv(apebs), m0 < # pebs → m0 < # pebs ⊦ ⟪abort⟫ ⟨aubi_io_read_vidhdr#(m2, apebs; avhdr0; isbad, err0)⟩ (avhdr = avhdr0 ∧ (bitflips ↔ isbad) ∧ err = err0), m0 < # pebs ∧ ¬ pebs[m0].bad

• Proof step 111:

  apebs[m2] = mkpeb(aehdr, avhdr1, buf, m1, false), avhdr = avhdr0, m = EB_PAGE_SIZE, m0 = m2, m0 < # pebs, m2 < # apebs, abs(pebs, apebs), mtd-cons(pebs), ubi-io-inv(apebs) ⊦ m0 < # pebs

Rule argument

Additional information