Proof step 46 from proof prepost-init-vols-mappings (previous step)

Heuristic symbolic execution applied rule choose right

And obtained the following new goals

• Proof step 47:

  # apebs = # wlar, # wlar0 = # apebs, apebs[n] = mkpeb(aehdr, avhdr, buf, m, boolvar), q0 = q1, recs = recs1, recs2 = recs0 -- (VTBL_VOLID × VTBL_LNUM), vtblpnum = n, bflipset-cons(bflipset, wlar), bflipset-cons(bflipset0, wlar0), unique-sqns(apebs), unmapped-vols(vols0), valid-eraseq(wlar, q), valid-eraseq(wlar0, q1), valid-eraseq-stronger(apebs, q1), valid-recs(apebs, wlar0, recs0), valid-vtbl(apebs, vols, wlar, vtblpnum), valid-vtbl(apebs, vols0, wlar0, n), valid-wl(apebs, wlar), valid-wl(apebs, wlar0), ladr ∈ recs, q1 ⊆ q, recs ⊥ vols, ∀ v, m, n. v × m ∈ recs ∧ recs[v × m].pnum = n ∨ v ∈ vols ∧ m < # vols[v] ∧ vols[v][m] = ⌜n⌝ ↔ wlar[n].status = used ∧ n < # apebs ∧ apebs[n].vidhdr.valid? ∧ apebs[n].vidhdr.vol = v ∧ apebs[n].vidhdr.leb = m ∧ n ≠ vtblpnum, ∃ vtbl. is-encoded(vtbl, apebs[vtblpnum].data) ∧ valid-eraseq-strong(apebs, vtbl, q) ⊦ ⟪let n0 = recs[ladr].pnum in {if ladr.vol ∈ vols ∧ ladr.leb < # vols[ladr.vol] then vols[ladr.vol][ladr.leb] := ⌜n0⌝ else {wlar[n0].status := erasing; q := q + eq-entry(n0, ladr.vol × ladr.leb); bflipset := bflipset -- n0}; recs := recs -- ladr}⟫ ( ( unique-sqns(apebs) ∧ valid-vtbl(apebs, vols, wlar, vtblpnum) ∧ ¬ VTBL_VOLID ∈ vols ∧ ¬ VTBL_VOLID × VTBL_LNUM ∈ recs ∧ # apebs = # wlar ∧ valid-wl(apebs, wlar) ∧ valid-eraseq(wlar, q) ∧ (∃ vtbl. is-encoded(vtbl, apebs[vtblpnum].data) ∧ valid-eraseq-strong(apebs, vtbl, q)) ∧ bflipset-cons(bflipset, wlar) ∧ recs ⊥ vols ∧ q1 ⊆ q ∧ (∀ v, m, n. v × m ∈ recs ∧ recs[v × m].pnum = n ∨ v ∈ vols ∧ m < # vols[v] ∧ vols[v][m] = ⌜n⌝ ↔ wlar[n].status = used ∧ n < # apebs ∧ apebs[n].vidhdr.valid? ∧ apebs[n].vidhdr.vol = v ∧ apebs[n].vidhdr.leb = m ∧ n ≠ vtblpnum)) ∧ # recs < # recs1), recs = ∅, VTBL_VOLID ∈ vols, VTBL_VOLID × VTBL_LNUM ∈ recs, VTBL_VOLID ∈ vols0, n ∈ q1

• Proof step 151:

  # apebs = # wlar, # wlar0 = # apebs, apebs[n] = mkpeb(aehdr, avhdr, buf, m, boolvar), q0 = q1, recs = recs1, recs2 = recs0 -- (VTBL_VOLID × VTBL_LNUM), vtblpnum = n, bflipset-cons(bflipset, wlar), bflipset-cons(bflipset0, wlar0), unique-sqns(apebs), unmapped-vols(vols0), valid-eraseq(wlar, q), valid-eraseq(wlar0, q1), valid-eraseq-stronger(apebs, q1), valid-recs(apebs, wlar0, recs0), valid-vtbl(apebs, vols, wlar, vtblpnum), valid-vtbl(apebs, vols0, wlar0, n), valid-wl(apebs, wlar), valid-wl(apebs, wlar0), q1 ⊆ q, recs ⊥ vols, ∀ v, m, n. v × m ∈ recs ∧ recs[v × m].pnum = n ∨ v ∈ vols ∧ m < # vols[v] ∧ vols[v][m] = ⌜n⌝ ↔ wlar[n].status = used ∧ n < # apebs ∧ apebs[n].vidhdr.valid? ∧ apebs[n].vidhdr.vol = v ∧ apebs[n].vidhdr.leb = m ∧ n ≠ vtblpnum, ∃ vtbl. is-encoded(vtbl, apebs[vtblpnum].data) ∧ valid-eraseq-strong(apebs, vtbl, q) ⊦ recs = ∅, VTBL_VOLID ∈ vols, VTBL_VOLID × VTBL_LNUM ∈ recs, VTBL_VOLID ∈ vols0, n ∈ q1, ∃ ladr. ladr ∈ recs

Rule argument

Additional information