[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 196 from proof inv-recover (previous step)

# wlar1 = # wlar0, # wlar = # wlar0, # wlar0 = # wlar0.mapIndices(nx, λ wle. wle.ec:= 0), # apebs0 = # wlar0, wlar0.mapIndices(nx, λ wle. wle.ec:= 0)[m2] = wl-entry(m4, used), wlar0[m2] = wl-entry(m3, used), vols[v][m] = ⌜m2⌝ , recs0[VTBL_VOLID × VTBL_LNUM] = recovery-entry(m1, avhdr.sqn), apebs0[m1] = mkpeb(aehdr, avhdr, buf1, m0, false), vols1[v][m] = unmapped, m1 < # wlar0, nx < # wlar0, m < # vols[v], m < # vols1[v], m2 < # wlar0, bflipset-cons(bflipset2, wlar0.mapIndices(nx, λ wle. wle.ec:= 0)), bflipset-cons(bflipset1, wlar1), bflipset-cons(bflipset, wlar), bflipset-cons(bflipset0, wlar), bflipset-cons(bflipset2, wlar0), indices-erasing(wlar, nx), is-encoded(vtbl0, buf1), is-max(apebs0, vols, wlar0.mapIndices(nx, λ wle. wle.ec:= 0), q0, bflipset2, m1, sqnum), ubi-io-inv(apebs0), ubi-io-peb-inv(mkpeb(aehdr, avhdr, buf1, m0, false)), unique-sqns(apebs0), unmapped-vols(vols0), valid-ebatbl(apebs0, wlar1, vols1, m1), valid-ebatbl(apebs0, wlar0, vols, m1), valid-ebatbl(apebs0, wlar0.mapIndices(nx, λ wle. wle.ec:= 0), vols, m1), valid-eraseq(q1), valid-eraseq(wlar1, q1), valid-eraseq(apebs0, q1), valid-eraseq(wlar, q), valid-eraseq(wlar0, q0), valid-eraseq(q0), valid-eraseq(wlar0.mapIndices(nx, λ wle. wle.ec:= 0), q0), valid-eraseq(apebs0, q0), valid-eraseq-strong(apebs0, vtbl0, q0), valid-eraseq-stronger(apebs0, q), valid-global-sqn(apebs0, vtblpnum5), valid-global-sqn(apebs0, sqnum), valid-indices(wlar0, nx), valid-peb(v, m, apebs0[m2]), valid-recs(apebs0, wlar, recs0), valid-recs-sqns(apebs0, recs0), valid-vtbl(apebs0, vols1, wlar1, m1), valid-vtbl(apebs0, vols0, wlar, m1), valid-vtbl(apebs0, vols, wlar0, m1), valid-vtbl(apebs0, vols, wlar0.mapIndices(nx, λ wle. wle.ec:= 0), m1), valid-vtbl-weak(apebs0, m1), valid-wl(apebs0, wlar1), valid-wl(apebs0, wlar), valid-wl(apebs0, wlar0.mapIndices(nx, λ wle. wle.ec:= 0)), VTBL_VOLID × VTBL_LNUM ∈ recs0, v ∈ vols, v ∈ vols1, q ⊆ q0, m2 < # wlar0 → (wlar0[m2].status = erroneous ↔ apebs0[m2].bad) ∧ (wlar0[m2].status = free → apebs0[m2].vidhdr = empty) ∧ (wlar0[m2].status ≠ erroneous ∧ wlar0[m2].status ≠ erasing → apebs0[m2].echdr = aechdr(wlar0[m2].ec)) ∧ (wlar0[m2].status = used → (∃ v, m. valid-peb(v, m, apebs0[m2]) ∧ apebs0[m2].vidhdr.sqn = valid-sqns(v, m, apebs0).max)) ⊦ m2 = m1, dups(nx), m1 ∈ q0, VTBL_VOLID ∈ vols, m1 ∈ q1, VTBL_VOLID ∈ vols0, m1 ∈ q, VTBL_VOLID ∈ vols1, eq-entry(m2, v × m) ∈ q1, m2 ∈ q0

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 197:
# wlar1 = # wlar0, # wlar = # wlar0, # wlar0 = # wlar0.mapIndices(nx, λ wle. wle.ec:= 0), # apebs0 = # wlar0, apebs0[m2].echdr = aechdr(m3), apebs0[m2].vidhdr.sqn = valid-sqns(v0, m5, apebs0).max, wlar0.mapIndices(nx, λ wle. wle.ec:= 0)[m2] = wl-entry(m4, used), wlar0[m2] = wl-entry(m3, used), vols[v0][m5] = ⌜m2⌝ , recs0[VTBL_VOLID × VTBL_LNUM] = recovery-entry(m1, avhdr.sqn), apebs0[m1] = mkpeb(aehdr, avhdr, buf1, m0, false), vols1[v0][m5] = unmapped, m1 < # wlar0, nx < # wlar0, m2 < # wlar0, m5 < # vols[v0], m5 < # vols1[v0], bflipset-cons(bflipset2, wlar0.mapIndices(nx, λ wle. wle.ec:= 0)), bflipset-cons(bflipset1, wlar1), bflipset-cons(bflipset, wlar), bflipset-cons(bflipset0, wlar), bflipset-cons(bflipset2, wlar0), indices-erasing(wlar, nx), is-encoded(vtbl0, buf1), is-max(apebs0, vols, wlar0.mapIndices(nx, λ wle. wle.ec:= 0), q0, bflipset2, m1, sqnum), ubi-io-inv(apebs0), ubi-io-peb-inv(mkpeb(aehdr, avhdr, buf1, m0, false)), unique-sqns(apebs0), unmapped-vols(vols0), valid-ebatbl(apebs0, wlar1, vols1, m1), valid-ebatbl(apebs0, wlar0, vols, m1), valid-ebatbl(apebs0, wlar0.mapIndices(nx, λ wle. wle.ec:= 0), vols, m1), valid-eraseq(q1), valid-eraseq(wlar1, q1), valid-eraseq(apebs0, q1), valid-eraseq(wlar, q), valid-eraseq(wlar0, q0), valid-eraseq(q0), valid-eraseq(wlar0.mapIndices(nx, λ wle. wle.ec:= 0), q0), valid-eraseq(apebs0, q0), valid-eraseq-strong(apebs0, vtbl0, q0), valid-eraseq-stronger(apebs0, q), valid-global-sqn(apebs0, vtblpnum5), valid-global-sqn(apebs0, sqnum), valid-indices(wlar0, nx), valid-peb(v0, m5, apebs0[m2]), valid-recs(apebs0, wlar, recs0), valid-recs-sqns(apebs0, recs0), valid-vtbl(apebs0, vols1, wlar1, m1), valid-vtbl(apebs0, vols0, wlar, m1), valid-vtbl(apebs0, vols, wlar0, m1), valid-vtbl(apebs0, vols, wlar0.mapIndices(nx, λ wle. wle.ec:= 0), m1), valid-vtbl-weak(apebs0, m1), valid-wl(apebs0, wlar1), valid-wl(apebs0, wlar), valid-wl(apebs0, wlar0.mapIndices(nx, λ wle. wle.ec:= 0)), VTBL_VOLID × VTBL_LNUM ∈ recs0, v0 ∈ vols, v0 ∈ vols1, q ⊆ q0 ⊦ m2 = m1, apebs0[m2].bad, dups(nx), m1 ∈ q0, VTBL_VOLID ∈ vols, m1 ∈ q1, VTBL_VOLID ∈ vols0, m1 ∈ q, VTBL_VOLID ∈ vols1, eq-entry(m2, v0 × m5) ∈ q1, m2 ∈ q0

Rule argument

Additional information

Used simplifier rules: lf-mapped-valid-peb: ⊦ v ∈ vols ∧ m < # vols[v] ∧ vols[v][m] = ⌜n⌝ ∧ valid-ebatbl(apebs, wlar, vols, n0) ∧ valid-wl(apebs, wlar) → valid-peb(v, m, apebs[n]);% ⊦ m < n → n ≠ 0; (s)%f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic%lf-02: ⊦ m < n ∧ m = n0 → n0 < n; (forward) from specification nat-basic% ⊦ used ≠ free; (s)% ⊦ wl-entry(m, stat).ec = m; (s)% ⊦ used ≠ erasing; (s)% ⊦ used ≠ erroneous; (s)% ⊦ wl-entry(m, stat).status = stat; (s)%⊦ valid-peb(v0, m0, apeb) → (valid-peb(v1, m1, apeb) ↔ v0 = v1 ∧ m0 = m1); (s)