[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 6 from proof prepost-init-vols-mappings (previous step)

# wlar = # apebs, apebs[n] = mkpeb(aehdr, avhdr, buf, m, boolvar), q0 = q, recs = recs0 -- (VTBL_VOLID × VTBL_LNUM), vtblpnum = n, bflipset-cons(bflipset, wlar), unique-sqns(apebs), unmapped-vols(vols), valid-eraseq(wlar, q), valid-eraseq-stronger(apebs, q), valid-recs(apebs, wlar, recs0), valid-vtbl(apebs, vols, wlar, n), valid-wl(apebs, wlar) ⊦ ⟪while recs ≠ ∅ do {/* (prepost-init-vols-mappings : invariant 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 ∧ q` ⊆ 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) wfbound # recs) */; choose ladr with ladr ∈ recs in 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}}⟫ ( valid-ebatbl(apebs, wlar, vols, n) ∧ valid-vtbl(apebs, vols, wlar, n) ∧ ¬ VTBL_VOLID ∈ vols ∧ # apebs = # wlar ∧ bflipset-cons(bflipset, wlar) ∧ valid-wl(apebs, wlar) ∧ valid-eraseq(wlar, q) ∧ q0 ⊆ q ∧ (∃ vtbl. is-encoded(vtbl, buf) ∧ valid-eraseq-strong(apebs, vtbl, q))), VTBL_VOLID ∈ vols, n ∈ q

Heuristic annotation applied rule annotation right

And obtained the following new goals

Proof step 7:
# wlar = # apebs, apebs[n] = mkpeb(aehdr, avhdr, buf, m, boolvar), q0 = q, recs = recs0 -- (VTBL_VOLID × VTBL_LNUM), vtblpnum = n, bflipset-cons(bflipset, wlar), unique-sqns(apebs), unmapped-vols(vols), valid-eraseq(wlar, q), valid-eraseq-stronger(apebs, q), valid-recs(apebs, wlar, recs0), valid-vtbl(apebs, vols, wlar, n), valid-wl(apebs, wlar) ⊦ n ∈ q, VTBL_VOLID ∈ vols, 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 ∧ q ⊆ 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)
Proof step 46:
# wlar0 = # apebs, # apebs = # wlar, apebs[n] = mkpeb(aehdr, avhdr, buf, m, boolvar), q0 = q1, recs = recs1, recs2 = recs0 -- (VTBL_VOLID × VTBL_LNUM), vtblpnum = n, bflipset-cons(bflipset0, wlar0), bflipset-cons(bflipset, wlar), unique-sqns(apebs), unmapped-vols(vols0), valid-eraseq(wlar0, q1), valid-eraseq(wlar, q), valid-eraseq-stronger(apebs, q1), valid-recs(apebs, wlar0, recs0), valid-vtbl(apebs, vols0, wlar0, n), valid-vtbl(apebs, vols, wlar, vtblpnum), valid-wl(apebs, wlar0), valid-wl(apebs, wlar), 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) ⊦ ⟪choose ladr with ladr ∈ recs in 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 = ∅, n ∈ q1, VTBL_VOLID ∈ vols0, VTBL_VOLID × VTBL_LNUM ∈ recs, VTBL_VOLID ∈ vols
Proof step 156:
# wlar0 = # apebs, # apebs = # wlar, apebs[n] = mkpeb(aehdr, avhdr, buf, m, boolvar), q0 = q1, recs = ∅, recs2 = recs0 -- (VTBL_VOLID × VTBL_LNUM), vtblpnum = n, bflipset-cons(bflipset0, wlar0), bflipset-cons(bflipset, wlar), unique-sqns(apebs), unmapped-vols(vols0), valid-eraseq(wlar0, q1), valid-eraseq(wlar, q), valid-eraseq-stronger(apebs, q1), valid-recs(apebs, wlar0, recs0), valid-vtbl(apebs, vols0, wlar0, n), valid-vtbl(apebs, vols, wlar, vtblpnum), valid-wl(apebs, wlar0), valid-wl(apebs, wlar), 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) ⊦ n ∈ q1, VTBL_VOLID ∈ vols0, VTBL_VOLID × VTBL_LNUM ∈ recs, VTBL_VOLID ∈ vols, valid-ebatbl(apebs, wlar, vols, n) ∧ valid-vtbl(apebs, vols, wlar, n) ∧ ¬ VTBL_VOLID ∈ vols ∧ # apebs = # wlar ∧ bflipset-cons(bflipset, wlar) ∧ valid-wl(apebs, wlar) ∧ valid-eraseq(wlar, q) ∧ q0 ⊆ q ∧ (∃ vtbl. is-encoded(vtbl, buf) ∧ valid-eraseq-strong(apebs, vtbl, q))

Rule argument

rule: invariant right arg: bound: # recs inv: 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 ∧ q` ⊆ 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) fmapos: right 1 pos: right 1

Additional information

Used formulas: 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 ∧ q` ⊆ 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 = # recs